Formale Verifikation durch Übersetzung der `core`- und `alloc`-Crates von Rust nach Coq

 (formal.land)
1 Punkte von GN⁺ 2024-05-16 | 1 Kommentare | Auf WhatsApp teilen

Übersetzung der core- und alloc-Crates von Rust

Erster Lauf 🐥

  • Mit coq-of-rust wurden die alloc- und core-Crates von Rust erstmals übersetzt, wobei zwei Coq-Dateien mit jeweils mehreren hunderttausend Zeilen Code erzeugt wurden.
  • Das zeigt, dass das Tool auch bei großen Codebasen funktioniert, aber der erzeugte Coq-Code kompiliert nicht. Fehler treten nur selten auf, etwa einmal alle paar tausend Zeilen.

Größe des eingegebenen Rust-Codes (gemäß dem Befehl cloc)

  • alloc: 26.299 Zeilen Rust-Code

  • core: 54.192 Zeilen Rust-Code

  • Da Makros expandiert und dann übersetzt werden müssen, ist die tatsächlich zu übersetzende Größe noch größer.

Aufteilung des erzeugten Codes 🪓

  • Die wichtigste Änderung bestand darin, die von coq-of-rust erzeugte Ausgabe in jeweils eine Datei pro eingegebener Rust-Datei aufzuteilen.
  • Das ist möglich, weil die Übersetzung unabhängig von der Reihenfolge der Definitionen erfolgen kann. Zyklische Abhängigkeiten zwischen Rust-Dateien sind in Coq zwar verboten, die Aufteilung ist aber trotzdem möglich.

Umfang der Ausgabe

  • alloc: 54 Coq-Dateien, 171.783 Zeilen Coq-Code
  • core: 190 Coq-Dateien, 592.065 Zeilen Coq-Code

Vorteile der Code-Aufteilung

  • Der erzeugte Code lässt sich leichter lesen und durchsuchen
  • Er lässt sich einfacher kompilieren, da parallel kompiliert werden kann
  • Debugging ist einfacher, da man sich auf eine Datei konzentrieren kann
  • Nicht kompilierbare Dateien lassen sich leichter ignorieren
  • Änderungen an einzelnen Dateien lassen sich leichter nachverfolgen, was die Wartung vereinfacht

Einige Bugfixes 🐞

  • Es gab einen Bug durch Kollisionen zwischen Modulnamen. Dieser trat bei der Wahl des Modulnamens für impl-Blöcke auf.
  • Um die Eindeutigkeit zu erhöhen, wurden mehr Informationen in den Modulnamen aufgenommen, zum Beispiel where-Klauseln.

Beispiel

  • Implementierung des Typs Mapping für das Trait Default:

    #[derive(Default)]
struct Mapping<K, V> {
  // ...
}

  • Vorheriger Coq-Code:

    Module Impl_core_default_Default_for_dns_Mapping_K_V.
(* ...trait implementation ... *)
End Impl_core_default_Default_for_dns_Mapping_K_V.

  • Überarbeiteter Coq-Code:

    Module Impl_core_default_Default_where_core_default_Default_K_where_core_default_Default_V_for_dns_Mapping_K_V.
(* ... *)

Liste der nicht kompilierbaren Dateien

  • alloc/boxed.v

  • core/any.v

  • core/array/mod.v

  • core/cmp/bytewise.v

  • core/error.v

  • core/escape.v

  • core/iter/adapters/flatten.v

  • core/net/ip_addr.v

  • Das entspricht 4 % aller Dateien. Auch in Dateien, die kompilieren, können noch nicht behandelte Rust-Konstrukte vorkommen.

Beispiele 🔎

Quellcode der Methode unwrap_or_default des Typs Option

pub fn unwrap_or_default(self) -> T
where
  T: Default,
{
  match self {
    Some(x) => x,
    None => T::default(),
  }
}

Übersetzter Coq-Code

Definition unwrap_or_default (T : Ty.t) (τ : list Ty.t) (α : list Value.t) : M :=
  let Self : Ty.t := Self T in
  match τ, α with
  | [], [ self ] =>
    ltac:(M.monadic
      (let self := M.alloc (| self |) in
      M.read (|
        M.match_operator (|
          self,
          [
            fun γ =>
              ltac:(M.monadic
                (let γ0_0 :=
                  M.get_struct_tuple_field_or_break_match (|
                    γ,
                    "core::option::Option::Some",
                    0
                  |) in
                let x := M.copy (| γ0_0 |) in
                x));
            fun γ =>
              ltac:(M.monadic
                (M.alloc (|
                  M.call_closure (|
                    M.get_trait_method (| "core::default::Default", T, [], "default", [] |),
                    []
                  |)
                |)))
          ]
        |)
      |)))
  | _, _ => M.impossible
  end.

Vereinfachter Funktionscode

Definition unwrap_or_default {T : Set}
  {_ : core.simulations.default.Default.Trait T}
  (self : Self T) :
  T :=
  match self with
  | None => core.simulations.default.Default.default (Self := T)
  | Some x => x
  end.
  • Diese vereinfachte Definition wird bei der Codeverifikation verwendet. Der Gleichheitsbeweis befindet sich in CoqOfRust/core/proofs/option.v.

