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

Der Informatiker Dr. Ralf Jung ©Timo Mann

Alle Fotos anzeigen

Ralf Jung, Doktorand der Universität des Saarlandes und Forscher am Max-Planck-Institut für Softwaresysteme in Saarbrücken, hat einen maßgeblichen Beitrag zur Sicherheit der Programmiersprache ‚Rust‘ geleistet. Die neue und zunehmend beliebte Programmiersprache wird sowohl von kleinen Startups als auch von den größten Technologie-Konzernen der Welt für die Entwicklung von Betriebssystemen, Webbrowsern und anderen sicherheitskritischen Anwendungen eingesetzt. 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 ‚Doctoral 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 Doctoral 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 mit dem 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
jung@mpi-sws.org
+49 (681) 9303 8717

Prof. Dr. Derek Dreyer
dreyer@mpi-sws.org
+49 (681) 9303 8701

 

Hintergrund Saarland Informatics Campus:

800 Wissenschaftlerinnen und Wissenschaftler und rund 2100 Studierende aus mehr als 80 Nationen machen den Saarland Informatics Campus (SIC) zu einem der führenden Standorte für Informatik in Deutschland und Europa. Fünf weltweit angesehene Forschungsinstitute, nämlich das Deutsche Forschungszentrum für Künstliche Intelligenz (DFKI), das Max-Planck-Institut für Informatik, das Max-Planck-Institut für Softwaresysteme, das Zentrum für Bioinformatik und das Cluster für „Multimodal Computing and Interaction“ sowie die Universität des Saarlandes mit drei vernetzten Fachbereichen und 24 Studiengänge decken das gesamte Themenspektrum der Informatik ab.

 

Redaktion:
Philipp Zapf-Schramm
Kompetenzzentrum Informatik Saarland
Saarland Informatics Campus
Telefon: +49 681 302-70741
E-Mail: pzapf@mmci.uni-saarland.de