Verständnis und Weiterentwicklung der Programmiersprache Rust

Abstract

Rust ist eine junge systemnahe Programmiersprache. Sie vereint die Sicherheit und das Abstraktionsniveau von Sprachen wie Java und Haskell mit der Kontrolle von Systemressourcen, wie C und C++ sie bieten. Meine Dissertation [Ju20a] untersucht die Sicherheitsgarantien von Rust erstmals formell und trägt somit entscheidend zum besseren Verständnis und zur Entwicklung dieser zunehmend bedeutsamen Sprache bei. Dafür habe ich drei Systeme entwickelt und im Beweisassistenten Coq verifiziert: RustBelt, Iris, und Stacked Borrows. RustBelt ist ein formelles Modell des Typsystems von Rust einschließlich eines Korrektheitsbeweises, welcher die Sicherheit von Speicherzugriffen und Nebenläufigkeit zeigt. RustBelt ist in der Lage, einige komplexe Komponenten der Standardbibliothek von Rust zu verifizieren, obwohl die Implementierung dieser Komponenten intern unsichere Sprachkonstrukte verwendet. RustBelt ist nur möglich dank der Entwicklung von Iris, einem Framework zur Konstruktion von Separationslogiken zur Programmverifikation von beliebigen Programmiersprachen. Die Stärke von Iris liegt in der Mo ̈glichkeit, neue Beweismethoden mit Hilfe weniger einfacher Bausteine herzuleiten. Stacked Borrows ist eine Erweiterung der Spezifikation von Rust, die es dem Compiler erlaubt, den Quelltext mit Hilfe der im Typsystem kodierten Alias-Informationen besser zu analysieren. So werden neue mächtige intraprozedurale Optimierungen ermöglicht.