Verifying Rust cryptography in SymCrypt, from standards to code

在 SymCrypt 中验证 Rust 加密技术，从标准到代码 - 微软研究院

/.itemprop=publisher

/itemprop=image

在 SymCrypt 中验证 Rust 加密技术，从标准到代码

发布于 2026 年 7 月 13 日

作者：Son Ho（研究员）、Cédric Fournet（高级首席研究经理）、Antoine Delignat-Lavaud（研究员）、Samuel Lee（首席软件工程师）、Jason Fisher（首席小组工程经理）、Jessica Krynitsky（高级项目经理）

分享本页

• 在 Facebook 上分享

• 在 X 上分享

• 在 LinkedIn 上分享

• 在 Reddit 上分享

• 订阅我们的 RSS 订阅源

/#single-header

Rust、Lean、Aeneas 和 AI 代理如何帮助扩展生产加密算法的形式化验证

一目了然

• SymCrypt 使用 Rust、Aeneas 和 Lean 开发新的验证加密技术，提供更高的安全保障。

• 我们证明其代码能够安全且正确地实现标准算法，特别是后量子加密算法。

• 我们首次发布经过验证的代码、规范、属性和证明，涵盖 SHA-3 和 ML-KEM。

• Aeneas 能够验证大量 Rust 代码，并在 Lean 中提供高效的自动化工具支持证明工作。

• 代理通过编写可独立验证的证明，实现了自动化的扩展。

形式化验证的介绍与动机

加密代码是现代计算的基础。它保护操作系统、云服务、固件、消息系统以及连接它们的协议。小错误可能带来不成比例的后果：一个简单的算术错误、缺失的边界检查或错误的状态转换都可能破坏原本设计良好的安全性。

测试和审计仍然是必要的，但仅靠这些并不足够。加密实现通常经过优化，采用常数时间设计，针对特定架构，并且刻意保持底层实现。实际部署的代码很少像标准中描述的算法那样简洁：它包含约简操作、位操作、SIMD 内联函数、精心设计的循环结构，以及针对多种环境的可移植性层。

形式化验证通过部署机器可检查的证明来弥补这一缺陷，而非仅依赖测试。验证不再只是检查代码通常行为正确，而是为所有满足给定前提条件的输入实现精确的数学规范。

去年六月，微软宣布将在 SymCrypt（微软产品和服务中使用的加密提供库，包括 Windows 和 Azure）中对用 Rust 编写的新型算法进行形式化验证。新的加密实现采用安全的 Rust 编写，然后通过 Aeneas（opens in new tab）工具链在 Lean（opens in new tab）形式化证明框架中进行验证。这尤其适用于后量子加密领域，该领域需要对复杂算法进行快速且安全的实现。这种组合提供了双重保障：Rust 排除了大类的内存安全漏洞，而 Lean 证明则通过从标准推导出的形式化规范建立了功能正确性。

其结果是生产加密领域的新验证方法论：在开发者编写代码时即进行验证，保留面向性能的实现选择，并使证明过程具备足够的可扩展性以适应不断演进的代码库。

图1. 软件验证中的智能体（随机性，蓝色）和工具（算法性，绿色）。人工工作重点在于审查标准的形式化和主要属性。智能体负责编写证明和中间属性。编译、代码提取和证明验证是确定性过程，而非智能体驱动。

SymCrypt 中的验证现状

我们已开源了 SymCrypt 的一个分支（在新标签页中打开），其中包含形式化规范和证明。这个公开分支将证明工件与验证的 Rust 算法实现并行展示，展示了该方法论如何应用于生产级密码代码。SymCrypt 不是一个独立的研究原型；它是微软的开源密码库，被用于包括 Windows 和 Azure Linux 在内的各种产品和服务中。

此次发布的首个版本包含了完整的 Rust ML-KEM 和 SHA3 代码证明，这些代码目前正用于 Windows 的内部构建版本。SymCrypt 正在将基于 Rust、Lean 和 Aeneas 的工作流程扩展到更多原生 Rust 算法，并将其集成到 Windows 和 Linux 的生产版本中，例如经过验证的 Rust 代码实现 AES-GCM、FrodoKEM 和 ML-DSA 等算法。本文其余部分将以 SymCrypt 的工作作为具体示例进行说明，从公共标准如何转化为可执行的 Lean 规范开始。

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

第一步是形式化算法应执行的操作。对于密码学原语，权威来源通常是公开标准：NIST 规范、IETF RFC 或其他经过仔细审查的算法描述。

在我们的方法中，Lean 规范的设计会尽量贴近标准。当标准描述循环、数组更新或数学运算时，Lean 模型会尽可能遵循相同的结构。这种语法上的接近性非常重要：它使形式化规范更容易审计，因为审查者可以将标准与 Lean 代码并排对比。

Lean 还允许我们编写可执行的规范。这意味着我们可以将形式化模型与官方测试向量进行运行，以捕获转录错误、边界错误或对标准的误解。对于 ML-KEM 等算法，我们还可以进一步证明高层次的数学属性，例如证明数论变换的形式化模型与相关多项式环上的预期操作一致。

一个代表性示例是 ML-KEM 中的数论变换（NTT）。标准将该算法描述为对 256 个模 q 系数的原地变换，包含三个嵌套循环，使用常数 ζ（= 17）的连续幂来更新系数对。

以下是 Lean 中对 NIST 标准的直接翻译，尽可能贴近原始语法：

Lean 版本有意镜像标准的结构：相同的循环嵌套、相同的 ζ 选择和相同的系数更新，便于人工逐行审查。同时，它也是可执行的，并使用数学类型，因此可以与已知测试向量进行验证，并连接到关于 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函数可能引发恐慌的事实。

