New Study Verifies Safety of Rust

Slashdot reader Beeftopia writes:

Rust has two modes: its default, safe mode, and an unsafe mode. In its default, safe mode, Rust prevents memory errors, such as “use-after-free” errors. It also prevents “data races” which is unsynchronized access to shared memory. In its unsafe mode (via use of the “unsafe” block), in which some of its APIs are written, it allows the use of potentially unsafe C-style features. The key challenge in verifying Rust’s safety claims is accounting for the interaction between its safe and unsafe code. This article from April’s issue of Communications of the ACM provides an overview of Rust and investigates its safety claims.
The article is co-authored by Ralf Jung, a prominent postdoctoral researcher in the ‘Foundations of Programming’ research group at the Max Planck Institute for Software Systems. And (spoiler alert) Jung has just received one of two ‘Honorable Mentions’ for the ‘Dissertation Award’ of the ‘Association for Computing Machinery’ (ACM), reports a nonprofit site operated by the American Association for the Advancement of Science:In his dissertation, Ralf Jung now provides the first formal proof that the safety promises of Rust actually hold. “We were able to verify the safety of Rust’s type system and thus show how Rust automatically and reliably prevents entire classes of programming errors,” says Ralf Jung.

In doing so, he also successfully addressed a special aspect of the programming language: “The so-called ‘type safety’ goes hand in hand with the fact that Rust imposes restrictions on the programmer and does not allow everything that the programmer wants to do. Sometimes, however, it is necessary to write an operation into the code that Rust would not accept because of its type safety,” the computer scientist continues. “This is where a special feature of Rust comes into play: programmers can mark their code as ‘unsafe’ if they want to achieve something that contradicts the programming language’s safety precautions. Together with international collaborators, including my thesis advisor Derek Dreyer, we developed a theoretical framework that allows us to prove that Rust’s safety claims hold despite the possibility of writing ‘unsafe’ code,” Jung says.

This proof, called RustBelt, is complemented by Ralf Jung with a tool called Miri, with which ‘unsafe’ Rust code can be automatically tested for compliance with important rules of the Rust specification - a basic requirement for correctness and safety of this code. “While RustBelt was a great success, especially in academic circles, Miri is already established in industry as a tool for security testing of programs written in Rust,” explains Ralf Jung… The ACM states: “Through Jung’s leadership and active engagement with the Rust Unsafe Code Guidelines working group, his work has already had profound impact on the design of Rust and laid essential foundations for its future.”