Claude liefert formale Beweise für Absturzfreiheit in 123 Open-Source-Bibliotheken

Claude liefert formale Beweise für Absturzfreiheit in 123 Open-Source-Bibliotheken auf Assembler-Ebene

Das Frontier Red Team von Anthropic hat am 22. Oktober gemeinsam mit der Firma Theorem eine Arbeit veröffentlicht. Darin schreibt Claude formale Beweise für 239 Fuzz-Test-Einstiegspunkte aus Googles OSS-Fuzz-Initiative. Diese Einstiegspunkte stammen aus 123 Open-Source-Bibliotheken. Zu den Autoren gehören Keane Lucas, Nicholas Carlini und Nickolai Zeldovich.

Der Umfang beträgt rund 180 Millionen Zeilen Beweis für den Rocq-Beweisassistenten. Ein typischer Beweis hat etwa 600.000 Zeilen und bezieht sich auf eine Binärdatei mit median 18.000 RISC-V-Instruktionen. Nach Angaben der Autoren lief das Vorhaben wenige Wochen.

Beim Schreiben der Beweise habe Claude außerdem hunderte Bugs gefunden, die trotz Billionen Testläufen jahrelang unentdeckt geblieben seien. Das ist eine Angabe der Autoren. Eine genaue Zahl nennt das vorliegende Material nicht.

Die Autoren nennen die Arbeit, so wörtlich, „to our knowledge“ den ersten groß angelegten Einsatz von KI für formale Verifikation von Produktionssoftware auf Assembler-Ebene. Dabei handelt es sich um eine Selbstauskunft, die nicht unabhängig geprüft ist.

Vom Fuzz-Test zur geprüften Spezifikation: Wer was liefert

Ausgangspunkt ist ein bereits bestehender Fuzz-Test. An dessen Einstiegspunkt zählt jeder Absturz als Fehler. Dieser Code wird für RISC-V kompiliert. Zusammen mit Theorems Prozesssemantik für RISC-V und Linux sowie der Eigenschaft „kein Absturz“ ergibt sich die formale Spezifikation. Claude schreibt den Beweis, und der Rocq-Beweisprüfer prüft ihn maschinell.

Spezifikation und Eigenschaft stammen also nicht frei erfunden von Claude, sondern aus Fuzz-Test und Theorem-Semantik. Das Modell übernimmt die Beweisarbeit. Die Korrektheit sichert der Prüfer: Ein fehlerhafter Beweis würde nicht akzeptiert.

Bewiesen wird, dass das Programm bei beliebiger Eingabe unter 64 MB nicht abstürzt. Das gilt über modellierte Linux-Antworten und Speicherlayouts hinweg. Vorausgesetzt werden ein single-threaded, statisch gelinktes RISC-V-Binary mit festem Speicherbudget unter Linux. Die Autoren halten die Eigenschaft für eng gefasst, aber anspruchsvoll. Eine allgemeine Sicherheitsgarantie ist sie nicht. Andere Schwachstellenklassen, Mehrfädigkeit oder andere Laufzeitumgebungen deckt sie nicht ab.

Hunderte Bugs ohne Zahl, CVE oder Patch-Stand: Was offen bleibt

Offen bleibt, was hinter den „hunderten Bugs“ steckt. Das Material nennt keine genaue Fehlerzahl, keine Schweregrade, keine CVE-Kennungen und keinen Patch-Stand. Eine Liste betroffener Bibliotheken fehlt ebenfalls. Ob Nutzer der 123 Bibliotheken handeln müssen, lässt sich daraus nicht ableiten.

Die These der Autoren, formale Verifikation werde mit besseren Modellen ein wesentlicher Bestandteil sicherer Softwareentwicklung, ist eine Einschätzung von Anthropic. Die Arbeit belegt sie nicht. Replikationen durch Dritte und Kosten-Nutzen-Daten stehen aus.

Von der Arbeit zu trennen ist Anthropics separates Offenlegungs-Dashboard. Laut Stand 2. Oktober stehen dort 6.157 offengelegte Schwachstellen in 591 Projekten. Das Dashboard betrifft ein anderes Programm. Seine Zahlen lassen sich den 123 verifizierten Bibliotheken nicht zuordnen.