Ralf Jung, a doctoral student of Saarland University and now postdoc at the Max Planck Institute for Software Systems in Saarbrücken, has made a significant contribution to the safety of the 'Rust' programming language.
The new and increasingly popular programming language is widely used from small startups to the world's largest technology corporations to develop operating systems, web browsers and other safety-critical applications. For his doctoral thesis, in which Jung established the first formal foundations for safe systems programming in Rust, he has now received several internationally renowned awards.
Ralf Jung is a postdoctoral researcher in Professor Derek Dreyer's 'Foundations of Programming' research group at the Max Planck Institute for Software Systems in Saarbrücken. Since 2015 Jung has been focusing on the programming language which was originally sponsored by Mozilla: "Rust was exciting for me because there is a very tempting promise behind it: to be a programming language that enables precise control over a system's memory usage and resource allocation, while at the same time automatically preventing many widespread programming errors," says Ralf Jung.
The weight of this promise alone is shown by the use of the programming language in practice: Although a first stable version of Rust was only released in 2015, the programming language is already being used by many large tech corporations such as Microsoft, Google, Amazon, Dropbox and Facebook. 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.
For his dissertation entitled 'Understanding and Evolving the Rust Programming Language'. Ralf Jung has received several national and international awards. Jung's work received one of two 'Honorable Mentions' for the 'Dissertation Award' of the 'Association for Computing Machinery' (ACM). 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.” The ACM Dissertation Award is advertised internationally for the entire field of computer science and is thus considered to be one of the most prestigious awards for computer science dissertations worldwide.
He has also received the 'Doctoral Dissertation Award' of 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 is also a recipient of the Otto Hahn Medal of the Max Planck Society, which is awarded annually for particularly outstanding scientific achievements made in connection with a dissertation.
www.uni-dsaarland.de
