Anthropic lässt Claude für 123 Open-Source-Biblio­theken rund 180 Millionen Zeilen Kor­rekt­heits­be­weise erzeugen und findet dabei Hunderte Fehler

Anthropics Frontier Red Team hat gemeinsam mit dem Partner Theorem Claude Kor­rekt­heits­be­weise für 239 Einstiegspunkte aus 123 Open-Source-Bibliotheken schreiben lassen, veröffentlicht am 22. Oktober. Die Bibliotheken stammen aus OSS-Fuzz, einer Initiative von Google, die geeignete Open-Source-Projekte laufend mit Fuzz-Tests prüft. Für jeden dieser Einstiegspunkte ist bewiesen: Das kompilierte Programm endet bei jeder Eingabe unter 64 MB regulär, ohne Speicherfehler und ohne verletzte Zusicherung. Der Beweiscode umfasst rund 180 Millionen Zeilen für Rocq, einen Beweisprüfer, der maschinell kontrolliert, ob ein Beweis seine Vorgabe erfüllt. Auf dem Weg dorthin stieß Claude auf Hunderte Fehler, darunter solche, die trotz Billionen Testläufen jahrelang unentdeckt geblieben waren. Nach Angaben von Anthropic hat Claude sie selbst behoben, bevor der jeweilige Beweis gelang.

Aus dem Fuzz-Test wird die Vorgabe

Ein Beweis braucht eine Vorgabe dafür, was korrekt heißt, und an dieser Stelle scheitert formale Verifikation meist schon vor dem ersten Schritt. Für einen Bilddecoder lässt sich das aufschreiben, für einen Texteditor oder einen Browser kaum. Das Team hat die Frage umgangen und die Fuzz-Tests genommen, die die Entwickler der Bibliotheken ohnehin geschrieben hatten. Ein solcher Test öffnet einen Einstiegspunkt in den Code, ein Fuzzer schickt dort Unmengen halbzufälliger Eingaben hinein, und jeder Absturz gilt als Fehler, der den Autoren wichtig ist. Speicherfehler macht dabei AddressSanitizer sichtbar, ein Werkzeug, das ein Programm abstürzen lässt, sobald es Speicher falsch anspricht. Ein Fuzzer findet umso mehr, je länger er läuft, vollständig wird seine Suche nie. Aus dem Test wurde deshalb eine Vorgabe über die kompilierten Maschinenbefehle für Prozessoren der Bauart RISC-V: Der Test stürzt bei keiner Eingabe unter 64 MB ab. Gelingt der Beweis, kann Fuzzing an diesem Einstiegspunkt auf RISC-V nichts mehr finden.

Seit seL4 eine Rechnung in Personenjahren

Bisher galt formale Verifikation als Arbeit für wenige Spezialisten, die sich nur bei Code lohnt, von dem viel abhängt. Den Maßstab nennt Anthropic selbst: Den Betriebs­sys­tem­kern seL4 zu schreiben kostete zwei Personenjahre, ihn formal zu verifizieren 20. Beweise werden oft um ein Vielfaches länger als der Code, den sie absichern. So blieb das Verfahren auf Fälle wie die Bordsoftware von Airbus beschränkt, und für eine Bibliothek, die Bilder dekodiert oder Daten packt, kam es nicht in Frage.

Jetzt hat Claude über wenige Wochen eigenständig gearbeitet. Ein typischer Beweis umfasst etwa sechs­hun­dert­tau­send Zeilen und sichert ein Programm ab, das im Median achtzehntausend Maschinenbefehle lang ist. Diese Menge liest kein Mensch, und das muss auch keiner: Rocq prüft, ob der Beweis die Vorgabe erfüllt. Vertrauen muss ein Entwickler drei Bausteinen: den formalen Modellen von RISC-V und von Linux-Prozessen, die Theorem gebaut hat, dem genauen Wortlaut der bewiesenen Sätze und dem Beweisprüfer selbst. Diese Grundlage wächst mit der Zahl der Projekte nicht mit. Wer sie härtet, härtet sie für jede Bibliothek zugleich, und das ist nach Anthropic eine weit kleinere Aufgabe, als jede Zeile der abgesicherten Programme zu prüfen. Damit wandern die Kosten von den Personenjahren je Projekt zu einer gemeinsamen Grundlage, die man einmal prüft.

Geprüft wird, worauf viele Programme bauen

Anthropic begründet die Arbeit mit einer Verschiebung auf der Seite der Angreifer. Sprachmodelle finden Fehler im Code inzwischen leicht und können sie ausnutzen, und die üblichen Abwehrmittel reichen dafür nach Anthropic nicht mehr aus. Ein Fuzzer sucht Fehler einzeln. Ein Beweis zeigt für eine ganze Fehlerklasse, dass es an einem Einstiegspunkt keinen Vertreter mehr gibt. Im Mittelpunkt stehen Speicherfehler, die Anthropic zu den führenden Ursachen von Sicherheitslücken zählt.

