6 ms·

There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ http

There's a lot of interest in formally verifying things about the unsafe subset of Rust, for example the Rust Belt project: http://plv.mpi-sws.org/rustbelt/ http://plv.mpi-sws.org/rustbelt/. One thing I've not well understood is how these efforts may be affected by some of the conversations around the unsafe code guidelines effort: https://github.com/rust-lang/rfcs/pull/1643 https://github.com/rust-lang/rfcs/pull/1643 https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model

vog 9y ago
Just curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)
- ekidd 9y ago
  > That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? I write a fair bit of production and hobby Rust, some of it very performance-intensive. And at this point, 'unsafe' is already very rare in the code I see. The most common uses: 1. For implementing certain core data structures based on pointers. This is pretty rare—there are good implementations of just about everything I need, either from the 'std::collections' library (which uses a moderate amount of 'unsafe') or from third parties (who tend to use much less 'unsafe'). 2. For the FFI. Again, this is increasingly rare: More and more key libraries are now available as pure Rust, and the "big" C libraries typically have well-maintained bindings. 3. Theoretically, for performance. But I've written tons of high-performance, benchmarked Rust without ever touching 'unsafe'. And I do feed a fair bit of my code through fuzzers, and they've never found an exploitable weakness. So my gut feeling? There really isn't much 'unsafe' out there. And the small amount of 'unsafe' code that exists is probably—based on my experience fuzzing it—"safer" than all but the very best C/C++ code. I can live with that for now, on a strictly practical level.
- dikaiosune 9y ago
  There are already a lot of cases where LLVM can successfully optimize away things like safe Rust's bounds checks in loops. There are also efforts to include "const generics" which will let you use e.g. array lengths as generics that may be able to teach LLVM new optimizations. Maybe someday in the far future that will grow into some kind of dependent typing extension for Rust? That could potentially allow for safe, bounds-check free array access that would currently require unsafe. But I don't know if that would allow for proving the kinds of things this article discusses. Ultimately though, the unsafe subset is pretty small and is generally in my experience only interesting when building heavily reused abstractions (the kinds of lock-free algorithms OP discusses for example). It'll be really cool if these efforts expose some ways to shrink reliance on unsafe code, but I'm personally not sweating it.
- sanxiyn 9y ago
  There is interest in enabling safe interface, that is, improving Rust the language so that you can provide safe interface with better performance. A good example is so-called "streaming iterator". There is less interest in changing Rust so that currently unsafe implementation (not interface) of safe interface can be made safe, that is, verified by compiler. As grandparent stated, and I agree, as long as interface is safe I don't think it is important that implementation is verified by compiler (hence safe) or some external tool or hand proof.
  - michaelmior 9y ago
    Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?
    - kibwen 9y ago
      This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.
      - nickpsecurity 9y ago
        Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.
        kibwen 9y ago
        Can you give me an example of something that safe Rust doesn't allow, thereby requiring the unsafe keyword to implement, but that also contains an error that passes the Rust compiler silently but that Frama-C or SPARK would statically detect?

vog 9y ago

Just curious: Are there also attempts in the reverse direction? That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? (maybe even compiles down to the same machine code)

ekidd 9y ago
> That is, are there attempts to improve the Rust language and/or optimizer such that more and more "unsafe" sections can be replaced by safe code that has the same performance? I write a fair bit of production and hobby Rust, some of it very performance-intensive. And at this point, 'unsafe' is already very rare in the code I see. The most common uses: 1. For implementing certain core data structures based on pointers. This is pretty rare—there are good implementations of just about everything I need, either from the 'std::collections' library (which uses a moderate amount of 'unsafe') or from third parties (who tend to use much less 'unsafe'). 2. For the FFI. Again, this is increasingly rare: More and more key libraries are now available as pure Rust, and the "big" C libraries typically have well-maintained bindings. 3. Theoretically, for performance. But I've written tons of high-performance, benchmarked Rust without ever touching 'unsafe'. And I do feed a fair bit of my code through fuzzers, and they've never found an exploitable weakness. So my gut feeling? There really isn't much 'unsafe' out there. And the small amount of 'unsafe' code that exists is probably—based on my experience fuzzing it—"safer" than all but the very best C/C++ code. I can live with that for now, on a strictly practical level.
dikaiosune 9y ago
There are already a lot of cases where LLVM can successfully optimize away things like safe Rust's bounds checks in loops. There are also efforts to include "const generics" which will let you use e.g. array lengths as generics that may be able to teach LLVM new optimizations. Maybe someday in the far future that will grow into some kind of dependent typing extension for Rust? That could potentially allow for safe, bounds-check free array access that would currently require unsafe. But I don't know if that would allow for proving the kinds of things this article discusses. Ultimately though, the unsafe subset is pretty small and is generally in my experience only interesting when building heavily reused abstractions (the kinds of lock-free algorithms OP discusses for example). It'll be really cool if these efforts expose some ways to shrink reliance on unsafe code, but I'm personally not sweating it.
sanxiyn 9y ago
There is interest in enabling safe interface, that is, improving Rust the language so that you can provide safe interface with better performance. A good example is so-called "streaming iterator". There is less interest in changing Rust so that currently unsafe implementation (not interface) of safe interface can be made safe, that is, verified by compiler. As grandparent stated, and I agree, as long as interface is safe I don't think it is important that implementation is verified by compiler (hence safe) or some external tool or hand proof.
- michaelmior 9y ago
  Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?
  - kibwen 9y ago
    This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.
    - nickpsecurity 9y ago
      Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.
      - kibwen 9y ago
        Can you give me an example of something that safe Rust doesn't allow, thereby requiring the unsafe keyword to implement, but that also contains an error that passes the Rust compiler silently but that Frama-C or SPARK would statically detect?