Anthropic: Claude weist Sicherheitseigenschaften in 123 Bibliotheken nach

Anthropic veröffentlichte Forschungsergebnisse am 22. Oktober 2026. Darin berichtete das Unternehmen, dass Claude in Zusammenarbeit mit Theorem maschinell überprüfte formale Beweise für Sicherheitseigenschaften auf Ebene des RISC-V-Assembliercodes erstellt habe – für 239 Einstiegspunkte von Fuzzing-Tests in 123 Open-Source-Bibliotheken.

Anthropic zufolge behob Claude die gefundenen Fehler und bewies anschließend, dass die Programme bei jeder Eingabe unter 64 MB sowie bei jeder modellierten Reaktion des Linux-Betriebssystems und jeder Speicherbelegung stets regulär beendet werden, ohne Fehler der Speichersicherheit auszulösen oder Assertions scheitern zu lassen. Die Beweise setzen voraus, dass das Programm als statische Binärdatei mit einem einzelnen Thread und einem festen Speicherbudget auf einer RISC-V-CPU mit Linux ausgeführt wird. Anthropic erklärte, die Beweise umfassten rund 180 Millionen Zeilen Rocq; ein typischer Beweis erstrecke sich über rund 600.000 Zeilen und decke Binärdateien mit einer medianen Länge von 18.000 RISC-V-Instruktionen ab. Nach Kenntnis des Unternehmens handelt es sich um den ersten groß angelegten Versuch, KI für die formale Verifikation von Produktionssoftware auf Assembliercode-Ebene einzusetzen.

Ein Teil der Beweise sowie die zugrunde liegende RISC-V- und Betriebssystemsemantik wird auf GitHub veröffentlicht. Anthropic erklärte außerdem, die für das Projekt entwickelten, bislang nicht öffentlichen vertrauenswürdigen Komponenten freizugeben, ebenso vollständige Beweise für Fuzzing-Tests, bei denen keine Änderungen nötig waren, und Spezifikationen für Fuzzing-Tests, deren Beweise nicht erbracht werden konnten. Beweise, die einen nicht behobenen Fehler offenlegen könnten, würden hingegen zurückgehalten.

Fuzzing-Tests in formale Beweise umwandeln

Bei diesem Ansatz wird der vorhandene, kompilierbare Fuzzing-Test jeder Bibliothek in eine formale Spezifikation umgewandelt, die eine Regel festlegt: Der Test stürzt bei keiner Eingabe unter 64 MB ab. Die Spezifikation bezieht sich auf kompilierte RISC-V-Instruktionen und verwendet die formale Semantik des RISC-V-Befehlssatzes und von Linux-Prozessen von Theorem. Der Rocq-Beweisprüfer verifiziert jeden abgeschlossenen Beweis anhand der Spezifikation. Anthropic zufolge müssen Entwickler daher nur drei Komponenten vertrauen: den formalen Modellen für RISC-V und Linux-Prozesse, den exakten Theoremaussagen und dem Rocq-Prüfer selbst.

Anthropic erklärte, das Verfahren auf Hunderte von Projekten in Googles OSS-Fuzz-Initiative angewendet zu haben. Diese bietet qualifizierten Open-Source-Projekten kontinuierliche Fuzzing-Tests und instrumentiert C- und C++-Programme automatisch mit AddressSanitizer – einem Werkzeug, das ein Programm abstürzen lässt, sobald unzulässig auf Speicher zugegriffen wird. Ein Anhang vom 22. Oktober 2026 führt den vollständigen bewiesenen Satz aus: Bei allen Eingaben unter 64 MiB und allen Speicherbelegungen lösen weder die mit ASan instrumentierte noch die nicht instrumentierte Binärdatei einen Fehler aus, brechen ab oder zeigen nicht modelliertes Verhalten; außerdem erzeugen beide identische Lese- und Schreibspuren, identisches Beendigungsverhalten und denselben endgültigen Dateisystemzustand.

