11–20 of 109 posts
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...
- 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/
I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, u…
Experience has shown this hypothesis to be false, especially concerning low level systems programming languages and security issues.
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...
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. s…
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.
Does this prove that the current borrowck rules are sufficient to catch all possible mistakes? For example, does it catch stuff like https://github.com/rust-lang/rust/issues/31287 or https://github.com/rust-lang/rust/issues/38899 ?
What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics of the language to cover things that the borrow checker cannot cover, you can write proofs that demonstrate that the language is still sound given the addition of those types. This helps demonstrate that one of the fundamental design goals of Rust, have a sim…
Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_b..., it is not at all clear that these rules cover everything to me. There are some complex side conditions, isn't it easy to miss something there?
Earlier quoted context omitted.
What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics of the language to cover things that the borrow checker cannot cover, you can write proofs that demonstrate that the language is still sound given the addition of those types. This helps demonstrate that one of the fundamental design goals of Rust, have a sim…
> I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases. Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_b... , it is not at all clear that these rules cover everything to me. There are some complex side conditions, i…
I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, u…
Rust is a direct contender to C and C++, not to script or GC languages. Please compare apples to apples.
And all of this is not even relevant to usability issues he tries to discuss.
I have recently performed a relatively simple development by using programming languages on which I had low-to-to-no experience: Perl (low), Ruby (no), Rust (no) and Go (no). Note that I am quite adaptable on the programming language front and that this small experiment was precisely meant to showcase these adaptability skills. Rust was, by far, the most difficult-to-learn, difficult-to-research, counter-intuitive, u…
> The higher the freedom, the better the results delivered by a sensible/knowledgeable person. Experience has shown this hypothesis to be false, especially concerning low level systems programming languages and security issues.
Earlier quoted context omitted.
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. s…
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…
fn trait_obj(foo: &Trait)...
Earlier quoted context omitted.
What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics of the language to cover things that the borrow checker cannot cover, you can write proofs that demonstrate that the language is still sound given the addition of those types. This helps demonstrate that one of the fundamental design goals of Rust, have a sim…
> I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases. Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_b... , it is not at all clear that these rules cover everything to me. There are some complex side conditions, i…
The RustBelt work addressed one of the big open questions; is it possible to treat `unsafe` code in a modular fashion, or does all analysis of unsafe code have to consider all possible interactions with all other modules which use `unsafe` code as well?
That was in many ways quite a big question about the design of Rust; can you prove or very each module which uses `unsafe` independently?
The borrow checker, on the other hand, is an entirely local analysis. It can get quite complex, especially as you allow for more fine-grained borrow checking to make it convenient to use compound objects, and introduce non-lexical lifetimes which help reduce the number of restrictions on what you can do, but since it's entirely local, it's a much more tractable problem.
I think that it would be good to eventually formalize the full Rust borrow checker, and of course it's always good to fix these soundness bugs, but there are some more important open questions right now like fully specifying Rust's memory model (https://github.com/nikomatsakis/rust-memory-model) so it's possible to know what kinds of aliasing you can actually do in `unsafe` code, and which will be safe even under future versions of the compiler.
The RustBelt work so far is just a nice foundation getting Rust to be more formally analyzed and specified. There's a lot of work left to be done.
Earlier quoted context omitted.
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…
Nit: IIRC one can receive a trait object through a stack based reference. 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.