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.
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.
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.
Editor:
Philipp Zapf-Schramm
Competence Center Computer Science
Saarland Informatics Campus
Phone: +49 681 302-70741
E-Mail: pzapf@mmci.uni-saarland.de
Dr. Ralf Jung
jung@mpi-sws.org
+49 (681) 9303 8717
Prof. Dr. Derek Dreyer
dreyer@mpi-sws.org
+49 (681) 9303 8701
The dissertation entitled 'Understanding and Evolving the Rust Programming Language' can be found at https://people.mpi-sws.org/~jung/thesis.html.
https://awards.acm.org/doctoral-dissertation
https://etaps.org/2021/doctoral-dissertation-award
https://www.mpg.de/preise/otto-hahn-medaille
Ralf Jung, Ralf Jung is a postdoctoral researcher at the Max Planck Institute for Software Systems
Timo Mann
MPI-SWS
Professor Derek Dreyer, research group leader at the Max Planck Institute for Software Systems
Bertram Somieski
MPI-SWS
Criteria of this press release:
Business and commerce, Journalists, Scientists and scholars
Information technology, Mechanical engineering
transregional, national
Research results, Scientific Publications
English
You can combine search terms with and, or and/or not, e.g. Philo not logy.
You can use brackets to separate combinations from each other, e.g. (Philo not logy) or (Psycho and logy).
Coherent groups of words will be located as complete phrases if you put them into quotation marks, e.g. “Federal Republic of Germany”.
You can also use the advanced search without entering search terms. It will then follow the criteria you have selected (e.g. country or subject area).
If you have not selected any criteria in a given category, the entire category will be searched (e.g. all subject areas or all countries).