RustBelt: Logical Foundations for the Future of Safe Systems Programming

together the low-level flexibility of modern C++ with a strong
"ownership-based" type system guaranteeing type safety, memory safety,
and data race freedom. As such, Rust has the potential to
revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having to give
up low-level control over performance.

Unfortunately, none of Rust's safety claims have been formally
investigated, and it is not at all clear that they hold. To rule out
data races and other common programming errors, Rust's core type
system prohibits the aliasing of mutable state.  This is too
restrictive, however, for a number of essential data structures, and
thus Rust's standard libraries make widespread internal use of
"unsafe" features of the language.  The Rust developers claim that
such "unsafe" code has been properly encapsulated, so that Rust's
language-level safety guarantees are preserved, but this claim is
called into question by various safety bugs uncovered in Rust in the
past year.

In the RustBelt project, funded by an ERC Consolidator Grant, we aim
to develop the first formal tools for verifying the safety of Rust.
To tackle this challenge, we will build on recent breakthrough
developments in the area of Concurrent Separation Logic, in particular
our work on the Iris and GPS program logics.  In the talk, I will
explain what Concurrent Separation Logic is, why it is relevant to the
Rust verification effort, what problems remain in developing a program
logic suitable for Rust, and how Iris and GPS make progress toward
that goal.