Eine formale Methode zum Kompilieren von C in sicheres Rust

• Kompilieren von C in sicheres Rust

• Die Popularität von Rust steigt rasant, aber viele wichtige Codebasen sind immer noch in C geschrieben, und es ist nicht realistisch, diese manuell neu zu schreiben. Daher erscheint die automatische Übersetzung von C nach Rust als attraktive Alternative.

• Mehrere bestehende Arbeiten nutzen zunehmend verschiedene Funktionen von Rust (z. B. unsafe), um immer größere Teile von C abzudecken. Obwohl die Aussicht auf vollständige Automatisierung attraktiv ist, wird die Speichersicherheitsgarantie von Rust außer Kraft gesetzt, wenn Code erzeugt wird, der von unsafe abhängt; damit geht der Hauptvorteil verloren, eine bestehende Codebasis in eine speichersichere Sprache zu portieren.

• Wir erforschen einen anderen Weg: die Übersetzung von C in sicheres Rust, also die Erzeugung von Code, der das Rust-Typsystem einhält und damit Speichersicherheit einfach garantieren kann.

• Unsere Forschung umfasst mehrere neuartige Beiträge:

  • Typorientierte Übersetzung von Teilen von C nach sicherem Rust
  • Eine neue statische Analyse auf Basis eines "Split-Tree", mit der sich C-Pointerarithmetik mithilfe von Rust-Slices und Slice-Operationen ausdrücken lässt
  • Eine Analyse, die exakt ableitet, welche Borrowings mutabel sein müssen
  • Eine Kompilierungsstrategie für C-Strukturtypen, die mit der Unterscheidung zwischen non-owning- und owning-Zuweisung in Rust kompatibel ist

• Wir wenden diese Methodik auf formal verifizierte C-Codebasen an: die Kryptobibliothek HACL* sowie den Binär-Parser und den Serializer von EverParse. Wir zeigen, dass die unterstützte Teilmenge von C ausreicht, um beide Anwendungen in sicheres Rust zu übersetzen.

• Die Auswertung zeigt, dass bei einigen Verstößen gegen die Aliasing-Regeln von Rust eine automatisierte, gezielte Umformung ausreicht; der Einfluss der eingefügten strategischen Kopien auf die Performance ist gering.

• Insbesondere bei der Anwendung auf HACL* führte unser Ansatz dazu, dass eine verifizierte Kryptobibliothek mit 80.000 Zeilen, die moderne Algorithmen implementiert, vollständig in reinem Rust geschrieben wurde. Dies ist der erste Fall dieser Art.

[GN⁺]

Hacker News Kommentar

• Beim Portieren von Projekten auf Rust habe ich ein paar Schlussfolgerungen gezogen

  • Die Umwandlung eines C-Programms nach Rust findet Fehler schnell, weil Rusts strenge Beschränkungen greifen
  • Eine automatische Migration von C nach Rust ist kein vollständig gelöstes Problem, da die beiden Sprachen grundlegend unterschiedlich entworfen sind
  • In manchen Fällen kann ein Porting von C nach Rust unmöglich sein, da die Unsicherheit im Design selbst angelegt ist
  • Verbesserte Werkzeuge werden den Portierungsprozess weiter vereinfachen

• Eine formell verifizierte C-Codebasis unterscheidet sich von einer typischen System-C-Codebasis

• 2002 veröffentlichten Forscher einen Beitrag über Cyclone, einen sicheren C-Dialekt, und fanden dabei bei der Portierung von C nach Cyclone Sicherheitsfehler

  • Solche manuelle oder automatisierte Konvertierungen können die Einführung sicherer Sprachen fördern und bestehende Fehler aufdecken

• Eine einfache Übersetzung nach Rust kann sichere und unsichere Teile erzeugen; manuelle Arbeit kann sich darauf konzentrieren, die Sicherheit der unsicheren Bereiche zu prüfen

  • Auch wenn der unsichere Teil groß ist, kann es Vorteile geben

• Ich habe wenig Hoffnung auf den Ansatz, nur einen kleinen Teil von C zu kompilieren

  • weil Rusts Ownership-Modell zu stark von realen C-Programmen abweicht

• Neugier auf den Vergleich mit Zigs C-Umwandlungsfunktion

  • Zig erzeugt eine gute Mischung aus neuem und bestehendem C-Code und kann auch als C-Compiler verwendet werden
  • Warum ziehen Linux-Kernel-Maintainer Zig nicht als Alternative zu C in Betracht?

• Frage, ob C2Rust formal korrekten Code erzeugen kann

  • Es fehlt ein Link zum Quellcode, aus dem der Rust-Code erzeugt wurde

• Wenn eine C-Bibliothek funktioniert, kann es sinnvoll sein, sie mit Rusts unsafe zu migrieren

  • Rust hat im Allgemeinen zu wenige Bibliotheken

• Interessanterweise hat eine hohe Optimierungsstufe die Geschwindigkeit von Rust nicht wesentlich verbessert

  • Ich bin neugierig, wie gut eine direkte Übersetzung von C nach Rust auf dem Optimierungslevel O3 funktioniert