Amazon Science

A decade of mathematical certainty: Reflections on the Automated Reasoning Group

8.5内容质量

TL;DR · AI 摘要

AWS通过自动化推理组将形式验证技术规模化应用于生产系统，每日处理数十亿查询，数学证明AWS基础设施的正确性。

核心要点

  • ARG自2016年成立以来构建的系统每日处理数十亿查询，验证AWS基础设施数学正确性
  • Tiros和Zelkova工具演变为IAM Access Analyzer等服务，被数百万客户用于安全分析
  • 形式验证已证明Nitro隔离引擎、加密实现等关键AWS组件的正确性

结构提纲

按章节快速跳转。

  1. §引言

    2016年成立的ARG将形式验证从学术研究转化为AWS生产系统。

  2. ·技术演进

    Tiros和Zelkova工具发展为IAM Access Analyzer等客户服务。

  3. ›关键验证案例

    数学证明了Nitro隔离引擎和加密实现等核心AWS组件的正确性。

  4. ·生产规模应用

    ARG系统每日处理数十亿查询，保障AWS基础设施可靠性。

  5. ›行业影响

    验证技术从Intel/NASA扩展到AWS规模的基础设施验证。

思维导图

用一张图看清主题之间的关系。

查看大纲文本（无障碍 / 无 JS 友好）
  • 自动化推理与形式验证
    • 核心工具
      • Tiros
      • Zelkova
    • 生产应用
      • IAM Access Analyzer
      • Reachability Analyzer
    • 验证成果
      • Nitro Isolation Engine
      • 加密实现
      • 授权引擎

金句 / Highlights

值得收藏与分享的关键句。

#形式验证#AWS#自动化推理#安全#系统验证
打开原文

数学上的确定性十年：对自动化推理小组的反思 - 亚马逊科学

自动化推理

数学上的确定性十年：对自动化推理小组的反思

自动化推理小组成立十年后，数学逻辑已从学术研究转向生产服务，保障数百万客户工作负载的安全——这证明了系统可以被数学证明为正确，而不仅仅是大概率正确。

作者：Byron Cook 2026年8月11日 8分钟阅读

分享

  • 复制链接
  • 电子邮件
  • X
  • 领英
  • Facebook
  • Line
  • Reddit
  • QZone
  • 新浪微博
  • 微信
  • WhatsApp

分享到微信

x

关键要点

  • 亚马逊自动化推理小组（ARG）自2016年启动以来，将形式验证从学术研究转化为每日处理数十亿查询的生产系统，通过数学证明AWS基础设施的正确性，而不仅仅是测试。
  • ARG的基础工具Tiros和Zelkova演变为面向客户的服务，包括IAM访问分析器、Amazon Inspector和可达性分析器，数百万客户依赖这些服务进行具有数学保证的安全性和网络分析。
  • 该小组通过形式验证和SMT求解器，证明了关键AWS基础设施的正确性，包括Nitro隔离引擎、密码实现以及每秒处理十亿次API调用的授权引擎。

此回答是否有帮助？

2016年，亚马逊的一个小型研究团队通过启动自动化推理小组（ARG）向世界宣布我们的存在。我们的愿景是大胆的：不仅测试AWS系统，而是用数学逻辑以数学上的确定性证明它们能正确运行。

在随后的十年中，我们从探索形式验证的进展是否能缓解AWS规模下之前难以解决的问题，转变为构建AWS安全性和可靠性方法中基础的系统。我们小组的生产服务每天处理数十亿次查询。

这是回顾我们如何将前沿的形式验证和程序分析技术应用于亚马逊独特挑战的回顾。我们相信，通过AWS规模的数学严谨性，可以解决现实世界的安全和基础设施问题。毕竟，我们研究的工具已经在英特尔和NASA等地方证明了其成功。我们没有完全预料到的是，这些技术的应用范围会如此广泛。

从演示到大规模生产

2016年我们举办第一次ARG演示日时，向AWS安全团队展示了多个雄心勃勃的项目。每个项目都代表了解决同一基本问题的不同方法：我们如何用数学证明系统是安全且正确的？当天提出的答案为2026年AWS和客户继续依赖的系统奠定了基础。