在这种情况下，定理指出，如果数组满足良好性不变量（确保它表示一个有效的多项式），那么运行Rust模型ntt将返回数学规范Spec.ntt结果的良好表示，前提是将底层数组转换为高层多项式。

将这种方法扩展到实际加密代码中的每个函数需要大量自动化。Lean的可扩展性使我们能够构建一个自动化梯度，包含符号执行、算术、数组和位向量推理的战术。这种体验更接近调试：自动化处理常规证明义务，而当目标无法自动关闭时，工程师可以检查并完善证明。

支持内在函数和多种架构

生产环境中的加密不能忽视硬件。SymCrypt必须在从嵌入式和内核环境到云服务的各种环境中运行。它还需要在可用时利用平台特定的指令，包括SIMD内在函数和架构特定的优化路径。

因此，仅适用于可移植参考实现的验证故事是不完整的。我们需要验证实际部署的代码：调度逻辑、优化例程以及针对特定目标的变体。

以下为翻译后的 Markdown 内容：

下方代码改编自 NTT 内部使用的 ntt_layer 函数。该函数针对 x86-64 和 aarch64 架构采用不同编译方式，实现对特定目标或通用实现的动态调度。在 x86-64 平台上，它会检查 SSE2 指令的可用性；在 aarch64 平台上则检查 Neon 指令的支持情况。

由于 rustc 的输出本质上是目标依赖的，我们的工具链会针对每个需要验证的编译目标多次编译代码，随后合并对应的模型。实际上，这种合并操作将 Rust 代码中通过 cfg 属性实现的静态调度，转化为 Lean 模型中 x86-64 与 aarch64 之间的第一层动态调度。遵循 Rust 代码的处理方式，这些特定目标的模型会进一步动态调度到 XMM、Neon 和通用实现的模型中。

对于 intrinsic 函数需要特殊处理。一些底层包装器（尤其是涉及原始指针操作或暴露平台指令的实现）通过经过仔细审查的小型 Lean 规范进行建模。其他实现则可以使用 Rust 代码进行建模，这些代码可基于硬件参考文档进行测试，随后被翻译并验证。外围的安全 Rust 代码会针对这些模型进行验证。这种方式在保持性能优势的同时，将可信表面控制得非常狭窄。

关键的一点是，验证过程并不需要牺牲优化。该方法论旨在保留生产代码的复杂性（包括 intrinsic、调度和平台特定实现），同时仍能证明一个可审计的正确性声明。

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

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

为实现这一点，我们通过自动生成的仪表板展示验证结果。这些仪表板以开发者友好的方式总结定理：前置条件、后置条件、覆盖函数、可信模型和剩余假设。工程师无需打开 Lean 即可查看验证内容。例如，下图展示了我们 ntt 函数的仪表板页面。

Figure 2. 展示 Rust 函数 mlkem.ntt 正确实现 NIST 标准中 NTT 的定理仪表板页面。

规范清晰呈现了 Lean 形式化开发中包含的定理声明：它通过水平线将函数输入和前置条件与后置条件分隔开，并使用完全限定名称配合链接导航到 Rust 和 Lean 定义。

这种反馈机制对于审查 intrinsic、特定目标代码和边界条件的假设特别有用。例如，密码学开发者可以检查定理是否完整地捕捉了代码应保证的内容，发现形式化声明过于宽松或前置条件错误等问题。

仪表板还将验证与持续开发对齐。当Rust代码发生变化时，Lean模型和证明可以重新生成并重放。当证明失败时，这会成为一个信号：要么实现方式发生了需要更新证明的变更，要么变更暴露了与规范之间的实际差异。

这将形式验证从一次性研究产物转变为工程工作流程的一部分。

代理证明

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

我们在两个方面使用代理。首先，它们帮助将标准转换为Lean规范。由于生成的规范是可执行的，与原始标准保持一致，经过官方测试用例验证，由数学定理支持，并且比实现本身简单得多，即使代理参与了起草，也可以对其进行彻底审计。

其次，代理帮助编写和维护证明。借助合适的库、战术、示例和文档，代理可以处理大量证明工作：展开生成的模型，为辅助函数应用规范，处理算术义务，以及在重构后修复证明。

这特别强大，因为Rust代码和Lean证明是分离的。代理不需要注释或修改生产环境的Rust实现来使证明通过。它们在证明端运行，只有当Lean验证通过且最终定理明确陈述所需保证而没有引入未经审查的假设时，结果才会被接受。

实际上，这改变了验证的经济性。以前需要数月专家努力的工作现在可以大幅加速。证明工程师的角色从手动编写每个证明转变为设计规范、整理自动化、审查定理陈述，并指导代理完成证明。

结论

验证密码学经常面临艰难的权衡：最强的保证来自于专用工具链、生成代码和难以被产品团队采用的工作流程。Rust、Lean、Aeneas和代理证明自动化使我们能够重新审视这种权衡。

通过验证原样编写的Rust代码，从标准中推导出可审计的规范，支持优化的多架构实现，并将证明结果反馈给开发人员，形式验证可以成为正常密码工程的一部分，而不是事后研究练习。

这就是长期承诺：保持快速、可移植、可维护且由开发人员掌控的密码代码，同时携带经过机器验证的证据，证明其实现了预期实现的标准。

[在新标签页中打开](链接)

作者介绍

卡片列包装器

卡片

卡片主体

Son Ho

研究员

卡片页脚

了解更多

Cédric Fournet

高级首席研究经理

Antoine Delignat-Lavaud

首席研究员

Samuel Lee

首席软件工程师

Jason Fisher

首席小组工程经理

微软

Jessica Krynitsky

高级项目经理

研究领域

• 编程语言与软件工程

• 安全、隐私与密码学