Dem Anhang zufolge schrieb Claude während des Projekts rund eine Milliarde Zeilen Rocq, von denen etwa 180 Millionen den Beweisprüfer passierten. Für den 391 Zeilen umfassenden Parser-Einstiegspunkt von cJSON wurde ein Beweis mit 630.000 Zeilen erstellt; für fftw3, in das 51.000 Zeilen eingebunden waren, ein Beweis mit 480.000 Zeilen. Da Claude den Code vor Abschluss eines Beweises ändern durfte, erklärte Anthropic, Änderungen mit Abzügen belegt, zusätzliche Anerkennung für den Nachweis der durch eine Änderung betroffenen Eingaben vergeben und Änderungen protokolliert und überprüft zu haben, um Reward-Hacking entgegenzuwirken.

Bei den Beweisversuchen entdeckte Fehler

Anthropic berichtet, dass bei den Beweisversuchen Hunderte von Fehlern aufgedeckt wurden, darunter viele, die ein Fuzzer wahrscheinlich nicht finden würde. Beim Beweis für den Einstiegspunkt einer Bibliothek entdeckte Claude in einem Dekompressor einen Unterlauf eines Zählers, der zu einem Schreibzugriff außerhalb des gültigen Speicherbereichs führte – allerdings nur bei Eingaben von etwa 20 MB mit einer seltenen, spezifischen Speicherbelegung. Zu den weiteren Funden gehörten ein Lesezugriff außerhalb des gültigen Speicherbereichs in einem Bilddecoder, der eine 64-MB-Eingabe und mehr als 2 GB Speicher erforderte, ein solcher Lesezugriff, der eine bestimmte Abfolge von Aufrufen über zwei Handles für dieselbe Datei voraussetzte, sowie die erneute Entdeckung von CVE-2026-56132 in libexpat, für die eine tief verschachtelte Eingabe erforderlich war.

Claude fand außerdem Logikfehler, die nie zu einem Absturz führen, darunter eine Einschränkung, welche Dateien eine Anwendung laden kann und die nicht immer durchgesetzt wird. Anthropic zufolge deckten Verifikationsversuche bei mehreren weitverbreiteten, kritischen Anwendungen einen bislang unbekannten Logikfehler auf, der seit mehr als einem Jahrzehnt unentdeckt geblieben war. Bei dem Versuch, einen weitverbreiteten PDF-Reader zu verifizieren, fand das Unternehmen innerhalb einer Woche ebenso viele Sicherheitsfehler, wie üblicherweise in einem Jahr gemeldet werden.

Weitere Experimente und Erkenntnisse zur Effizienz

Über OSS-Fuzz hinaus bat Anthropic Claude, eine formale Spezifikation von RFC 1950 zu erstellen – dem technischen Dokument, das das zlib-Kompressionsformat definiert – und anschließend zu beweisen, dass die zlib-Implementierung des Linux-Kernels dieses korrekt umsetzt. Claude bewies die für x86 kompilierte Binärdatei direkt und verwendete dafür eine von Claude erzeugte formale Semantik des x86-Befehlssatzes. Anthropic erklärte, das Verfahren für ein halbes Dutzend weiterer weitverbreiteter Bibliotheken wiederholt und dabei geringfügige, nicht ausnutzbare Fehler in Sonderfällen gefunden zu haben, die derzeit upstream gemeldet werden. Das Unternehmen berichtete außerdem, dass bei der Erzeugung der x86-Semantik Hunderte Fehler in der offiziellen Referenzdokumentation und eine kleinere Zahl von Fehlern in der Hardware selbst entdeckt wurden und dass sich durch schrittweises Durchlaufen der Semantik ein Ubuntu-Benutzerbereich auf einem Linux-Kernel starten lässt.