自动化推理小组首个十年的关键里程碑。

Sean McLaughlin做了题为“用于推理虚拟私有云（VPC）的自动工具”的演讲。他指出，VPC网络的增长导致对能够识别配置错误或安全漏洞的自动化推理解决方案的需求增加。他的解决方案是“一个名为Tiros的工具，简单来说，它能回答关于您网络的问题。”

Tiros 成为了 Amazon Inspector 服务中网络安全性分析功能的基础，该服务被数百万在云端构建应用的客户使用。Tiros 同时也被 AWS 内部用于自动化检查许多 AWS 服务的合规认证和安全不变量遵循情况。如今，它同时为 Amazon Inspector 和 Reachability Analyzer 提供支持。这项工作后来分拆出来，形成了 Zelkova，该工具利用自动化推理分析策略及其未来影响。Zelkova 为 S3 Block Public Access 和 IAM Access Analyzer 等工具提供支持，还有许多其他工具也依赖它。

同样，当天关于深度自动分析在关键基础设施中应用的演讲，最终演变为我们证明 TLS 握手过程正确性以及密码学、存储和虚拟化代码其他属性的工作。

我们的愿景非常大胆：不仅用数学逻辑测试 AWS 系统，还要用数学确定性证明这些系统确实正确运行。

我们展示的一些小规模项目也产生了巨大影响。当我们展示针对高价值基础设施的演绎验证工作时，这项技术主要应用于我们密码协议的核心部分。随着证明助手（如 Lean，由我们 AR 团队的高级首席科学家 Leo de Moura 创建）等自动化工具的兴起，这项工作的重要性如今显著增长。我们现在可以将这些工具与语言模型结合，为更多更大规模的系统寻找证明。事实上，我们为 Nitro Confidentiality Engine 宣布的证明就是这一趋势的体现。它也是我们 AWS 策略解释器证明以及近期对密码学基础正确性证明工作的基础。

客户依赖的数学保证

过去十年间，ARG 的研究原型已演变为数百万 AWS 客户每天使用的服务。

IAM Access Analyzer 使用 Zelkova 帮助客户（如 USAA 和 GoTo）识别对其资源的非预期访问。客户不再依赖安全策略的正确配置，而是获得其策略实际允许权限的数学证明。

Reachability Analyzer 基于我们在 2016 年展示的 Tiros 服务构建，帮助客户在不发送任何数据包的情况下理解网络连接性。它通过数学分析所有可能的网络路径，判断目标是否可达，若不可达则识别阻断组件。

Amazon Bedrock Guardrails with Automated Reasoning 将数学验证引入生成式 AI。该功能通过形式逻辑验证模型响应是否符合定义策略，有效防止 AI 幻觉，验证准确率高达 99%。

这些面向客户的服务有一个共同基础：它们使用可满足性模理论（SMT）求解器和其他自动化推理技术，为系统行为提供数学保证，远超传统测试能力。

证明云基础设施下的核心系统

尽管面向客户工具展示了自动化推理的实用价值，但我们在 AWS 内部基础设施上的部分工作最具挑战性——这些系统必须绝对正确，因为数百万个工作负载依赖它们。

我们使用自动化推理技术证明了基础设施的正确性，包括：

  • AWS Nitro 隔离引擎
  • 加密实现方案如 s2n-bignum
  • AWS 数据中心中运行的启动代码
  • 存储系统如 S3

在一项特别雄心勃勃的项目中，我们通过形式化验证完全替换了处理每秒十亿次 API 调用的授权引擎。我们使用规范和证明，将新引擎与千万亿次生产环境授权记录进行了验证。

这些内部验证工作展示了自动化推理如何为云基础设施最基础的层级提供数学级的确定性。

意想不到的发现

我们十年工作的最大意外发现是：自动化推理不仅让系统更安全，还常常让系统更高效且更易于维护。当团队需要为验证编写精确规范时，他们经常发现更简单优雅的解决方案。

自动化推理不仅让系统更安全：它常常让系统更高效且更易于维护。

