如何借助 Rust、Lean、Aeneas 和 AI agent 为生产级密码学算法规模化形式化验证

概览

SymCrypt 使用 Rust、Aeneas 和 Lean 开发新的经过验证的密码学算法，以提供更高的安全保障。我们证明其代码安全且正确地实现了标准算法，尤其是后量子密码学算法。我们首先为 SHA-3 和 ML-KEM 发布了经过验证的代码、规范、属性和证明。Aeneas 能够验证 Rust 代码的很大一部分，并在 Lean 中提供高效的自动化支持，以辅助证明工作。Agent 通过编写可独立验证的证明来实现自动化的规模化。

形式化验证的引言与动机

密码学代码是现代计算的基石。它保护着操作系统、云服务、固件、消息系统以及连接它们的协议。微小的错误可能造成巨大的后果：一次算术失误、缺少边界检查或错误的状态转换，都可能破坏一个原本设计良好的方案的安全性。测试和审计仍然至关重要，但仅靠它们是不够的。密码学实现通常是经过优化的、恒定时间的、特定于架构的，并且有意保持底层。实际发布的代码很少像标准中的简洁算法：它包含约简、位操作、SIMD 内联函数、精心设计的循环以及针对多种环境的可移植层。

形式化验证通过部署机器检查的证明来弥补这一差距，而不是仅仅依赖测试。验证不是仅仅检查代码通常是否行为正确，而是对所有满足所述前置条件的输入实现精确的数学规范。

去年六月，微软宣布将对 SymCrypt 中用 Rust 编写的新算法进行形式化验证。SymCrypt 是跨 Windows 和 Azure 等产品和服务使用的密码学提供程序。新的密码学实现正在用安全的 Rust 编写，然后使用 Aeneas 工具链在 Lean 形式化证明框架中进行验证。这尤其适用于后量子密码学，后者需要复杂算法的快速安全实现。

这种组合为我们提供了两层保障：Rust 排除了大类的内存安全错误，而 Lean 证明则根据从标准推导出的形式化规范建立了功能正确性。其结果是产生了一种用于生产级密码学的新验证方法论：在开发者编写代码时进行验证，保留面向性能的实现选择，并使证明过程具有足够的可扩展性以跟上不断演进的代码库。

图 1. 用于软件验证的 Agent（随机的，蓝色）和工具（算法性的，绿色）。人类工作专注于审查标准的形式化和主要属性。Agent 编写证明和中间属性。编译、代码提取和证明验证是确定性的，而非 agentic 的。

SymCrypt 中的验证状态

我们已经开源了一个 SymCrypt 分支，其中包含形式化规范和证明。这个公共分支将证明产物与它们所验证的 Rust 算法实现一同提供，展示了该方法论如何应用于生产级密码学代码。SymCrypt 不是一个独立的研究原型；它是微软的开源密码学库，用于包括 Windows 和 Azure Linux 在内的产品和服务。此次首次发布包含了当前 Windows 内部版本中使用的 Rust ML-KEM 和 SHA3 代码的完整证明。SymCrypt 正在将相同的基于 Rust、Lean 和 Aeneas 的工作流扩展到更多 Rust 原生算法，并将它们集成到 Windows 和 Linux 的生产版本中，例如包括 AES-GCM、FrodoKEM 和 ML-DSA 的经过验证的 Rust 代码。

本文的其余部分将以此 SymCrypt 工作为具体示例，从公共标准如何成为可执行的 Lean 规范开始。

将标准转化为形式化的 Lean 规范

第一步是形式化算法应该做什么。对于密码学原语，真相来源通常是公共标准：NIST 规范、IETF RFC 或其他经过仔细审查的算法描述。在我们的方法中，Lean 规范被设计为尽可能贴近标准。当标准描述一个循环、一个数组更新或一个数学运算时，Lean 模型尽可能遵循相同的结构。这种语法上的接近很重要：它使形式化规范更容易审计，因为审查者可以并排比较标准和 Lean。

Lean 还允许我们编写可执行的规范。这意味着我们可以针对官方测试向量运行形式化模型，以捕获转录错误、差一错误或对标准的误解。对于像 ML-KEM 这样的算法，我们可以更进一步，证明高级数学属性，例如展示数论变换的形式化模型对应于相关多项式环上的预期运算。

