RustBelt: Securing the foundations of the Rust programming language Jung et al., POPL, 2018

Yesterday we saw the value of meta-engineering development processes in order to produce better (more secure) outcomes. Included in Bernstein’s recommendations was careful selection of programming language. Rust is a language in that spirit.

It has long been a “holy grail” of programming languages research to overcome this seemingly fundamental tradeoff and design a language that offers programmers both high-level safety and low-level control. Rust, developed at Mozilla Research, comes closer to achieving this holy grail than any other industrially supported programming language to date.

We’ve seen some advocates stating the case for Rust as the systems programming language of the future in previous editions of The Morning Paper. There’s something important lurking beneath Rust’s safety claims though:

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 type system through libraries that internally use unsafe features.

We’d really like to know whether those claims hold or not, and if so under what conditions, and that’s what today’s paper choice is all about. The authors give a formal and machine checked safety proof for a meaningful subset of Rust. If a library uses unsafe features, this gives a framework to say what verification condition it must satisfy for it to be considered a safe extension to the language. Many of the standard Rust libraries have been verified in this way, including Arc, Rc, Cell, RefCell, Mutex, RwLock, mem::swap, thread::spawn, rayon::join, and take_mut.

Now be warned, this is not an easy paper (it’s POPL, we should expect nothing less – I like to imagine the PC have an ‘intellectual intimidation’ criteria in the review process, and no paper falling below a certain threshold can be accepted!). And even though it runs to 34 pages, you’d really need to consult the even longer technical report to fully understand everything. Fortunately for most of us it suffices to know that the work exists, the results it demonstrates, and the implications for Rust. So those are the aspects I’ll focus on today.

Rust, the ‘unsafe’ safe language

At the heart of the Rust type system is an idea that has emerged in recent years as a unifying concept connecting both academic and mainstream language design: ownership. In its simplest form, the idea of ownership is that, although multiple aliases to a resource may exist simultaneously, performing certain actions on the resource (such as reading and writing a memory location) should require a “right” or “capability” that is uniquely “owned” by one alias at any point during the execution of the program. Although the right is uniquely owned, it can be “transferred” from one alias to another… In more complex variations, ownership can be shared between aliases, but only in a controlled manner.

Ownership can be captured in the type system. In Rust, if ownership of an object is shared between multiple aliases, then none of them can be used to directly mutate it. This can be enforced automatically and eliminates a range of common low-level programming errors such as “use after free” data races. But many low-level data structures and synchronization mechanisms depend on the ability to mutate aliased state.

Consequently, to overcome this restriction, the implementations of Rust’s standard libraries make widespread use of unsafe operations, such as “raw pointer” manipulations for which aliasing is not tracked. The developers of these libraries claim that their uses of unsafe code have been properly “encapsulated”, meaning that if programmers make use of the APIs exported by these libraries but otherwise avoid the use of unsafe operations themselves, then their programs should never exhibit any unsafe/undefined behaviors.

Rust programmers typically strive to avoid the use of unsafe in their own code, but nevertheless, unsafe elements are brought in via library usage.

The most basic form of ownership in Rust is exclusive ownership, in which at most one thread is allowed to mutate a given location. Ownership can be transferred between threads, which may happen for example when invoking a function. Once ownership has moved, the original owner can no longer access the variable (an attempt to do so results in a compile-time error).

In addition to permanent ownership transfer, ownership can be borrowed, granting access for the duration of a function call (mutable references). Once the function returns, the original owner can continue to access the variable.

… the exclusive nature of this access guarantees that no other party will access the vector in any way during the function call.

Mutable references are exclusive, there are also shared references which can be duplicated, permitting aliasing. Shared references are read-only.

Every reference has a lifetime, which determines for example how long a loan lasts when borrowing.

Using unsafe, mutation is permitted through a shared reference (this is known as “interior mutability”). Interior mutability is outside of the type system, and implemented in the standard library using unsafe code (for example, the Cell and Mutex types).

How do you approach proving safety? Introducing RustBelt

The first challenge is to find a suitable logic language for modelling Rust itself. For this the authors selected Iris, a higher-order concurrent separation logic with support in Coq. Separation logic enables independent (modular) reasoning over parts of the state with something called the frame rule that tells you how subsequent composition behaves.

…Iris comes with built-in support for reasoning modularly about ownership. Moreover, the main selling point of Iris is its support for deriving custom program logics for different domains… In the case of RustBelt, we used Iris to derive a novel lifetime logic, whose primary feature is a notion of the borrow propositions that mirrors the “borrowing mechanism” for tracking aliasing in Rust.

is the formal version of Rust developed by the authors (see §3), at a level very close to Rust’s Mid-level Intermediate Representation (MIR). Programs are represented in a continuation passing style and the memory model supports pointer arithmetic. The operational semantics of are then given by translation into a core lambda calculus equipped with primitive values, pointer arithmetic, and concurrency.

To detect [such] data races, every location is equipped with some additional state (resembling a reader-writer lock), which is checked dynamically to see if a particular memory access is permitted. We have shown in Coq that if a program has a data race, then it has an execution where these checks fail. As a consequence if we can prove that a program cannot get stuck (which implies that the checks always succeed, in all executions), then the program is data-race free.

RustBelt is a semantic model of types in Iris (see §4). A new Iris library is developed to model lifetime logic, which enables modelling the temporary and potentially shared ownership of Iris resources (§5)

Modelling types with interior mutability (§6) requires picking semantic interpretations for the abstract types exported by the library (e.g., Cell), and proving that each publicly exported function satisfies the semantic interpretation of the type.

With all this work in hand, it then becomes possible to define semantic interpretations of the judgments from the type system.

Key results

The authors are able to show (‘fundamental theorem of logical relations’) that for any inference rule of the type system, the resulting Iris theorem holds. Using this theorem, it becomes possible to glue together safe and unsafe code:

Given a program that is syntactically well-typed except for certain components that are only semantically (but not syntactically) well-typed, the fundamental theorem tells us that the entire program is semantically well-typed.

In addition, the adequacy theorem guarantees that a semantically well-typed program is memory and thread safe: it will never perform any invalid memory access and will not have data races.

Put together, these theorems establish that, if the only code in a program that is not syntactically well-typed appears in semantically well-typed libraries, then the program is safe to execute.

Caveats and future work

“We had to make some concessions in our modelling: we do not model…”

• more relaxed forms of atomic accesses, which Rust uses for efficiency in libraries like Arc
• Rust’s trait objects, which can pose safety issues due to their interactions with lifetimes
• stack unwinding when a panic occurs, which can cause similar issues to exception safety in C++
• automatic destruction, “which has already caused problems for which the Rust community still does not have a modular solution.”
• a few details unrelated to ownership, such as type-polymorphic functions and “unsized” types.

Despite these limitations, we believe we have captured the essence of Rust’s ownership discipline… In fact, our verification work resulted in uncovering and fixing a bug in Rust’s standard library, demonstrating that our model of Rust is realistic enough to be useful.

The future work plan is to fill some of the above mentioned gaps and bring closer to MIR, the most important intermediate language in the Rust compiler. The type system is also being used to shed light on features currently being sketched for Rust itself, such as non-lexical lifetimes.