Derek Dreyer: Proving the Safety of Rust with RustBelt and Iris

For several years at the Max Planck Institute for Software Systems, we have been working on RustBelt. The exciting part is applying logical foundations—type systems, theories and proofs developed over many years—to Rust, a real programming language that is actively being developed.

I will explain what makes Rust interesting, the problem of establishing its safety guarantees, and the technology we have built to address it. The larger question is whether we can have both high-level safety and the low-level control needed for systems programming.

High-level languages provide useful abstractions and automatic memory management; systems applications often need finer control of resources and traditionally use languages such as C or C++. Rust aims to bridge that divide: low-level control, strong type and memory safety, and freedom from data races, backed by industrial development.

A central source of trouble in low-level code is unrestricted mutation combined with aliasing. Multiple references can point to an object while one changes, deallocates or reallocates it, producing dangling pointers, use-after-free errors, data races and invalidated iterators.

Rust uses an ownership type system to constrain that combination. In the simplified core story, an object can be mutable or have multiple active aliases, but not both at once. Owning a value gives control of its resources; with no other active access, the owner can mutate or deallocate it.

Ownership alone would be too restrictive, so Rust also permits borrowing. A shared reference can be copied and aliased, but does not allow ordinary mutation through it. A unique mutable borrow permits mutation while ensuring it is the only active alias for that access.

For a simple demonstration, create a vector, push 42 and then iterate over the elements. That works. Move the push into the loop, however, and an analogous C++ program risks invalidating the iterator: growing the vector may reallocate its storage, leaving an iterator pointing to freed memory.

Rust rejects the modified program. Iterating creates an immutable shared borrow; calling push needs a mutable borrow. The compiler reports the conflict because the iterator still holds the shared access while push would change the vector.

Move push to after the loop and the shared borrow has ended. Mutable access is available again, so the program compiles. The example illustrates a static analysis that prevents a real class of errors, not just a restriction on syntax.

That standard explanation is useful, but it is also incomplete. Sometimes an implementation really does need mutation and aliasing together: doubly linked lists, locks, channels and reference counting all involve changing state shared by multiple parties.

Rust supports such behavior behind APIs. A Mutex gives synchronized access to an object through a lock. An Arc, or atomic reference-counted pointer, allows that mutex to be shared safely across threads, using a reference count to manage its lifetime.

In a small example, we spawn ten threads and explicitly clone an Arc for each one. Ownership of each clone moves into its thread; the thread acquires the mutex and gets mutable access to the underlying object. The threads race to acquire the lock, but the client is ordinary safe Rust.

These libraries expand what a safe client can express. Their internals cannot all be written under the core safe discipline: they use unsafe code, including operations such as dereferencing raw pointers whose aliases the type system does not track.

The promise is that these unsafe details are encapsulated by safe interfaces. A client written in the safe fragment should not observe undefined behavior through those APIs. This is a strong and valuable claim, but it also creates opportunities for subtle bugs.

Around 2015, Aaron Turon described fearless concurrency and highlighted a scoped-threads API that let spawned threads borrow from the parent’s stack frame. The API used unsafe code internally. A bug was discovered around the time of the post, roughly two weeks before Rust 1.0.

The issue involved an interaction with Rc, a reference-counting API: the combination could lead to use-after-free even though each API seemed safe on its own. The scoped-threads API was deprecated and other approaches were developed. How can we gain confidence that such soundness bugs do not occur?

RustBelt aims to build logical foundations for a core Rust language, verify its type system and important libraries, and give developers a way to evaluate future APIs. Its purpose is to let the language grow while preserving confidence in its safety.

What does a safety proof mean? The traditional syntactic approach, often called progress and preservation, lifts well-typedness from a program to machine states and shows that execution preserves it. When the program fits a fixed set of typing rules, this can yield a simple proof of well-defined behavior.

That approach is not enough for Rust as described here: a library implementation may deliberately contain code outside the safe typing rules. RustBelt instead uses semantic safety. Informally, a library is safe if no well-typed client can use it to produce undefined behavior.

What counts as undefined behavior is itself an active research question. For this work, the model includes conditions such as not accessing unallocated memory and avoiding data races under an operational definition. The precise guarantee is relative to the formal semantics used in the proof.

The team defines a core calculus called LambdaRust, modeled after Rust’s mid-level intermediate representation. Its operational semantics can get stuck in a bad state. The safety theorem shows that appropriately well-typed programs in this model do not reach such a state.

