runtimeverification/kernel-c-to-rust-spikeHärtung von Kernel-C-Parsern durch Rust-Umschreibung + differentielles Fuzzing + formale Verifikation. Erstes Ziel: UVC (CVE-2024-53104).
Kann ein sicherheitskritischer C-Parser im Linux-Kernel gehärtet werden, indem man ihn in Rust neu schreibt, wobei nachgewiesen wird, dass der Neuentwurf äquivalent zum Original ist, und er anschließend formal verifiziert wird? Dieser Spike durchläuft die vollständige Schleife an einem Ziel: dem UVC-Video-Deskriptor-Parser (uvc_parse_format/uvc_parse_frame aus drivers/media/usb/uvc/, v7.2-rc2), ausgewählt, weil er zwei unabhängige Speichersicherheits-CVEs mit sechzehn Jahren Abstand aufwies (CVE-2008-3496, CVE-2024-53104, letztere im CISA-KEV-Katalog).
Das C-Blatt extrahieren (c/). Die Parsing-Logik byte-genau aus dem Kernel kopiert; nur die Umgebung gestubbt (// SPIKE-STUB). Kompiliert zu einer C-ABI-Bibliothek. Das extrahierte Blatt enthält den Zähl-Durchlauf und die größenbasierte Allokation, sodass die Fehlerklasse von CVE-2024-53104 (Parsen schreibt über das hinaus, was die Zählung allokiert hat) erreichbar ist und nicht wegabstrahiert wurde.
In Rust neu schreiben (rust/). Dasselbe Parsing-Blatt in sicherem Rust, gleiche C-ABI und Ergebnisstruktur. Jede Abweichung vom C ist mit // DEVIATION markiert und dokumentiert.
Differentielles Fuzzing (fuzz/). Ein LibAFL-Harness auf stabilem rustc treibt beide Implementierungen mit einer Eingabe an und vergleicht die Ausgaben feldweise. Ergebnis: Nach Behebung einer Portierungsabweichung an einer compilerabhängigen Stelle mit vorzeichenbehaftetem Überlauf null Divergenzen über 54.019 Ausführungen bei 93 % Kantenabdeckung. Im originalgetreuen v7.2-rc2-Code ist kein Out-of-Bounds-Zugriff erreichbar (beide CVEs sind gepatcht). Eine optionale Negativkontrolle (--features vuln, in beiden Sprachen gespiegelt) führt die CVE-2024-53104-Abweichung wieder ein: Bei derselben Eingabe führt das C einen Heap-Out-of-Bounds-Schreibzugriff aus (ASan), das Rust gerät sicher in eine Panik. Details: fuzz/RESULTS.md.
Formale Verifikation (verify/). Das originalgetreue Rust-Blatt extrahiert über Charon und Aeneas nach Lean 4 ohne sorry im generierten Code und ohne Union-Blocker (anders als beim Binder-Spike). Zwei Theoreme, in verify/VERIFY-REPORT.md und ROADMAP.md:
ok / kontrolliertes fail / Nichtterminierung, niemals ein Ergebnis mit undefiniertem Verhalten): bewiesen, sorry-frei. Dies macht die Speichersicherheitseigenschaft, die dem C fehlt, als geprüfte Aussage explizit.sorry-frei bewiesen, zusammen mit zwei wiederverwendbaren Aeneas-Schleifenbeweisprinzipien und Div-Freiheit für die 5 strukturell terminierenden Schleifen. Der Rest reduziert sich auf einen benannten funktionalen Korrektheitskern für den Positionsdurchlauf (vier formulierte Lemmata); siehe ROADMAP.md.Die Schleife ist an einem Ziel durchgängig demonstriert. Der Neuentwurf ist durch differentielles Fuzzing als äquivalent zum C nachgewiesen; der Speichersicherheitsunterschied wird durch die Negativkontrolle konkret gemacht; das Rust extrahiert sauber nach Lean und seine Totale-Sicherheit-Eigenschaft ist maschinell geprüft. Für das Keine-Panik-Theorem ist die Zähl-Invariante (der Kern von CVE-2024-53104) sorry-frei bewiesen und die verbleibende Arbeit auf einen benannten funktionalen Korrektheitskern reduziert, der formuliert, aber noch nicht bewiesen ist. Der vollständige Beweisstatus und die offenen Lemmata stehen in ROADMAP.md.
c/ — das extrahierte C-Blatt und seine Stubsrust/ — der Neuentwurf in sicherem Rustfuzz/ — der differentielle LibAFL-Fuzzer, Ergebnisse und CVE-Klassen-Kontrolleverify/ — Charon/Aeneas/Lean-Extraktion und TheoremeROADMAP.md — Beweisstatus und die verbleibenden offenen LemmataOPEN_CHALLENGES.md — konkrete Aufgaben, die ein Beitragender übernehmen kann*/README.md, fuzz/RESULTS.md, verify/VERIFY-REPORT.md — Details pro PhaseKernel v7.2-rc2 (schreibgeschützte Referenz). Rust stable 1.94.0. LibAFL 0.15. Charon 909ff09a (v0.1.220, --preset=aeneas), Aeneas c2015b86, Lean/mathlib v4.31.0.