AWS 系统正确性实践

利用形式化和半形式化方法

Marc Brooker 和 Ankush Desai

AWS (Amazon Web Services) 致力于提供客户完全信任的可靠服务。这需要维持最高标准的安全性、持久性、完整性和可用性——而系统正确性是实现这些优先事项的基石。2015 年 4 月发表在 Communications of the ACM 上的一篇题为《Amazon Web Services 如何使用形式化方法》的论文，重点介绍了确保关键服务正确性的方法，这些服务此后已成为 AWS 客户使用最广泛的服务之一。

该方法的核心是 TLA+，这是一种由 Leslie Lamport 开发的形式化规约语言。我们在 AWS 使用 TLA+ 的经验揭示了在实践中应用形式化方法的两个显着优势。首先，我们可以在开发的早期阶段识别并消除细微的 bug —— 这些 bug 会逃避传统的测试方法。其次，我们获得了深刻的理解和信心，可以在保持系统正确性的同时实施积极的性能优化。

此外，15 年前，AWS 的软件测试实践主要依赖于构建时的单元测试（通常针对 mocks）和有限的部署时集成测试。从那时起，我们显着改进了我们的正确性实践，将形式化和半形式化方法都集成到开发过程中。随着 AWS 的发展，形式化方法变得越来越有价值——不仅用于确保正确性，还用于性能改进，尤其是在验证低级和高级优化的正确性方面。这种系统化的系统正确性方法已成为 AWS 规模的倍增器，通过提高开发人员的速度来加快开发周期，同时为客户提供更具成本效益的服务。

本文概述了 AWS 用于交付复杂服务并对其正确性充满信心的形式化方法组合。我们考虑对形式化方法的广泛定义，其中包括这些严格的技术——从传统的形式化方法（如定理证明、演绎验证和模型检查）到更轻量级的半形式化方法（如基于属性的测试、fuzzing 和运行时监控）。

P 编程语言

随着 2010 年代初在 AWS 中将形式化方法的使用扩展到最初的团队之外，我们发现许多工程师难以学习 TLA+ 并提高生产力。这种困难似乎源于 TLA+ 的一个决定性特征：它是一种高级、抽象的语言，更像是数学，而不是大多数开发人员熟悉的命令式编程语言。虽然这种数学性质是 TLA+ 的一个显着优势，并且我们仍然同意 Lamport 关于数学思维益处的观点，但我们也寻求一种语言，该语言可以让我们对系统设计的关键方面进行模型检查（以及稍后证明），同时对程序员来说更容易接受。

我们在 P 编程语言中找到了这种平衡。 P 是一种基于状态机的语言，用于分布式系统的建模和分析。使用 P，开发人员将他们的系统设计建模为通信状态机，这是一种 Amazon 开发人员群体熟悉的心理模型，他们中的大多数人都在开发基于微服务和 SOA（面向服务的架构）的系统。P 自 2019 年以来一直在 AWS 开发，并作为一项战略性开源项目进行维护。AWS 中构建一些旗舰产品的团队——从存储（例如，Amazon S3、EBS）到数据库（例如，Amazon DynamoDB、MemoryDB、Aurora）到计算（例如，EC2、IoT）——一直在使用 P 来推理其系统设计的正确性。

例如，P 用于将 S3 (Simple Storage Service) 从最终一致性迁移到强读后写一致性。S3 的一个关键组件是其索引子系统，这是一个对象元数据存储，可实现快速数据查找。为了实现强一致性，S3 团队必须对 S3 索引协议栈进行多项重要的更改。由于这些更改很难在 S3 规模上正确实现，并且团队希望以高度的正确性信心交付强一致性，因此他们使用 P 来正式建模和验证协议设计。P 帮助在开发过程的早期阶段消除了几个设计级别的 bug，并允许团队放心地交付高风险优化，因为可以使用模型检查对其进行验证。