这在一定程度上归功于自动化推理带来的系统化方法。与验证特定场景下的系统行为不同，自动化推理使用逻辑来验证所有可能场景下的系统行为。我们不再需要考虑所有可能的输入场景及其潜在问题，而是定义系统应如何工作，并确定实现该行为的必要条件。然后我们可以通过数学证明验证这些条件是否成立。换句话说，我们可以验证系统本身是否正确。

这一发现验证了我们长期以来的信念：数学严谨性与工程实践并非对立力量，而是相辅相成的。形式化验证所需的严谨性经常揭示出原本可能被忽视的简化机会。

构建代理 AI 的基础

我们十年前开始的研究使我们独特地准备好了迎接下一代 AI 发展。我们在分布式系统和关键代码验证方面的工作，现在直接应用于验证 AI 生成的代码。同时，我们对误配置 AWS 策略和 VPC 网络的研究，现在也用于验证 AI 生成内容的正确性。

这一演进的证据体现在我们最近的一些发布中。Amazon Bedrock Guardrails 与自动化推理检查功能的结合标志着一个重要里程碑，使工具从需要深度专业知识的工具转变为直接嵌入到日常服务构建者使用的功能。

Amazon Bedrock AgentCore 中的策略功能使用自动化推理来为代理操作设置明确边界，确保代理在自主运行时始终处于定义的合规边界内。团队可以使用自然语言指定代理可以访问的工具和数据，当与 AgentCore Gateway 集成时，系统可在毫秒级时间内检查策略。

在 Kiro 这个智能体开发环境中，我们推出了一项需求分析能力，该能力通过自动推理证明在编写代码之前，软件需求中不存在矛盾、歧义和漏洞，从而提升代码准确性并避免未来的调试周期。构建 Kiro 的团队也使用自动推理技术，在公开发布功能之前验证底层 AI 生成代码的正确性。

随着 AI 智能体变得越来越自主并承担更复杂的任务，对其行为提供数学保证的需求变得至关重要。当 AI 智能体向具有形式化规范的系统提出代码修改建议时，这些系统可以自动将这些修改与数学证明进行验证。自动推理为构建不仅强大而且可证明安全可靠的 AI 系统提供了实现路径。

十年的协作

如果没有我们组建的才华横溢的团队以及信任我们帮助保障其关键基础设施的客户，这项工作将无法实现。在 AWS，各团队正在持续扩展自动推理能力。

十年来，我们将复杂性转化为可证明的正确性。

高级首席科学家 Daniel Kroening 及其团队在 Annapurna 推动硬件验证工作。高级应用科学家 Nadia Labai 正在开创自动形式化研究，教导 AI 系统将自然语言转换为形式化数学证明。AWS 安全部门的高级应用科学家 Tristan Ravitch 及其团队推出了 Peri，该工具可自动跟踪 AWS 和 Amazon 所有账户中的数据流，且对服务团队零上架流程。

这些努力使 AWS 有能力让下一个十年的自动推理工作与第一个十年一样具有变革性——甚至可能更加深远。

我们已实现的成果

十年后，我对我们取得的成就感到无比激动。我们证明了自动推理在每一层都能带来可衡量的价值：从防止配置错误到为 AI 系统行为提供数学保证。我们展示了数学严谨性与实际工程可以协同工作，以规模化解决真实客户问题。

从 2016 年首次演示日到今天，这段旅程体现了 AWS 将学术成果转化为客户每日依赖的服务的承诺。我们通过数学确定性建立了信任的基础——这一基础将在我们迎接下一个十年 AI 创新时发挥关键作用。

祝未来十年一切顺利。

研究领域

  • 自动推理
  • 安全、隐私和滥用预防

标签

  • 智能体 AI
  • 亚马逊网络服务（AWS）
  • 形式化验证

关于作者

亚马逊副总裁兼杰出科学家 Byron Cook 是形式化验证领域的领军人物，因其在 SAT、SMT 和符号模型检测方面的贡献而闻名，这些技术已应用于生物系统、计算机操作系统、编程语言和安全领域。Byron 在亚马逊的自动推理工作提高了云环境的保障水平，并带来了新的客户功能。