Rust software for cryptography verified using AI and Lean tactics
Scaling Verification of Cryptographic Software with Aeneas, Rust, and Lean
Cryptography and Security
Summary
Cryptographic software needs to be both secure and efficient, but verifying it can be very complex. The authors developed a new way to check the correctness of real-world cryptographic code written in Rust, using mathematical tools and AI helpers. Their method turns Rust code into simpler models and builds proofs that ensure the software works safely and correctly. They tested their approach on Microsoft’s cryptography library, showing it meets performance and safety needs while being easier to verify. This helps build more trustworthy cryptographic software that runs efficiently on modern computers.
What this means in practice
- •For software security engineers: Build and verify cryptographic software in Rust that is both safe from bugs and performant across platforms like x86-64 and ARM.
- •For embedded system developers: Integrate formally verified cryptographic routines into embedded devices, ensuring panic-free operation and correctness without sacrificing speed.
Authors
Son Ho, Cédric Fournet, Jonathan Protzenko, Michael Naehrig, Joshua Clune, Patrick Longa, Guillaume Boisseau, Fernando Leal Sánchez, Aymeric Fromherz, Antoine Delignat-Lavaud
Abstract
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.