PDFAWS 的系统正确性实践
利用形式化和半形式化方法
马克·布鲁克和安库什·德赛
AWS (亚马逊云科技) 致力于提供客户可以完全信任的可靠服务。这要求保持安全、持久性、完整性和可用性的最高标准——系统正确性是实现这些优先事项的基石。2015 年 4 月发表在 Communications of the 上的一篇题为“亚马逊云科技如何使用形式化方法”的论文，重点介绍了确保关键服务正确性的方法，这些服务此后已成为 AWS 客户最广泛使用的服务之一。21
这种方法的核心是 TLA+，14 这是一种由莱斯利·兰波特开发的形式化规范语言。我们在 AWS 使用 TLA+ 的经验揭示了在实践中应用形式化方法的两个显著优势。首先，我们可以及早地识别和消除开发中的细微错误——这些错误是传统的测试方法难以发现的。其次，我们获得了深入的理解和信心，可以在保持系统正确性的同时实施积极的性能优化。
此外，15 年前，AWS 的软件测试实践主要依赖于构建时单元测试（通常针对模拟对象）和有限的部署时集成测试。从那时起，我们显著改进了我们的正确性实践，将形式化和半形式化方法都融入到开发过程中。随着 AWS 的发展，形式化方法变得越来越有价值——不仅用于确保正确性，还用于性能改进，尤其是在验证低级和高级优化的正确性方面。这种系统化的系统正确性方法已成为 AWS 规模下的力量倍增器，通过提高开发人员的效率来加快开发周期，同时为客户提供更具成本效益的服务。
本文概述了 AWS 用于交付复杂服务并对其正确性充满信心的形式化方法组合。我们考虑了形式化方法的广泛定义，其中涵盖了这些严谨的技术——从传统的形式化方法，如定理证明，7,10 演绎验证，18 和模型检查，8,14 到更轻量级的半形式化方法，如基于属性的测试，6,19 模糊测试，9 和运行时监控。11
P 编程语言
随着形式化方法的使用在 2010 年代初期扩展到 AWS 的初始团队之外，我们发现许多工程师难以学习和高效地使用 TLA+。这种困难似乎源于 TLA+ 的定义性特征：它是一种高级、抽象的语言，更像数学，而不是大多数开发人员熟悉的命令式编程语言。虽然这种数学本质是 TLA+ 的一个显著优势，并且我们仍然同意兰波特关于数学思维益处的观点，15 但我们也寻求一种语言，使我们能够对系统设计的关键方面进行模型检查（并在以后证明），同时对程序员来说更易于接受。
我们在 P 编程语言中找到了这种平衡。8 P 是一种基于状态机的语言，用于分布式系统的建模和分析。使用 P，开发人员将他们的系统设计建模为通信状态机，这是一种亚马逊开发人员群体熟悉的心理模型，他们中的大多数人基于微服务和 SOA（面向服务的架构）开发系统。P 自 2019 年以来一直在 AWS 开发，并作为战略开源项目进行维护。22 AWS 中构建其一些旗舰产品（从存储（例如，Amazon S3、EBS）到数据库（例如，Amazon DynamoDB、MemoryDB、Aurora）到计算（例如，EC2、IoT））的团队一直在使用 P 来推理其系统设计的正确性。
例如，P 被用于将 S3（简单存储服务）从最终一致性迁移到强读后写一致性。1 S3 的一个关键组件是其索引子系统，这是一个对象元数据存储，可实现快速数据查找。为了实现强一致性，S3 团队不得不对 S3 索引协议栈进行几项重要的更改。25 由于这些更改在 S3 规模下很难正确实现，并且团队希望以对正确性的高度信心交付强一致性，因此他们使用 P 来正式建模和验证协议设计。P 帮助在开发过程的早期消除了几个设计级别的错误，并使团队能够自信地交付有风险的优化，因为可以使用模型检查对其进行验证。
2023 年，AWS 的 P 团队构建了 PObserve，它提供了一个新工具，用于在测试和生产期间验证分布式系统的正确性。借助 PObserve，我们从分布式系统的执行中获取结构化日志，并事后验证它们是否与系统正式 P 规范允许的行为相匹配。这允许弥合系统设计的 P 规范与生产实现（通常使用 Rust 或 Java 等语言）之间的差距。虽然在设计时验证协议有很多好处，但在运行时监控实现的相同属性，使得对形式化规范的投资更有价值，并解决了实践中形式化方法部署的经典问题（即，将设计时验证与系统实现联系起来）。
轻量级形式化方法
AWS 使形式化方法更接近其工程团队的另一种方式是通过采用轻量级形式化方法。
基于属性的测试
利用轻量级形式化方法最显著的单一示例是 Amazon S3 的 ShardStore，该团队在整个开发周期中使用基于属性的测试，既用于测试正确性，又用于加速开发（Bornholt 等人详细描述了这一点。4）。他们方法中的关键思想是将基于属性的测试与开发人员提供的正确性规范、覆盖率引导的模糊测试（一种输入分布由代码覆盖率指标引导的方法）、故障注入（在测试期间模拟硬件和其他系统故障）和最小化（自动减少反例以帮助人工引导调试）相结合。
确定性模拟
AWS 广泛使用的另一种轻量级方法是确定性模拟测试，其中分布式系统在单线程模拟器上执行，该模拟器可以控制所有随机性来源，例如线程调度、计时和消息传递顺序。然后针对特定故障或成功场景编写测试，例如分布式协议中特定阶段参与者的故障。系统中的不确定性由测试框架控制，允许开发人员指定他们认为有趣的排序（例如，过去导致错误的排序）。测试框架中的调度程序也可以扩展，用于模糊化排序或探索所有可能的排序以进行测试。
确定性模拟测试将系统属性（如延迟和故障下的行为）的测试更接近构建时而不是集成测试。这加快了开发速度，并在测试期间提供了更完整的行为覆盖率。AWS 在线程排序和系统故障的构建时测试方面所做的一些工作已作为 shuttle (https://github.com/awslabs/shuttle) 和 turmoil (https://github.com/tokio-rs/turmoil) 项目的一部分开源。
持续模糊测试或随机测试输入生成
持续模糊测试，特别是覆盖率引导的可扩展测试输入生成，对于在集成时测试系统正确性也很有效。例如，在 Amazon Aurora 的数据分片功能（Aurora Limitless Database3）的开发过程中，我们广泛使用模糊测试来测试系统的两个关键属性。首先，通过模糊化 SQL 查询（和整个事务），我们验证了在分片上对 SQL 执行进行逻辑分区的逻辑是正确的。合成大量随机 SQL 模式、数据集和查询，并在被测引擎上运行，并将结果与基于非分片引擎的版本的 oracle 进行比较（以及其他验证方法，例如 SQLancer23 首创的方法）。
模糊测试与故障注入测试相结合，对于测试数据库正确性的其他方面（如原子性、一致性和隔离性）也很有用。在数据库测试中，事务是自动生成的，使用正式指定的正确性 oracle 定义其正确行为，然后针对被测系统执行事务和事务内语句的所有可能的交错。我们还使用事后验证隔离等属性（遵循 Elle13 等方法）。
故障注入即服务
2021 年初，AWS 推出了 FIS（故障注入服务）2，目标是使基于故障注入的测试可供广泛的 AWS 客户使用。FIS 允许客户将模拟故障（从 API 错误到 I/O 暂停和实例失败）注入到他们在 AWS 上的基础设施的测试或生产部署中。注入故障使客户能够验证他们构建到其架构中的弹性机制（例如故障转移和运行状况检查）是否确实有效以提高可用性，并且不会引入正确性问题。基于 FIS 的故障注入测试被 AWS 客户和亚马逊内部广泛使用。例如，Amazon.com 在 2024 年 Prime Day 准备期间运行了 733 个基于 FIS 的故障注入实验。
2014 年，Yuan 等人发现，在经过测试的分布式系统中，92% 的灾难性故障是由对非致命错误的错误处理触发的。许多被告知这项研究的分布式系统从业人员感到惊讶，这个百分比竟然没有更高。快乐场景的灾难性故障很少见，仅仅是因为系统的快乐场景经常执行，测试更好（无论是隐式还是显式），并且比错误场景简单得多。故障注入测试和 FIS 使从业人员更容易测试其系统在故障和失败下的行为，从而缩小快乐场景和错误场景错误密度之间的差距。
虽然故障注入不被认为是形式化方法，但它可以与形式化规范相结合。使用形式化规范定义预期行为，然后将故障注入期间和之后的结果与指定的行为进行比较，可以捕获比仅检查指标和日志中的错误（或让人类查看并说“是的，看起来差不多”）更多的错误。
亚稳态和涌现系统行为
在过去十年中，人们对一类特定的系统故障越来越感兴趣：其中一些触发事件（如过载或缓存清空）导致分布式系统进入一种状态，在这种状态下，如果没有干预（如将负载降低到正常水平以下），系统将无法恢复。这类故障被称为亚稳态故障，5 是云系统中不可用性最重要的原因之一。图 1（改编自 Bronson 等人5）说明了一种常见的亚稳态行为类型：系统负载的增加最初会遇到 goodput 的增加，然后是饱和，然后是拥塞，goodput 降至零（或接近零）。从那里，系统无法通过略微降低负载恢复到健康状态。相反，它必须沿着虚线走，并且可能要到负载显著降低后才能恢复。即使在简单的系统中也存在这种类型的行为。例如，它可以在大多数具有超时和重试客户端逻辑的系统中触发。
传统的分布式系统建模形式化方法通常侧重于安全性（不会发生坏事）和活性（最终会发生好事），但亚稳态故障提醒我们，系统具有多种行为，不能简单地这样分类。我们越来越多地转向离散事件模拟来理解系统的涌现行为，既投资于定制的系统模拟，也投资于允许使用现有系统模型（以 TLA+ 和 P 等语言构建）来模拟系统行为的工具。扩展详尽的模型检查器，如 TLA+ 的 TLC 与概率模拟，还可以生成统计结果，如后验延迟分布，使模型检查可用于理解延迟 SLA（服务级别协议）的可实现性等任务。
形式化证明
在某些情况下，本文迄今为止列举的形式化方法是不够的。例如，对于授权和虚拟化等关键安全边界，正确性证明可能是期望的，并且值得创建它们所需的重大投资。
2023 年，AWS 推出了 Cedar 授权策略语言，用于编写指定细粒度权限的策略。Cedar 专为自动化推理和形式化证明而设计。12,24 该语言旨在非常适合证明，并且实现是在具有验证意识的编程语言 Dafny 中构建的。使用 Dafny，该团队能够证明该实现满足各种安全属性。这种类型的证明超越了测试。它在数学意义上是一种证明。该团队还应用了差异测试方法，使用 Dafny 代码作为正确性 oracle 来验证生产就绪的 Rust 实现的正确性。将 Dafny 代码和测试程序以及 Cedar 实现一起作为开源发布，允许 Cedar 用户检查团队在正确性方面的工作。
另一个例子是 Firecracker VMM（虚拟机监控器）。Firecracker 使用一种名为 virtio 的低级协议，将模拟硬件设备（如网卡或固态硬盘）暴露给在 VM 内部运行的客户机内核。这种模拟设备是一个关键的安全边界，因为它是不可信的客户机和可信主机之间最复杂的交互。Firecracker 团队使用了一个名为 Kani20 的工具，该工具能够正式推理 Rust 代码，以证明此安全边界的关键属性。同样，这里的证明超越了测试，并确保此边界的关键属性无论客户机尝试做什么都成立。
围绕程序行为的证明是 AWS 软件正确性计划的重要组成部分，因此我们支持 Kani、Dafny18 和 Lean16 等工具以及为它们提供支持的底层工具（如 SMT（可满足性模理论）求解器）的开发。
使用形式化模型和规范的能力——用于在设计时对系统进行模型检查，用于通过运行时监控验证生产中的行为，作为正确性 oracle，用于模拟涌现系统行为，以及用于构建关键属性的证明——使 AWS 能够将开发这些规范的工程工作分摊到更大的业务和客户价值上。
超越正确性的好处
最后，正如前面提到的 2015 年的论文中所讨论的那样，形式化方法是安全地提高云系统性能的关键部分。在 P 和 TLA+ 中为 Aurora 关系数据库引擎的关键提交协议建模，使我们能够识别将分布式提交的成本从两次网络往返减少到 1.5 次网络往返的机会，而不会牺牲任何安全属性。对于采用形式化方法的团队来说，这类故事很常见，这至少由两种不同的动态驱动。
首先，深入思考和正式写下分布式协议的行为，迫使人们以结构化的方式思考，从而对协议的结构和要解决的问题产生更深入的见解。
其次，能够正式检查（并且在某些情况下，证明）提议的设计优化是正确的，这使得天生保守的分布式系统工程师在协议设计选择方面更大胆，而不会增加风险，并提高了开发人员交付可靠服务的速度。
这些生产力和成本效益不仅限于高级设计优化，还限于通常被忽略的低级代码。在一个例子中，AWS 团队在我们的基于 ARM 的 Graviton 2 处理器上识别了 RSA（Rivest-Shamir-Adleman）公钥加密方案实现的优化，这可以将吞吐量提高多达 94%。17
使用 HOL Light 交互式定理证明器，该团队能够证明这些优化的正确性。鉴于云 CPU 周期中有很大一部分用于密码学，这种类型的优化可以显著降低基础设施成本并有助于可持续性，同时提高客户可见的性能。
未来的挑战和机遇
尽管在过去 15 年中，在 AWS 扩展形式化和半形式化测试方法方面取得了显著成功，但一些挑战仍然存在，尤其是在形式化方法在工业界的采用方面。形式化方法工具的主要障碍包括其陡峭的学习曲线和所需的专业领域知识。此外，许多这些工具仍然具有学术性质，并且缺乏用户友好的界面。
即使是成熟的半形式化方法也面临采用挑战。例如，确定性模拟是一种关键的分布式系统测试技术，已在 AWS 和 FoundationDB 等项目中成功使用，但对于许多加入 AWS 的经验丰富的分布式系统开发人员来说仍然陌生。在采用其他经过验证的方法（如故障注入测试、基于属性的测试和模糊测试）方面也存在类似的差距。挑战在于教育分布式系统开发人员了解这些测试方法和工具，并教授严谨思维的艺术。
教育差距始于学术层面，即使是基本的形式化推理方法也很少被教授，这使得顶尖院校的毕业生难以采用这些工具。尽管形式化方法和自动化推理对于行业应用至关重要，但它们仍然被视为小众领域。我们预计，工业界对形式化方法和自动化推理的更多采用将吸引更多人才进入该领域。
大规模系统的亚稳态和其他涌现特性代表了另一个关键研究领域，也面临着类似的意识挑战。导致亚稳态系统行为的常见做法，例如“超时时重试 N 次”，尽管已知存在问题，但仍被广泛推荐。当前用于理解涌现系统行为的工具和技术仍处于早期阶段，使得系统稳定性建模既昂贵又复杂。该领域正在进行的研究具有广阔的进步潜力。
展望未来，我们相信大型语言模型和 AI 助手将显著帮助解决形式化方法在实践中的采用挑战。正如 AI 辅助单元测试已广受欢迎一样，预计这些工具很快将帮助开发人员创建形式化模型和规范，使这些先进技术更容易为更广泛的开发人员社区所接受。
结论
构建可靠和安全的软件需要一系列方法来推理系统正确性。除了行业标准的测试方法（如单元测试和集成测试）之外，AWS 还采用了模型检查、模糊测试、基于属性的测试、故障注入测试、确定性模拟、基于事件的模拟以及执行跟踪的运行时验证。形式化方法一直是开发过程的重要组成部分——也许最重要的是，形式化规范作为测试 oracle，为 AWS 的许多测试实践提供正确的答案。正确性测试和形式化方法仍然是 AWS 的关键投资领域，这些领域已经看到的投资回报加速了这一进程。
参考文献
1. 亚马逊云科技。2020 年。Amazon S3 现在为所有应用程序自动提供强读后写一致性； https://aws.amazon.com/about-aws/whats-new/2020/12/amazon-s3-now-delivers-strong-read-after-write-consistency-automatically-for-all-applications。（宣布为所有 AWS 区域的所有 S3 操作自动提供强读后写一致性。）
2. 亚马逊云科技。2021 年。宣布 AWS 故障注入模拟器正式发布，这是一种完全托管的服务，用于运行受控实验； https://aws.amazon.com/about-aws/whats-new/2021/03/aws-announces-service-aws-fault-injection-simulator/。
3. 亚马逊云科技。2023 年。宣布 Amazon Aurora Limitless Database； https://aws.amazon.com/about-aws/whats-new/2023/11/amazon-aurora-limitless-database/。
4. Bornholt, J.、Joshi, R.、Astrauskas, V.、Cully, B.、Kragl, B.、Markle, S.、Sauri, K.、Schleit, D.、Slatton, G.、Tasiran, S.、Van Geffen, J.、Warfield, A. 2021 年。使用轻量级形式化方法验证 Amazon S3 中的键值存储节点。在 SIGOPS 第 28 届操作系统原理研讨会论文集中，836–850； https://dl.acm.org/doi/10.1145/3477132.3483540。
5. Bronson, N.、Aghayev, A.、Charapko, A.、Zhu, T. 2021 年。分布式系统中的亚稳态故障。在操作系统热点研讨会论文集中，221–227； https://dl.acm.org/doi/10.1145/3458336.3465286。
6. Claessen, K.、Hughes, J. 2000 年。QuickCheck：Haskell 程序随机测试的轻量级工具。在第五届 SIGPLAN 国际函数式编程会议论文集中，268–279； https://dl.acm.org/doi/10.1145/351240.351266。
7. de Moura, L.、Ullrich, S. 2021 年。Lean 4 定理证明器和编程语言。在自动演绎 – CADE 28（第 28 届国际自动演绎会议，计算机科学讲义第 12699 卷，625–635。Springer； https://dl.acm.org/doi/10.1007/978-3-030-79876-5_37。
8. Desai, A.、Gupta, V.、Jackson, E.、Qadeer, S.、Rajamani, S.、Zufferey, D. 2013 年。P：安全的异步事件驱动编程。 SIGPLAN 通知 48(6), 321–332； https://dl.acm.org/doi/10.1145/2499370.2462184。
9. Fioraldi, A.、Maier, D.、Eißfeldt, H.、Heuse, M. 2020 年。AFL++：结合模糊测试研究的增量步骤。在第 14 届 Usenix 进攻性技术研讨会中； https://www.usenix.org/conference/woot20/presentation/fioraldi。
10. Harrison, J. 2009 年。HOL Light：概述。在第 22 届高阶逻辑定理证明国际会议论文集，德国慕尼黑，编辑，S. Berghofer、T. Nipkow、C. Urban 和 M. Wenzel，60–66，计算机科学讲义第 5674 卷。施普林格出版社； https://link.springer.com/chapter/10.1007/978-3-642-03359-9_4。
11. Havelund, K.、Rosu, G. 2019 年。运行时验证 – 17 年后。在运行时验证，第 18 届国际会议，RV 2018，塞浦路斯利马索尔，编辑，C. Colombo 和 M. Leucker，3–17，计算机科学讲义第 11237 卷。Springer； https://link.springer.com/book/10.1007/978-3-030-03769-7。
12. Hicks, M. 2023 年。我们如何使用自动化推理和差异测试构建 Cedar。亚马逊科学； https://www.amazon.science/blog/how-we-built-cedar-with-automated-reasoning-and-differential-testing。
13. Kingsbury, K.、Alvaro, P. 2020 年。Elle：从实验观察中推断隔离异常。VLDB 汇刊 14(3), 268–280； https://dl.acm.org/doi/10.14778/3430915.3430918。
14. Lamport, L. 2002 年。系统规范：硬件和软件工程师的 TLA+ 语言和工具。艾迪生韦斯利专业版。
15. Lamport, L. 2015 年。谁在没有绘制蓝图的情况下建造房屋？ 通讯 58(4), 38–41； https://dl.acm.org/doi/10.1145/2736348。
16. Lean Prover Community. 2024 年。Lean 4。GitHub； https://github.com/leanprover/lean4。
17. Lee, J.、Becker, H.、Harrison, J. 2024 年。形式化验证使 RSA 更快——并且部署更快。亚马逊科学； https://www.amazon.science/blog/formal-verification-makes-rsa-faster-and-faster-to-deploy。
18. Leino, K. R. M. 2010 年。Dafny：用于函数正确性的自动程序验证器。在第 16 届逻辑编程、人工智能和推理国际会议论文集中，348–370。施普林格出版社； https://dl.acm.org/doi/10.5555/1939141.1939161。
19. MacIver, D. R.、Hatfield-Dodds, Z. 等人。2019 年。Hypothesis：一种基于属性的测试的新方法。开源软件杂志 4(43), 1891； https://joss.theoj.org/papers/10.21105/joss.01891.pdf。
20. Monteiro, F.、Roy, P. 2023 年。使用 Kani 验证 AWS Firecracker 中的安全边界。技术报告，亚马逊云科技； https://model-checking.github.io/kani-verifier-blog/2023/08/31/using-kani-to-validate-security-boundaries-in-aws-firecracker.html。
21. Newcombe, C.、Rath, T.、Zhang, F.、Munteanu, B.、Brooker, M.、Deardeuff, M. 2015 年。亚马逊云科技如何使用形式化方法。 通讯 58(4), 66–73。 https://dl.acm.org/doi/10.1145/2699417。
22. P Team. 2024 年。P：用于分布式系统形式化规范的编程语言。 https://github.com/p-org/P。（在 AWS 和 Microsoft 中广泛用于分布式系统的形式化验证。）
23. Rigger, M.、Su, Z. 2020 年。通过枢轴查询合成测试数据库引擎。在第 14 届 Usenix 操作系统设计和实现研讨会，第 38 条，667–682； https://dl.acm.org/doi/10.5555/3488766.3488804。
24. Rungta, N. 2024 年。每天进行数万亿次形式化验证的授权！Splash 主题演讲； https://2024.splashcon.org/details/splash-2024-keynotes/3/Trillions-of-Formally-Verified-Authorizations-a-day-。
25. Vogels, W. 2021 年。深入了解 S3 一致性。所有事物分布式； https://www.allthingsdistributed.com/2021/04/s3-strong-consistency.html。（描述 Amazon S3 中强一致性实现的博客文章。）
马克·布鲁克是亚马逊云科技的杰出工程师，专注于 AI 和数据库。他对分布式系统、无服务器、系统正确性和形式化方法感兴趣。马克拥有开普敦大学电气工程博士学位。
安库什·德赛是亚马逊云科技的首席应用科学家，专注于构建工具和技术，以帮助开发人员交付具有高度正确性保证的分布式服务。他对提高开发人员生产力、形式化方法、系统测试、模糊测试和分布式系统感兴趣。安库什拥有加州大学伯克利分校计算机科学博士学位。
版权 © 2024 年归所有者/作者所有。出版权已许可给 。
最初发表于 Queue 第 22 卷，第 6 期——
在 数字图书馆 中评论本文
更多相关文章
阿喀琉斯·贝内托普洛斯 - 数据中心计算机的中间表示
我们已经到了分布式计算无处不在的地步。内存应用程序数据大小正在超过单台机器的容量，因此需要将其分区到集群中；在线服务具有高可用性要求，这只能通过将系统部署为多个冗余组件的集合来满足；高持久性要求只能通过数据复制来满足，有时甚至跨越广阔的地理距离。
大卫·R·莫里森 - 模拟：分布式系统中未充分利用的工具
模拟在 AI 系统的出现中发挥着巨大的作用：我们需要一种高效、快速且经济高效的方式来训练 AI 代理在我们的基础设施中运行，而模拟绝对提供了这种能力。
马特·法塔、菲利普-约瑟夫·阿里达、帕特里克·哈恩、贝琪·拜尔 - 企业到云端：谷歌的虚拟桌面
超过四分之一的 Googler 使用内部、数据中心托管的虚拟桌面。这种本地产品位于企业网络中，允许用户开发代码、访问内部资源以及从世界任何地方远程使用 GUI 工具。在其最显著的特性中，虚拟桌面实例可以根据手头的任务调整大小，具有持久的用户存储，并且可以在企业数据中心之间移动以跟随出差的 Googler。直到最近，我们的虚拟桌面都是使用名为 Ganeti 的自制开源虚拟集群管理系统托管在谷歌企业网络上可商购的硬件上的。今天，这项重要且对谷歌至关重要的工作负载在 GCP（谷歌计算平台）上运行。
帕特·赫兰 - 超越分布式事务的生活
本文探讨并命名了在拒绝分布式事务的世界中，在大型关键任务应用程序的实现中使用的一些实用方法。主题包括细粒度应用程序数据的管理，这些数据可能会随着应用程序的增长而随着时间推移重新分区。设计模式支持在这些可重新分区的数据块之间发送消息。
© 保留所有权利。