Den Nutzen hat, wer eine dieser Bibliotheken einbindet. Ein Bilddecoder oder ein Kompressor steckt in vielen Programmen, und nach Anthropic muss jede Abhängigkeit nur einmal verifiziert werden. Dazu kommt die Verteilung der Abhängigkeiten: Wenige gemeinsam genutzte Bibliotheken stehen unter einem großen Teil aller Software. Der Partner Theorem beschreibt deshalb, wie sich die ganze Paketsammlung Nix verifizieren ließe, samt grundlegender Bausteine wie glibc, OpenSSL und cURL. Er bietet außerdem an, dieselbe Pipeline für weitere Open-Source-Projekte zu fahren.

Zwei Bedingungen bleiben. Die meisten Anwender betreiben diese Bibliotheken auf x86 oder ARM, und glibc kommt dort erst beim Programmstart hinzu. Bewiesen ist das Verhalten statisch gebundener Programme auf RISC-V. Und ruft ein Programm die Bibliothek falsch auf, kann es den Speicher trotzdem beschädigen. Dagegen hilft erst eine Festlegung je öffentlicher Funktion, an die sich jeder Aufrufer hält.

Ein Beweis kann außerdem mehr sichern als den Speicher. Viele Fuzz-Tests brechen ab, sobald eine fachliche Eigenschaft verletzt ist. Der Test für das Kom­pres­si­ons­ver­fahren LZO etwa verlangt, dass gepackte und wieder entpackte Daten dem Original gleichen. Wer beweist, dass dieser Test nie abstürzt, hat die Eigenschaft selbst bewiesen.

Auch wo ein Beweis scheitert, bleibt ein Ertrag: die Fehler, die Claude auf dem Weg gefunden hat. Darunter sind solche, die ein Fuzzer kaum trifft, denn er arbeitet meist mit Eingaben bis etwa 1 MB. Einen Schreibzugriff außerhalb des Puffers in einem Dekompressor löste erst eine Eingabe von rund 20 MB mit einem seltenen Aufbau aus.

Ein Thread, ein statisches Programm, ein RISC-V-Prozessor

Naheliegend wäre der Schluss, 123 Bibliotheken seien nun nachweislich sicher. Der Beweis gilt aber unter Annahmen, die Anthropic selbst aufzählt: Das Programm läuft mit einem einzigen Thread, statisch gebunden, mit festem Speicherbudget, auf einem RISC-V-Prozessor unter Linux. Bewiesen ist das Verhalten der Maschinenbefehle für diese Architektur, wo dieselben Bibliotheken übersetzt für andere Prozessoren laufen, reicht er nicht hin. Die Vorgabe beschreibt außerdem genau das, was der Fuzz-Test prüft: Absturz, Speicherfehler, verletzte Zusicherung. Was ein Test dieser Art nicht erfasst, erfasst auch der Beweis nicht. Anthropic schreibt, das Vorhaben sei noch weit davon entfernt, alle möglichen Fehler zu beheben. Verbleibende Fehler liegen nach dieser Darstellung in den drei vertrauten Bausteinen oder außerhalb dessen, was der Beweis abdeckt. Weitere Architekturen und Teile des Betriebssystems hält das Team für erreichbar, sie müssten dafür einheitlich formal beschrieben werden.

Hunderte Fehler aus einer Quelle

Wie schwer die gefundenen Fehler wogen und ob Claudes Korrekturen in den Projekten angekommen sind, ist offen. Versucht hat das Team die Beweise bei Hunderten Projekten aus OSS-Fuzz, gelungen sind sie für 239 Einstiegspunkte, und wie viele scheiterten, beziffert der Bericht nicht. Alle Angaben stammen von Anthropic, das die Arbeit selbst durchgeführt hat und die eingesetzten Modelle anbietet. Zur Gegenprobe veröffentlicht das Unternehmen einen Teil der Beweise, die noch nicht öffentlichen vertrauten Bausteine und die Vorgaben für jene Fuzz-Tests, deren Beweis nicht gelang.

Die Kosten in Token sinken, gemessen an 36 Aufgaben

Die wichtigste Grenze nennt Anthropic selbst: Ein Beweis kann Hunderte Millionen Token verbrauchen. Für die Breite der Software müsste das deutlich billiger werden, und zwei Messungen im Bericht sprechen dafür. An 36 kleinen Aufgaben aus dem Code von OSS-Fuzz bewies Opus 5.5 die Hälfte mit rund 40 Prozent weniger Token als Opus 5. Durften Agenten die Beweise der anderen übernehmen, brauchten sie 17 Prozent weniger Token als allein. In 30 von 34 fertigen Beweisen lag der gemeinsame Weg unter dem Schnitt der Einzelarbeit.

Im großen Lauf über OSS-Fuzz geschah dasselbe ohne Vorgabe. Den Großteil eines Beweises macht Code aus, den jedes Programm enthält, etwa der Start der C-Laufzeit und AddressSanitizer. Agenten übernahmen deshalb fertige Beweise anderer Teams und passten sie an.

Gemessen ist das an Modellen von Anthropic und an Aufgaben, die Anthropic selbst gebaut hat. Weiter reicht der Ausblick: Anthropic erwartet, dass der Trend anhält, und rechnet damit, dass formale Verifikation für fast jede Produktivsoftware bald so praktikabel wird wie Fuzzing heute. Eine Messung zu diesem Satz enthält der Bericht nicht.