Campus Event Calendar
Event Entry
What and Who
Understanding and Evolving the Rust Programming Language
Ralf Jung
MMCI
SWS Student Defense Talks - Thesis Proposal
AG 3, SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Tuesday, 10 December 2019
10:00
120 Minutes
E1 5
029
Saarbrücken
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. In this talk I will present my thesis work 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.
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.
Contact
Claudia Richter
9303 9103
--email hidden
Video Broadcast
Yes
Kaiserslautern
G26
111
FP Space 2 (8796)
passcode not visible
logged in users only
Claudia Richter, 12/09/2019 16:30 -- Created document.