For those who don’t know, 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 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 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.
Ralf Jung now provides the first formal proof that the safety promises of Rust actually hold.
"We can verify the safety of Rust's type system and thus show how Rust automatically and reliably prevents entire classes of programming errors", said Ralf Jung.
In doing so, he successfully addressed a special aspect of the programming language 'type safety' which works 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 said.
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", explained 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."
