Safe Systems Programming in Rust:

The Promise and the Challenge

Ralf Jung Jacques-Henri Jourdan Robbert Krebbers Derek Dreyer

MPI-SWS, Université Paris-Saclay, CNRS, LRI, TU Delft, MPI-SWS,
Germany France The Netherlands Germany

this control comes at a steep cost. For example, Microsoft

Key Insights recently reported that 70% of the security vulnerabilities they
• Rust is the first industry-supported programming language fix are due to memory safety violations [33], precisely the
to overcome the longstanding tradeoff between the safety type of bugs that strong type systems were designed to rule
guarantees of higher-level languages (like Java) and the out. Likewise, Mozilla reports that the vast majority of critical
control over resource management provided by lower-level bugs they find in Firefox are memory-related [16]. If only
“systems programming” languages (like C and C++). there were a way to somehow get the best of both worlds: a
• It tackles this challenge using a strong type system based safe systems programming language. . .
on the ideas of ownership and borrowing, which statically Enter Rust. Sponsored by Mozilla and developed actively
prohibits the mutation of shared state. This approach en- over the past decade by a large and diverse community of
ables many common systems programming pitfalls to be contributors, Rust supports many common low-level program-
detected at compile time. ming idioms and APIs derived from modern C++. However,
• There are a number of data types whose implementations unlike C++, Rust enforces the safe usage of these APIs with
fundamentally depend on shared mutable state and thus a strong static type system.
cannot be typechecked according to Rust’s strict ownership In particular, like Java, Rust protects programmers from
discipline. To support such data types, Rust embraces the memory safety violations (e.g., “use-after-free” errors). But
judicious use of unsafe code encapsulated within safe APIs.
Rust goes further by defending programmers against other,
• The proof technique of semantic type soundness, together more insidious anomalies that no other mainstream language
with advances in separation logic, has enabled us to begin can prevent. For example, consider data races: unsynchro-
building rigorous foundations for Rust’s approach to safe nized accesses to shared memory (at least one of which is
systems programming as part of the RustBelt project.
a write). Even though data races effectively constitute unde-
fined (or weakly-defined) behavior for concurrent code, most
There is a longstanding tension in programming language “safe” languages (such as Java and Go) permit them, and they
design between two seemingly irreconcilable desiderata. are a reliable source of concurrency bugs [35]. In contrast,
Rust’s type system rules out data races at compile time.
• Safety. We want strong type systems that rule out large Rust has been steadily gaining in popularity, to the point
classes of bugs statically. We want automatic memory that it is now being used internally by many major indus-
management. We want data encapsulation, so that we can trial software vendors (such as Dropbox, Facebook, Ama-
enforce invariants on the private representations of objects zon, and Cloudflare) and has topped StackOverflow’s list
and be sure that they will not be broken by untrusted code. of “most loved” programming languages for the past four
• Control. At least for “systems programming” applications years. Microsoft’s Security Response Center Team recently
like web browsers, operating systems, or game engines, announced that it is actively exploring an investment in the
where performance or resource constraints are a primary use of Rust at Microsoft to stem the tide of security vulnera-
concern, we want to determine the byte-level representa- bilities in system software [26, 6].
tion of data. We want to optimize the time and space usage The design of Rust draws deeply from the wellspring of
of our programs using low-level programming techniques. academic research on safe systems programming. In particu-
We want access to the “bare metal” when we need it. lar, the most distinctive feature of Rust’s design—in relation
to other mainstream languages—is its adoption of an own-
Sadly, the conventional wisdom goes, we can’t have ership type system (which in the academic literature is often
everything we want. Languages like Java give us strong referred to as an affine or substructural type system [37]).
safety, but it comes at the expense of control. As a result, for Ownership type systems help the programmer enforce safe
many systems programming applications, the only realistic patterns of lower-level programming by placing restrictions
option is to use a language like C or C++ that provides on which aliases (references) to an object may be used to
fine-grained control over resource management. However, mutate it at any given point in the program’s execution.

1 2020/2/1
 However, Rust goes beyond the ownership type systems still points to the old buffer. In other words, adding a new
