Informatiker beweist Sicherheit der Programmiersprache Rust – und wird international preisgekrönt

Für seine Doktorarbeit, in der Jung den ersten formalen Beweis für die Sicherheit von Rust liefert, hat er nun mehrere international renommierte Preise erhalten.

Der promovierte Informatiker Ralf Jung forscht als Postdoctoral Researcher in Professor Derek Dreyers Forschungsgruppe ‚Foundations of Programming‘ am Saarbrücker Max-Planck-Institut für Softwaresysteme. Dort befasst er sich bereits seit 2015 schwerpunktmäßig mit der ursprünglich aus dem Hause Mozilla stammenden Programmiersprache: „Rust war für mich spannend, da ein sehr verlockendes Versprechen dahintersteckt: Eine Programmiersprache zu sein, die genauste Kontrolle über die Speichernutzung und Ressourcenverteilung eines Systems ermöglicht, während sie gleichzeitig viele weit verbreitete Programmierfehler automatisch verhindert“, sagt Ralf Jung.

Wie schwer allein dieses Versprechen wiegt, zeigt der Einsatz der Programmiersprache in der Praxis: Obwohl eine erste stabile Version von Rust erst 2015 veröffentlicht wurde, findet die Programmiersprache schon jetzt Einsatz bei vielen großen Tech-Konzernen wie Microsoft, Google, Amazon, Dropbox und Facebook. In seiner Dissertation liefert Ralf Jung nun den ersten formalen Beweis dafür, dass die Sicherheitsversprechen von Rust wirklich zutreffend sind.

„Wir konnten die sogenannte Typsicherheit verifizieren und damit zeigen, wie Rust automatisch und zuverlässig ganze Klassen von Programmierfehlern verhindert“, sagt der Informatiker. Dabei ist es ihm gelungen, ein besonderes Alleinstellungsmerkmal der Programmiersprache aufzugreifen: „Mit der Typsicherheit geht einher, dass Rust dem Programmierer Restriktionen setzt und nicht alles, was der Programmierer tun möchte, zulässt. Manchmal ist es aber nötig, einen Vorgang ins Programm zu schreiben, den Rust aufgrund seiner Typsicherheit eigentlich nicht akzeptieren würde“, so der Informatiker weiter. „Hier greift dann eine Besonderheit von Rust: Programmierer können ihren Code als ‚unsicher‘ markieren, wenn sie etwas erreichen wollen, das den Sicherheitsvorkehrungen der Programmiersprache widerspricht. Zusammen mit einem internationalen Team haben mein Doktorvater Derek Dreyer und ich einen theoretischen Rahmen entwickelt, mit dem wir beweisen können, dass die Sicherheitsversprechen von Rust trotz der Möglichkeit ‚unsicheren‘ Code zu schreiben, standhalten“, sagt Jung.

Diesen Beweis mit dem Namen RustBelt ergänzt Ralf Jung um ein Tool namens Miri , mit dem ‚unsicherer‘ Rust-Code vollautomatisch auf die Einhaltung wichtiger Regeln der Rust-Spezifikation getestet werden kann – eine Grundvoraussetzung für Korrektheit und Sicherheit dieses Codes. „Während RustBelt vor allem in akademischer Hinsicht ein großer Erfolg war, ist Miri bereits in der Industrie als Werkzeug für Sicherheitstests von in Rust geschriebenen Programmen etabliert“ erläutert Ralf Jung.

Für seine Dissertation unter dem Titel ‚Understanding and Evolving the Rust Programming Language‘ wurde Ralf Jung mehrfach national und international ausgezeichnet. So erhielt Jungs Arbeit eine von zwei ‚Honorable Mentions‘ für den ‚Dissertation Award‘ der ‚Association for Computing Machinery‘ (ACM). In der Begründung heißt es: „Durch Jungs führende Rolle und sein aktives Engagement in der ‚Rust Unsafe Code Guidelines' Arbeitsgruppe hat seine Arbeit bereits tiefgreifende Auswirkungen auf das Design von Rust und wesentliche Grundlagen für die Zukunft der Programmiersprache gelegt.“ Der „ACM Dissertation Award“ wird weltweit für das gesamte Feld der Informatik ausgeschrieben und gilt als eine der international renommiertesten Auszeichnungen für Dissertationen im Bereich der Informatik.

Außerdem hat er den ‚Doctoral Dissertation Award‘ der ‚European Joint Conferences on Theory & Practice of Software‘ (ETAPS) erhalten, eine der wichtigsten Auszeichnungen im Bereich der Software-Wissenschaft in Europa. Zudem ist er Preisträger der Otto-Hahn-Medaille der Max-Planck-Gesellschaft, mit der jährlich besonders herausragende wissenschaftliche Leistungen, die im Zusammenhang mit einer Dissertation erbracht wurden, ausgezeichnet werden.

Originalpublikation:

Die Dissertation Titel ‚Understanding and Evolving the Rust Programming Language‘ ist zu finden unter https://people.mpi-sws.org/~jung/thesis.html

Weitere Informationen:

https://awards.acm.org/doctoral-dissertation

 

https://etaps.org/2021/doctoral-dissertation-award

https://www.mpg.de/preise/otto-hahn-medaille

Fragen beantworten:

Dr. Ralf Jung
Mail:  jung(at)mpi-sws.org
+49 (681) 9303 8717

Prof. Dr. Derek Dreyer
Mail: dreyer(at)mpi-sws.org

+49 (681) 9303 8701