devgo.cn当你为AWS账户编写一条IAM策略时，怎么确保它不会意外开放敏感权限？传统做法是反复测试、审计，但总有遗漏的可能。亚马逊的答案是：用数学证明。过去十年，他们的自动推理组（ARG）一直在做这件事——不是靠测试，而是用形式化验证（一种用数学逻辑证明系统行为在所有可能场景下都正确的方法）来保证云基础设施的安全性和可靠性。
2016年，一个小型研究团队在亚马逊内部成立了ARG，目标是利用数学逻辑不仅测试AWS系统，而且证明它们正确工作。当时这个想法听起来很激进，但团队相信，像英特尔和NASA已经成功应用的形式化验证技术，也能在亚马逊规模下解决现实世界的安全和基础设施问题。十年后，他们的生产服务每天处理数十亿次查询，成果渗透到AWS的各个角落。
ARG的第一个演示日展示了几个项目，每个都回答了同一个根本问题：如何用数学证明系统安全正确？其中Sean McLaughlin演示的Tiros工具，能回答关于虚拟私有云（VPC）网络的任何连通性问题。Tiros后来成为Amazon Inspector中网络安全性分析功能的基础，也被AWS内部用于自动化合规检查。今天它同时驱动Amazon Inspector和Reachability Analyzer。另一个项目Zelkova，用自动推理分析策略及其未来影响，催生了S3 Block Public Access和IAM Access Analyzer等工具。这些服务的核心是SMT求解器（可满足性模理论求解器，一种能判断逻辑公式是否可满足的自动推理工具），它们提供关于系统行为的数学保证，远超传统测试的能力。
除了面向客户的服务，ARG最挑战性的工作集中在AWS内部基础设施——那些必须绝对正确的系统，因为数百万工作负载依赖于它们。他们用自动推理证明了Nitro隔离引擎（保护云实例的硬件安全模块）的正确性；验证了加密库s2n-bignum；证明了数据中心启动代码和S3存储系统的正确性。最令人印象深刻的是，他们完整证明并无缝替换了整个授权引擎——这个引擎每秒处理10亿API调用。他们用规范和证明，验证了新引擎对数千万亿次生产授权行为的正确性。ARG还利用证明助手Lean（一种帮助开发者构建形式化证明的自动化工具，由团队科学家Leo de Moura创建）来验证Nitro机密性引擎等更深层的系统，这为后续证明AWS策略解释器和加密基础的正确性奠定了基础。
一个意外的发现是：自动推理不仅让系统更安全，还让它们更高效、更易维护。当团队必须为验证编写精确规范时，他们常常发现更简单、更优雅的解决方案。这是因为自动推理采用系统性方法：不是考虑所有可能的输入场景并检查它们如何出错，而是定义系统应该如何工作，然后通过数学证明验证那些条件是否成立。这种纪律迫使团队深入思考，往往揭示出隐藏的简化机会。
随着AI时代的到来，ARG的研究找到了新应用。Amazon Bedrock Guardrails with Automated Reasoning checks用形式逻辑验证AI模型输出是否符合定义策略，防止幻觉，达到99%的验证准确率。Policy in Amazon Bedrock AgentCore用自动推理为代理行为设定清晰边界，确保自主操作时遵守合规要求。团队甚至可以用自然语言指定代理能访问哪些工具和数据。
对于开发者来说，这个故事的核心启示是：在关键系统设计中引入形式化验证，虽然前期需要投入编写精确规范，但长期回报巨大——不仅能获得数学级别的保证，还能倒逼出更简洁的设计。这种方法特别适用于安全策略、网络配置、加密协议、访问控制等需要高保证的场景。亚马逊的经验表明，数学严谨性和实用工程不是对立的，而是互补的。当你下次配置云资源时，不妨想想：如果有一个工具能数学证明你的策略正确，你会用它吗？
内容与图片版权归原作者所有 · 原文: https://www.amazon.science/blog/a-decade-of-mathematical-certainty-reflections-on-the-automated-reasoning-group