一个代表性的例子是来自 ML-KEM 的数论变换（NTT）。标准将该算法描述为对模 q 的 256 个系数的原地变换，具有三个嵌套循环，使用常数 ζ (= 17) 的连续幂更新系数对。以下是 NIST 标准在 Lean 中的直接翻译，试图尽可能贴近原始语法：

Lean 版本刻意镜像了标准的结构：相同的循环嵌套、相同的 zeta 选择以及相同的系数更新，便于逐行人工审查。同时，它是可执行的，并使用数学类型，因此可以针对已知向量进行测试，并连接到关于 NTT 代数含义的更高级定理。

总之，Lean 规范是一个简洁、可执行、具有数学意义的模型，它足够贴近标准，可供密码学家和证明工程师共同审查。

将形式化规范连接到代码

一旦规范被形式化，下一个挑战就是将其连接到实现。我们不要求开发人员用面向验证的语言重写生产级密码学代码，也不生成产品团队必须维护的代码。相反，我们验证工程师编写的 Rust 代码，完全按照他们编写的方式。

Aeneas 通过将 Rust 的中间表示翻译成纯 Lean 模型来实现这一点。Rust 的所有权和借用规则在这里至关重要。它们让 Aeneas 能够安全地消除大量关于指针别名、活跃性和可变性的推理，这些推理使得对 C 风格代码的验证成本高昂。例如，一个原地更新数组的 Rust 函数，在 Lean 中变成了一个显式接收并返回函数式数组的函数。可变借用被转换为值变换。这保留了重要的行为，同时向证明工程师呈现一个更容易推理的函数式模型。

一旦进入 Lean，该函数就可以配备一个定理，声明它精炼了一个形式化规范。换句话说，对于每个满足所需边界和良好形式条件的输入，实现函数返回与源自标准的 Lean 规范相同的数学结果。

这种风格保持了职责的清晰分离。软件工程师继续编写惯用的、高性能的 Rust 代码。验证工程师则针对生成的 Lean 模型工作，并证明关于它们的定理。Rust 代码和证明并存，但证明负担不会使代码变得不自然。

回到 NTT 示例，其 Rust 实现是一个函数 fn ntt(&mut [u16; 256])，它使用可变借用来原地更新数组。Lean 翻译将其纯化为一个函数 ntt : Array U16 256#usize → Result (Array U16 256#usize)，它直接输出更新后的数组，同时将其包装在 Result 类型中以显式捕获 Rust 函数可能 panic 的事实。在这种情况下，定理声明：如果数组满足一个良好形式不变量（确保它表示一个有效的多项式），那么运行 Rust 模型 ntt 会返回数学规范 Spec.ntt 结果的良好形式表示，并经过从底层数组到高层多项式的转换。

将这一点扩展到真实密码学代码中的每个函数需要大量的自动化。Lean 的可扩展性使我们能够使用用于符号执行、算术、数组和位向量推理的策略来构建自动化的梯度。体验变得更接近调试：自动化处理常规的证明义务，而工程师可以在目标未自动关闭时检查和细化证明。

支持内联函数和多架构

生产级密码学不能忽视硬件。SymCrypt 必须在从嵌入式、内核环境到云服务的各种环境中运行。它还需要在可用时利用平台特定的指令，包括 SIMD 内联函数和特定于架构的优化路径。因此，一个仅适用于可移植参考实现的验证故事是不完整的。我们需要验证实际发布的代码：分发逻辑、优化例程和特定于目标的变体。

下面的代码改编自 NTT 内部使用的 ntt_layer 函数。该函数针对 x86-64 和 aarch64 进行不同的编译，允许动态分发到特定于目标或可移植的实现。在 x86-64 上，它检查 SSE2 指令的可用性，而在 aarch64 上，它检查 Neon。

由于 rustc 的输出本质上是特定于目标的，我们的工具链多次编译代码，每个需要验证的编译目标一次，然后合并相应的模型。实际上，这个合并操作将 Rust 代码中 cfg 属性允许的静态分发，转变为 Lean 模型中 x86-64 和 aarch64 之间的第一层动态分发。遵循 Rust 代码的做法，这些特定于目标的模型随后自身动态分发给 XMM、Neon 和通用实现的模型。

