从意外发现到效率革命：亚马逊云科技大规模应用自动推理提升系统效率

在亚马逊云科技应用自动推理的10多年时间里，我们发现经过验证的代码通常比它所替代的未经验证的代码性能更好。

这主要是因为在验证过程中我们所做的bug修复通常会提升代码的运行性能。自动推理让开发人员有信心去探索额外的优化，进一步提升系统性能。我们发现验证的代码更容易更新、修改和操作，这减少了半夜的日志分析和调试环节。

自动推理的基本概念

在亚马逊云科技，我们努力为客户构建简单、易用的服务。但在这种简单的背后却是庞大、复杂的分布式系统，每秒处理着数十亿个请求。验证这些复杂系统的正确性是一个极大的挑战。我们的服务随着新功能的增加、组件的重新设计、安全的增强和性能的优化，一直处于不断变化和发展的状态。很多变化本身就是非常复杂的，必须在不影响亚马逊云科技本身或客户的安全性和韧性的前提下进行。

设计评审、代码审计、压力测试和故障注入是我们经常以及未来都会一直使用的宝贵工具。然而，我们发现仍然需要使用额外的技术来确认许多情况下的正确性。细微的bug仍可能逃过检测，尤其是在大规模、容错架构中。有些问题甚至可能源于最初的系统设计，而不是实施缺陷。随着我们服务规模和复杂性的增长，我们不得不使用基于数学和逻辑的更强大技术作为对传统测试方法的补充。这就是人工智能(AI)的一个分支自动推理发挥作用的地方。

传统测试侧重于在特定场景下验证系统行为，而自动推理旨在使用逻辑来验证系统在任何可能场景下的行为。即使是一个中等复杂的系统，要重现可能发生的每一种可能状态和参数的组合，所需的时间也是难以想象的。自动推理可以通过计算系统正确性的逻辑证明来快速、高效地取得相同的效果。

使用自动推理需要我们的开发者具有不同的思维方式。我们不是试图考虑所有可能的输入场景及其可能出错的方式，而是定义系统应该如何工作，并识别出让它正确运行必须满足的条件。然后，我们可以使用数学证明来验证这些条件是否为真。换句话说，我们可以验证系统是否正确。

自动推理将系统的规范和实施以数学的形式进行审核，然后使用算法来验证系统的数学表示是否满足规范。通过把我们的系统编码为数学系统，并使用形式逻辑对其进行推理，自动推理使我们能够有效和权威地解答有关系统未来行为的关键问题。系统能做什么?它将做什么?它永远不会做什么?自动推理可以帮助回答系统的这些问题，即便是最复杂的、大规模的和潜在无限的系统——这些场景是单单通过传统测试无法彻底验证的。

自动推理能让我们达到完美的程度吗?不能，因为它仍然依赖于对系统组件的正确行为以及系统与其环境模型之间关系的某些假设。例如，系统模型可能错误地假设底层组件(如编译器和处理器)没有任何bug(尽管也可以对这些组件进行验证)。话虽如此，与使用传统软件开发和测试方法相比，自动推理让我们更有信心达到正确性。

更快的开发

自动推理不仅仅是数学家和科学家的工具。我们的 Amazon Simple Storage Service (Amazon S3) 工程师每天都在使用自动推理来防止bug。S3的背后是世界上最大、最复杂的分布式系统之一，它存储了400万亿个对象、EB级别的数据并通常需要每秒处理1.5亿个请求。S3由许多子系统组成，这些子系统本身就是分布式系统，其中许多由数万台机器组成。S3一直不断增加新的功能，同时它也被我们的客户大量使用中。

S3索引子系统是S3的一个关键组件，它是一个对象元数据存储，来支持快速的数据查找。该组件包含一个非常大的、复杂的数据结构和精密的优化算法。以S3的这种大规模，这些算法对于人类来说很难正确使用，同时我们也不能容许S3在查找时发生任何错误，为此我们大约每个季度都会进行新的改进，但任何更改都是在极其谨慎和大量测试的前提下进行的。

基于我们15年的经验，S3是一个构建良好以及经过充分测试的系统。然而，我们曾一度无法确认S3索引子系统中一个bug的根本原因。该系统能够从异常中自动恢复，因此该bug的存在并没有影响系统的行为。但我们并不满足于此。

为什么这个bug存在这么久?像S3这样的分布式系统拥有大量组件，每个组件都有自己的异常情况(corner cases)，而且有可能同时发生很多异常情况。就S3而言，它拥有超过300个微服务，这些异常情况的潜在组合的数量是巨大的。即使开发人员有证据证明bug存在，并可能知道引起bug的根本原因，但对于开发人员来说，他们不可能考虑到所有异常情况，更不用说这些异常情况的不同组合了。

