Doctoral thesis on RustBelt awarded several times Type safety put to the test in Rust
The programming language Rust should be particularly secure. In his dissertation, doctoral student Ralf Jung verified the type safety and improved the possibilities of generating unsafe code if necessary with his tool “Miri”.
Companies on the topic
Ralf Jung PhD student at Saarland University and researcher at the Max Planck Institute for Software Systems in Saarbrücken.
(Picture: MPI-INF)
Ralf Jung is a doctoral student at Saarland University and a researcher at the Max Planck Institute for Software Systems in Saarbrücken. Since 2015, he has been working on the Rust programming language, which was originally designed by Mozilla.
The programming language is exciting for him, because there is a very tempting promise behind it, Jung reports: “To be a programming language that allows the most precise control over the memory use and resource distribution of a system, while at the same time it automatically prevents many widespread programming errors.“
In his dissertation “Understanding and Evolving the Rust Programming Language”, Ralf Jung provides the first formal proof that Rust fulfills its safety promises: “We were able to verify the so-called type safety and thus show how Rust automatically and reliably prevents entire classes of programming errors.“
With type security, Rust doesn’t allow everything the programmer wants to do, Jung explains. “Sometimes, however, it is necessary to write a process into the program that Rust would not actually accept due to its type security,” says the computer scientist. If the programmer wants to circumvent the security precautions, he can mark his as therefore “unsafe”.
“Together with an international team, my doctoral supervisor Derek Dreyer and I have developed a theoretical framework that will allow us to prove that Rust’s security promises stand up despite the possibility of writing ‘unsafe’ code, ” Jung reports. The computer scientist has added a tool called Miri to this proof with the name RustBelt.
Miri automatically tests Rust code marked as “unsafe” for compliance with important rules of the Rust specification. “While RustBelt was a great success, especially in academic terms, Miri is already established in the industry as a tool for safety tests of programs written in Rust,” explains Ralf Jung.
Ralf Jung received national and international awards for his dissertation. Thus, his work received one of two” Honorable Mentions “for the” Dissertation Award ” of the Association for Computing Machinery (ACM). Jung has also received the” Doctoral Dissertation Award ” of the European Joint Conferences on Theory & Practice of Software (ETAPS), an award in the field of software science in Europe. The Max Planck Society has also awarded him the Otto Hahn Medal for outstanding scientific achievements.
(ID: 47524923)
