Seminar: Modern Verification for a Rust-Centric World
Microsoft Research
Add to Calendar
2024-05-17 11:00:00
2024-05-17 12:00:00
America/New_York
Seminar: Modern Verification for a Rust-Centric World
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.