Aeneas

Context

One of the main challenges of program verification today consists in finding a way of efficiently reasoning about low-level, effectful programs. This problem has led to the development of a large collection of frameworks and logics ^1234567 which make various compromises between ease of verification and expressiveness. Despite the intense research effort in this area, verifying such programs still represents a daunting task ⁸⁹¹⁰¹¹.

Following the development of the Rust programming language¹², the recent years have seen the emergence of a new line of research ^131415161718 which attempts to leverage the Rust type system to improve scalability when reasoning about low-level programs. Rust is indeed a perfect target for program verification, as its static ownership discipline strikes a good balance between a fine-grained, expressive control of memory, making it a language of choice for system programming, and strong memory guarantees, which can be leveraged to ease program verification.

A key insight which drove the design of several frameworks¹⁴¹⁵¹⁷ is that a large subset of Rust doesn’t require to explicitly reason about memory, which typically involves tedious, low-level proofs. Instead, proof engineers can focus on the functional behavior of their programs. This is what led to the development of the Aeneas¹⁸ toolchain, which works essentially as a compiler: given a Rust program, Aeneas compiles it to a pure, functional model that gets extracted to an interactive theorem prover. By stating and proving theorems about this model, proof engineers can then prove functional correctness properties about the original code. Aeneas currently has backends for F*, Coq and Lean, the latter being our main backend today.

Research Topics

Use Cases

We are interested in using Aeneas to specify and verify various large use cases, which include but are not limited to cryptographic applications ⁸⁹ or storage systems¹⁰. Making this verification amenable would imply extending the subset supported by Aeneas as well as improving its automation.

Extending the Translation

The translation is a work in progress: we currently support a quite large subset of Rust, but of course not the whole of Rust. A fundamental limitation is that the pure translation can only handle a subset of safe Rust: it can’t be applied to unsafe code, as for instance manipulating raw pointers requires modeling memory, and it can also not support (safe) concurrent code, interior mutability or I/O. We are currently working on connecting Aeneas to a separation logic framework, so that we can benefit from the pure translation wherever possible, but can also resort to stateful reasoning wherever necessary. As a simple example, think about a Mutex: both the lock and unlock functions are stateful¹⁹, and it is possible to use separation logic about them. However, what happens between lock and unlock likely fits within the subset supported by Aeneas’ pure translation. This means that one would only have to pay the price of using separation logic at a limited number of places, and would benefit from Aeneas’ pure translation speedup elsewhere.

There is still a lot of remaining work to do on this topic:

• connecting the pure translation with a separation logic framework is hard: it both requires a bit of thinking to make it work in theory, and a fair amount of engineering to make the framework usable in practice.
• a key challenge is to allow having local reasoning by means of separation logic, so the use of separation logic is not contaminating. For instance, one might want to formally verify a low-level implementation of Vec by means of separation logic, but use a high-level, pure view of vectors elsewhere (for instance, use lists in the translation).
• proving the soundness of the connection is also an open research problem
• we might want to have a hierarchy of effects, to reason about functions which do not modify the state, are total, partial, etc. It is unclear how to make the framework usable in that context: we would need a way of automatically lifting theorems from one effect to the other, for instance.
• of course, we need to apply this framework to use cases to see whether it really works!

Soundness

The translation works by doing some sort of a symbolic execution of the Rust programs, and this symbolic execution actually borrow-checks the program at the same time, which means we do not need to trust the Rust borrow-checker. In some situations, we can even borrow-check programs that are rejected by the current Rust borrow-checker, because it is not precise enough. We have a pen and paper proof that (a subset of) the symbolic execution acts as a borrow-checker - essentially, if one successfully symbolic evaluates a Rust program, then this program is memory safe. We are currently working on mechanizing this pen and paper proof. Some future work includes extending this proof (the pen and paper proof as a first step, then the mechanized proof) to prove that the translation itself is correct. Finally, on the longer term, we would be interested in having a proof generation mechanism: Aeneas would generate a deep-embedding of a program, its functional translation, together with a proof that the deep-embedding refines the functional translation.

Lean Backend: Proof Experience and Automation

A lot of work is going into the Lean backend to make the proof experience pleasant and scalable. We are always interested in making the backend more user-friendly and more automated.

Notes & References