open some things in new tabs

[web.git] / personal / _posts / 2017-07-08-rustbelt.md

diff --git a/personal/_posts/2017-07-08-rustbelt.md b/personal/_posts/2017-07-08-rustbelt.md
index 48adba147d002469240f214ddd06e9e88870d939..a37df23e86e84da08e85c8feb1fd960a16b6096a 100644 (file)
--- a/personal/_posts/2017-07-08-rustbelt.md
+++ b/personal/_posts/2017-07-08-rustbelt.md
@@ -1,6 +1,7 @@
 ---
 title: "RustBelt: Securing the Foundations of the Rust Programming Language"
 categories: research rust
 ---
 title: "RustBelt: Securing the Foundations of the Rust Programming Language"
 categories: research rust

+forum: https://internals.rust-lang.org/t/rustbelt-securing-the-foundations-of-the-rust-programming-language/5509

 ---
 
 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).
 ---
 
 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).


@@ -30,7 +31,7 @@ The paper is now undergoing peer review; some time in fall we will be notified w
 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)).
 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).
 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)).
 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/).
+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/).

 
 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/).
 
 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/).