Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminars LFCS seminar: Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming

LFCS seminar: Derek Dreyer: RustBelt: Logical Foundations for the Future of Safe Systems Programming

— filed under: ,

What
  • LFCS Seminar
  • Upcoming events
When Aug 16, 2018
from 03:00 PM to 04:00 PM
Where IF 4.31/4.33
Add event to calendar vCal
iCal

Abstract:

Rust is a new systems programming language, sponsored by Mozilla, that
promises to overcome the seemingly fundamental tradeoff in language
design between high-level safety guarantees and low-level control over
resource management.  Unfortunately, none of Rust's safety claims have
been formally proven, and there is good reason to question whether
they actually hold.  Specifically, Rust employs a strong,
ownership-based type system, but then extends the expressive power of
this core type system through libraries that internally use unsafe
features.

In this talk, I will present RustBelt
(http://plv.mpi-sws.org/rustbelt), the first formal (and
machine-checked) safety proof for a language representing a realistic
subset of Rust.  Our proof is extensible in the sense that, for each
new Rust library that uses unsafe features, we can say what
verification condition it must satisfy in order for it to be deemed a
safe extension to the language.  We have carried out this verification
for some of the most important libraries that are used throughout the
Rust ecosystem.

After reviewing some essential features of the Rust language, I will
describe the high-level structure of the RustBelt verification and
then delve into detail about the secret weapon that makes RustBelt
possible: the Iris framework for higher-order concurrent separation
logic in Coq (http://iris-project.org).  I will explain by example how
Iris generalizes the expressive power of O'Hearn's original concurrent
separation logic in ways that are essential for verifying the safety
of Rust libraries.  I will not assume any prior familiarity with
concurrent separation logic or Rust.

This is joint work with Ralf Jung, Jacques-Henri Jourdan, Robbert
Krebbers, Hoang-Hai Dang, Jan-Oliver Kaiser, and the rest of the Iris team.

Short Bio:

Derek Dreyer is a professor of computer science at the Max Planck
Institute for Software Systems (MPI-SWS) in Saarbruecken, Germany, and
recipient of the 2017 ACM SIGPLAN Robin Milner Young Researcher Award.
His research runs the gamut from the type theory of high-level
functional languages, down to the verification of compilers and
low-level concurrent programs under relaxed memory models. He is
currently leading the RustBelt project, which focuses on building the
first formal foundations for the Rust programming language.

Document Actions