这种复杂性促使我们探索如何使用自动推理来探索可能隐藏在这些状态中的可能状态和错误。通过构建系统的正式规范，我们能够找到bug并证明未来不存在此类bug。使用自动推理也让我们有信心每一两个月发布一次更新和改进，而不是一年只发布三或四次。

更快的代码

Amazon Identity and Access Management (IAM)服务的正确性是确保我们客户工作负载安全的基础。每个发送到亚马逊云科技的请求即每个API 调用都由IAM授权引擎处理，这会涉及到数百万客户、数千种资源类型和数百种亚马逊云科技的服务。这种请求每秒就超过12亿次。这是亚马逊云科技中对安全要求最高以及需要高度扩展的软件之一。

在亚马逊云科技，任何改变在进入到生产环境之前，我们需要有极高的信心确保系统保持安全和正确。使用自动推理，我们可以证明我们的系统在几乎所有情况下遵守特定的安全属性。我们称之为可证明的安全性。自动推理不仅使我们能够为客户提供可证明的安全保证，还让我们能够大规模交付功能、安全性和优化。

与S3一样，IAM在过去超过15年时间里，已经成为一个经过时间考验的、值得信赖的系统。但我们想进一步提高标准。我们构建了一个正式规范来捕获现有IAM授权引擎的行为，将其策略评估原则编码为可证明的定理，并使用自动推理构建了一个新的、更高效的实施。今年早些时候，我们部署了新的经过证明正确的授权引擎——没人注意到。自动推理使我们能够无缝地用经证明正确的替换物代替授权引擎，一个最关键的亚马逊云科技基础设施之一。

有了规范和证明，我们可以很有信心的安全、积极地优化代码。在IAM的大规模下，每一微秒的性能改进都意味着更好的客户体验和我们自身更好的成本优化。我们优化了字符串匹配、删除了不必要的内存分配和冗余计算、加强了安全性并提高了可扩展性。每次更新后，我们都会再次运行证明，来确认系统仍在正确运行。

现在，优化后的IAM授权引擎相比之前快了50%。如果不使用自动推理，我们根本不可能这么有信心地进行如此重要的优化。

更快的代码部署

大多数在线安全交易都受到加密保护。例如，RSA加密算法通过生成两个密钥来保护数据：一个用于加密数据，另一个用于解密数据。这些密钥实现了安全的数据传输以及安全的数字签名。在加密这种场景下，正确性和性能至关重要——加密算法中的一个bug可能是灾难性的。

随着亚马逊云科技客户将工作负载迁移到Amazon Graviton上，针对ARM指令集的密码优化的好处也得到凸显。但是，通过加密优化获得更好的性能是很复杂的，这使得验证修改后的加密算法是否正常运行变得困难。在我们开始使用自动推理之前，对密码学库进行优化通常需要数月的审查，才能获得足够的信心将其投入生产环境。

自动推理的力量就在于此：正式验证使RSA更快，部署也更快。当我们将自动推理应用于椭圆曲线密码学时，我们也看到了类似的提升。

形成一个良性循环

我们在过去十多年间，在亚马逊云科技的内部越来越多的应用自动推理技术来证明我们的云基础设施和服务的正确性。我们经常使用这些方法不仅用于验证正确性，而且还用于增强安全性和可靠性，以及最小化设计缺陷。可以使用自动推理为一个系统创建一个精确且可测试的模型，使用该模型快速验证更改是否安全，或者发现它们是不安全的来避免对生产环节产生有害影响。

我们可以回答关于我们基础设施的一些关键问题，来检测可能导致数据泄露的错误配置。我们可以阻止一些我们无法通过其他技术发现的微妙但严重的错误进入生产环境。有了模型检查，我们获得了显著的性能优化，这是我们以往不敢尝试的。自动推理为关键系统按预期运行提供了严格的数学保证。

亚马逊云科技是唯一一家如此大规模使用自动推理的云提供商。随着越来越多的人使用自动推理工具，这让我们在提升自动推理工具的可用性和可扩展性上更容易进行大量的投入。我们发现自动推理工具越易于使用，它们的功能就会变得越强大，同时自动推理工具的采用率也会变得越高。我们越能证明云基础设施的正确性，对于那些看重安全的客户而言我们的云就越有吸引力。正如前文所述，我们不仅能够提高安全性，还能更快地为客户提供更高性能的代码，并最终节约客户的成本。

我们正处于一个新时代的开端，在这个时代大规模云架构的关键属性，诸如安全、合规性、可用性、持久性和防护等都可以实现自动证明。亚马逊与众不同之处就在于，我们从基础就用可靠的数学推理并持续分析我们所构建的一切，防止从AI幻觉到分析虚拟机监控程序、密码学和分布式系统等潜在问题的发生。