Fazit

  • Durch die Formalisierung der Standardbibliothek wird die Verifikationsarbeit für Rust-Programme vertrauenswürdig.

  • Das nächste Ziel besteht weiterhin darin, den noch umständlichen Beweisprozess zu vereinfachen. Insbesondere sollen Schritte wie Namensauflösung, Einführung fortgeschrittener Typen und Entfernung von Seiteneffekten bei der Darstellung der Gleichwertigkeit zur ursprünglichen Rust-Implementierung getrennt werden.

  • Wer sich für die formale Verifikation von Rust-Projekten interessiert, kann sich unter contact@formal.land melden. Formale Verifikation bietet das höchste Sicherheitsniveau, indem mathematisch garantiert wird, dass bezogen auf eine gegebene Spezifikation keine Bugs vorhanden sind.

Tags:

  • coq-of-rust
  • Rust
  • Coq
  • Übersetzung
  • core
  • alloc

Meinung von GN⁺

  1. Integration von Rust und Coq: Die Integration von Rust und Coq kann erheblich dazu beitragen, die Stabilität von Rust-Programmen zu erhöhen. Die Kombination aus der Sicherheit von Rust und der formalen Verifikation von Coq ist besonders für kritische Anwendungen sehr nützlich.
  2. Bedeutung der Automatisierung: Die automatische Übersetzung mit dem Tool coq-of-rust ist zuverlässiger als manuelle Arbeit. Dennoch ist Vorsicht geboten, da im Verifikationsprozess weiterhin Fehler auftreten können.
  3. Umgang mit komplexen Codebasen: Bei großen Codebasen hilft die Aufteilung des Codes enorm bei Wartung und Debugging. Das ist besonders in Teamumgebungen ein wichtiger Faktor.
  4. Notwendigkeit formaler Verifikation: Formale Verifikation ist besonders in kritischen Bereichen wie Finanzen, Medizin und Luftfahrt unverzichtbar. Die Kombination aus Rust und Coq kann in solchen Bereichen großen Mehrwert bieten.
  5. Aspekte bei der Einführung neuer Technologien: Bei der Einführung neuer Technologien sollten die Lernkurve und die Kompatibilität mit bestehenden Systemen berücksichtigt werden. Werkzeuge zur formalen Verifikation wie Coq können eine steile Lernkurve haben und erfordern daher ausreichende Schulung und Vorbereitung.

Verwandte Beiträge

1 Kommentare

 
GN⁺ 2024-05-16
Hacker-News-Kommentar

Zusammenfassung der Hacker-News-Kommentare

  • Zuverlässigkeit automatischer Übersetzungswerkzeuge

    • Automatische Übersetzungswerkzeuge gewinnen an Vertrauen. coq-of-rust wurde in Rust geschrieben und kann in Coq übersetzt werden, um seine Korrektheit zu beweisen. Das ähnelt einem Ansatz zur Abwehr von Ken Thompsons Angriff.

  • Programmgröße und Verifikation

    • Die Größe von Programmen, die mit halbautomatischen Beweissystemen wie Coq verifiziert wurden, ist klein. Die Kosten für eine 100%ige Garantie können zehnmal höher sein als die für eine 99,9999%ige Garantie.

  • Fehlermöglichkeiten im Übersetzungsprozess

    • Es ist wahrscheinlich, dass beim Übersetzen von Code nach Coq Fehler entstehen. Dadurch wird die Gültigkeit der Verifikation des Originalcodes infrage gestellt.

  • Beiträge mit Bezug zu Kryptowährungen

    • Es wurde ein Blogbeitrag mit wenig Bezug zu Kryptowährungen eingereicht. Es gibt auch einen Beitrag über einen ähnlichen Ansatz für Python.

  • Grenzen formaler Verifikation

    • Jemand erinnert sich daran, dass selbst in einem formal verifizierten C-Compiler Bugs gefunden wurden. Das wirft Fragen zur Vertrauenswürdigkeit von Coq selbst und der Übersetzung auf.

  • Formale Verifikation von Rust

    • Es wird gefragt, ob eine formal verifizierte Rust-Standardbibliothek bedeuten würde, dass man formale Garantien für die Speicherbehandlung erhält, solange kein unsafe verwendet wird.

  • Schreiben formaler Verifikationsspezifikationen

    • Es wird gefragt, ob das Schreiben formaler Verifikationsspezifikationen dem Schreiben komplexerer Property-Tests ähnelt. Property-Tests zu schreiben ist schwierig und zeitaufwendig.

  • Vergleich mit anderen Ansätzen

    • Es wird um einen Vergleich mit Ansätzen wie Aeneas oder RustHornBelt gebeten. Insbesondere interessiert, wie Pointer und veränderliche Borrows behandelt werden.

  • Rust-Einführung im Kernel

    • Es wird gefragt, ob solche Bemühungen die Einführung von Rust im Kernel beschleunigen könnten.

  • Ergänzung eines Rust-Backends für F*

    • Es wird gefragt, wie viel Arbeit nötig wäre, um F* um ein Rust-Backend zu erweitern.