An audience member asks whether one could add verified primitives to a syntactic proof. The difficulty is finding a scalable approach in which new APIs can be added without revising all existing proofs. Semantic safety lets us prove a new API against a shared model independently.

The semantic model maps a type or API interface to a safety contract: a verification condition that its implementation must satisfy. We define this interpretation once for the type system. It tells us what must be established before an implementation can be linked safely with other code.

We prove a general theorem that an implementation entirely in the safe fragment satisfies its corresponding contract by construction. An implementation using unsafe features has an additional manual proof burden: show that it meets that contract. The proof may be difficult, but the obligation is explicit.

Our work focuses on the framework, a meaningful subset of Rust and a number of widely used APIs, rather than full automation. Future verification tools might make the proofs more systematic. During this work we did find a few bugs, including one in Mutex and another in Arc involving relaxed memory.

A shared semantic model allows library proofs to be independent. For the earlier Rc and scoped-threads interaction, one implementation would fail its verification against the chosen model. We accounted for Rc and verified it; the problematic scoped-threads API would not pass that proof.

The result is always relative to the memory model we define. Our initial model is relatively simple and not fully realistic. A faithful model must account both for what Rust developers intend and for safe compilation to LLVM; this remains an open problem.

We are also working on a richer model that admits more undefined behavior to support compiler optimizations, but at the time of this talk RustBelt has not yet been adapted to it. This distinction matters when interpreting the reach of a formal safety result.

There is flexibility in the semantic model. New, adventurous APIs may not be verifiable under its current interpretation, so the framework must evolve. The proofs are machine-checked in Coq: changing the model still requires work, but Coq identifies where existing proofs need revision.

The overall project has several adjustable parameters: the language and its semantics, the interpretation of types, the APIs verified and the memory model. Our paper used a core fragment of Rust with sequentially consistent concurrency; making each part more faithful is continuing work.

The next question is which logic should express these contracts. We use a descendant of separation logic. Hoare logic reasons about code through preconditions, postconditions and invariants; separation logic extends it to reason effectively about pointer-manipulating programs.

The fit with Rust is ownership. In separation logic, assertions describe ownership of resources, echoing the ownership central to Rust’s type system. For a concurrent language, however, we need a concurrent extension of the logic, and there are many different ones.

A 2010 paper observed a disturbing trend: each new library or concurrency primitive seemed to require a new separation logic. A supposedly general semantic model cannot scale if every new API requires replacing its underlying logic. We want a framework from which stronger reasoning principles can be derived.

A second challenge is the memory model. Much early concurrent separation logic assumed sequential consistency, as if threads took turns changing global state and each mutation became immediately visible. Actual concurrency and C++-style atomics permit more complex relaxed-memory behavior.

Our work follows two lines: Iris, a unifying framework for concurrent separation logic, and logics that account for relaxed memory. Later work encoded a line of relaxed-memory logics in Iris as well. The framework is mechanized in Coq and can accommodate more than one language or memory model.

A quick introduction to Hoare logic: a triple has a command C, a precondition P and a postcondition Q. If P holds initially, C executes safely; if it terminates with a value, Q holds of the result. This is a partial-correctness statement, not a promise that every command terminates.

Separation logic changes what assertions describe. An assertion that x points to v says the current thread owns that location and it contains v. Ownership means the thread can reason about and mutate that location without interference from another linked thread.

The separating conjunction P * Q says both assertions hold over disjoint pieces of state. For physical memory, x points to v * y points to w therefore describes different locations: x and y do not alias. This makes the boundary between two threads’ resources explicit.

The disjoint concurrency rule says we may verify two parallel commands independently if each operates on its own resources. We combine their preconditions and postconditions using separating conjunction. One thread changing x and another changing y cannot overwrite each other when the initial assertion establishes separate ownership.

Shared state needs another rule: an invariant. We establish a property R over shared state and allow an atomic command to access that state temporarily, provided it restores R afterwards. The invariant acts as an assumption at the start of the operation and a guarantee at its end.

Atomicity matters because another thread must not observe the invariant while it is temporarily broken. If a multi-step operation changed an even number to odd and then back again, another thread could intervene in the middle and find its assumed property false.

For a simplified mutex, represent the lock by a location containing zero when unlocked and one when locked. The lock method loops around an atomic compare-and-swap until it changes zero to one; unlock sets the location back to zero.

