@@ -60,13 +60,13 @@ Prof. Dr. Christoph Kreitz, Universität Potsdam\\[1\baselineskip]
# Überblick
Die Programmiersprache Rust \cite{rustlang22} bietet seinen Usern durch Ownership und Borrowing ein System, mit dem Race Conditions und Memory Corruption statisch erkannt werden können, da der Borrowchecker außerhalb von sogenannten \lstinline{unsafe}-Blöcken nicht zulässt, dass es zu einem Zeitpunkt mehrere Aliase mit Schreibzugriff auf eine Ressource gibt. Laut einer Analyse von Microsoft \cite{thomas19} lassen sich etwa 70 Prozent der in ihren Produkten vorkommenden Bugs auf solche Fehler zurückführen, die mit safe Rust nicht auftreten können.
Die Programmiersprache Rust \cite{klabnik19} bietet seinen Usern durch Ownership und Borrowing ein System, mit dem Race Conditions und Memory Corruption statisch erkannt werden können, da der Borrowchecker außerhalb von sogenannten \lstinline{unsafe}-Blöcken nicht zulässt, dass es zu einem Zeitpunkt mehrere Aliase mit Schreibzugriff auf eine Ressource gibt. Laut einer Analyse von Microsoft \cite{thomas19} lassen sich etwa 70 Prozent der in ihren Produkten vorkommenden Bugs auf solche Fehler zurückführen, die mit safe Rust nicht auftreten können.
Allerdings schützt Rusts Typsystem nicht vor anderen Fehlern, insbesondere kann man mit ihm nur grobe Spezifikationen ausdrücken. Einige Programmiersprachen wie Lean \cite{lean22} nutzen Dependent Types und Beweisobjekte, um präzise Aussagen über Code machen zu können, haben jedoch den Nachteil, dass nicht alle dieser Aussagen automatisch bewiesen werden können. Außerdem wird das Typsystem dadurch deutlich komplexer.
Allerdings schützt Rusts Typsystem nicht vor anderen Fehlern, insbesondere kann man mit ihm nur grobe Spezifikationen ausdrücken. Einige Programmiersprachen wie Lean \cite{moura15} nutzen Dependent Types und Beweisobjekte, um präzise Aussagen über Code machen zu können, haben jedoch den Nachteil, dass nicht alle dieser Aussagen automatisch bewiesen werden können. Außerdem wird das Typsystem dadurch deutlich komplexer.
Einen Mittelweg kann man mit sogenannten Refinement Types gehen. Bei ihnen werden Typen mit gewissen Bedingungen eingeschränkt, die von einem SMT-Solver wie Z3 \cite{z322} teilweise automatisch gelöst werden können. Ein User kann dadurch mit überschaubarem zusätzlichen Aufwand mehr Sicherheiten über den eigenen Code gewinnen.
Einen Mittelweg kann man mit sogenannten Refinement Types gehen. Bei ihnen werden Typen mit gewissen Bedingungen eingeschränkt, die von einem SMT-Solver wie Z3 \cite{moura08} teilweise automatisch gelöst werden können. Ein User kann dadurch mit überschaubarem zusätzlichen Aufwand mehr Sicherheiten über den eigenen Code gewinnen.
Refinement Types wurden bereits in verschiedenen Sprachen implementiert, zum Beispiel LiquidHaskell \cite{liquid22} als Erweiterung für die Sprache Haskell \cite{haskell22} oder ATS \cite{ats22}, bei dem Refinement Types builtin sind.
Refinement Types wurden bereits in verschiedenen Sprachen implementiert, zum Beispiel LiquidHaskell \cite{moura08} als Erweiterung für die Sprache Haskell \cite{haskell22} oder ATS \cite{xi10}, bei dem Refinement Types builtin sind.
Bisher findet die Forschung hauptsächlich an funktionalen Programmiersprachen statt, obwohl die Mehrheit der Anwendungen in einem imperativen Stil geschrieben wird. Rust ist eine imperative Programmiersprache, hat aber Einflüsse aus funktionalen Sprachen. Deshalb bietet es sich an, Rust um Refinement Types zu erweitern. Zusammen mit dem schon vorhandenen Typsystem erhält man eine ausdrucksstarke Spezifikationssprache, die sehr viele Anwendungsfälle abdeckt.
...
...
@@ -85,7 +85,7 @@ Es gibt mehrere Projekte, Rust eine formale Semantik zu geben: Oxide \cite{weiss
## Verifikation von Rust
Es gibt schon einige Ansätze zur formalen Verifikation von Rust-Code. Das Projekt RustBelt \cite{rustbelt22} versucht, die \lstinline{unsafe}-Teile der Standardbibliothek von Rust formal zu verifizieren.
Es gibt schon einige Ansätze zur formalen Verifikation von Rust-Code. Das Projekt RustBelt \cite{jung17rustbelt} versucht, die \lstinline{unsafe}-Teile der Standardbibliothek von Rust formal zu verifizieren.
Das Crate *refinement* \cite{refinement22} implementiert Refinement Types, eine Überprüfung findet allerdings nur zur Laufzeit statt und es gibt einen gewissen Overhead für User, die selbst Casts durchführen und dabei auftretende Fehler zur Laufzeit behandeln müssen.
...
...
@@ -107,7 +107,7 @@ Daher soll aufbauend auf einer der vorhandenen formalen Semantiken für Rusts Ow
Das Forschungsvorhaben lässt sich in drei Teile aufgliedern, die jeweils verschiedene Methoden erfordern:
Zu Beginn des Vorhabens möchte ich untersuchen, wie sich Refinement Types in eine formale Semantik für Rust einbinden lassen. Dazu vergleiche ich verschiedene bereits vorhandene Semantiken für Rust \cite{reed15, kan20, weiss21} nach ihrer Komplexität und Erweiterbarkeit, um eine der Semantiken als Grundlage für meine Arbeit auszuwählen. Dann möchte ich eine Formalisierung von Refinement Types \cite[siehe][]{rondon08,vekris16, kooi21} finden, die sich gut in die ausgewählte Semantik einpflegen lässt, und die Korrektheit der Semantik beweisen.
Zu Beginn des Vorhabens möchte ich untersuchen, wie sich Refinement Types in eine formale Semantik für Rust einbinden lassen. Dazu vergleiche ich verschiedene bereits vorhandene Semantiken für Rust \cite{reed15, kan20, weiss21} nach ihrer Komplexität und Erweiterbarkeit, um eine der Semantiken als Grundlage für meine Arbeit auszuwählen. Dann möchte ich eine Formalisierung von Refinement Types \cite[siehe][]{rondon08,vekris2016refinement, kooi21} finden, die sich gut in die ausgewählte Semantik einpflegen lässt, und die Korrektheit der Semantik beweisen.
Der zweite Teil beschäftigt sich mit der Implementation eines Systems, *Verdigris*, das Refinement Types für Rust umsetzt. Da Compiler-Plugins anscheinend deprecated werden sollen,^[Siehe \href{https://github.com/rust-lang/rust/pull/64675}{diesen Pull Request} und \href{https://github.com/rust-lang/rust/issues/29597}{dieses Issue}.] nutze ich vermutlich prozedurale Macros. Das System könnte auch als installierbares Subcommand für Cargo angeboten werden wie Clippy \cite{clippy22} und Expand \cite{expand22}.
