意外的发现：自动推理常常使系统更高效且更易维护

关键要点

在最近一次访问美国国防高级研究计划局(DARPA)时，我提到了一个引人关注的趋势：在过去的10年中，我们在亚马逊网络服务(AWS)中应用自动推理时发现，经过正式验证的代码通常比其替代的未验证代码更具性能。

这种现象的原因在于，在正式验证过程中所进行的错误修复，通常会对代码的运行时产生积极影响。此外，自动推理还让我们的开发者在探索额外的优化时充满信心，从而进一步提升系统性能。我们发现，经过正式验证的代码更容易更新、修改和操作，从而减少了深夜日志分析和调试会议的次数。在本篇文章中，我将分享三个在与DARPA讨论时提到的例子。

自动推理：基础知识

在AWS，我们努力构建简单直观的服务供客户使用。然而，这种简单性下面却是庞大且复杂的分布式系统，这些系统每秒要处理数十亿个请求。验证这些复杂系统的正确性是一个重大挑战。我们的生产服务处于不断演变的状态，随着新功能的引入、组件的重新设计、安全性的增强和性能的优化，许多更改本身也很复杂，并且必须在不影响AWS或客户的安全性和弹性的前提下进行。

设计评审、代码审核、压力测试和故障注入等方法都是我们日常使用的宝贵工具，并且我们始终会继续使用。然而，我们发现需要补充这些技术，以确认许多情况下的正确性。微妙的错误仍然可能逃脱检测，特别是在大型、容错架构中。某些问题甚至可能根植于原始系统设计中，而不是实施缺陷。随着服务规模和复杂性的增长，我们不得不采用更强大的基于数学和逻辑的技术来补充传统的测试方法。这就是自动推理这一人工智能(AI)分支发挥作用的地方。

传统测试注重验证系统在特定场景下的行为，而自动推理旨在利用逻辑验证系统在任何可能场景下的行为。在一个中等复杂的系统中，复制所有可能的状态和参数组合所需的时间是不可行的。使用自动推理，可以通过计算系统正确性的逻辑证明，快速有效地实现相同的效果。

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

自动推理通过数学的视角观察系统的规格和实现，然后应用算法方法验证系统的数学表示是否满足规格。通过将我们的系统编码为数学系统，并使用形式逻辑进行推理，自动推理能够有效且权威地回答有关系统未来行为的关键问题。系统可以做什么？它会做什么？它绝对不会做什么？自动推理可以帮助回答这些问题，即使在最复杂、大规模且潜在的无界系统中，这些场景都无法通过传统测试方法进行详尽验证。

然而，自动推理能否帮助我们实现完美呢？并不能，因为它仍然依赖于对系统组件正确行为及其与环境模型关系的某些假设。例如，系统模型可能错误地假设底层组件如编译器和处理器没有错误尽管也可以对这些组件进行形式验证。尽管如此，自动推理允许我们在正确性方面获得比传统软件开发和测试方法更高的信心。

更快的开发

自动推理并不仅仅适用于数学家和科学家。我们的亚马逊简单存储服务(Amazon S3)工程师每天都在利用自动推理来预防错误。S3的简单接口背后是世界上最大且最复杂的分布式系统之一，存储着400万亿个对象和数十亿的数据，并且通常处理超过15亿个请求每秒。S3由多个子系统组成，每个子系统本身也是一个分布式系统，其中许多系统由数万台机器组成。新的功能不断被添加，而S3则在客户的重度使用下运行。

S3的一个关键组件是S3索引子系统，这是一个对象元数据存储，可以实现快速数据查找。该组件包含了非常大且复杂的数据结构，采用复杂且优化的算法。由于算法在S3规模下很难由人类准确实现，而我们不能在S3查找中容忍错误，因此我们每季度进行一次改进，因为需要极其谨慎和广泛的测试来自信地进行修改。

S3是一个建立在15年经验之上的良好构建和经受测试的系统。然而，S3索引子系统中存在一个错误，我们一时没有找到根本原因。系统能够自动从异常中恢复，因此这个错误并未影响系统的行为。不过，我们并不满意。

为什么这个错误存在这么久？像S3这样的分布式系统有大量组件，每个组件都有各自的边界情况，且多个边界情况可能同时发生。对于拥有超过300个微服务的S3来说，这些边界情况的可能组合数量是巨大的。开发者根本无法考虑所有这些边界情况，即使他们有证据表明错误的存在，且对其根源有一定想法更不用说所有可能的边界情况组合了。

这种复杂性促使我们考虑如何利用自动推理探索潜在的状态和可能隐含的错误。通过构建系统的正式规格，我们得以找出这个错误，并证明不存在其它类型的错误。使用自动推理也让我们有信心将在每一到两个月的时间内发布更新和改进，而不仅仅是每年三到四次。

更快速的代码