内联函数需要稍微不同的处理。一些底层包装器，尤其是那些操作原始指针或暴露平台指令的包装器，由经过仔细审查的小型 Lean 规范建模。其他的可以使用 Rust 代码建模，这些代码可以针对硬件参考文档进行测试，然后进行翻译和验证。周围的 safe Rust 代码随后针对这些模型进行验证。这保持了可信计算基的狭窄，同时保留了硬件加速的性能优势。

重要的一点是，验证不需要放弃优化。该方法论旨在保留生产代码的复杂性——包括内联函数、分发和平台特定实现——同时仍然证明一个单一的、可审计的正确性声明。

将形式化保证反馈给代码开发者

只有在开发者能够理解已证明的内容时，形式化验证才能在一个工程组织中规模化。仅仅在仓库中存在一个证明是不够的；保证必须是可见的、可审查的，并与工程师维护的代码同步。

为了支持这一点，我们通过自动生成的仪表板来展示验证结果。这些仪表板以开发者友好的术语总结定理：前置条件、后置条件、覆盖的函数、可信模型和剩余假设。工程师无需打开 Lean 就能看到哪些内容已被验证。

例如，下面是我们 ntt 函数的仪表板显示的页面。

图 2. 定理的仪表板页面，显示 Rust 函数 mlkem.ntt 正确实现了 NIST 标准中指定的 NTT。规范清晰地展示了 Lean 形式化开发中包含的定理陈述：它将函数输入和前置条件与后置条件分开，将它们放在水平线上方，并使用带有链接的完全限定名称来导航到 Rust 和 Lean 定义。

这个反馈循环对于审查关于内联函数、特定目标代码和边界条件的假设特别有用。例如，密码学开发者可以检查定理是否完全捕捉了他们期望代码保证的内容，并注意到形式化陈述太弱，或者前置条件错误。

仪表板还将验证与持续开发对齐。随着 Rust 代码的变化，Lean 模型和证明可以被重新生成和重放。当证明失败时，该失败成为一个信号：要么实现以需要更新证明的方式发生了变化，要么该变化暴露了与规范的真实差异。这将形式化验证从一次性的研究产物转变为工程工作流的一部分。

Agentic 证明

最后的要素是超越传统策略的自动化：AI agent。Lean 非常适合这一点，因为证明是由一个小的可信内核进行机器检查的。Agent 可以提出一个证明脚本，但 Lean 独立验证该证明是否有效。

我们在两个地方使用 agent。首先，它们帮助将标准翻译成 Lean 规范。由于生成的规范是可执行的、与原始标准对齐、经过官方向量测试、得到数学定理支持，并且比实现简单得多，即使 agent 帮助起草了它，它也可以被彻底审计。

其次，agent 帮助编写和维护证明。有了正确的库、策略、示例和文档，agent 可以处理大量的证明工作：展开生成的模型、应用辅助函数的规范、处理算术义务以及在重构后修复证明。这一点尤其强大，因为 Rust 代码和 Lean 证明是分离的。Agent 不需要注释或修改生产 Rust 实现就能使证明通过。它们在证明侧工作，并且只有当 Lean 验证了结果并且最终定理陈述了所需的保证而没有引入未经审查的假设时，结果才会被接受。

在实践中，这改变了验证的经济性。以前需要专家数月努力的工作现在可以显著加速。证明工程师的角色从手动编写每个证明转变为设计规范、管理自动化、审查定理陈述以及引导 agent 完成其证明。

结论

经过验证的密码学常常面临一个艰难的权衡：最强的保证来自专门的工具链、生成的代码以及产品团队难以采用的工作流。Rust、Lean、Aeneas 和 agentic 证明自动化让我们能够重新审视这一权衡。通过按原样验证 Rust 代码、从标准推导出可审计的规范、支持优化的多架构实现，并将证明结果反馈给开发者，形式化验证可以成为常规密码学工程的一部分，而不是事后的研究练习。这就是长期的承诺：密码学代码保持快速、可移植、可维护且由开发者拥有，同时携带机器检查的证据，证明它实现了其旨在实现的标准。

本文最初发表于 Microsoft Research。