Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2017 · Proceedings of the ACM on Programming Languages
Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust's safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.
Metadata: Crossref. Abstracts retain their original authors’ rights.
Original HN comments, with labels from simple text rules. A label describes the whole comment and may miss context or irony. Read the discussion to make up your own mind. About the labels
3 selected excerpts · 3 total mentions
The closest thing is probably RustBelt [0], which proved the soundness of a subset of Rust that included borrowing/lifetimes. This was later extended to include relaxed memory accesses [1]. Neither of these papers include the trait system, unfortunately, and I'm not aware of another line of research that does (yet?). [0]: https://dl.acm.org/doi/10.1145/3158154 [1]: https://plv.mpi-sws.org/rustbelt/rbrlx/paper.pdf
Second problem: sandbox aren't perfect either. It's indeed useful, as part of a defense-in-depth approach, but it's far from sufficient. Memory safety could solve the problem altogether, but then again no program is 100% memory safe, there's always some kind of primitive that uses memory-unsafe code under the hood, so it's not perfect either. The “perfect” solution would probably be: - use memory safe languages - all primitives using memory unsafe stuff should get formally verified Rust is kind of aiming at this (with things like [1] and [2]), but it's not there yet. [1]: https://dl.acm.org/doi/pdf/10.1145/3158154 [2]: https://github.com/rust-secure-code/safety-dance
According to the RustBelt paper [0]: > so long as the only unsafe code in a well-typed λRust program is confined to libraries that satisfy their verification conditions, the program is safe to execute. I think the main caveat is that IIRC, the RustBelt unsafe rules do not cover ALL uses of unsafe in the wild, they analyze only a subset of Rust as whole, and of course, unsafe usage actually has to obey the rules. But I'm hardly an expert here. That bug report basically says they broke the unsafe rules and thus the guarantee no longer holds (and there is UB). [0] https://dl.acm.org/doi/abs/10.1145/3158154
More from the same topics.
Haoran Xu, Fredrik Kjolstad
Fast compilation is important when compilation occurs at runtime, such as query compilers in modern database systems and WebAssembly virtual machines in modern browsers.
Ross Mcilroy, Jaroslav Sevcik, Tobias Tebbi +2
The recent discovery of the Spectre and Meltdown attacks represents a watershed moment not just for the field of Computer Security, but also of Programming Languages.
Daniel Ingalls
This paper presents a personal view of the evolution of six generations of Smalltalk in which the author played a part, starting with Smalltalk-72 and progressing through Smalltalk-80 to Squeak and Etoys.
Donald E. Knuth