Mit dem Partner Theorem hat Anthropic formale Beweise auf RISC-V-Ebene für OSS-Fuzz-Projekte erstellt. Dabei fand Claude seit Jahren übersehene Fehler.
Fuzz-Tests
Claude beweist Absturzfreiheit für 123 Open-Source-Bibliotheken
Anthropic hat formale Beweise für die Sicherheit von 123 Open-Source-Bibliotheken auf der Ebene des kompilierten Maschinencodes erstellen lassen. Das hat das Frontier Red Team des Unternehmens am 22. Oktober in einer Forschungsarbeit veröffentlicht, entstanden in Zusammenarbeit mit dem Unternehmen Theorem. Nach Angaben von Anthropic ist es der erste großflächige Versuch, mit KI formale Verifikation auf Produktivsoftware auf Assembler-Ebene anzuwenden.
Bei der formalen Verifikation wird Code in ein mathematisches Modell übertragen. Anschließend wird bewiesen, dass er bestimmte Regeln immer einhält. Bislang war das sehr aufwendig: Die Entwicklung des Betriebssystemkerns seL4 dauerte zwei Personenjahre, seine formale Verifikation 20 Personenjahre.
Aus Fuzz-Tests werden Beweise
Als Grundlage dienten die Fuzz-Tests aus Googles Initiative OSS-Fuzz. Bei diesen Tests werden Programme mit großen Mengen zufälliger Eingaben auf Abstürze geprüft, ohne dass jeder mögliche Pfad abgedeckt wird. Anthropic wandelte die Tests in eine Spezifikation um, nach der das Programm bei keiner Eingabe unter 64 MB abstürzt, auch nicht durch Speicherfehler. Claude bewies diese Eigenschaft innerhalb weniger Wochen für 239 Einsprungpunkte in 123 Bibliotheken. Die Beweise im System Rocq umfassen zusammen rund 180 Millionen Zeilen, ein typischer Beweis rund 600.000 Zeilen. Manuell geprüft werden müssen sie nicht, das übernimmt der Rocq-Beweisprüfer. Vertrauen müssen Anwender den Modellen von RISC-V und Linux-Prozessen, den bewiesenen Aussagen und dem Prüfer selbst.
Fehler, die Fuzzer nicht finden
Bei den Beweisversuchen fand Claude Hunderte Fehler und behob sie, bevor der Beweis gelang. Darunter war ein Unterlauf in einem Dekompressor, der nur bei Eingaben von rund 20 MB mit einem bestimmten Aufbau zu einem Schreibzugriff außerhalb des Speicherbereichs führte. Fuzzer arbeiten meist mit Eingaben bis 1 MB. Zudem fand Claude die bekannte Lücke CVE-2026-56132 in libexpat erneut. In separaten Versuchen bewies Claude, dass die zlib-Implementierung im Linux-Kernel die Spezifikation RFC 1950 korrekt umsetzt. Bei einem verbreiteten PDF-Reader fanden die Forscher in einer Woche so viele Sicherheitslücken, wie sonst in einem Jahr gemeldet werden.
Einschränkungen
„‚Formal verifiziert’ bedeutet nicht ‚fehlerfrei’”, schreiben die Autoren. Die Beweise gelten nur unter bestimmten Annahmen, nämlich für statische, single-threaded Programme auf einem RISC-V-Prozessor mit Linux und der C-Bibliothek musl. In der Praxis laufen die Bibliotheken meist auf x86 oder ARM mit glibc. Zudem erkennt der verwendete AddressSanitizer nicht alle Speicherfehler, und nicht alle Einsprungpunkte jeder Bibliothek wurden verifiziert. Ein weiterer Nachteil sind die Kosten: Ein Beweis kann Hunderte Millionen Tokens erfordern. Laut Anthropic benötigt Claude Opus 5.5 für die Hälfte von 36 Testaufgaben rund 40 Prozent weniger Tokens als Opus 5, und die Wiederverwendung von Beweisen senkte den Verbrauch um 17 Prozent.
Einen Teil der Beweise sowie die Semantik für RISC-V und Linux haben Anthropic und Theorem auf GitHub veröffentlicht. Theorem bietet an, das Verfahren für weitere Open-Source-Projekte anzuwenden.
(red)
