Abstract:
We present Aeneas, a new verification toolchain for Rust programs based on a lightweight functional translation. We leverage Rust’s rich region-based type system to eliminate memory reasoning for a large class of Rust programs by translating them to a pure lambda-calculus, as long as they do not rely on interior mutability or unsafe code. Doing so, we relieve the proof engineer of the burden of memory-based reasoning, allowing them to instead focus on *functional* properties of their code.
Bio:
Son Ho is a PhD applicant working on program verification in the Prosecco team at Inria, under the supervision of Karthikeyan Bhargavan and Jonathan Protzenko. His research aims at making formal verification more practical and scalable to contribute to a wider adoption in the industry. He started my research journey by working at Prove&Run, a company which develops verified micro-kernels, then joined the Everest project, whose goal is to develop a verified, secure communications stack with a strong focus on HTTPS, by joining the Prosecco team to start a PhD. By confronting himself with the current limitations of their verification tools, he finally decided to work on his current project, Aeneas, which is a new toolchain aimed at verifying safe Rust programs. With this new toolchain, they hope to overcome some of the limitations they identified in order to drastically expand the class of programs they can currently verify at Prosecco.