AWS身份与访问管理(IAM)服务的正确性对于我们客户工作负载的安全性至关重要。在数百万客户、成千上万的资源类型和数百种AWS服务中，每个API调用每个对AWS的请求都由IAM授权引擎处理。每天处理超过12亿个请求，这是AWS最安全且高度可扩展的软件之一。

在AWS中，任何更改进入生产之前，我们需要有极高的信心确保系统保持安全和正确。通过使用自动推理，我们可以证明我们的系统在各种情况下都遵循特定的安全属性。我们称之为可验证安全性。不仅如此，自动推理使我们能够向客户提供可验证的安全保证，同时还提升了功能、安全和优化的交付能力。

与S3类似，IAM已经经过15年的演变，成为一个经过时间考验和信任的系统。但我们想要提高标准。我们构建了一套形式规格，该规格捕获了现有IAM授权引擎的行为，并将其策略评估原则形式化为可证明的定理，然后使用自动推理构建一个新的、更高效的实现。今年早些时候，我们部署了新的经过证明正确的授权引擎但是没有人注意到。自动推理使我们能够无缝地用经过证明正确的等效物替代AWS基础设施中最关键的部分之一授权引擎。

有了该规格和证明，我们可以在高度自信的情况下安全且积极地优化代码。在IAM的大规模环境中，每微秒的性能提升都能带来更好的客户体验和更好的成本优化。我们优化了字符串匹配，消除了不必要的内存分配和冗余计算，加强了安全性，并提升了可扩展性。在每次更改之后，我们重新运行了我们的证明，以确认系统仍在正确运行。

优化后的IAM授权引擎比它的前任快50。如果没有使用自动推理，我们根本无法如此自信地进行这些有影响力的优化。如果您想深入了解我们是如何做到的，请查看这次AWS reInforce 会议。

更快的部署更快的代码

大多数安全在线交易都受到加密的保护。例如，RSA加密算法通过生成两个密钥来保护数据：一个用于加密数据，另一个用于解密数据。这些密钥不仅保障了数据传输的安全，还支持安全的数字签名。在加密的背景下，正确性和性能都是至关重要的加密算法中的错误可能会带来灾难。

随着AWS客户将其工作负载迁移到AWS Graviton，为ARM指令集优化加密的好处逐渐显现。但优化加密以提高性能是复杂的，这使得验证已修改的加密算法是否运行正常变得困难。在我们开始使用自动推理之前，加密库的优化通常需要数月的审查，以获取发布到生产环境的信心。

自动推理的力量进入这里：形式验证使RSA加速，且加速部署。当我们将自动推理应用于椭圆曲线密码学时，我们也看到类似的改进。

正循环的形成

在过去的十年里，我们逐渐在AWS中应用自动推理技术，以证明我们的云基础设施和服务的正确性。我们不仅经常利用这些方法进行正确性验证，还增强了安全性和可靠性，最大限度地减少设计缺陷。自动推理可以用来创建精确且可测试的系统模型，我们可以快速验证变更是否安全或者在不会对生产造成伤害的情况下了解到它们是不安全的。

我们能够回答关于基础设施的关键问题，以检测可能暴露数据的配置错误。我们可以帮助阻止潜在的但严重的错误进入生产，这些错误在其他技术下是无法发现的。我们可以大胆进行性能优化，而如果没有模型检查，这种优化是我们绝对不敢尝试的。自动推理提供了严密的数学保证，确保关键系统按预期表现。

AWS是首个也是唯一一个在如此规模上应用自动推理的云服务提供商。随着自动推理工具的采用增加，帮助我们正当其更大规模投资于改进自动推理工具的可用性和可扩展性变得更加容易。自动推理工具越容易使用，功能越强大，采用率便越高。我们越能够证明云基础设施的正确性，对于追求安全的客户，云便越具吸引力。正如本文中的例子所示，我们不仅能够提高安全保证，还能更快地向客户提供高性能代码，这转化为我们最终可以转嫁给客户的成本节约。

我预测，我们正处于一个新的时代的开端，在这一时代中，安全性、合规性、可用性、耐用性和安全等关键属性能够在大规模云架构中自动被证明。从预防AI幻觉的潜在问题到分析虚拟机监控程序、加密技术和分布式系统，拥有严谨的数学推理作为基础并持续分析我们的构建项目使亚马逊脱颖而出。

了解更多

如果您对本文有反馈，请在评论部分提交评论。如果您对本文有任何问题，请联系AWS支持。

Byron CookByron是伦敦大学学院(UCL)的计算机科学教授，英国皇家工程院院士。Byron于2015年创立了亚马逊自动推理组，目前担任AWS自动推理副总裁和杰出科学家。Byron的兴趣领域包括计算机和网络安全、程序分析与验证、编程语言、定理证明、逻辑、硬件设计、操作系统及生物系统。

标签：可验证安全性，安全博客