In einem weiteren Experiment entwickelte Claude in Rust einen Interpreter für eine große Teilmenge von Python und bewies mithilfe des Verifizierungswerkzeugs Verus, dass dieser den in einer wissenschaftlichen Arbeit beschriebenen CPython-Semantiken entspricht. Im technischen Anhang heißt es, dass alle 17 Stufen des Interpreters bewiesen wurden. Der Satz lautet: „Immer wenn der Interpreter ein Ergebnis zurückgibt, entspricht dieses Ergebnis der Vorgabe der formalen Semantik.“ Anthropic zufolge ergaben empirische Tests mit 1,7 Millionen zufällig generierten Python-Programmen in 99,95 % der Fälle ein identisches Verhalten wie bei CPython. Von sieben absichtlich eingebauten Fehlern blieben fünf bei zufälligen Tests unentdeckt, während alle sieben den Beweis scheitern ließen.

Um die Effizienz zu messen, erstellte Anthropic 36 kleine Verifizierungsaufgaben, indem reale Einstiegspunkte von OSS-Fuzz verkleinert wurden. So entstanden Programme mit 283–2.491 Anweisungen und auf 64 Byte begrenzten Eingaben. AddressSanitizer wurde dabei durch eine „Mini-ASan“-Laufzeitumgebung mit etwa 100 Anweisungen ersetzt. Anthropic zufolge beweist Opus 5.5 die Hälfte der Aufgaben mit etwa 40 % weniger Tokens als Opus 5. Laut Anthropic benötigten Agenten, die in einem gemeinsamen Arbeitsbereich die Beweise der anderen kopieren durften, 17 % weniger Tokens als Agenten, die allein arbeiteten. Einige Agenten waren erfolgreich, nachdem sie zuvor allein gescheitert waren; allein arbeitende Agenten konnten zwei der Beweise nicht fertigstellen. Das Unternehmen erklärte, derselbe Wiederverwendungseffekt habe sich auch im großen Maßstab während des OSS-Fuzz-Projekts gezeigt: Agententeams kopierten fertige Beweise und passten sie an, da ein großer Teil jedes Beweises gemeinsamen C-Laufzeitcode und Initialisierungscode von AddressSanitizer abdeckt.

Genannte Einschränkungen und das OSS-Verify-Programm

Anthropic betont, dass die Beweise nicht bedeuten, die Bibliotheken seien fehlerfrei: Verbleibende Fehler könnten in den vertrauenswürdigen Komponenten oder außerhalb des Geltungsbereichs der Beweise liegen. Die Beweise decken statische, einkanalige RISC-V-Binärdateien ab, die mit musl libc gelinkt sind. Die meisten Nutzer verwenden diese Bibliotheken jedoch auf x86 oder ARM und linken sie dynamisch mit glibc; zudem erkennt AddressSanitizer nicht alle Fehler bei der Speichersicherheit. Das Unternehmen erklärte, es erwarte, dass diese Einschränkungen mit der Weiterentwicklung der Modelle beherrschbar werden.

Theorem bietet qualifizierten Open-Source-Projekten dieselbe Pipeline über sein Programm OSS Verify kostenlos an. Die Aufnahme erfolgt per Pull Request, der die Dateien project.yaml, Dockerfile und build.sh zum Repository des Programms hinzufügt. Theorem zufolge prüft das Unternehmen Projekte nach ähnlichen Kriterien wie OSS-Fuzz und räumt weit verbreiteter kritischer Infrastruktur Priorität ein. Laut Theorem erhalten die Maintainer einen vom Rocq-Kernel geprüften Rocq-Beweis dafür, dass jedes Fuzz-Ziel bei keiner Eingabe von bis zu 64 MiB abstürzt. Während der Beweisführung gefundene Fehler werden den Maintainerinnen und Maintainer privat per E-Mail mitgeteilt; eine Frist für die Offenlegung gibt es nicht. Die Erstellung von Beweisen kann mehrere Tage dauern. Theorems Fahrplan sieht vor, das gesamte Nix-Ökosystem zu verifizieren, einschließlich kritischer Infrastruktur wie glibc, OpenSSL und cURL.