SymCrypt 中 Rust 密码学的形式化验证：从标准到代码
Rust、Lean、Aeneas 和 AI 智能体如何助力量产密码学算法的形式化验证
- SymCrypt 借助 Rust、Aeneas 和 Lean 来开发经过验证的新密码学实现，以提供更高的安全保障。
- 我们证明其代码能够安全、正确地实现各类标准算法，尤其是后量子密码学算法。
- 我们正陆续开源经过验证的代码、规约、性质及证明，首批涵盖 SHA-3 和 ML-KEM。
- Aeneas 能够验证大部分 Rust 代码，并在 Lean 中提供高效自动化以支撑证明工作。
- 智能体通过编写可独立校验的证明，进一步扩展了自动化的规模。
密码学代码是现代计算的基石。它守护着操作系统、云服务、固件、消息系统以及连接它们的各类协议。一个微小的失误都可能带来远超其份量的后果：一次算术上的疏忽、一个遗漏的边界检查、或一次错误的状态转换，都可能瓦解原本完善设计的安全性。
测试与审计仍然不可或缺，但仅靠它们并不够。密码学实现通常经过高度优化、具有常量时间特性、面向特定架构，并且有意保持底层。真正发布的代码很少和标准中那个简洁的算法长得一样：它包含模运算、位操作、SIMD 内建函数、精心设计的循环，以及为适应多种环境而添加的可移植层。
形式化验证正是为了弥补这一缺口——用机器可校验的证明取代单纯依赖测试的方法。验证并不仅仅检查代码在通常情况下行为正确，而是针对所有满足前置条件的输入，给出一个精确的数学规约。
去年 6 月，微软宣布将对 SymCrypt 中用 Rust 编写的新算法进行形式化验证。SymCrypt 是 Windows 和 Azure 等产品与服务所使用的加密提供商。新的加密实现正以安全的 Rust 语言编写，随后在 Lean（在新标签页中打开） 形式化证明框架中使用 Aeneas（在新标签页中打开） 工具链完成验证。这在后量子密码学领域尤为关键，因为它们需要复杂算法的高性能安全实现。这种组合为我们带来两层保障：Rust 消除了大类内存安全缺陷，而 Lean 证明则针对源自标准的形式化规范建立了功能正确性。
由此诞生了一种面向生产级密码学的新型验证方法：在开发者编写代码的同时进行验证，保留面向性能的实现选择，并使证明过程具有足够可扩展性，以跟上不断演进的代码库。
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）。该标准将算法描述为对 256 个模 q 系数进行的原地变换，通过三层嵌套循环，利用常数 ζ（= 17）的各次幂来更新成对的系数。
以下是 NIST 标准在 Lean 中的直接翻译，尽量贴近原始语法：
这个 Lean 版本刻意复刻了标准的结构：相同的循环嵌套、相同的 ζ 值选取、相同的系数更新方式，便于逐行人工审核。同时，它是可执行的，并使用数学类型，因此可以对照已知测试向量进行验证，并与关于 NTT 代数含义的高层定理建立联系。总之，Lean 规范是一个简洁、可执行、具备数学意义的模型，对标准的贴合程度足以同时供密码学家和证明工程师审阅。
将形式化规范与代码关联
规范形式化之后，下一个挑战是将其与实现关联起来。我们不要求开发者用面向验证的语言重写生产环境中的密码学代码，也不会生成需要产品团队接手维护的代码。相反，我们验证工程师实际编写的 Rust 代码，且代码保持原样。
Aeneas 通过将 Rust 的中间表示翻译为纯 Lean 模型来达成这一目标。Rust 的所有权和借用机制在这里至关重要：它们使 Aeneas 能够安全地省去大量关于指针别名、生命周期和可变性的推理——而这些正是 C 风格代码验证成本高昂的原因。
例如，一个在 Rust 中原地更新数组的函数，在 Lean 中会变成一个显式接收并返回函数式数组的函数。可变借用被翻译为值变换。这种方式在保留关键行为的同时，为证明工程师呈现了一个更易于推理的函数式模型。
进入 Lean 之后，就可以为该函数配备一个定理，声明它精化（refines）于某个形式化规范。也就是说，对于每个满足所需边界和良态条件的输入，实现函数返回的数学结果与源自标准的 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 的可扩展性让我们能够构建出一整套自动化手段，覆盖符号执行、算术、数组以及位向量推理。整体体验更接近调试：自动化负责处理常规的证明义务，当某个目标无法自动闭合时，工程师再去检查和细化证明。
支持 intrinsic 与多种架构
生产级的密码学不能忽视硬件。SymCrypt 必须运行在各种环境中，从嵌入式、内核场景一直到云服务。同时，它也需要在条件允许时利用平台特有的指令，包括 SIMD intrinsic 以及针对特定架构优化的路径。
因此，一种只对可移植参考实现有效的验证方案是不完整的。我们需要验证真正交付出去的代码：包括调度逻辑、优化过的例程，以及针对特定平台的变体。
下面的代码改编自 NTT 内部使用的 ntt_layer 函数。该函数在 x86-64 和 aarch64 上采用不同的编译方式，从而可以在面向特定平台的实现和可移植实现之间进行动态分派。在 x86-64 上，它检查 SSE2 指令是否可用；而在 aarch64 上，它检查 Neon 是否可用。
因为 rustc 的输出天然与目标平台相关，我们的工具链会按需验证的每个编译目标各编译一次代码，然后再合并对应的模型。实际上，这个合并过程把 Rust 代码里通过 cfg 属性实现的静态分发，变成了 Lean 模型中 x86-64 与 aarch64 之间的一层动态分发。接着，这些面向特定目标的模型会按照 Rust 代码的做法，再动态分发到 XMM、Neon 以及通用实现的模型上。
内建函数（intrinsics）需要稍有不同的处理方式。一些底层封装，尤其是那些操作裸指针或暴露平台指令的，会用经过仔细评审的 Lean 规约来建模。另一些则可以用 Rust 代码建模，与硬件参考文档比对测试后，再翻译并进行形式验证。围绕它们的 safe Rust 代码会针对这些模型进行验证。这样既保持了硬件加速带来的性能优势，又把可信面控制得很窄。
关键在于，验证并不意味着放弃优化。这套方法的目标是：保留生产代码中的各种复杂性——包括内建函数、分发机制以及平台相关实现——同时仍然证明一条单一、可审计的正确性声明。
把形式化保证反馈给代码开发者
形式化验证要在工程团队里规模化推广，前提是开发者能理解已经证明了什么。仅仅把证明放在仓库里是不够的；它必须对工程师维护的代码可见、可审阅，并且与之保持同步。
为此，我们通过自动生成的仪表板来展示验证结果。这些仪表板用开发者能理解的术语来汇总定理：前置条件、后置条件、覆盖的函数、可信模型以及剩余假设。工程师无需打开 Lean 就能看到已验证的内容。例如，下图展示的是仪表板为我们 ntt 函数显示的页面。
该规范清晰地呈现了 Lean 形式化开发中包含的定理陈述：它在水平线下方列出后置条件，上方列出函数输入和前置条件，并使用带链接的全限定名以便跳转到 Rust 和 Lean 的定义。
这个反馈循环对审查关于内建函数、特定目标代码以及边界条件的假设特别有用。例如，密码学开发者可以检查定理是否完整捕捉了他们期望代码保证的内容，从而发现形式化陈述过于薄弱，或者某个前置条件有误。
这些仪表盘也让验证与持续开发保持同步。随着 Rust 代码的变更，Lean 模型和证明可以重新生成并回放。当证明失败时，这种失败本身成为一种信号：要么是实现发生了需要更新证明的改动，要么是这个改动暴露了与规范之间真正的偏差。
这就把形式化验证从一次性研究产物转变为工程工作流的一部分。
智能体驱动的证明
最后一个要素是超越传统策略的自动化：AI 智能体。Lean 非常适合这一点，因为证明由一个小型的可信核心进行机器检查。智能体可以提出证明脚本，但 Lean 会独立验证该证明是否有效。
我们在两个环节使用智能体。首先，它们帮助将标准翻译成 Lean 规范。由于生成的规范是可执行的、与原始标准对齐的、针对官方向量进行过测试的、由数学定理支撑的，并且比实现简单得多，因此即便有智能体协助起草，也能对其进行彻底审计。
其次，智能体帮助编写和维护证明。借助合适的库、策略、示例和文档，智能体可以承担大量证明工作：展开生成的模型、应用辅助函数的规范、处理算术义务，以及在重构后修复证明。
这种做法的强大之处在于，Rust 代码与 Lean 证明是相互分离的。Agent 无需对生产环境中的 Rust 实现加注或修改就能完成证明。它们只在证明一侧工作，只要 Lean 验证通过，并且最终定理在陈述了所需保证的同时没有引入未经审查的假设，结果就会被接受。
在实际操作中，这改变了验证的成本结构。过去需要专家耗费数月才能完成的工作，如今可以大幅加速。证明工程师的角色也发生了变化——不再亲手编写每一条证明，而是转向设计规约、编排自动化工具、审查定理陈述，并引导 Agent 完成证明。
结语
验证过的密码学一直以来都面临着一个两难困境：最强的保证往往依赖专用工具链、生成代码以及难以被产品团队采用的工作流。而 Rust、Lean、Aeneas 以及基于 Agent 的证明自动化，让我们有机会重新审视这个权衡。
通过对实际编写的 Rust 代码进行验证、从标准中推导出可审计的规约、支持针对多架构的优化实现，并将证明结果反馈给开发者，形式化验证可以成为日常密码学工程的一部分，而不再是事后的研究活动。
这正是我们追求的长期愿景：密码学代码既保持快速、可移植、易维护、由开发者自主掌控，又附带机器可检验的证据，证明它确实实现了它所声称的标准。
在新标签页中打开
作者简介
Son Ho
研究员
了解更多Cédric Fournet
高级首席研究经理
了解更多
Antoine Delignat-Lavaud
首席研究员
了解更多
Samuel Lee
首席软件工程师
了解更多Jason Fisher
首席集团工程经理
Microsoft
了解更多
Jessica Krynitsky
高级项目经理
Microsoft
了解更多
编程语言与软件工程 
安全、隐私与密码学