2023 年，AWS 的 P 团队构建了 PObserve，它提供了一个新工具，用于在测试和生产过程中验证分布式系统的正确性。使用 PObserve，我们从分布式系统的执行中获取结构化日志，并在事后验证它们是否与系统的正式 P 规范允许的行为相匹配。这允许弥合系统设计的 P 规范和生产实现（通常使用 Rust 或 Java 等语言）之间的差距。虽然在设计时验证协议有很多好处，但对实现的相同属性进行运行时监控使得对形式化规范的投资更有价值，并解决了在实践中部署形式化方法的经典问题（即，将设计时验证与系统实现联系起来）。

轻量级形式化方法

AWS 将形式化方法更贴近其工程团队的另一种方式是采用_轻量级形式化方法_。

基于属性的测试

利用轻量级形式化方法的最显着例子是 Amazon S3 的 ShardStore，该团队在整个开发周期中都使用了基于属性的测试，既可以测试正确性，又可以加快开发速度（Bornholt 等人对此进行了详细描述）。他们方法中的关键思想是将基于属性的测试与开发人员提供的正确性规范、覆盖率引导的 fuzzing（一种输入分布由代码覆盖率指标引导的方法）、故障注入（在测试期间模拟硬件和其他系统故障）和最小化（自动减少反例以帮助人工指导的调试）相结合。

确定性模拟

AWS 广泛使用的另一种轻量级方法是确定性模拟测试，其中分布式系统在单线程模拟器上执行，该模拟器可以控制所有随机性来源，例如线程调度、计时和消息传递顺序。然后，针对特定的故障或成功场景编写测试，例如参与者在分布式协议的特定阶段发生故障。系统中不确定性由测试框架控制，允许开发人员指定他们认为有趣的排序（例如，过去导致 bug 的排序）。还可以扩展测试框架中的调度程序，以进行排序的 fuzzing 或探索所有可能的排序以进行测试。

