大规模应用自动推理提升系统效率

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

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

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

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

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

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

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

Amazon S3索引子系统是Amazon S3的一个关键组件，它是一个对象元数据存储，支持快速查找数据。该组件包含一个庞杂的数据结构和精密的优化算法。这些算法对于开发者来说很难被精准掌握，并且Amazon S3在查找时不能被容许发生任何错误，为此亚马逊云科技大约每个季度都会在极其谨慎和大量测试的前提下进行新的改进。

凭借亚马逊云科技15年的经验积淀，Amazon S3已发展成为一个稳健且经过严格测试的系统。然而，在Amazon S3索引子系统中曾出现一个难以追溯根源的bug，虽然系统具备自动异常恢复能力，让这个bug无法对整体系统造成影响，但它的存在并不能让一直追求更高稳定性和可靠性的亚马逊云科技开发人员满足。

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

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

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

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

与Amazon S3一样，Amazon IAM在过去超过15年时间里，已经成为一个经过时间考验的、值得信赖的系统。但亚马逊云科技想进一步提高标准，通过构建一个正式规范来捕获现有Amazon IAM授权引擎的行为，将其策略评估原则编码为可证明的规范，并使用自动推理实现更高效的实施。今年早些时候，通过使用自动推理工具，亚马逊云科技得以成功将原有授权引擎无缝替换并高效实施。

依托于规范和证明的支持，亚马逊云科技能够更有信心地安全优化代码。由于Amazon IAM的广泛应用，每一微秒的性能改进都意味着更好的客户体验和更好的成本优化。通过优化字符串匹配、删除不必要的内存分配和冗余计算，加强Amazon IAM的安全性并提高可扩展性。每次更新之后，开发团队都会重新运行证明，以确保系统继续按照预期运行。

如今，优化后的Amazon IAM授权引擎相比之前提速50%。自动推理不仅提高了性能，还极大增强了亚马逊云科技开发团队对系统稳定性的信心。

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

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

通过使用自动推理进行正式验证，不仅加速了RSA算法的运行效率，也加快了其部署速度；并且将这种应用于椭圆曲线密码学（一种加密技术）时，还能显著提升性能。

在过去十余年的时间里，亚马逊云科技积极应用自动推理技术确保其云基础设施和服务的正确性，同时增强其安全性和可靠性，并将设计缺陷最小化。开发人员可以使用自动推理为系统创建一个精确且可测试的模型，使用该模型快速验证更改是否安全，或者识别出安全隐患，以防止对生产环境造成不利影响。

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

亚马逊云科技在自动推理领域拥有先进的技术和经验积累，并大量投资提升其可用性和可扩展性。自动推理工具的可用性能增强其功能和采用率，同时验证云基础设施的正确性，并吸引重视安全的客户。自动推理不仅提高安全性，还能加速提供高性能代码，帮助客户节省成本。

经过10多年的实践，我们发现验证过的代码性能更佳，因为验证过程中的bug修复提升了代码的运行性能。自动推理强化开发者信心，激励他们探索更深层次的优化，这不仅简化了代码的维护和操作，还显著提升了系统的整体性能。