4 ms·

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-foundations-of-the-rus

by fovc 9y ago

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-foundations-of-the-rust-programming-language/ https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...

nickpsecurity 9y ago
From the Adrian Colyer's review, we find the title might be misleading depending on what ownership model entails for a given developer’s use of the language: “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.
- dikaiosune 9y ago
  For clarification, "trait objects" are a subset of the trait system, and have much less use in rust programs than traits overall. A trait object is a dynamically dispatched pointer (often owned through Box or Arc), as opposed to the usually statically dispatched generic usage of traits that's more common in rust. 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!
- lambda 9y ago
  You can avoid 1 if you do no multithreading, or if you accept a slower implementation of Arc. 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.
  - dikaiosune 9y ago
    Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...
    - lambda 9y ago
      Sorry, you are right about that. You can have trait objects without an allocator. 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.
      - Argorak 9y ago
- Jweb_Guru 9y ago
  FYI, (1) is (almost) definitely being addressed in the near future.
matt_d 9y ago
Two recent talks about the project: - Derek Dreyer, Workshop on Software Correctness and Reliability 2017 (48 min): https://www.youtube.com/watch?v=Y9vemQmVeLI https://www.youtube.com/watch?v=Y9vemQmVeLI - Ralf Jung, POPL 2018 (25 min): https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/
- fmap 9y ago
  Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk https://www.youtube.com/watch?v=8Xyk_dGcAwk

by fovc 9y ago

nickpsecurity 9y ago

From the Adrian Colyer's review, we find the title might be misleading depending on what ownership model entails for a given developer’s use of the language: “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.

dikaiosune 9y ago
For clarification, "trait objects" are a subset of the trait system, and have much less use in rust programs than traits overall. A trait object is a dynamically dispatched pointer (often owned through Box or Arc), as opposed to the usually statically dispatched generic usage of traits that's more common in rust. 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!
lambda 9y ago
You can avoid 1 if you do no multithreading, or if you accept a slower implementation of Arc. 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.
- dikaiosune 9y ago
  Nit: IIRC one can receive a trait object through a stack based reference. fn trait_obj(foo: &Trait)...
  - lambda 9y ago
    Sorry, you are right about that. You can have trait objects without an allocator. 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.
    - Argorak 9y ago
Jweb_Guru 9y ago
FYI, (1) is (almost) definitely being addressed in the near future.

matt_d 9y ago

Two recent talks about the project: - Derek Dreyer, Workshop on Software Correctness and Reliability 2017 (48 min): https://www.youtube.com/watch?v=Y9vemQmVeLI https://www.youtube.com/watch?v=Y9vemQmVeLI - Ralf Jung, POPL 2018 (25 min): https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/

fmap 9y ago
Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk https://www.youtube.com/watch?v=8Xyk_dGcAwk