确定性模拟测试将系统属性（例如延迟和故障下的行为）的测试从集成测试转移到构建时。这加快了开发速度，并为测试期间提供更完整的行为覆盖。AWS 在线程排序和系统故障的构建时测试方面所做的一些工作已作为 shuttle (https://github.com/awslabs/shuttle) 和 turmoil (https://github.com/tokio-rs/turmoil) 项目的一部分进行了开源。

持续 fuzzing 或随机测试输入生成

持续的 fuzzing，尤其是覆盖率引导的可扩展测试输入生成，对于在集成时测试系统正确性也有效。例如，在开发 Amazon Aurora 的数据分片功能（Aurora Limitless Database）期间，我们广泛使用 fuzzing 来测试系统的两个关键属性。首先，通过 fuzzing SQL 查询（和整个事务），我们验证了在分片上进行 SQL 执行的逻辑分区是正确的。生成大量的随机 SQL 模式、数据集和查询，并在被测引擎上运行，并将结果与基于引擎的非分片版本的 oracle 进行比较（以及其他验证方法，例如 SQLancer 开创的方法）。

Fuzzing 与故障注入测试相结合，也可用于测试数据库正确性的其他方面，例如原子性、一致性和隔离性。在数据库测试中，会自动生成事务，使用正式指定的正确性 oracle 定义其正确行为，然后针对被测系统执行事务和事务中语句的所有可能的交错。我们还使用事后验证属性，例如隔离（遵循 Elle 等方法）。

故障注入即服务

2021 年初，AWS 推出了 FIS (Fault Injection Service)，旨在使基于故障注入的测试可供广泛的 AWS 客户使用。FIS 允许客户将模拟故障（从 API 错误到 I/O 暂停和实例故障）注入到 AWS 上其基础设施的测试或生产部署中。注入故障允许客户验证他们已构建到其架构中的弹性机制（例如故障转移和运行状况检查）实际上可以提高可用性，并且不会引入正确性问题。基于 FIS 的故障注入测试被 AWS 客户广泛使用，并且在 Amazon 内部也被广泛使用。例如，Amazon.com 运行了 733 个基于 FIS 的故障注入实验，为 2024 年的 Prime Day 做准备。

2014 年，Yuan 等人发现，经过测试的分布式系统中 92% 的灾难性故障是由对非致命错误的错误处理触发的。许多被告知这项研究的分布式系统从业者惊讶于该百分比没有更高。快乐路径的灾难性故障很少见，仅仅因为系统的快乐路径经常执行，测试得更好（无论是隐式还是显式），并且比错误情况简单得多。故障注入测试和 FIS 使从业者可以更轻松地测试其系统在故障下的行为，从而缩小了快乐路径和错误路径 bug 密度之间的差距。

虽然故障注入不被认为是形式化方法，但它可以与形式化规范相结合。使用形式化规范定义预期行为，然后在故障注入期间和之后将结果与指定的行为进行比较，可以捕获比仅检查指标和日志中的错误（或让人类查看并说“是的，看起来不错”）更多的 bug。

亚稳态和涌现系统行为

在过去的十年中，人们对一类特殊的系统故障越来越感兴趣：其中一些触发事件（如过载或缓存清空）导致分布式系统进入一种没有干预就无法恢复的状态（例如，将负载降低到正常水平以下）。这类故障被称为_亚稳态故障_，是云系统中不可用性的最重要因素之一。图 1（改编自 Bronson 等人）说明了一种常见的亚稳态行为：系统负载的增加最初会遇到吞吐量的增加，然后是饱和，然后是拥塞和吞吐量降至零（或接近零）。从那里，系统无法通过稍微降低负载来恢复到健康状态。相反，它必须遵循虚线，并且可能要到负载显着降低后才能恢复。即使在简单的系统中也存在这种类型的行为。例如，它可以由大多数具有超时和重试客户端逻辑的系统触发。

用于建模分布式系统的传统形式化方法通常侧重于_安全性_（不会发生坏事）和_活性_（最终会发生好事），但亚稳态故障提醒我们，系统具有各种无法以这种方式整齐地分类的行为。我们越来越多地转向离散事件仿真来理解系统的涌现行为，既投资于定制的系统仿真，也投资于允许使用以 TLA+ 和 P 等语言构建的现有系统模型来仿真系统行为的工具。扩展详尽的模型检查器（如 TLA+ 的 TLC）和概率仿真，还可以生成统计结果，如后验延迟分布，从而使模型检查可用于理解延迟 SLA（服务级别协议）的可实现性等任务。

形式化证明

在某些情况下，本文中列举的到目前为止的形式化方法是不够的。例如，对于授权和虚拟化等关键安全边界，正确性证明既是可取的，也值得创建它们所需的重大投资。

2023 年，AWS 推出了 Cedar 授权策略语言，用于编写指定细粒度权限的策略。Cedar 专为自动化推理和形式化证明而设计。该语言的设计非常适合证明，并且该实现是在验证感知的编程语言 Dafny 中构建的。使用 Dafny，该团队能够证明该实现满足各种安全属性。这种类型的证明超出了测试范围。它是在数学意义上的证明。该团队还应用了一种差异测试方法，使用 Dafny 代码作为正确性 oracle 来验证生产就绪的 Rust 实现的正确性。将 Dafny 代码和测试程序作为开源以及 Cedar 实现一起发布，允许 Cedar 用户检查团队在正确性方面所做的工作。

另一个例子是 Firecracker VMM（虚拟机监控器）。Firecracker 使用一种名为 virtio 的低级协议向在 VM 内部运行的访客内核公开模拟的硬件设备（例如网卡或固态驱动器）。此模拟设备是一个关键的安全边界，因为它是不可信的访客和可信主机之间最复杂的交互。Firecracker 团队使用了一个名为 Kani 的工具，该工具能够正式地推理 Rust 代码，以证明此安全边界的关键属性。同样，此处的证明超出了测试范围，并确保此边界的关键属性无论访客尝试做什么都保持不变。

围绕程序行为的证明是 AWS 软件正确性计划的重要组成部分，因此我们支持 Kani、Dafny 和 Lean 等工具的开发，以及为这些工具提供支持的底层工具（如 SMT (satisfiability modulo theories) 求解器）。

使用形式化模型和规范——用于在设计时进行模型检查系统，用于通过运行时监控来验证生产中的行为，通过充当正确性 oracle，用于模拟涌现的系统行为，以及用于构建关键属性的证明——允许 AWS 将开发这些规范的工程工作分摊到更大的业务和客户价值上。

超越正确性的好处

最后，正如前面提到的 2015 年论文中所讨论的那样，形式化方法是安全地提高云系统性能的关键部分。在 P 和 TLA+ 中建模 Aurora 关系数据库引擎的关键提交协议，使我们能够发现一个机会，即将分布式提交的成本从两次网络往返减少到 1.5 次，而不会牺牲任何安全属性。对于采用形式化方法的团队来说，这些类型的案例很常见，这至少是由两种不同的动态驱动的。

首先，深入思考并正式编写分布式协议的行为会迫使一种结构化的思维方式，从而导致对协议结构和要解决的问题的更深入的见解。

其次，能够正式检查（并且在某些情况下证明）所提出的设计优化是正确的，这使得天生保守的分布式系统工程师可以在不增加风险的情况下更大胆地做出协议设计选择，并提高开发人员交付可靠服务的速度。

这些生产力和成本优势不仅限于高级设计优化，还限于通常被忽略的低级代码。在一个例子中，AWS 团队发现了对其基于 ARM 的 Graviton 2 处理器上的 RSA (Rivest-Shamir-Adleman) 公钥加密方案实现的优化，这可以将吞吐量提高多达 94%。

使用 HOL Light 交互式定理证明器，该团队能够证明这些优化的正确性。鉴于云 CPU 周期中用于密码学的高百分比，这种类型的优化可以显着降低基础设施成本并有助于可持续性，同时提高客户可见的性能。

未来的挑战和机遇

尽管在过去 15 年中，AWS 在扩展形式化和半形式化测试方法方面取得了显着的成功，但仍然存在一些挑战，尤其是在形式化方法的工业采用中。形式化方法工具的主要障碍包括其陡峭的学习曲线和所需的专门领域专业知识。此外，许多这些工具本质上仍然是学术性的，并且缺乏用户友好的界面。

即使是完善的半形式化方法也面临着采用挑战。例如，确定性模拟是 AWS 和 FoundationDB 等项目中成功使用的关键分布式系统测试技术，但对于加入 AWS 的许多经验丰富的分布式系统开发人员来说仍然不熟悉。在采用其他成熟的方法（如故障注入测试、基于属性的测试和 fuzzing）方面也存在类似的差距。挑战在于让分布式系统开发人员了解这些测试方法和工具，教授严谨思维的艺术。

教育差距始于学术层面，即使是基本的正式推理方法也很少被教授，这使得顶尖机构的毕业生很难采用这些工具。虽然形式化方法和自动推理对于行业应用至关重要，但它们仍然被视为利基领域。我们预计，行业对形式化方法和自动推理的更多采用将吸引更多人才加入该领域。

大规模系统的亚稳态和其他涌现属性代表了另一个面临类似意识挑战的关键研究领域。导致亚稳态系统行为的常见做法，例如“超时时重试 N 次”，尽管已知存在问题，但仍被广泛推荐。用于理解涌现系统行为的当前工具和技术仍处于早期阶段，使得系统稳定性建模既昂贵又复杂。该领域正在进行的研究具有令人鼓舞的进步潜力。

展望未来，我们相信大型语言模型和 AI 助手将显着帮助解决形式化方法在实践中的采用挑战。正如 AI 辅助单元测试越来越受欢迎一样，预计这些工具很快将帮助开发人员创建形式化模型和规范，从而使这些先进技术更易于更广泛的开发人员社区访问。

结论

构建可靠和安全的软件需要一系列方法来推理系统正确性。除了行业标准测试方法（如单元和集成测试）之外，AWS 还采用了模型检查、fuzzing、基于属性的测试、故障注入测试、确定性模拟、基于事件的模拟和执行跟踪的运行时验证。形式化方法一直是开发过程的重要组成部分——也许最重要的是，形式化规范作为测试 oracle，为 AWS 的许多测试实践提供正确的答案。正确性测试和形式化方法仍然是 AWS 的关键投资领域，这些领域已经看到的投资回报加速了这些领域的投资。

参考文献

[参考文献列表，略]