Computer Scientist proves safety claims of the programming language Rust

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.

###

Original Publication:

The dissertation entitled ‘Understanding and Evolving the Rust Programming Language’ can be found at

https:/

/

people.

mpi-sws.

org/

~jung/

thesis.

html

.

Further Information:

https:/

/

awards.

acm.

org/

doctoral-dissertation


https:/

/

etaps.

org/

2021/

doctoral-dissertation-award


https:/

/

www.

mpg.

de/

preise/

otto-hahn-medaille

Questions can be directed at:

Dr. Ralf Jung


jung@mpi-sws.org


+49 (681) 9303 8717

Prof. Dr. Derek Dreyer


dreyer@mpi-sws.org


+49 (681) 9303 8701

Background Saarland Informatics Campus:

800 scientists and about 2100 students from more than 80 nations make the Saarland Informatics Campus (SIC) one of the leading locations for computer science in Germany and Europe. Five world-renowned research institutes, namely the German Research Center for Artificial Intelligence (DFKI), the Max Planck Institute for Computer Science, the Max Planck Institute for Software Systems, the Center for Bioinformatics and the Cluster for “Multimodal Computing and Interaction” as well as Saarland University with three departments and 24 degree programs cover the entire spectrum of computer science.

Editor:

Philipp Zapf-Schramm

Competence Center Computer Science

Saarland Informatics Campus

Phone: +49 681 302-70741

E-Mail:

pzapf@mmci.uni-saarland.de

Public relations work at the Saarland Informatics Campus is supported by the Competence Center Computer Science Saarland, funded by the European Regional Development Fund (ERDF) and the Saarland State Chancellery.