Seminar: Modern Verification for a Rust-Centric World
Host
Anish Athalye
MIT
Abstract: Over the past several years, we have authored and verified large amounts of systems code through the Low* toolchain, which compiles a subset of F* to C. HACL*, a verified cryptographic library, is our flagship project, and compiles 100,000 lines of Low* to 80,000 lines of fast, verified C code. Parts of HACL* have made it into Python, Firefox or the Linux kernel.
However, C is no longer the target of choice. The White House, large companies (e.g. Microsoft) and the software community at large all have embraced Rust as a new, safe language that the whole community should transition to. In that new Rusty world, how does one modernize our verification tools to leverage this new ecosystem?
In this talk, I will describe three evolutions of our toolchain that bring us into the new Rust-centric world.
• A new Low* -> Rust transition pipeline allows us to compile existing code, such as HACL*, directly to Rust. This allows us to avoid rewriting old code.
• A new verification toolchain, Aeneas, takes unsafe-free Rust programs and converts them to a pure equivalent, that can then be reasoned upon in various theorem provers, such as F*, Lean, or Coq. This is our new way of verifying Rust programs and allows us to author fresh code directly in Rust.
• A new compiler from Rust to C provides a backwards-compatibility story for the transition period where new verified software is authored in Rust directly, but engineering constraints preclude immediate adoption of the Rust toolchain.
However, C is no longer the target of choice. The White House, large companies (e.g. Microsoft) and the software community at large all have embraced Rust as a new, safe language that the whole community should transition to. In that new Rusty world, how does one modernize our verification tools to leverage this new ecosystem?
In this talk, I will describe three evolutions of our toolchain that bring us into the new Rust-centric world.
• A new Low* -> Rust transition pipeline allows us to compile existing code, such as HACL*, directly to Rust. This allows us to avoid rewriting old code.
• A new verification toolchain, Aeneas, takes unsafe-free Rust programs and converts them to a pure equivalent, that can then be reasoned upon in various theorem provers, such as F*, Lean, or Coq. This is our new way of verifying Rust programs and allows us to author fresh code directly in Rust.
• A new compiler from Rust to C provides a backwards-compatibility story for the transition period where new verified software is authored in Rust directly, but engineering constraints preclude immediate adoption of the Rust toolchain.