Saarbrücken Computer Scientist proves safety claims of the programming language Rust

Bild der Pressemitteilung

Computer Scientist Ralf Jung ©Timo Mann


View all images

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 ‘Doctoral 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 Doctoral 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

All Images

Professor Derek Dreyer ©Bertram Somieski Professor Derek Dreyer ©Bertram Somieski
Informatiker Ralf Jung ©Timo Mann Informatiker Ralf Jung ©Timo Mann


Die Öffentlichkeitsarbeit am Saarland Informatics Campus wird unterstützt durch das Kompetenzzentrum Informatik Saarland, gefördert aus Mitteln des Europäischen Fonds für regionale Entwicklung (EFRE) und Mitteln der Staatskanzlei Saarland.

Logo Europäischer Fonds für regionale Entwicklung
Logo Staatskanzlei Saarland