Microsoft 使用 Lean 和 Aeneas 在 SymCrypt 中发布经过验证的 ML-KEM 和 SHA-3 代码

Microsoft 已开源其 SymCrypt 密码库的一个分支，其中包含 ML-KEM 和 SHA-3 的 Rust 实现的正式规范和证明。此次发布展示了一种方法论，即生产级算法使用安全的 Rust 编写，并使用 Aeneas 工具链针对源自标准的 Lean 模型进行验证。

• 该方法利用 Aeneas 将 Rust 的中层表示转换为纯 Lean 模型，利用 Rust 的所有权规则简化对内存安全的推理。
• 正式规范的设计旨在紧密反映 NIST 或 IETF RFC 等公共标准，允许针对官方向量进行可执行测试以及逐行的人工审查。
• 开源分支包含当前用于 Windows insider 构建的 ML-KEM 和 SHA-3 代码的完整证明，并计划将此工作流程扩展到 AES-GCM、FrodoKEM 和 ML-DSA。

该方法论通过结合 Rust 的内存安全保证与 Lean 的功能正确性证明，提供两层保障，旨在为生产级密码算法扩展形式化验证。