of prior work in at least two novel and exciting ways: element to v has turned vptr into a dangling pointer. This
is possible because both pointers were aliasing: an action
1. Rust introduces the mechanisms of borrowing and life-
through a pointer (v) will in general also affect all its aliases
times, which make it much easier to express common
(vptr). The entire situation is visualized as follows:
C++-style idioms and ensure that they are used safely.
v
2. Rust also provides a rich set of APIs—e.g., for concur-
rency abstractions, efficient data structures, and memory 10 10
vptr 11 11
management—which fundamentally extend the power of
12
the language by supporting more flexible combinations
of aliasing and mutation than Rust’s core type system al- The fact that vptr is now a dangling pointer becomes
lows. Correspondingly, these APIs cannot be implemented a problem in the fourth line. Here we load from vptr, and
within the safe fragment of Rust: rather, they internally since it is a dangling pointer, this is a use-after-free bug.
make use of potentially unsafe C-style features of the lan- In fact, the problem is common enough that one instance of
guage, but in a safely encapsulated way that is claimed it has its own name: iterator invalidation, which refers to the
not to disturb Rust’s language-level safety guarantees. situation where an iterator (usually internally implemented
with a pointer) gets invalidated because the data structure it it-
These aspects of Rust’s design are not only essential to
erates over is mutated during the iteration. It most commonly
its success—they also pose fundamental research questions
arises when one iterates over some container data structure in
about its semantics and safety guarantees that the program-
a loop, and indirectly, but accidentally, calls an operation that
ming languages community is just beginning to explore.
mutates the data structure. Notice that in practice the call to
In this article, we begin by giving the reader a bird’s-eye
the operation that mutates the data structure (push_back in
view of the Rust programming language, with an emphasis
line 3 of our example) might be deeply nested behind several
on some of the essential features of Rust that set it apart from
layers of abstraction. In particular when code gets refactored
its contemporaries. Second, we describe the initial progress
or new features get added, it is often near impossible to de-
made in the RustBelt project, an ongoing project funded
termine if pushing to a certain vector will invalidate pointers
by the European Research Council (ERC), whose goal is to
elsewhere in the program that are going to be used again later.
provide the first formal (and machine-checked) foundations
for the safety claims of Rust. In so doing, we hope to inspire Comparison with garbage-collected languages
other members of the computer science research community
to start paying closer attention to Rust and to help contribute The typical way to avoid use-after-free bugs is to introduce
to the development of this groundbreaking language. garbage collection: languages like Java, Go, or OCaml only
deallocate memory when it can longer be used by the program.
Thus, there can be no dangling pointers and no use-after-free.
Motivation: Pointer Invalidation in C++ One problem with that approach is that, to make garbage
To demonstrate the kind of memory safety problems that collection efficiently implementable, such languages gener-
arise commonly in systems programming languages, let us ally do not permit pointers that point into a data structure. For
consider the following C++ code: example, one would use ArrayList<Integer> to represent
a vector of integers in Java. Contrary to C++, where the un-
1 std::vector<int> v { 10, 11 };
derlying buffer of the vector directly contains the integers, the
2 int *vptr = &v[1]; // Points *into* ‘v‘.
Java variant is a vector of references to integers. A reference
3 v.push_back(12);
to an element of the array is obtained by simply copying the
4 std::cout << *vptr; // Bug (use-after-free)
reference stored in the buffer. This sacrifices performance
In the first line, this program creates a std::vector (a and control over memory layout in return for safety.
growable array) of integers. The initial contents of v, the two On top of that, garbage collection does not even properly
elements 10 and 11, are stored in a buffer in memory. In the solve the issue of iterator invalidation. Mutating a collection
second line, we create a pointer vptr that points into this while iterating over it in Java cannot lead to dangling pointers,
buffer; specifically it points to the place where the second but it may lead to a ConcurrentModificationException
element (with current value 11) is stored. Now both v and being thrown at run time. Similarly, while Java does prevent
vptr point to (overlapping parts of) the same buffer; we say security vulnerabilities caused by null pointer misuse, it does
that the two pointers are aliasing. In the third line, we push so with run-time checks that raise a NullPointerException.
a new element to the end of v. The element 12 is added In both of these cases, while the result is clearly better than
after 11 in the buffer backing v. If there is no more space for the corresponding undefined behavior of a C++ program, it
an additional element, a new buffer is allocated and all the still leaves a lot to be desired: instead of shipping incorrect
existing elements are moved over. Let us assume this is what code and then detecting issues at run time, we want to prevent
happens here. Why is this case interesting? Because vptr the bugs from occurring in the first place.