Let P describe the resource the mutex protects. Anyone can call lock under a trivial precondition; once lock terminates, the caller gains P. To unlock, the caller must return P, and afterward no longer owns it. The specification is independent of the particular resource represented by P.

Two threads can each acquire the lock, use P in a critical section, restore it and unlock. Each thread’s proof can be done independently. The mutex’s shared invariant connects the physical lock state to the ownership of the protected resource.

The invariant has two cases. When x points to zero, the lock is free and the invariant holds P. When x points to one, the lock is held and P has been transferred out to a thread; that thread can temporarily alter the protected state while it holds the lock.

To prove successful lock acquisition, open the invariant in the unlocked case and temporarily obtain x pointing to zero together with P. The atomic compare-and-swap changes zero to one. Restore the invariant with x pointing to one and keep P as the postcondition.

This is a simplified presentation that omits important details, but it shows the proof pattern. In Coq, the proof is interactive: combine a rule for independent resources with a rule for accessing and restoring shared invariants.

Basic concurrent separation logic is powerful but cannot conveniently express every property we need. A shared counter that only increases is a statement about how state evolves, not just a property of a single state. Protocols may also require saying which thread can change something at a particular time.

Advanced logics use permissions, tokens or capabilities—logical state that describes the roles participants can take. Many such extensions appeared, with increasingly complicated primitive rules. Each often came with a separate soundness model, making it hard to compose results proved in different logics.

Iris seeks a more fundamental basis. Its central ingredients are invariants and user-defined logical, or ghost, state. From these, we can derive rules of sophisticated concurrent logics and develop new reasoning principles suited to a particular application.

For RustBelt, we needed a borrow proposition expressing temporary ownership of a resource for a lifetime, followed by the original owner regaining control. Instead of inventing a separate logic, we encoded this as a logical API in Iris, proved it sound there and used it to build the Rust semantic model.

Return to Arc, with a simplified object containing data and a reference count. Clone atomically increments the count and returns an alias. Print accesses the data; drop decrements the count and frees the object if it was the final reference. This is illustrative rather than an exact implementation of Rust’s Arc.

RustBelt associates each type with a predicate describing ownership of a value. Here Arc(x) means permission to access shared data through handle x. Each method starts with that permission: clone returns Arc(x) * Arc(y), print retains Arc(x), and drop consumes it.

The clone specification seems puzzling. The returned y is an alias of x, so both predicates concern the same physical object. How can separating conjunction apply? The answer is that these predicates describe logically separate permissions, not exclusive ownership of separate physical memory.

Each Arc permission is a countable privilege that can be passed to a thread without trampling another privilege. The number of such privileges must correspond to the object’s reference count. A second logical predicate, Count(x, n), records how many Arc permissions exist.

If Count(x, n) and a separate Arc(x) both hold, n must be positive: the latter is evidence of at least one permission. A logical update can raise the count from n to n + 1 while creating a permission, or consume a permission while lowering the count.

An invariant ties that logical state to physical state. For some n, the logical count is n; either n is zero or the object is allocated with physical count n. When n is zero, the object has been deallocated. The invariant keeps the two descriptions in step.

Each method begins with Arc(x). Combined with Count(x, n) in the invariant, that implies n is at least one, so the object is allocated. The methods can therefore access x. Consider clone: it performs an atomic fetch-and-increment.

Open the invariant for the atomic operation. In a concrete illustration, suppose the current count is two. The proof obtains temporary ownership of the physical state and changes the count to three. It then has to restore the invariant, but the logical count is still two.

Use the logical update to bring that count to three and spawn another Arc permission. Physical and logical state now agree, so the invariant can be restored. The new permission remains in the postcondition, exactly as the clone specification requires.

This follows the familiar concurrent-separation-logic pattern: open an invariant, manipulate state and restore it. The addition is simultaneous manipulation of logical state. The proof relies on rules about that state, so those rules themselves need justification.

Iris provides a framework for justifying application-specific logical-state rules. A generic algebraic structure called a partial commutative monoid can represent the chosen logical state. From a small number of primitive proof rules, one can derive the soundness of the higher-level axioms used in the example.

RustBelt uses these ideas to model Rust types and verify safe abstractions built from unsafe internals. Iris supplies a flexible modern separation logic for expressing the semantic model and scaling the reasoning to realistic Rust code, within the limits of the formal model.