密码学代码支撑着现代计算系统中的重要防护。了解一种新方法如何帮助开发者在编写代码时验证其正确性，同时在实现和演进过程中保持速度和适应性。https://t.co/mgPeyXohDV https://t.co/G6EXSuQwcz

扩展密码学验证以提升计算机安全

来源：https://www.microsoft.com/en-us/research/blog/verifying-rust-cryptography-in-symcrypt-from-standards-to-code/

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

图表展示了验证密码代码的过程。标准中的算法被转换为形式化规范，而 Rust 代码被转换为代码模型。然后通过证明和验证步骤对规范和代码模型进行比较。## 概览

• SymCrypt 使用 Rust、Aeneas 和 Lean 开发新的经过验证的密码学，以提供更高的安全保障。
• 我们证明其代码安全且正确地实现了标准算法，特别是针对后量子密码学。
• 我们最初发布经过验证的 SHA-3 和 ML-KEM 的代码、规范、属性和证明。
• Aeneas 允许验证 Rust 代码的很大一部分，并在 Lean 中提供高效的自动化以支持证明工作。
• 代理通过编写可以独立验证的证明来扩展自动化。

形式验证的介绍与动机

密码学代码是现代计算的基础。它保护着操作系统、云服务、固件、消息系统以及连接它们的协议。微小的错误可能导致巨大的后果：一个算术失误、遗漏的边界检查或错误的状态转换都可能破坏原本安全的设计。

测试和审计仍然是必不可少的，但它们本身是不够的。密码学实现通常经过优化、常时执行、针对特定架构，并且故意保持在低级层面。发布的代码很少看起来像标准中的简洁算法：它包含了归约、位操作、SIMD 内建函数、精心设计的循环以及针对多种环境的可移植层。

形式验证通过部署机器检查的证明而不是仅仅依赖测试来解决这一差距。验证不是仅仅检查代码通常表现正确，而是对所有满足规定前提条件的输入实现精确的数学规范。

去年六月，微软宣布我们将对 SymCrypt 中用 Rust 编写的新算法进行形式验证。SymCrypt 是微软的密码学库，用于包括 Windows 和 Azure 在内的产品和服务。新的密码学实现正在使用安全 Rust 编写，然后通过 Aeneas 工具链在 Lean 形式证明框架中进行验证。这尤其适用于后量子密码学，它需要复杂算法的快速安全实现。这种组合为我们提供了两层保障：Rust 排除了大量内存安全错误，而 Lean 证明则针对从标准导出的形式规范建立了功能正确性。

其结果是产生了一种用于生产级密码学的新验证方法论：在开发者编写代码时进行验证，保留面向性能的实现选择，并使证明过程足够可扩展以跟上不断发展的代码库。

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

我们开源了一个 SymCrypt 分支，其中包含形式规范和证明。该公共分支将证明工件与它们验证的 Rust 算法实现一起提供，展示了该方法如何应用于生产级密码代码。SymCrypt 不是一个独立的研究原型；它是微软的开源密码学库，用于包括 Windows 和 Azure Linux 在内的产品和服务。

此首次发布包括当前在 Windows 内部版本中使用的 Rust ML-KEM 和 SHA3 代码的完整证明。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）。标准将该算法描述为一个对模 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 函数仪表板显示的页面。

已验证的 symcrust::mlkem::ntt 函数形式规范截图。页面显示了一个绿色的“已验证”徽章，指向 Lean 模型和源代码的链接，以及一个说明 NTT 实现必须满足的数学条件的规范。图2. 证明 Rust 函数 mlkem.ntt 正确实现了 NIST 标准中指定的 NTT 的定理的仪表板页面。规范清晰地展示了 Lean 形式开发中包含的定理陈述：它将函数输入和前置条件放在水平线上方，后置条件放在下方，并使用完全限定名称以及指向 Rust 和 Lean 定义的链接。

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

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

这使形式验证从一个一次性的研究工件转变为工程工作流的一部分。

代理式证明

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

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

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

这尤其强大，因为 Rust 代码和 Lean 证明是分离的。代理不需要注释