Adrian Colyer did a good write up of this paper recently on The Morning Paper : https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...
“We had to make some concessions in our modelling: we do not model…
1. more relaxed forms of atomic accesses, which Rust uses for efficiency in libraries like Arc
2. Rust’s trait objects, which can pose safety issues due to their interactions with lifetimes
3. stack unwinding when a panic occurs, which can cause similar issues to exception safety in C++
4. automatic destruction, “which has already caused problems for which the Rust community still does not have a modular solution.”
5. a few details unrelated to ownership, such as type-polymorphic functions and “unsized” types.”
Also shows why it’s good to have a semantics in the beginning covering the whole language like with ML or later SPARK Ada. It forces language developers to spot and address these corner cases early on. Good news is that, like with SPARK, one might just subset their use of Rust to exclusively what has been proven with no use of anything else. Is anything on the list common enough in most Rust development where it can’t be avoided and must be verified later? I’ve obviously seen many people mention traits. Arc and automatic destruction safety not being proven is a bit ironic given they’re presumably there to boost safety versus raw pointers and manual destruction.
EDIT: Thanks for quick, clarifying replies about these. It's looking like a subsetting approach can work.
Embedded code in Rust almost always avoids 1, 2, 3, and 4. Arc is used for freeing dynamically allocated memory when all references, including across threads, are dropped, but if you're running without dynamic memory allocation, you don't need that. Trait objects also require allocation. Embedded targets also generally don't implement stack unwinding, and stack unwinding can be disabled on other targets as well; it's really only most useful in larger applications in which you want some threads to be able to continue running even if another thread panics. Automatic destruction can be fairly easily avoided if you're running without an allocator, as it is mostly used for freeing such allocated memory, as well as a few things like file handles and the like.
The things covered in 5 might be harder to avoid, but also more likely to be amenable to being covered by further versions of the RustBelt work.
So yes, using a subset of Rust without these features is quite feasible, and often done when working in embedded (aka no_std) code.
I don't know SPARK Ada that well, but I believe it has similar constraints of no dynamic allocation. If you can do without dynamic allocation in Rust, many of the problematic features wouldn't be used.
That is, what RustBelt analyzes right now is a language which has an analogue to Rust's borrow checker, but is much much simpler overall; and they ported Rust's implementation of several types of shared mutable or owned references over to this language to verify them.
There is a lot of Rust outside of these few caveats that hasn't been covered; these are just the things which could be in scope of the RustBelt work that haven't been covered by it.
Here are a few things that there's ongoing work on that you would want to finish before saying you were confident in a using a formally verified language:
1. The memory model. This gives a formal definition of what kinds of aliasing assumptions the compiler is able to make about raw pointers in `unsafe` code. This is being worked on here: https://github.com/nikomatsakis/rust-memory-model 2. The borrow checker. While the RustBelt work shows that a much simpler borrow checker can be sound, Rust's borrow checker has to deal with a much more complicated language, and there are few known soundness bugs in it (discussed elswhere in this thread). You'd want that to be formally modeled and verified. 3. The type system. Rust has a fairly full featured type system, so you want to ensure that's sound 4. The compiler itself. Even once you have sound code in a sound language, you need to make sure that the compiler follows the rules and compiles it correctly. 5. Any libraries or code that you are using which might be using `unsafe`. The RustBelt work so far has done so for a few core primitives, as well as a couple of third-party libraries, but of course you'd want to re-do this work against the full language (or a real-world subset, not LambdaRust that this paper used) and include any other libraries that you might need to use.
So, I'd say that there's a good chance that the RustBelt work could be extended to include one or more of these listed features before all of the rest of the above has been done. It will be a while before you could have a usable, verified subset of Rust, but once you do I think it could be a good alternative to something like SPARK, or development in C following extremely stringent rules and compiling with CompCert.
fn trait_obj(foo: &Trait)...
I'm not sure how common a pattern that is. Many people like to avoid trait objects and just parameterize the function on a type bounded by the trait in that case. And impl Trait is replacing some of the other cases in which you had to return an allocated trait object.
Anyhow, you're right, I was wrong that people couldn't be using trait objects in an embedded context with no allocator, but I also think it's perfectly reasonable to write in a subset of Rust in which you don't use trait objects at all.
Box<Trait> is so pervasive because it's currently the easiest way to get type erasure in return position.
Destructors aren't guaranteed to run in Rust, they aren't necessary for memory safety. It's a fair concern to note that they aren't modeled, because they are pervasive and can impact memory safety, but they don't exist to support it.
Panics not being modeled is of course also a big gap, although you could always compile your code with panic=abort if you wanted to dodge that issue!
- Derek Dreyer, Workshop on Software Correctness and Reliability 2017 (48 min): https://www.youtube.com/watch?v=Y9vemQmVeLI
- Ralf Jung, POPL 2018 (25 min): https://plv.mpi-sws.org/rustbelt/popl18/