使用 Aeneas、Rust 和 Lean 扩展密码学软件的验证规模

中文摘要 AI 辅助

我们开发了一种验证密码学软件的新方法。我们针对用 Rust 编写的生产代码，以性能和系统集成为目标，而非验证的便利性。Rust 的所有权纪律使 Aeneas 能够在 Lean 中提取该代码的纯模型，从而免除了我们对指针活性和别名进行底层推理的需要。Lean 的可扩展性使我们能够开发策略和库，极大地简化对提取的 Rust 代码的推理。我们设计并调整了我们的工具链，以促进 AI 的使用。智能体自主编写形式化证明，这些证明由 Lean 内核独立验证。智能体还协助密码学标准和平台特定内建函数的正式化，这仍然需要专家设计和审查。我们将我们的方法应用于微软的密码学提供程序 SymCrypt。我们验证了其对 SHA-3 和 ML-KEM 等算法的实现，这些算法已从 C 移植到 Rust。我们还用实验性优化以及 FrodoKEM、ML-DSA 和 HPKE 等算法的实现扩展了 SymCrypt，以探索编写、调整和验证密码学代码的可扩展性。我们 237 KLOC 的 Lean 开发确立了 16.7 KLOC 的 Rust 代码的安全、无恐慌和功能正确性，这些代码支持 x86-64 和 ARM 平台的后量子密码套件。我们的评估表明，经过验证的 Rust 可以满足 SymCrypt 的性能、可移植性、部署和可维护性要求。

英文摘要

We develop a new methodology for verifying cryptographic software. We target production code written in Rust for performance and system integration, rather than verification convenience. Rust's ownership discipline enables Aeneas to extract a pure model of this code in Lean, relieving us from low-level reasoning about pointer liveness and aliasing. Lean's extensibility lets us develop tactics and libraries that greatly simplify reasoning about extracted Rust code. We design and tune our toolchain to facilitate the use of AI. Agents autonomously write formal proofs, which are independently verified by the Lean kernel. Agents also assist in the formalization of cryptographic standards and platform-specific intrinsics, which still requires expert design and review. We apply our methodology to SymCrypt, Microsoft's cryptographic provider. We verify its implementations of algorithms such as SHA-3 and ML-KEM, which were ported from C to Rust. We also extend SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code. Our 237~KLOC Lean development establishes safety, panic-freedom, and functional correctness of 16.7~KLOC of Rust code supporting post-quantum cipher suites for x86-64 and ARM platforms. Our evaluation shows that verified Rust can meet SymCrypt's performance, portability, deployment, and maintainability requirements.

发表机构

• Microsoft（微软）
• Google（谷歌）
• CMU（卡内基梅隆大学）
• Inria（法国国家信息与自动化研究所）
• ENS Paris-Saclay（巴黎萨克雷高等师范学院）

机构由 AI 辅助整理，请以论文原文为准。