Doktorarbeit zu RustBelt mehrfach ausgezeichnet Typsicherheit in Rust auf den Prüfstand gestellt

Die Programmiersprache Rust soll besonders sicher sein. In seiner Dissertation hat Doktorand Ralf Jung die Typsicherheit verifiziert und mit seinem Tool „Miri“ die Möglichkeiten verbessert, bei Bedarf auch unsicheren Code zu erzeugen.

Ralf Jung ist Doktorand der Universität des Saarlandes und Forscher am Max-Planck-Institut für Softwaresysteme in Saarbrücken. Dort befasst er sich bereits seit 2015 mit der ursprünglich von Mozilla konstruierten Programmiersprache Rust.

Die Programmiersprache sei für ihn spannend, weil ein sehr verlockendes Versprechen dahinterstecke, berichtet Jung: „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.“

In seiner Dissertation „Understanding and Evolving the Rust Programming Language“ liefert Ralf Jung den ersten formalen Beweis dafür, dass Rust seine Sicherheitsversprechen einhält: „Wir konnten die sogenannte Typsicherheit verifizieren und damit zeigen, wie Rust automatisch und zuverlässig ganze Klassen von Programmierfehlern verhindert.“

Mit der Typsicherheit geht einher, dass Rust nicht alles zulässt, was der Programmierer tun möchte, erläutert Jung. „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. Will der Programmierer die Sicherheitsvorkehrungen umgehen, kann er seinen als deshalb als „unsicher“ markieren.

„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“, berichtet Jung. Diesen Beweis mit dem Namen RustBelt hat der Informatiker um ein Tool namens Miri ergänzt.

Miri testet als „unsicher“ gekennzeichneten Rust-Code automatisch auf die Einhaltung wichtiger Regeln der Rust-Spezifikation. „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 wurde Ralf Jung national und international ausgezeichnet. So erhielt seine Arbeit eine von zwei „Honorable Mentions“ für den „Dissertation Award“ der Association for Computing Machinery (ACM). Außerdem hat Jung den „Doctoral Dissertation Award“ der European Joint Conferences on Theory & Practice of Software (ETAPS) erhalten, eine Auszeichnung im Bereich der Software-Wissenschaft in Europa. Zudem hat ihn die Max-Planck-Gesellschaft mit der Otto-Hahn-Medaille für herausragende wissenschaftliche Leistungen bedacht.

(ID:47524923)