From: Ralf Jung Date: Sat, 8 Jul 2017 21:02:26 +0000 (-0700) Subject: post on RustBelt paper X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/99b016f4e15bde5b5cbd85815813c71b949f97fe post on RustBelt paper --- diff --git a/personal/_posts/2017-07-08-rustbelt.md b/personal/_posts/2017-07-08-rustbelt.md new file mode 100644 index 0000000..48adba1 --- /dev/null +++ b/personal/_posts/2017-07-08-rustbelt.md @@ -0,0 +1,38 @@ +--- +title: "RustBelt: Securing the Foundations of the Rust Programming Language" +categories: research rust +--- + +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). +Quoting from the abstract: + +> Rust is a new systems programming language that promises to overcome +the seemingly fundamental tradeoff between high-level safety +guarantees and low-level control over resource management. +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 core type system through +libraries that internally use unsafe features. In this paper, we give +the first formal (and machine-checked) safety proof for a language +representing a realistic subset of Rust. Our proof is extensible 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 extension to the language. We have carried out +this verification for some of the most important libraries that are +used throughout the Rust ecosystem. + + + +This paper is the result of almost two years of work by the [RustBelt](http://plv.mpi-sws.org/rustbelt/) research project to [formalize Rust's type system]({{ site.baseurl }}{% post_url 2015-10-12-formalizing-rust %}). +The paper is now undergoing peer review; some time in fall we will be notified whether the paper got accepted or not. + +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` (inspired by [Abomonation](http://www.frankmcsherry.org/serialization/2015/05/04/unsafe-at-any-speed.html)). +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 %}). +For all the details, have a [look at the paper](https://www.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf). +If that's not enough details, you can also check out [all our formal proofs](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/). + +Of course, I am far from the only person who worked on this. +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/). +I also benefited a lot from countless discussions with the Rust community at large, and with Aaron and Niko in particular. +You guys rock!