Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross
Die meisten Softwares sind voller Fehler, die KI jetzt problemlos finden und ausnutzenkann. Die gängigen Abwehrmaßnahmen gegen Cyberangriffe sind nicht mehr ausreichend: Wir brauchen Möglichkeiten zu beweisen, dass Code fehlerfrei ist. Formale Softwareverifikation könnte diese Garantie liefern, erforderte historisch jedoch jahrelange Expertenarbeit, was sie für die meisten realen Projekte unpraktikabel machte. In einer Zusammenarbeit mit Theoremzeigen wir jedoch, dass dies nicht mehr gilt: LLMs können nun formale Beweise in großem Umfang erstellen und ermöglichen so neue Softwareentwicklungs-Workflows mit bewiesenen Sicherheitsgarantien. Mit Claude haben wir Sicherheitseigenschaften auf der Ebene von Assembler-Code (RISC-V) in über 100 realen Open-Source-Softwarebibliotheken bewiesen. Nach unserem Wissen stellt dies den ersten groß angelegten Versuch dar, mit KI formale Verifikation auf Produktionssoftware auf der Ebene von Assembler-Code anzuwenden. Beim Schreiben der Beweise entdeckte Claude auch Fehler, die jahrelang der Erkennung entgangen waren, trotz Billionen von Testläufen. Da sich die Fähigkeiten der Modelle weiter verbessern, erwarten wir, dass formale Verifikation zu einem wesentlichen Bestandteil sicherer Softwareentwicklung wird.
Einführung
Selbst ausgereifte, intensiv getestete Software enthält Fehler, und LLMs werden zunehmend geschickter darin, sie zu finden. Der Linux-Kernel – eine der heute am gründlichsten getesteten Softwares, die auf Milliarden von Geräten weltweit eingesetzt wird – hatte kürzlich über 1,000 Schwachstellen offengelegt. Da Frontier-Modelle immer besser darin werden, scheinbar harmlose Fehler zu kritischen Exploits zu verketten , benötigen wir Techniken, die diese Fehler erkennen und beheben können, bevor sie in freier Wildbahn ausgenutzt werden können.
Idealerweise könnten solche Techniken alle Fehler finden und beheben und dann einen Beweis liefern, dass keine weiteren zu finden sind. Formale Verifikation ist eine Möglichkeit, dies zu tun. Bei der formalen Verifikation übersetzen Entwickler ihren Code in ein mathematisches Modell und versuchen dann zu beweisen, dass er stets einer bestimmten Menge von Sicherheitsregeln folgt. Gelingt dieser Beweis nicht, bedeutet das, dass ein Fehler im Code vorhanden sein könnte, der eine Regel verletzen würde, und die Art des Scheiterns deutet darauf hin, wie der Fehler aussehen könnte. Die Wiederholung dieses Prozesses (nach jeweils Beseitigung der Fehlerursache) führt letztlich zu einem Beweis, dass der Code frei von jedem Fehler ist, der diese Regeln verletzen würde.
Formale Verifikation ist jedoch nicht einfach. Beweise können ein Vielfaches des ursprünglichen Codes umfassen, und das Schreiben erfordert erheblichen Aufwand sowie ein seltenes, hochspezialisiertes Können. Beispielsweise brauchte die Implementierung des seL4-Betriebssystemkernels zwei Personenjahre, aber 20 Personenjahre , um ihn formal zu verifizieren. Dementsprechend war formale Verifikation bisher nur in wirklich missionkritischen Anwendungen praktikabel, wie z. B. Airbus’ Avionik-Code.
Aber LLMs machen es deutlich einfacher. Frontier-Modelle können mittlerweile Korrektheitsbeweise für reale Software vollständig autonom erstellen. Um das zu demonstrieren, baten wir Claude, nützliche Sicherheitseigenschaften über 123 Open-Source-Bibliotheken hinweg zu beweisen, darunter der Nachweis, dass einige ihrer ausführbaren Artefakte unter bestimmten Bedingungen niemals abstürzen. Konkret bewies Claude, dass diese Programme für jede Eingabe kleiner als 64 MB und jede modellierte Linux-Betriebssystemantwort (OS) und Speicherbelegung unter bestimmten Annahmen (nämlich dass das Programm als single-threaded statische Binärdatei mit festem Speicherbudget auf einer RISC-V1 CPU mit Linux OS läuft) immer normal beenden, ohne Speichersicherheitsfehler auszulösen oder fehlgeschlagene Assertions zu verursachen. Das ist noch weit davon entfernt, alle möglichen Fehler zu beheben, aber es bringt uns deutlich näher heran als zuvor und liefert eine Roadmap in diese Richtung.
Wir veröffentlichen einen Teil dieser Beweise damit jeder sie verifizieren und wiederverwenden kann, zusammen mit den RISC-V- und OS-Semantiken. Theorem, unser Kooperationspartner bei diesem Projekt, bietet außerdem an, dieselbe Pipeline für andere Open-Source-Projekteauszuführen, und veröffentlicht ein Claude-Skill um Entwicklern den Einstieg in die Verifikation ihres eigenen Codes zu erleichtern.
Formale Verifikation ist ein breites Feld mit vielen Methoden. Im Folgenden beschreiben wir auch unsere ersten Erkundungen mit anderen Methoden der formalen Verifikation, um andere Sicherheits- oder Softwareentwicklungsaufgaben zu beschleunigen, etwa die Bewertung der Sicherheit des zlib-Kompressionsalgorithmus, den Nachweis der Verhaltensäquivalenz eines in Rust geschriebenen Python-Interpreters und das Aufspüren lange bestehender Fehler in kritischer Software.
Die Zukunft der formalen Verifikation ist vielversprechend. Die Kosten für das Schreiben von Beweisen sinken, während die Modelle intelligenter werden. Zudem wird die Möglichkeit, Beweise über Codebasen hinweg wiederzuverwenden oder anzupassen, die Kosten amortisieren, wenn mehr Code formalisiert wird und die Methoden zum Erreichen von Sicherheitsgarantien standardisierter werden. Wir ermutigen alle Entwickler, formale Verifikation mit LLMs zu erkunden—insbesondere diejenigen, die es zuvor mit leistungsschwächeren Modellen versucht hatten und feststellten, dass es nicht funktionierte.
Im Rest dieses Beitrags gehen wir näher auf unsere Experimente zur formalen Verifikation ein.
Tests in Beweise umwandeln
Um zu beweisen, dass eine Software korrekt ist, müssen wir zunächst festlegen, was „korrekt“ überhaupt bedeutet. Korrektheit wird durch die Spezifikation (Spec) definiert. Bei manchen Programmen gibt es eine klare Möglichkeit, das beabsichtigte Verhalten des Programms formal zu spezifizieren. Beispielsweise nimmt ein PNG -Decoder eine Bytefolge entgegen und dekodiert diese Bytes (gemäß RFC 2083) in das entsprechende Bild. Aber bei den meisten Programmen ist es nicht so einfach. Was würde es bedeuten, dass ein Texteditor oder ein Webbrowser „korrekt“ ist? Die Schwierigkeit, eine umfassende und eindeutige Spezifikation zu erhalten, ist ein erhebliches Hindernis für die Verifikation von Software im größeren Maßstab.
Um dies für den Code in den Open-Source-Bibliotheken, die wir beweisen wollten, zu lösen, verfolgen wir den Ansatz, ihre bereits vorhandenen kompilierbaren Testsuiten automatisch in eine Spezifikation umzuwandeln, indem wir die Regel „diese Testsuite besteht immer“ kodifizieren, unter Verwendung eines allgemeinen Modells dafür, was es bedeutet, ein beliebiges RISC-V-kompiliertes Binary unter Linux auszuführen. Historisch war der Beweis solcher Spezifikationen nicht machbar, angesichts der inhärenten Komplexität, einen Beweis zu schreiben, der alle möglichen Verhaltensweisen und Interaktionen von zehntausenden Assembler-Instruktionen bei beliebigen Eingaben umfassen und darüber argumentieren kann (und der Tatsache, dass Beweise dadurch tendenziell extrem groß werden). Hier kommen die heutigen LLMs ins Spiel: Das Durcharbeiten von Millionen Codezeilen im pursuit eines klar definierten Ziels ist eine Aufgabe, für die LLMs hervorragend geeignet sind.
Für dieses Projekt begannen wir mit Fuzz-Tests. Bei diesen Tests schreiben Entwickler einen Einstiegspunkt2 in ihren Code, der Eingaben entgegennimmt, wobei jede Eingabe, die einen Absturz verursacht, ein Fehler ist, der den Autoren wichtig ist. Anschließend erzeugt der Fuzzer, eine Test-Engine, enorme Mengen halbzufälliger und mutierter Eingaben am Einstiegspunkt, um einen Fehler zu finden (visualisiert in Abbildung 1). Je länger ein Fuzzer läuft, desto mehr Fehler kann er finden. Dies ist jedoch inhärent ein Brute-Force-Prozess, ohne Garantie, dass jeder mögliche Codepfad ausgeführt wird, egal wie viele Eingaben man versucht.
Um alle Fehler zu finden, die durch einen Fuzz-Test offengelegt worden wären, haben wir den Fuzz-Test in eine Spezifikation umgewandelt, die über den kompilierten RISC-V-Instruktionen definiert ist. Die Spezifikation besagt, dass der Fuzz-Test für keine Eingabe kleiner als 64 MB abstürzt.3 Wenn Claude diese Spezifikation beweisen kann, wird der Fuzz-Test auf RISC-V überflüssig: Das Fuzzing dieses Einstiegspunkts wird niemals Fehler finden.
Wir haben dies für hunderte Projekte in Googles OSS-Fuzz Initiative getan, die kontinuierliches Fuzz-Testing für qualifizierte Open-Source-Projekte bereitstellt. OSS-Fuzz enthält tausende von Entwicklern geschriebene Einstiegspunkte, die fehlerhafte Code-Eigenschaften durch Abstürze aufdecken (zum Beispiel bei einer fehlgeschlagenen Assertion). OSS-Fuzz instrumentiert C- und C++-Programme automatisch mit AddressSanitizer4 (ASan), wodurch sie abstürzen, sobald auf Speicher unsachgemäß zugegriffen wird (was eine Hauptursache für Software-Sicherheitslückenist). Breit gefächerte Spezifikationen wie Speichersicherheit gelten für fast alle Software.
Im Zeitraum von wenigen Wochen, patchte Claude erfolgreich die von ihm gefundenen Fehler und bewies anschließend, dass es für 239 Einsprungpunkte über 123 verschiedene OSS-Fuzz-Bibliotheken hinweg bei keiner Eingabe (bis 64 MB) zu Abstürzen kommt. Diese Beweise operieren auf den kompilierten RISC-V-Instruktionen (d. h. ausführbaren Binärdateien) und umfassen etwa 180 Millionen Zeilen Rocq, wobei ein typischer Beweis etwa 600,000 Zeilen umfasst, um Sicherheitsgarantien für Binärdateien mit einer medianen Länge von 18,000 RISC-V-Instruktionen zu liefern. Diese Beweise entstehen, indem der RISC-V-Assemblecode mithilfe von Theorems RISC-V-Instruktions- und Linux-Prozess-Semantik in ein mathematisches Modell übersetzt wird. Das bedeutet, dass diese Beweise derzeit davon ausgehen, dass das Programm als single-threaded statische Binärdatei mit festem Speicherbudget auf einer RISC-V-CPU unter Linux läuft. Eine Erweiterung des Geltungsbereichs dieser Beweise ist gut erreichbar, da dies die Standardisierung von Semantiken für weitere Assemble-Architekturen und andere Betriebssystemprozesse erfordern würde. Siehe die Einschätzung eines Experten zu den von Claude geschriebenen Beweisen.
Obwohl dies ein enormes Volumen an Beweiscode ist, muss praktisch nichts davon manuell überprüft werden. Der Rocq-Proof-Checker stellt sicher, dass die Spezifikation vom Beweis korrekt erfüllt wird. Dadurch sind die einzigen Artefakte, denen ein Entwickler vertrauen muss:
- die formalen Modelle von RISC-V und von Linux-Prozessen;
- die exakten Theoremaussagen, die bewiesen wurden;
- der Rocq-Proof-Checker selbst.5
Das bedeutet nicht, dass diese Bibliotheken fehlerfrei sind. Stattdessen bedeutet es, dass alle verbleibenden Fehler entweder innerhalb der oben aufgeführten Artefakte zu finden sind oder außerhalb des Geltungsbereichs von Claudes Beweis liegen. Das Härtung dieser möglicherweise weiterhin fehlerhaften vertrauenswürdigen Komponenten (Rocq, RISC-V- und Linux-Semantik) ist nicht unerheblich, aber es ist eine weit besser handhabbare Aufgabe als das Debuggen jeder einzelnen Codezeile, die die skalierten Beweise abdecken – zumal dieser Ansatz eine beliebige Anzahl von Projekten absichern kann, ohne die Größe der vertrauenswürdigen Komponenten zu erhöhen.
Wir begrüßen eine unabhängige Überprüfung unserer Beweise und ermutigen zur Verfeinerung unseres Ansatzes. Zu diesem Zweck veröffentlichen wir die für dieses Projekt erstellten, noch nicht öffentlichen vertrauenswürdigen Komponenten (oben); Claudes vollständige Rocq-Beweise für Fuzz-Tests, die kein Patchen erforderten; sowie Spezifikationen für andere Fuzz-Tests, die wir nicht beweisen konnten.
Fehler finden und beheben
Oben haben wir gezeigt, dass man die von Entwicklern geschriebenen Tests (Fuzz-Tests) vieler Open-Source-Bibliotheken in Spezifikationen umwandeln kann, die Claude beweisen kann, dass sie immer bestehen – manchmal nach dem Patchen der verbleibenden Fehler, die es gefunden hat. Aus diesem Grund wurden beim Versuch, diese Spezifikationen zu beweisen, hunderte Fehler entdeckt.
Während Claudes Versuchen, hunderte Einsprungpunkte zu beweisen, traten zahlreiche Fehler auf. Um sicherzustellen, dass Claude nicht jedes Mal für einen Menschen anhalten musste, ließen wir Claude die von ihm gefundenen Fehler beheben: Es patchte den Code, wodurch die Spezifikation mit dem gepatchten Code neu generiert wurde, und anschließend fuhr Claude damit fort, diese neue Spezifikation zu beweisen.6
Viele der gefundenen Fehler sind solche, die ein Fuzzer wahrscheinlich nie finden würde. Fuzzer mutieren kleine Eingaben, typischerweise begrenzt auf 1 MB, und verlassen sich typischerweise auf Codeabdeckung, um sie zu Fehlern zu führen. Während Claude einen Einsprungpunkt in einer Bibliothek bewies, fand es einen Counter-Underflow in seiner Kopie eines Dekompressors, der zu einem Out-of-Bounds-Write führte, aber nur bei Eingaben von etwa 20 MB mit einem bestimmten, seltenen Layout. Weitere Fehler umfassen einen Out-of-Bounds-Read in einem Bilddecoder, der eine 64-MB-Eingabe und über 2 GB Speicher benötigte, einen Out-of-Bounds-Read in einer anderen Bibliothek, der eine bestimmte Abfolge von Aufrufen über zwei Handles auf dieselbe Datei benötigte, sowie die Wiederentdeckung von CVE-2026-56132 in libexpat, die tief verschachtelte Eingaben benötigte. Claude fand auch Logikfehler, die überhaupt nie abstürzen. Während es beispielsweise bewies, dass eine Bibliothek memory-safe ist, stellte es fest, dass eine Funktion zur Einschränkung, welche Dateien eine Anwendung laden darf, nicht immer durchgesetzt wird.
Das ultimative Ziel dieses Projekts war ein Beweis dafür, dass die nach RISC-V kompilierten Fuzz-Tests keine verbleibenden Abstürze mehr aufweisen. Fehler wie die oben genannten zeigen jedoch, dass der Prozess einen weiteren Nutzen hat, unabhängig davon, ob dieses Ziel erreicht wird: Allein der Versuch dieses Prozesses liefert echte Fehler, die behoben werden müssen.
Mehr als Speichersicherheit beweisen
Zu beweisen, dass ein Fuzz-Test keine Abstürze mehr findet, ist bedeutsamer, als es klingt. Es ist üblich, dass Fuzz-Tests in echtem Code auf Verletzungen bedeutsamer high-level Eigenschaften prüfen, wie etwa Encode-Decode-Roundtripping, Idempotenz, algebraische Gesetze, differentielles Testen, Selbstkonsistenz oder Äquivalenz zu Referenzimplementierungen. Zum Beispiel behauptet ein Fuzz-Test für den LZO-Kompressionsalgorithmus, dass, wenn man eine Eingabe komprimiert und anschließend dekomprimiert, das Ergebnis mit dem Original identisch ist. Wenn die Eigenschaft nicht gilt, stürzt das Programm ab – der Beweis, dass der Test nie abstürzt, ist also äquivalent zum Beweis der Eigenschaft selbst.
Dies kann auch auftreten, wenn die Eigenschaften nicht direkt vom Entwickler spezifiziert wurden. Damit Claude beispielsweise seinen OSS-Fuzz-Beweis für cpp-httplib abschließen konnte, war es notwendig, die Möglichkeit eines Stack-Overflows aufgrund zu großer Rekursion im std::set-Destruktor auszuschließen. Diese Rekursionstiefe ist durch die maximale Tiefe eines Baums begrenzt, sodass Claude beweisen musste (in Maschinencode!), dass der Red-Black-Tree-Rebalancing-Algorithmus von libc++ korrekt optimiert ist, um die Tiefe des Baums logarithmisch begrenzt zu halten.
Weitere Fallstudien zur formalen Verifikation
Formale Verifikation ist ein umfassendes Gebiet. Das obige Beispiel Fuzz-Test-zu-Beweis ist ein Fall, in dem LLMs die formale Verifikation durch die direkte Anwendung von Beweisen auf Maschinencode breiter nutzbar machen.
Wir haben auch Erfolg damit gehabt, LLMs in anderer Weise mit formaler Verifikation einzusetzen. Beispielsweise baten wir Claude, eine formale Spezifikation von RFC 1950, dem technischen Dokument, das das zlib-Kompressionsdateiformat definiert, zu schreiben. Anschließend ließen wir Claude beweisen, dass die zlib-Implementierung im Linux-Kernel diese Spezifikation korrekt implementiert. Wie bei den obigen Beispielen bewies Claude diese Eigenschaft auf Binärebene, nur dass Claude statt RISC-V die x86-kompilierte Binärdatei direkt bewies, und zwar unter Verwendung von Claude-generierten (und umfangreich getesteten) formalen Semantiken der x86-ISA.7 Wir wiederholten diesen Prozess dann für ein halbes Dutzend weiterer weit verbreiteter Bibliotheken. Dabei fanden wir einige kleinere (nicht ausnutzbare) Fehler in Randfällen, die derzeit upstream gemeldet werden. Aus dieser Übung ziehen wir zwei Schlüsse: (1) Diese äußerst gut getesteten Codebasen sind bereits fast vollständig korrekt, und (2) es ist möglich, End-to-End-Korrektheitseigenschaften über echte, bestehende Codebasen zu beweisen.
In einem anderen Experiment baten wir Claude, einen Interpreter für eine große Teilmenge von Python in Rust zu entwickeln und zu beweisen (unter Verwendung von Verus, einem Verifikationswerkzeug für Rust), dass er den in einer wissenschaftlichen Arbeit beschriebenen CPython-Semantiken entspricht. Anschließend maßen wir die Übereinstimmung mit CPythonVerhalten empirisch, indem wir über 1.7 Millionen zufällig generierte Python-Programme ausführten, und fanden in 99.95% der Tests identisches Verhalten mit CPython, wobei die verbleibenden Testunterschiede unscheinbare, bekannte Randfälle waren.
Wir fanden auch Probleme in mehreren weit verbreiteten und kritischen Anwendungen durch Versuche der formalen Verifikation einfacher Sicherheitseigenschaften. In einem davon entdeckten wir einen zuvor unbekannten Logikfehler, der seit mehr als einem Jahrzehnt verborgen war. Im Zuge einer Bemühung, einen weit verbreiteten PDF-Reader zu verifizieren, fanden wir in einer Woche so viele Sicherheitsfehler, wie üblicherweise in einem Jahr gemeldet werden.
Siehe das Appendix für weitere Details zu einigen dieser Bemühungen.
Dies ist erst der Anfang
Eine der wichtigsten Einschränkungen der LLM-unterstützten formalen Verifikation ist, dass die Beweise Hunderte von Millionen Token zur Erzeugung benötigen können. Kosteneffizienz ist entscheidend, wenn unser Ziel ist, diese Methoden für das gesamte Software-Ökosystem verfügbar zu machen. Glücklicherweise gibt es überzeugende Gründe zu erwarten, dass sich die Effizienz verbessern wird.
Neuere Modelle benötigen weniger Token
Wir haben 36 kleine Verifikationsaufgaben erstellt aus echtem OSS-Fuzz-Code. Opus 5.5 beweist die Hälfte davon mit etwa 40% weniger Token als Opus 5. Wir erwarten, dass sich dieser Trend fortsetzt, wenn Modelle auf langen Verifikationsaufgaben trainiert werden.
Beweise können wiederverwendet werden
Wenn Agenten separat arbeiten, duplizieren sie oft viel Aufwand. Beweise sind, wie Software, rekursiv aus kleineren Beweisen aufgebaut – und je kleiner die Beweise sind, desto wiederverwendbarer sind sie tendenziell. Um die Auswirkung davon zu messen, ließen wir Agenten die Beweise der anderen kopieren, während sie an der Beweisführung ihrer eigenen Ziele arbeiteten. Mit Zugriff auf diesen gemeinsamen Arbeitsbereich benötigten die Agenten 17% weniger Token als bei Arbeit allein, und einige Agenten waren sogar erfolgreich, nachdem sie zuvor in einem Solo-Versuch gescheitert waren.
Wir beobachteten dasselbe Phänomen in großem Maßstab während unseres OSS-Fuzz-Proof-Aufwands. Der Großteil eines Beweises betrifft Code, den jedes Programm enthält (insbesondere die Initialisierung der C-Runtime und von AddressSanitizer), sodass sehr unterschiedliche Programme am Ende deutlich überlappende Beweise haben können. Agententeams machten sich dies zunutze, indem sie den fertigen Beweis eines anderen Teams kopierten und ihn dann an ihr eigenes Programm anpassten (Abbildung 6).
Diese Wiederverwendbarkeit von Beweisen ist der Grund, warum Mathlib, eine gemeinsame Bibliothek formaler Mathematik in Lean, auf fast 300,000 Theoreme angewachsen ist, die von über 700 Beitragenden eingereicht wurden: Jeder neue Beweis baut auf dem bestehenden Korpus an Arbeit auf. Im Verlauf unseres OSS-Fuzz-Aufwands sammelten wir einen ähnlichen Korpus an Beweisen an, von denen wir einige in unsere Veröffentlichung aufnehmen (Beweise, die einen noch ungepatchten Bug in der Open-Source-Software offenbaren könnten, veröffentlichen wir nicht).
Wenn wir von diesen ersten Experimenten zu breiterem Einsatz übergehen, benötigen wir eine Strategie zur Verifizierung des enormen Bestands an bestehender Software, beginnend mit den kritischsten Abhängigkeiten. Wie wir gezeigt haben, lässt sich dies in großem Maßstab erreichen, indem man generische Specs verwendet und auf Binärebene arbeitet, wodurch die Notwendigkeit entfällt, gesamte Codebasen in eine andere Sprache umzuschreiben.
Dieser Ansatz erleichtert auch die Wiederverwendung von Beweisen auf Paketebene, was bedeutet, dass jede Abhängigkeit nur einmal verifiziert werden muss. Abhängigkeiten folgen einem Potenzgesetz: Schon das Beweisen einer kleinen Menge gemeinsam genutzter Bibliotheken macht einen großen Teil der Software beweisbar. Weitere Details finden Sie in Theorems Roadmap zur Verifizierung des gesamten Nix-Ökosystems, das kritische Infrastruktur wie glibc, OpenSSL und cURL umfasst.
Einschränkungen
In der Praxis kann die formale Verifizierung manchmal weniger über die Sicherheit des Codes beweisen, als wir uns wünschen würden.
„Formal verifiziert“ bedeutet nicht „bugfrei“. Claude kann einen Beweis schreiben, der zeigt, dass das Verhalten eines kompilierten Programms die Anforderungen einer formalen Spec erfüllt (die von einem externen Proof Checker verifiziert wird). Ein Proof Checker kann Ihnen jedoch nicht sagen, ob Ihre Spec der Realität entspricht. Um der Realität zu entsprechen, muss die Spec alles über die reale Maschine, auf der das verifizierte Programm läuft, korrekt umfassen und modellieren, einschließlich CPU und Betriebssystem. Wenn Bugs in verifiziertem Code auftauchen, liegt das daran, dass die Spec oder die angenommenen Semantiken der Maschine von der Realität abweichen. Glücklicherweise wissen wir dadurch auch, wo wir nach verbleibenden Bugs suchen müssen und wie wir ein System entwerfen können, in dem diese möglicherweise weiterhin buganfälligen Lücken minimiert werden. Im Folgenden sind die Arten aufgeführt, wie dies auf unsere Beweise zutrifft, sowie Ideen für zukünftige Arbeiten, die diese Lücken schließen würden.
Die reale Maschine tut etwas, das das Modell nicht beschreibt. Unsere Beweise beziehen sich auf single-threaded, statische RISC-V-Binärdateien, die gegen musl libc gelinkt sind. Die meisten Menschen führen diese Bibliotheken jedoch auf x86 oder ARM aus und linken sie dynamisch gegen glibc. Um diese Lücke zu schließen, bräuchten wir Systemmodelle, die eingesetzten Systemen stärker ähneln. Ein Schritt in diese Richtung wäre beispielsweise die Erzeugung präziser Semantiken für x86.
Die Aussage deckt möglicherweise nicht alles ab, was uns wichtig ist. Wir haben bewiesen, dass für jede Eingabe unter 64 MB an vielen Fuzzing-Einstiegspunkten in Google OSS-Fuzz, einschließlich ASan-Abstürzen, nie ein Crash auftritt. ASan erkennt jedoch nicht alle Memory-Safety-Bugs, und wir haben nicht alle Einstiegspunkte jeder Bibliothek verifiziert. Selbst wenn wir das getan hätten, würde die gesamte Bibliothek nicht durch die Verifizierung aller Einstiegspunkte abgedeckt (insbesondere wenn es toten Code gibt). Zusätzlich könnten echte Programme die Bibliothek falsch verwenden, was zu Speicherkorruption im Aufruferführt. Um diese Lücke zu schließen, müssten wir festlegen, was Aufrufer für jede öffentliche Funktion tun müssen, und die Aufrufer müssten sich strikt daran halten.
Wir erwarten, dass diese Einschränkungen handhabbar werden, wenn wir mehr über den Einsatz von LLMs für formale Methoden lernen und sich die Modelle weiter verbessern, und dass wir dann einen viel größeren Prozentsatz des Codes verifizieren können, auf den wir uns verlassen.
Fazit
Die Entwicklung ist klar: Formale Verifizierung, die historisch gesehen nur für maßgeschneiderte, von Experten erstellte Garantien im sicherheitskritischsten Code praktikabel war, wird bald für fast alle Produktionssoftware genauso praktikabel sein wie Fuzzing heute. Genau wie statische Typen, Testing-Frameworks und andere Korrektheits-Werkzeuge wird sich die Verifizierung von „aufgesetzt“ zu „eingebaut“ weiterentwickeln – angetrieben nicht nur von LLMs, sondern auch von Innovationen im Sprachdesign und in Entwicklungs-Workflows.
In der heutigen Welt – in der LLMs automatisch nach Code-Sicherheitslücken suchen und immer mehr davon finden – müssen wir Prozesse verwenden, die Code-Sicherheitseigenschaften garantieren können. LLM-skalierte formale Verifizierung ist ein vielversprechender Ansatz, um diese Garantien in einem Umfang und Maßstab zu sichern, der zuvor unerreichbar war. Wir ermutigen andere, damit zu experimentieren, damit wir gemeinsam eine Welt aufbauen können, in der sich robuste Software sehr weit verbreitet hat und Software-Bugs eine gut verstandene und schnell behebbare Seltenheit sind.
Lesen Sie den vollständigen Anhang.
Fußnoten
01RISC-V ist ein Prozessordesign, wie x86 oder ARM, das die Assembler-Instruktionen (die grundlegenden Befehle, die ein Chip ausführt) definiert, in die Software kompiliert wird.
02Ein Einprungspunkt (Entry Point) ist eine Vordertür in den Code, die von dessen Autoren zum Testen bereitgestellt wird. Jede Eingabe an den Einprungspunkt, die einen Absturz verursacht, ist ein Fehler, der den Autoren wichtig ist.
03Dies zu erhöhen erfordert nur minimale menschliche Mühe, um den Parameter zu ändern und die Spezifikation neu zu generieren, und dann Claude die Aussage erneut beweisen zu lassen.
04AddressSanitizer ist ein Compiler-Werkzeug, das einem Programm Prüfungen hinzufügt, sodass Speicherfehler wie Pufferüberläufe und Use-After-Free in dem Moment, in dem sie zur Laufzeit auftreten, erkannt und gemeldet werden.
05Technisch gesehen bedeutet das auch, dass wir der Hardware, dem Betriebssystem und dem OCaml-Compiler vertrauen müssen, auf die der Rocq-Proof-Checker angewiesen ist.
06Beachte, dass dies Tür und Tor für Reward Hacking offenlässt. Reward Hacking liegt vor, wenn ein KI-Modell einen Abkürzungsweg findet, der das gesteckte Ziel technisch erfüllt, ohne das tatsächlich Beabsichtigte zu tun – wie ein Student, der eine Prüfung besteht, indem er den Lösungsschlüssel auswendig lernt, statt den Stoff zu lernen. In diesem Kontext könnte Claude jeden Theorem beweisbar machen, indem er das Programm in eines umschreibt, das trivialerweise nie abstürzt. Um dies zu verhindern, bewerteten wir jeden Patch negativ und boten Zusatzpunkte dafür an, zu beweisen, welche Eingaben er ändert und wie wenige es sind. Wir protokollierten und prüften die Patches außerdem auf diese Fehlermodi.
07Wir sind der Ansicht, dass die Fähigkeit von Claude – vollständig autonom – die formale Semantik einer ISA zu generieren, eine eigenständige interessante Lektion darstellt. Zwar können wir nicht sicher sein, dass unsere Semantik selbst perfekt ist, doch empirisch haben wir festgestellt, dass das single-stepping durch unsere Semantik einen Ubuntu-Userspace auf einem Linux-Kernel booten kann. Die Generierung dieser Semantik deckte zudem Hunderte von Fehlern in der offiziellen Referenzdokumentation sowie eine kleinere Anzahl von Bugs in der Hardware selbst auf.