Formalization of a Rust Verifier
Rust is a recent entry in the field of systems programming languages which uses its type system to provide strong safety guarantees to programs.
In the safe fragment of Rust, the language statically checks the absence of memory unsafety, dataraces and more generally undefined behavior.
The strength of this type system has been leveraged by formal verification tools for Rust in tools like Prusti, Verus, Creusot or Aeneas.
These tools leverage the *explicit* guarantees or *capabilities* provided by the Rust type system to simplify reasoning about imperative, concurrent programs.
However, the type system of Rust is too restrictive to implement certain kinds of programs: cyclic data structures like doubly linked lists, concurrency or shared mutable state.
In these circumstances, Rust provides an opt-out through *interior mutability*.
When programs use interior mutability static guarantees are lost; the type system no longer describes where mutations can occur in a program.
Existing verifiers must thus reason conservatively about interior mutability, assuming values could change arbitrarily at any point.
Mendel is a new Rust verifier based on a notion of *implicit capabilities* which addresses this limitation of other verification tools.
With Mendel, it becomes possible to precisely and automatically reason about interior mutability, opening the door to low-effort verification of complex, concurrent software.
Unfortunately, though the implicit capabilities are intuitively justified, they do not have an accompanying formal proof of soundness.
This gap leaves doubts in the safety of software verified with Mendel.
Project
In this project, we want to formalize and mechanize a proof of soundness for a model of Mendel's implicit capability reasoning.
In particular, we want to build an extension to RustBelt, an existing formalization of the Rust type system, proving that the capability annotations of Mendel are justified for core Rust types, and that the framing rules enabled by these capabilities are justified.
Objectives
- Define the interpretations of all Mendel's capabilities in Iris.
- Prove the soundness of capability annotations for core types like Cell, Mutex and Arc in RustBelt.
- Formalize the framing rules of Mendel as RustBelt typing lemmas
- Verify the soundness of all Mendel's framing rules.
Prerequisites
The project will involve working with the Iris separation logic embedded in Coq, interest in formal methods and logic are recommended. Experience with a proof assistant such as Coq or Lean is required, but experience with separation logic is not.