RustBelt: Securing the foundations of the Rust programming language

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 10 January 2020

Proc. ACM Program. Lang. 2(POPL)
Association for Computing Machinery
New York, NY, USA
December 2017
Topic(s): types verification
Note(s): permission logic, Rust language, undefined behaviour, mir, Rust unsafe code, RustBelt verifier, Coq theorem prover

Rust aims to archive the holy grail of a language that gives low-control over resource management and safe high-level abstractions. It does this using a type system that restricts programs to eliminate unsafe programming practices coupled with a practice of extending that type system with libraries that are observably safe but that internally use “unsafe” operations. This paper provides a framework for proving that these libraries do not break the safety guarantees of the standard type system. Along the way, the paper gives a nice insight into the way that the community as a whole has been developing.

This paper departs from standard practice over the last 20 or so years of using syntactic techniques to prove results about the type system. They argue that these syntactic techniques are closed-world methods but Rust’s extensible type system requires an open-world approach. So they revert to the older practice of proving type soundness semantically. This is done in the Iris framework building on “step-indexed” logical relations for scalability.

After a tour of the key concepts in Rust’s ownership type system, they present lambda-rust which is at a level simile are to Rust’s Mid-level Intermediate Representations (MIR) and is (roughly) a continuation passing lambda calculus extended with lifetimes.

For a more detailed summary, I recommend the morning paper.

Rust language, RustBelt verifier