The new and increasingly popular programming language Rust is widely used, from small startups to the world's largest technology corporations, to develop operating systems, web browsers, and other security-critical applications. For his doctoral thesis, in which Jung laid the first formal foundations for programming secure systems in Rust, he has already received several internationally renowned awards.

Ralf Jung is a postdoctoral researcher in Professor Derek Dreyer's "Fundamentals of Programming" research group at the Max Planck Institute for Software Systems in Saarbrücken. Since 2015, Jung has focused on the programming language that was originally sponsored by Mozilla: "Rust excited me because it has a very tempting future: being a programming language that allows precise control over memory usage and resource allocation in a system, while automatically avoiding many common programming errors," says Ralf Jung.

The weight of this promise is demonstrated by the programming language's practical use: Although the first stable version of Rust wasn't released until 2015, the language is already used by many large technology companies such as Microsoft, Google, Amazon, Dropbox, and Facebook. In his doctoral thesis, Ralf Jung now provides the first formal proof that Rust's safety promises are actually fulfilled.

"We have been able to verify the safety of Rust's type system and thus show how Rust automatically and reliably avoids entire classes of programming errors," says Ralf Jung. In doing so, he also successfully addressed a special aspect of the programming language: "So-called 'type safety' goes hand in hand with the fact that Rust imposes restrictions on the programmer and doesn't allow everything they want to do. However, sometimes it's necessary to write an operation in the code that Rust wouldn't accept due to 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 security precautions. Together with international collaborators, including my thesis advisor Derek Dreyer, we developed a theoretical framework that allows us to demonstrate that Rust’s security claims hold true despite the possibility of writing ‘unsafe’ code,” says Jung.

This test, called RustBelt, is complemented by a tool called Miri, which can automatically verify that ‘unsafe’ Rust code complies with important rules of the Rust specification—a basic requirement for the correctness and security of this code. “While RustBelt has been very successful, especially in academic circles, Miri is already established in the industry as a tool for testing the security of programs written in Rust,” explains Ralf Jung.

For his dissertation entitled “Understanding and Evolution of the Rust Programming Language,” Ralf Jung has received several national and international awards. Jung's work received one of two Honorable Mentions in the Association for Computing Machinery (ACM) Dissertation Award. The ACM states: "Through Jung's leadership and active involvement with the Rust Unsafe Code Guidelines working group, his work has already had a profound impact on Rust's design and laid essential groundwork for its future." The ACM Dissertation Award is announced internationally for the entire field of computer science and is considered one of the most prestigious awards for computer science dissertations worldwide. He

has also received the Doctoral Dissertation Award from the European Joint Conferences on Theory & Practice of Software (ETAPS), one of the most important awards in the field of software science in Europe. He has also received the Otto Hahn Medal from the Max Planck Society, which is awarded annually for particularly outstanding scientific achievements related to a dissertation.

More information