personal/_posts/2017-07-08-rustbelt.md

   1 ---
   2 title: "RustBelt: Securing the Foundations of the Rust Programming Language"
   3 categories: research rust
   4 forum: https://internals.rust-lang.org/t/rustbelt-securing-the-foundations-of-the-rust-programming-language/5509
   5 ---
   6
   7 Just yesterday, we submitted our paper [RustBelt: Securing the Foundations of the Rust Programming Language](https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf).
   8 Quoting from the abstract:
   9
  10 > Rust is a new systems programming language that promises to overcome
  11 the seemingly fundamental tradeoff between high-level safety
  12 guarantees and low-level control over resource management.
  13 Unfortunately, none of Rust's safety claims have been formally proven,
  14 and there is good reason to question whether they actually hold.
  15 Specifically, Rust employs a strong, ownership-based type system, but
  16 then extends the expressive power of this core type system through
  17 libraries that internally use unsafe features.  In this paper, we give
  18 the first formal (and machine-checked) safety proof for a language
  19 representing a realistic subset of Rust.  Our proof is extensible in
  20 the sense that, for each new Rust library that uses unsafe features,
  21 we can say what verification condition it must satisfy in order for it
  22 to be deemed a safe extension to the language.  We have carried out
  23 this verification for some of the most important libraries that are
  24 used throughout the Rust ecosystem.
  25
  26 <!-- MORE -->
  27
  28 This paper is the result of almost two years of work by the [RustBelt](https://plv.mpi-sws.org/rustbelt/) research project to [formalize Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}).
  29 The paper is now undergoing peer review; some time in fall we will be notified whether the paper got accepted or not.
  30
  31 In case you wondered which "important libraries" we verified, the full list is `Rc`, `Arc`, `Cell` (including [`alias::one`](https://huonw.github.io/alias/alias/fn.one.html), which was recently [accepted into the standard library](https://github.com/rust-lang/rfcs/pull/1789)), `RefCell`, `Mutex`, `RwLock`, `thread::spawn`, `mem::swap`, [`take_mut::take`](https://docs.rs/take_mut/0.1.3/take_mut/fn.take.html) as well as converting `&&T` into `&Box<T>` (inspired by [Abomonation](http://www.frankmcsherry.org/serialization/2015/05/04/unsafe-at-any-speed.html)).
  32 Our model of Rust is somewhat simplified (e.g., we don't support unwinding after panics); still, we were actually able to [find a real bug]({{ site.baseurl }}{% post_url 2017-06-09-mutexguard-sync %}).
  33 For all the details, have a [look at the paper](https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf).
  34 If that's not enough details for your taste, you can also check out [all our formal proofs](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/).
  35
  36 Of course, I am far from the only person who worked on this.
  37 All these results were only possible because of my great collaborators, [Jacques-Henri Jourdan](https://jhjourdan.mketjh.fr/) and [Robbert Krebbers](http://robbertkrebbers.nl/), as well as my PhD advisor, [Derek Dreyer](http://www.mpi-sws.org/~dreyer/).
  38 I also benefited a lot from countless discussions with the Rust community at large, and with Aaron and Niko in particular.
  39 You guys rock!