[Pl-seminar] 10/4 Seminar: Ralf Jung: "Understanding and evolving the Rust programming language"

[Nathaniel Yazdani]

NUPRL Seminar Presents

Ralf Jung
MPI-SWS

11:00AM to 12:15PM
Friday, October 4th, 2019
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html <http://www.ccs.neu.edu/home/wand/directions.html>)

Understanding and evolving the Rust programming language

Abstract

Rust is a young and actively developed "systems programming language" that
promises to overcome the seemingly fundamental tradeoff between high-level
safety guarantees and low-level control over resource management.  This talk is
about my research on understanding and evolving this groundbreaking new
language.

The first part of the talk is about building formal foundations for the existing
Rust language.  Rust employs a strong, ownership-based type system to rule out
common systems programming anomalies, but then extends the expressive power of
this core type system through libraries that internally use unsafe features.
Unfortunately, this ``extensible'' aspect of the Rust language makes Rust's
safety claims rather non-obvious, and there is good reason to question whether
they actually hold.  To address this, we have developed RustBelt, the first
formal (and machine-checked) safety proof for a language representing a
realistic subset of Rust.  Our proof supports the extensible nature of Rust's
safety story 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 and compositional extension to the language.

The second part is about evolving the semantics of Rust to better support
compiler optimizations.  In particular, Rust's reference types provide strong
aliasing guarantees, which a clever optimizing compiler should be able to
exploit.  However, if no care is taken, unsafe code (which plays an essential
role in the Rust ecosystem, as mentioned above) can subvert these guarantees.
To address this, we have developed Stacked Borrows, a new operational semantics
for memory accesses in Rust.  On the one hand, Stacked Borrows defines an
aliasing discipline and declares programs violating it to have undefined
behavior, thus making it possible for us to formally verify the soundness of a
number of useful type-based intraprocedural optimizations.  On the other hand,
we have also implemented the Stacked Borrows semantics in Miri, an interpreter
for Rust, and run large parts of the Rust standard library test suite in Miri.
In so doing, we have validated that our semantics is sufficiently permissive to
account for real-world unsafe Rust code.

Bio

Ralf Jung is a PhD student at MPI-SWS in Saarbrücken, where he previously
completed his undergraduate degree with Saarland University. Ralf’s research
interests center around separation logic, operational semantics for low-level languages,
(semantic) type systems, and mechanized+modular proof for program verification. Ralf
also loves to learn about anything people do with Rust and the ways in which formal
methods could help.
-------------- next part --------------
HTML attachment scrubbed and removed