2 2020/2/1
Rust’s solution to pointer invalidation that consume can do whatever it desires with w, and the caller
In Rust, issues like iterator invalidation and null pointer may no longer access the memory backing this vector at all.
misuse are detected statically, by the compiler—they lead to a Resource management. Ownership in Rust does not just
compile-time error instead of a run-time exception. To explain prevent memory errors. It also forms the core of Rust’s ap-
how this works, consider the following Rust translation of proach to memory management and, more generally, resource
our C++ example: management: when a variable holding owned memory (e.g.,
1 let mut v = vec![10, 11]; a variable of type Vec<T>, which owns the buffer in memory
2 let vptr = &mut v[1]; // Points *into* ‘v‘. backing the vector) goes out of scope, we know for sure that
3 v.push(12); this memory will not be needed any more—so the compiler
4 println!("{}", *vptr); // Compiler error can automatically deallocate the memory at that point. To
this end, the compiler transparently inserts destructor calls,
Just like in the C++ version, there is a buffer in memory, just like in C++. For example, in the consume function, it is
and vptr points into the middle of that buffer (causing not actually necessary to call the destructor method (drop)
aliasing); push might reallocate the buffer, which leads to explicitly. We could have just left the body of that function
vptr becoming a dangling pointer, and that leads to a use- empty, and it would have automatically deallocated w itself.
after-free in line 4. As a consequence, Rust programmers rarely have to worry
But none of this happens; instead the compiler shows an about memory management: it is largely automatic, despite
error: “cannot borrow v as mutable more than once at a time”. the lack of a garbage collector. Moreover, the fact that mem-
We will come back to “borrowing” soon, but the key idea— ory management is also static (determined at compile time)
the mechanism through which Rust achieves memory safety yields enormous benefits: it helps not only to keep the max-
in the presence of pointers that point into a data structure— imal memory consumption down, but also to provide good
already becomes visible here: the type system enforces the worst-case latency in a reactive system such as a web server.
discipline (with a notable exception that we will come to And on top of that, Rust’s approach generalizes beyond mem-
later) that a reference is never both aliased and mutable at ory management: other resources like file descriptors, sockets,
the same time. This principle should sound familiar in the lock handles, and so on are handled with the same mecha-
context of concurrency, and indeed Rust uses it to ensure nism, so that Rust programmers do not have to worry, for
the absence of data races as well. However, as our example instance, about closing files or releasing locks. Using destruc-
that is rejected by the Rust compiler shows, the unrestricted tors for automatic resource management was pioneered in
combination of aliasing and mutation is a recipe for disaster the form of RAII (Resource Acquisition Is Initialization) in
even for sequential programs: in line 3, vptr and v alias (v C++ [31]; the key difference in Rust is that the type system
is considered to point to all of its contents, which overlaps can statically ensure that resources do not get used any more
with vptr), and we are performing a mutation, which leads after they have been destructed.
to a memory access error in line 4.
Mutable references. A strict ownership discipline is nice
and simple, but unfortunately not very convenient to work
Ownership and Borrowing with. Frequently, one wants to provide data to some function
The core mechanism through which Rust prevents uncon- temporarily, but get it back when that function is done. For
trolled aliasing is ownership. Memory in Rust always has a example, we want v.push(12) to grant push the privilege
unique owner, as demonstrated by the following example: to mutate v, but we do not want it to consume the vector v.
1 fn consume(w: Vec<i32>) { In Rust, this is achieved through borrowing, which takes
2 drop(w); // deallocate vector a lot of inspiration from prior work on region types [34, 13].
3 } For example, we could write:
4 let v = vec![10, 11]; 1 fn add_something(v: &mut Vec<i32>) {
5 consume(v); 2 v.push(11);
6 v.push(12); // Compiler error 3 }
4 let mut v = vec![10];
Here, we construct v similar to our first example, and then
5 add_something(&mut v);
pass it to consume. Operationally, just like in C++, parame-
6 v.push(12); // Ok!
ters are passed by value but the copy is shallow—pointers get
7 // v.push(12) is syntactic sugar for
copied but their pointee does not get duplicated. This means
8 // Vec::push(&mut v, 12)
that v and w point to the same buffer in memory.
Such aliasing is a problem if v and w would both be used The function add_something takes an argument of type
by the program, but an attempt to do so in line 6 leads to a &mut Vec<i32>, which indicates a mutable reference to a
compile-time error. This is because Rust considers ownership Vec<i32>. Operationally, this acts just like a reference in
of v to have moved to consume as part of the call, meaning C++, i.e., the Vec is passed by reference. In the type system,

3 2020/2/1
this is interpreted as add_something borrowing ownership are done, and returns both of their results. When join returns,
of the Vec from the caller. the borrow ends, so we can mutate v again.
The function add_something demonstrates what borrow- Just like mutable references, shared references have a
ing looks like in well-formed programs. To see why the com- lifetime. Under the hood, the Rust compiler is using a lifetime
piler accepts that code while rejecting our pointer invalidation to track the period during which v is temporarily shared
example from page 3, we have to introduce another concept: between the two threads; after that lifetime is over (on line 7),
lifetimes. Just like in real life, when borrowing something, the original owner of v regains full control. The key difference
misunderstanding can be prevented by agreeing up front on here is that multiple shared references are allowed to coexist
how long something may be borrowed. So, when a reference during the same lifetime, so long as they are only used for
gets created, it gets assigned a lifetime, which gets recorded reading, not writing. We can witness the enforcement of this
in the full form of the reference type: &’a mut T for life- restriction by changing one of the two threads in our example
time ’a. The compiler ensures that (a) the reference (v, in to || v.push(12): then the compiler complains that we
our example) only gets used during that lifetime, and (b) the cannot have a mutable reference and a shared reference to
referent does not get used again until the lifetime is over. the Vec at the same time. And indeed, that program has a
In our case, the lifetimes (which are all inferred by the fatal data race between the reading thread and the thread
compiler) just last for the duration of add_something and that pushes to the vector, so it is important that the compiler
Vec::push, respectively. Never is v used while the lifetime detects such cases statically.
of a previous borrow is still ongoing. Shared references are also useful in sequential code; for
In contrast, consider the example from page 3: example, while doing a shared iteration over a vector we can
still pass a shared reference to the entire vector to another
1 let mut v = vec![10, 11];
function. But for this article, we will focus on the use of
2 let vptr : &’a mut i32 = &mut v[1];
sharing for concurrency.
3 v.push(12);
4 println!("{}", *vptr); // Compiler error
Summary
Lifetime’a
In order to obtain safety, the Rust type system
The lifetime ’a of the borrow for vptr starts in line 2 and enforces the discipline that a reference is never
Aliasing
goes on until line 4. It cannot be any shorter because vptr both aliased and mutable. Having a value of
+
gets used in line 4. However, this means that in line 3, v is type T means you “own” it fully. The value
Mutation
used while an outstanding borrow exists, which is an error. of type T can be “borrowed” using a mutable
To summarize: whenever something is passed by value (as reference (&mut T) or shared reference (&T).
in consume), Rust interprets this as ownership transfer; when
something is passed by reference (as in add_something), Relaxing Rust’s Strict Ownership Discipline
Rust interprets this as borrowing for a certain lifetime. via Safe APIs
Shared references. Following the principle that we can Rust’s core ownership discipline is sufficiently flexible to
have either aliasing or mutation, but not both at the same account for many low-level programming idioms. But for im-
time, mutable references are unique pointers: they do not plementing certain data structures, it can be overly restrictive.
permit aliasing. To complete this picture, Rust has a second For example, without any mutation of aliased state, it is not
kind of reference, the shared reference written &Vec<i32> or possible to implement a doubly-linked list because each node
&’a Vec<i32>, which allows aliasing but no mutation. One is aliased by both its next and previous pointers.
primary use-case for shared references is to share read-only Rust adopts a somewhat unusual approach to this problem.
data between multiple threads: Rather than either (1) complicating its type system to account
for data structure implementations that do not adhere to it, or
1 let v = vec![10,11];
(2) introducing dynamic checks to enforce safety at run time,
2 let vptr = &v[1];
Rust allows its ownership discipline to be relaxed through the
3 join( || println!("v[1] = {}", *vptr),
development of safe APIs—APIs that extend the expressive
4 || println!("v[1] = {}", *vptr));
power of the language by enabling safely controlled usage
5 v.push(12);
of aliased mutable state. Although the implementations of
Here, we create a shared reference vptr pointing to (and these APIs do not adhere to Rust’s strict ownership discipline
borrowing) v[1]. The vertical bars here represent a closure (a point we return to on page 6), the APIs themselves make
(also sometimes called an anonymous function or “lambda”) critical use of Rust’s ownership and borrowing mechanisms
that does not take any arguments (the arguments would go to ensure that they preserve the safety guarantees of Rust as a
between the vertical bars). These closures are passed to join, whole. We have in fact already seen one example of such a
which is the Rust version of “parallel composition”: it takes safe API: Vec. Let us now look at a few other examples that
two closures, runs both of them in parallel, waits until both extend Rust’s ownership discipline in more interesting ways.

4 2020/2/1
Shared mutable state Reference counting
Rust’s shared references permit multiple threads to read We have seen that shared references provide a way to share
shared data concurrently. But threads that just read data are data between different parties in a program. However, shared
only half the story, so next we will look at how the Mutex references come with a statically determined lifetime, and
API enables one to safely share mutable state across thread when that lifetime is over, the data is uniquely owned again.
boundaries. At first, this might seem to contradict everything This works well with structured parallelism (like join in
we said so far about the safety of Rust: isn’t the whole point the previous example), but does not work with unstructured
of Rust’s ownership discipline that it prevents mutation of parallelism where threads are spawned off and keep running
shared state? Indeed it is, but we will see how, using Mutex, independently from the parent thread.
such mutation can be sufficiently restricted so as to not break In Rust, the typical way to share data in such a situation is
memory or thread safety. Consider the following example: to use an atomically reference-counted pointer: Arc<T> is a
pointer to T, but it also counts how many such pointers exist
1 let mutex_v = Mutex::new(vec![10, 11]);
and deallocates the T (and releases its associated resources)
2 join(
when the last pointer is destroyed. (This can be viewed as a
3 || { let mut v = mutex_v.lock().unwrap();
form of lightweight library-implemented garbage collection.)
4 v.push(12); },
Since the data is shared, we cannot obtain an &mut T from
5 || { let v = mutex_v.lock().unwrap();
an Arc<T>—but we can obtain an &T (where the compiler
6 println!("{:?}", *v) });
ensures that during the lifetime of the reference, the Arc<T>
We again use structured concurrency and shared references, does not get destroyed), as in this example:
but now we wrap the vector in a Mutex: the variable mutex_v 1 let arc_v1 = Arc::new(vec![10, 11]);
has type Mutex<Vec<i32>>. The key operation on a Mutex 2 let arc_v2 = Arc::clone(&arc_v1);
is lock, which blocks until it can acquire the exclusive lock. 3 spawn(move || println!("{:?}", arc_v2[1]));
The lock implicitly gets released by v’s destructor when the 4 println!("{:?}", arc_v1[1]);
variable goes out of scope. Ultimately, this program prints
either [10, 11, 12] if the first thread manages to acquire We start by creating an Arc that points to our usual vector.
the lock first, or [10, 11] if the second thread does. arc_v2 is obtained by cloning arc_v1, which means that
In order to understand how our example program type- the reference count gets bumped up by one, but the data
checks, let us take a closer look at lock. It (almost1 ) has type itself is not duplicated. Then we spawn a thread that uses
fn(&’a Mutex<T>) -> MutexGuard<’a, T>. This type arc_v2; this thread keeps running in the background even
says that lock can be called with a shared reference to a mu- when the function we are writing here returns. Because this
tex, which is why Rust lets us call lock on both threads: both is unstructured parallelism we have to explicitly move (i.e.,
closures capture an &Mutex<Vec<i32>>, and as with the transfer ownership of) arc_v2 into the closure that runs
vptr of type &i32 that got captured in our first concurrency in the other thread. Arc is a “smart pointer” (similar to
example, both threads can then use that reference concur- shared_ptr in C++), so we can work with it almost as if it
rently. In fact, it is crucial that lock take a shared rather were an &Vec<i32>. In particular, in lines 3 and 4 we can
than a mutable reference—otherwise, two threads could not use indexing to print the element at position 1. Implicitly, as
attempt to acquire the lock at the same time and there would arc_v1 and arc_v2 go out of scope, their destructors get
be no need for a lock in the first place. called, and the last Arc to be destroyed deallocates the vector.
The return type of lock, namely MutexGuard<’a, T>, is Thread safety
basically the same as &’a mut T: it grants exclusive access
There is one last type that we would like to talk about in
to the T that is stored inside the lock. Moreover, when it goes
this brief introduction to Rust: Rc<T> is a reference-counted
out of scope, it automatically releases the lock (an idiom
type very similar to Arc<T>, but with the key distinction that
known in the C++ world as RAII [31]).
Arc<T> uses an atomic (fetch-and-add) instruction to update
In our example, this means that both threads temporarily
the reference count, whereas Rc<T> uses non-atomic memory
have exclusive access to the vector, and they have a mutable
operations. As a result, Rc<T> is potentially faster, but not
reference that reflects that fact—but thanks to the lock prop-
thread-safe. The type Rc<T> is useful in complex sequential
erly implementing mutual exclusion, they will never both
code where the static scoping enforced by shared references
have a mutable reference at the same time, so the uniqueness
is not flexible enough, or where one cannot statically predict
property of mutable references is maintained. In other words,
when the last reference to an object will be destroyed so that
Mutex can offer mutation of aliased state in a sound way
the object itself can be deallocated.
because it implements run-time checks that make sure that
Since Rc<T> is not thread-safe, we need to make sure that
during each mutation, the state is not aliased.
the programmer does not accidentally use Rc<T> when they
1 Theactual type of lock wraps the result in a LockResult<...> for error should have used Arc<T>. This is important: if we take our
handling, which explains why we use unwrap on lines 4 and 8. previous Arc example, and replace all the Arc by Rc, the

5 2020/2/1
program has a data race and might deallocate the memory atomically checked for liveness and upgraded to a full Arc.
too early or not at all. However, quite remarkably, the Rust The destructor for Arc looks roughly as follows:
compiler is able to catch this mistake. The way this works is
1 fn drop(&mut self) {
that Rust employs something called the Send trait: a property
2 if self.inner().strong
of types which is only enjoyed by a type T if elements of
3 .fetch_sub(1, Release) != 1
type T can be safely sent to another thread. The type Arc<T>
4 { return; }
is Send, but Rc<T> is not. Both join and spawn require
5 atomic::fence(Acquire);
everything captured by the closure(s) they run to be Send,
6 unsafe { /*..*/ Global.dealloc(/*..*/); }
so if we capture a value of the non-Send type Rc<T> in a
7 }
closure, compilation will fail.
Rust’s use of the Send trait demonstrates how sometimes The correctness of drop relies on rather subtle concurrent
the restrictions imposed by strong static typing can lead to reasoning, and the Rust compiler simply has no way to verify
greater expressive power, not less. In particular, C++’s smart statically that the call to dealloc on line 6 is in fact safe.
reference-counted pointer, std::shared_ptr, always uses Alternatives to unsafe blocks. One could turn things like
atomic instructions2 , because having a more efficient non- Arc or Vec into language primitives. For example, Python
thread-safe variant like Rc is considered too risky. In contrast, and Swift have built-in reference counting, and Python has
Rust’s Send trait allows one to “hack without fear” [27]: it list as a built-in equivalent to Vec. However, these language
provides a way to have both thread-safe data structures (such features are implemented in C or C++, so it is not actually
as Arc) and non-thread-safe data structures (such as Rc) in any safer than the unsafe Rust implementation. Beyond that,
the same language, while ensuring modularly that the two do restricting unsafe operations to implementations of language
not get used in incorrect ways. primitives also severely restricts flexibility. For example,
Firefox uses a Rust library implementing a variant of Arc
Unsafe Code, Safely Encapsulated without support for weak references, which improves space
We have seen how types like Vec, Arc, and Mutex let Rust usage and performance for code that does not need them.
programs safely use features such as efficient growable arrays, Should the language provide primitives for every conceivable
reference counting, and shared mutable state. However, there spot in the design space of any built-in type?
is a catch: those types cannot actually be implemented in Another option to avoid unsafe code is to make the type
Rust. Or, rather, they cannot be implemented in safe Rust: the system expressive enough to actually be able to verify safety
compiler would reject an implementation of Arc for violating of types like Arc. However, due to how subtle correctness of
the aliasing discipline, and reject an implementation of Vec such data structures can be (and indeed Arc and simplified
for accessing potentially uninitialized memory. Of course, the variants of it have been used as a major case-study in several
implementation of Arc does not in fact violate the aliasing recent formal verification papers [10, 18, 8]), this basically
discipline, and Vec does not in fact access uninitialized requires a form of general-purpose theorem prover—and a
memory, but the arguments needed to establish those facts researcher with enough background to use it. The theorem
are too subtle for the Rust compiler to infer. proving community is quite far away from enabling develop-
To solve this problem, Rust has an “escape hatch”: Rust ers to carry out such proofs themselves.
does not just consist of the safe language we discussed
Safe abstractions. Rust instead decided to let programmers
so far—it also provides some unsafe features such as C-
write unsafe code, albeit with the expectation that unsafe code
style unrestricted pointers. The safety (memory safety and/or
should be encapsulated by safe APIs. As a user of Arc and
thread safety) of these features cannot be guaranteed by the
Vec, we are just as safe as we are in languages like Swift
compiler, so they are only available inside syntactic blocks
or Python—the compiler does not have to understand why
that are marked with the unsafe keyword. This way, one can
the implementations of those APIs are safe in order for it to
be sure to not accidentally leave the realm of safe Rust.
enforce that client code uses the APIs safely. This is in strong
For example, the implementation of Arc uses unsafe code
contrast to C++, in which even safe usage is not guaranteed.
to implement a pattern that would not be expressible in safe
C++ APIs like shared_ptr or vector are prone to misuse,
Rust: sharing without a clear owner, managed by thread-
leading to reference-counting bugs and iterator invalidation,
safe reference counting. Arc has to manually manage the
because C++ lacks the ability to enforce safe abstractions.
allocation holding the reference-counted object, and make
At the same time, in Rust unsafe components can be imple-
sure it only gets removed when the last reference is gone.
mented while still staying within the Rust ecosystem. This is
Moreover, it has to do all of that in a thread-safe way. This
different from implementing an efficient C/C++ extension for
is further complicated by support for “weak references”:
a language such as Python, where the programmer has to deal
references that do not keep the referent alive, but can be
with different languages and their untyped FFI boundary.
2 Moreprecisely, on Linux it uses atomic instructions if the program uses The ability to write unsafe code is like a lever that Rust
pthreads, i.e., if it or any library it uses might spawn a thread. programmers use to make the type system more useful

6 2020/2/1
without turning it into a theorem prover, and indeed we Semantic type soundness is ideal for reasoning about
believe this to be a key ingredient to Rust’s success. The programs that use a combination of safe and unsafe code. For
Rust community is developing an entire ecosystem of safely any library that uses unsafe code (such as Arc, Mutex, Rc,
usable high-performance libraries, enabling programmers to and Vec) one has to prove by hand that the implementation
build safe and efficient applications on top of them. satisfies the safety contract. For example:
But of course, there is no free lunch: it is up to the author Theorem 2. Arc satisfies its safety contract.
of a Rust library to somehow ensure that, if they use unsafe
code, they are being very careful not to break Rust’s safety For safe pieces of a program, the verification is automatic.
guarantees. On the one hand, this is a much better situation This is expressed by the following theorem, which says that
than in C/C++, because the vast majority of Rust code is if a component is written in the safe fragment of Rust, it
written in the safe fragment of the language, so Rust’s “attack satisfies its safety contract by construction.
surface” is much smaller. On the other hand, when unsafe Theorem 3 (Fundamental theorem). If a component e is
code is needed, it is far from obvious how a programmer is syntactically well-typed, then e satisfies its safety contract.
supposed to know if they are being “careful” enough.
To maintain confidence in the safety of the Rust ecosystem, Together, these imply that a Rust program is safe if the only
we therefore really want to have a way of formally specifying appearances of unsafe blocks are within libraries that have
and verifying what it means for uses of unsafe code to be been verified to satisfy their corresponding safety contracts.
safely encapsulated behind a safe API. This is precisely the What logic to use for safety contracts?
goal of the RustBelt project.
Semantic type soundness is an old technique, dating back at
least to Milner’s seminal 1978 paper on type soundness [28],
RustBelt: Securing the Foundations of Rust but scaling it up to realistic modern languages like Rust has
The key challenge in verifying Rust’s safety claims is ac- proven a difficult challenge. In fact, scaling it up to languages
counting for the interaction between safe and unsafe code. with mutable state and higher-order functions remained an
To see why this is challenging, let us briefly take a look at open problem until the development of “step-indexed logical
the standard technique for verifying safety of programming relations” [4, 2] developed as part of the Foundational Proof-
languages—the so called syntactic approach [38, 14]. Using Carrying Code project [3, 1] decades later.
that technique, safety is expressed in terms of a syntactic In RustBelt we build upon that work and follow the style of
typing judgment, which gives a formal account of the type recent “logical” accounts of logical relations [11, 12, 36, 25].
checker in terms of a number of mathematical inference rules. Most importantly, instead of using ordinary first-order or
higher-order logic to define the safety contracts and conduct
Theorem 1 (Syntactic type soundness). If a program e is the verification, we use a logic that provides a more suitable
well-typed w.r.t. the syntactic typing judgment, then e is safe. set of higher-level abstractions. In particular:
Unfortunately, this theorem is too weak for our purposes, • To handle the ownership aspects of Rust, we employ sep-
because it only talks about syntactically safe programs, thus aration logic [29, 30], an extension of Hoare logic [15]
ruling out programs that use unsafe code. For example, which is geared specifically toward modular reasoning
if true { e } else { crash() } is not syntactically about pointer-manipulating programs and which is cen-
well-typed, but it is still safe since crash() is never executed. tered around the concept of ownership.
• To handle borrows and lifetimes, we need custom rea-
The key solution: Semantic type soundness
soning principles. We have developed a domain-specific
To account for the interaction between safe and unsafe code, “lifetime logic” as an extension of separation logic.
we instead use a technique called semantic type soundness,
• To modularly verify libraries that implement concurrency
which expresses safety in terms of the “behavior” of the
primitives (like Arc) we need support for separately-
program rather than a fixed set of inference rules. The key
ownable resources governing shared physical state. For
ingredient of semantic soundness is a logical relation, which
that, we use fictional separation logic [17, 9].
assigns a safety contract to each API. Using techniques from
formal verification, one can then prove that an implementa- • To deal with the various forms of recursion in Rust, we
tion of the API satisfies the assigned safety contract: use step-indexing [5] and impredicativity [32].
Apart from these features, the complexity of Rust demands
∀Σ. that our logic support machine-checked formal proofs, as it
∃Φ. . . .  would be too tedious and error-prone to do proofs by hand.
Logical Formal All of the above features are provided by the Iris sep-
relation Safety verification aration logic framework [21, 19, 23, 20], which we have
API Code
contract developed over the past five years together with a growing

7 2020/2/1
network of collaborators, and which is implemented in the [15] C. A. R. Hoare. An axiomatic basis for computer programming.
Coq proof assistant [24, 22]. CACM, 12(10), 1969.
[16] D. Hosfelt. Implications of rewriting a browser component in
Conclusion and Outlook Rust, 2019. Blog post. https://hacks.mozilla.org/2019/02/
rewriting-a-browser-component-in-rust/.
In this paper we have given a bird’s-eye view of Rust, demon-
[17] J. B. Jensen and L. Birkedal. Fictional separation logic. In ESOP,
strating its core concepts like borrowing, lifetimes, and un- volume 7211 of LNCS, 2012.
safe code encapsulated inside safe APIs. These features have
[18] R. Jung, J.-H. Jourdan, R. Krebbers, and D. Dreyer. RustBelt: Securing
helped Rust become the first industry-supported language to the foundations of the Rust programming language. PACMPL,
overcome the tradeoff between safety and control. 2(POPL), 2018.
To formally investigate Rust’s safety claims, we described [19] R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer. Higher-order ghost
the proof technique of semantic type soundness, which has state. In ICFP, 2016.
enabled us to begin building a rigorous foundation for Rust [20] R. Jung, R. Krebbers, J.-H. Jourdan, A. Bizjak, L. Birkedal, and
in the RustBelt project. But there is still much work left to D. Dreyer. Iris from the ground up: A modular foundation for higher-
order concurrent separation logic. JFP, 28, 2018.
do. Although RustBelt has recently been extended to account
[21] R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon,
for the relaxed-memory concurrency model that Rust inherits L. Birkedal, and D. Dreyer. Iris: Monoids and invariants as an
from C++ [8], there are a number of other Rust features orthogonal basis for concurrent reasoning. In POPL, 2015.
and APIs that it does not yet cover. Notably, we still lack a [22] R. Krebbers, J.-H. Jourdan, R. Jung, J. Tassarotti, J.-O. Kaiser,
formal model of Rust’s “trait” system, a central organizing A. Timany, A. Charguéraud, and D. Dreyer. MoSeL: A general,
feature (akin to Haskell’s “type classes”), which is complex extensible modal framework for interactive proofs in separation logic.
PACMPL, 2(ICFP), 2018.
enough to have been the source of subtle soundness bugs [7].
Moreover, although verifying the soundness of an internally- [23] R. Krebbers, R. Jung, A. Bizjak, J. Jourdan, D. Dreyer, and L. Birkedal.
The essence of higher-order concurrent separation logic. In ESOP,
unsafe Rust library requires, at present, a deep background volume 10201 of LNCS, 2017.
in formal semantics, we hope to eventually develop formal [24] R. Krebbers, A. Timany, and L. Birkedal. Interactive proofs in higher-
methods that can be put directly in the hands of programmers. order concurrent separation logic. In POPL, 2017.
[25] M. Krogh-Jespersen, K. Svendsen, and L. Birkedal. A relational model
References of types-and-effects in higher-order concurrent separation logic. In
[1] A. Ahmed, A. W. Appel, C. D. Richards, K. N. Swadi, G. Tan, and POPL, 2017.
D. C. Wang. Semantic foundations for typed assembly languages. [26] R. Levick. Why Rust for safe systems programming, 2019. Blog
TOPLAS, 32(3), 2010. post. https://msrc-blog.microsoft.com/2019/07/22/why-
[2] A. J. Ahmed. Semantics of types for mutable state. PhD thesis, rust-for-safe-systems-programming/.
Princeton University, 2004. [27] N. Matsakis and A. Turon. Rust in 2016, 2015. Blog post. https:
[3] A. W. Appel. Foundational proof-carrying code. In LICS, 2001. //blog.rust-lang.org/2015/08/14/Next-year.html.
[4] A. W. Appel and D. McAllester. An indexed model of recursive types [28] R. Milner. A theory of type polymorphism in programming. Journal
for foundational proof-carrying code. TOPLAS, 23(5), 2001. of Computer and System Sciences, 17(3), 1978.
[5] A. W. Appel, P.-A. Melliès, C. Richards, and J. Vouillon. A very [29] P. W. O’Hearn, J. C. Reynolds, and H. Yang. Local reasoning about
modal model of a modern, major, general type system. In POPL, programs that alter data structures. In CSL, volume 2142 of LNCS,
2007. 2001.
[6] A. Burch. Using Rust in Windows, 2019. Blog post. https: [30] P. W. O’Hearn. Resources, concurrency, and local reasoning. Theoret-
//msrc-blog.microsoft.com/2019/11/07/using-rust-in- ical Computer Science, 375(1-3), 2007.
windows/. [31] B. Stroustrup. The C++ Programming Language. Addison-Wesley,
[7] comex. Unsoundness in ‘Pin‘, 2019. https://internals.rust- 2013.
lang.org/t/unsoundness-in-pin/11311. [32] K. Svendsen and L. Birkedal. Impredicative concurrent abstract
[8] H.-H. Dang, J.-H. Jourdan, J.-O. Kaiser, and D. Dreyer. RustBelt predicates. In ESOP, volume 8410 of LNCS, 2014.
meets relaxed memory. PACMPL, 4(POPL), 2020. [33] G. Thomas. A proactive approach to more secure code, 2019.
[9] T. Dinsdale-Young, M. Dodds, P. Gardner, M. J. Parkinson, and Blog post. https://msrc-blog.microsoft.com/2019/07/16/
V. Vafeiadis. Concurrent abstract predicates. In ECOOP, LNCS, a-proactive-approach-to-more-secure-code/.
2010. [34] M. Tofte and J. Talpin. Region-based memory management. Informa-
[10] M. Doko and V. Vafeiadis. Tackling real-life relaxed concurrency with tion and Computation, 132(2), 1997.
FSL++. In ESOP, volume 10201 of LNCS, 2017. [35] T. Tu, X. Liu, L. Song, and Y. Zhang. Understanding real-world
[11] D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical concurrency bugs in Go. In ASPLOS, 2019.
relations. LMCS, 7(2:16), 2011. [36] A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoare-
[12] D. Dreyer, G. Neis, A. Rossberg, and L. Birkedal. A relational modal style reasoning in a logic for higher-order concurrency. In ICFP,
logic for higher-order stateful ADTs. In POPL, 2010. 2013.
[13] D. Grossman, J. G. Morrisett, T. Jim, M. W. Hicks, Y. Wang, and [37] D. Walker. Substructural type systems. In B. C. Pierce, editor,
J. Cheney. Region-based memory management in Cyclone. In PLDI, Advanced Topics in Types and Programming Languages. MIT Press,
2002. 2005.
[14] R. Harper. Practical Foundations for Programming Languages (2nd [38] A. K. Wright and M. Felleisen. A syntactic approach to type soundness.
Edition). Cambridge University Press, 2016. Information and computation, 115(1), 1994.

8 2020/2/1