Claude hat für 123 Open-Source-Bibliotheken bewiesen, dass 239 ihrer Fuzz-Tests bei keiner Eingabe unter 64 MB abstürzen. Anthropic und der Partner Theorem halten den Versuch für den ersten dieser Größe, der Software im Produktiveinsatz auf Maschinencode-Ebene verifiziert. Gültig sind die Beweise bisher nur auf RISC-V-Prozessoren.
Ein Klick · kostenlosDr. Web bei Google bevorzugenMarkieren Sie drweb.de als bevorzugte Quelle. Dann sehen Sie unsere Artikel öfter unter den Top-Meldungen.Jetzt hinzufügenZwanzig Personenjahre steckten Fachleute in den Korrektheitsbeweis für den Betriebssystemkern seL4, zehnmal so viel wie in seine Entwicklung. Für die Beweise zu 123 Bibliotheken aus Googles Testprojekt OSS-Fuzz brauchte Claude laut Anthropic wenige Wochen.[1]
Das Wichtigste in Kürze
- Claude bewies für 239 Fuzz-Tests, dass keine Eingabe bis 64 MB einen Absturz oder Speicherfehler auslöst.
- Bei der Arbeit fand das Modell Hunderte Fehler, viele davon laut Anthropic für Fuzzer kaum auffindbar.
- Die Beweise umfassen rund 180 Millionen Zeilen in der Beweissprache Rocq und gelten für statisch gelinkte RISC-V-Programme unter Linux.
Was hat Claude bewiesen?
Ein Fuzzer schickt Millionen zufällig veränderter Eingaben durch ein Programm und meldet jede, die einen Absturz auslöst. Alle denkbaren Eingaben schafft kein Fuzzer. Anthropic hat deshalb die Regel „dieser Test schlägt nie fehl“ in eine mathematische Aussage über das kompilierte Programm übersetzt. Claude schrieb den Beweis, der Beweisprüfer von Rocq kontrolliert ihn. Vertrauen müssen Entwickler danach nur noch drei Bausteinen: den formalen Beschreibungen von RISC-V und Linux, den bewiesenen Aussagen und dem Prüfer selbst.[1]
Während der Beweisarbeit stieß Claude auf Fehler, die jahrelang unentdeckt geblieben waren. Ein Entpacker schrieb über das Ende seines Speicherbereichs hinaus, allerdings nur bei seltenen, rund 20 MB großen Eingaben. Fuzzer testen laut Anthropic meist nur bis etwa 1 MB. In der XML-Bibliothek libexpat fand Claude die bekannte Sicherheitslücke CVE-2026-56132 erneut.[1] Wie ergiebig die KI-Fehlersuche ist, zeigte zuletzt Aisle mit 18 von 24 neuen Lücken in curl.
Warum blieb formale Verifikation bisher die Ausnahme?
Der Informatiker Martin Kleppmann hat die Rechnung im Dezember 2025 aufgemacht: Die Kosten eines Fehlers tragen meist die Nutzer, die Kosten eines Beweises der Entwickler. Für die meisten Programme lohnte sich der Aufwand deshalb nicht. Kleppmann sagte voraus, dass KI-Modelle formale Verifikation in den Alltag der Softwareentwicklung bringen.[2]
Billig sind die Beweise noch nicht: Ein einzelner Beweis kostet laut Anthropic Hunderte Millionen Token. Opus 5.5 schafft die Hälfte von 36 Testaufgaben mit rund 40 % weniger Token als Opus 5.[1] Anthropic sieht einen Vorteil gegenüber dem Umschreiben in eine andere Sprache, wie bei der KI-gestützten Portierung von Postgres nach Rust: Die Beweise lassen den vorhandenen Code unangetastet.
Ein Beweis für RISC-V schützt noch keinen x86-Server, aber er zeigt, wo die übrigen Fehler stecken können.
Markus Seyfferth, Chefredakteur Dr. Web
Fuzzing und Beweis im Vergleich
Was bedeutet das für Softwarehersteller in der EU?
Die Beweise gelten laut Anthropic für statisch gelinkte RISC-V-Programme mit musl, die meisten Server laufen auf x86 oder ARM mit glibc. Der Speicherprüfer AddressSanitizer erkennt nicht jeden Speicherfehler, und ein Programm kann eine bewiesene Bibliothek falsch aufrufen.[1]
Für Hersteller in der EU zählt der Cyber Resilience Act. Ab dem 11. Dezember 2027 gelten laut BSI alle Pflichten, darunter der Umgang mit Schwachstellen über die gesamte Lebensdauer eines Produkts. Nicht kommerzielle Open-Source-Software ist ausgenommen.[3] Die Sorgfaltspflicht für eingebaute Bibliotheken liegt damit beim Hersteller, nicht bei den oft nur ein oder zwei Betreuern vieler Open-Source-Projekte, auf denen das Internet aufbaut.
- Abhängigkeiten abgleichen: Prüfen Sie anhand Ihrer Software-Stückliste (SBOM), welche eingebauten Bibliotheken in OSS-Fuzz stehen. Einen Teil der Beweise hat Theorem auf GitHub veröffentlicht.[4]
- Eigene Projekte anmelden: Pflegen Sie eine Open-Source-Bibliothek, können Sie sie bei Theorem kostenlos anmelden. Voraussetzung sind Fuzz-Tests, die sich als statisch gelinktes RISC-V-Programm bauen lassen.[5]
Laut Anthropic will Theorem die Paketsammlung Nix samt glibc, OpenSSL und cURL verifizieren.[1]
Quellen
5 Quellen anzeigenQuellen ausblenden
- AnthropicLLMs are making formal software verification feasible at a much larger scale
- Martin KleppmannPrediction: AI will make formal verification go mainstream
- Bundesamt für Sicherheit in der InformationstechnikCyber Resilience Act
- Theorem auf GitHuboss-verify-proofs (Rocq-Beweise zu OSS-Fuzz-Tests, veröffentlicht am 22. Oktober 2026)
- TheoremOSS Verify: Free formal verification for open source
Mehr Newshunger?
- Cohere will Aisle übernehmen: Das Prager Team fand 18 der 24 neuen curl-Lücken
- Anthropic öffnet Mythos 5.1 für mehr Sicherheitsteams und staffelt den Zugang in drei Stufen
- Die Menschen, die das Internet stützen: Elf von 23 Kernprojekten hängen an ein oder zwei Personen
- 570 Sicherheitslücken an einem Tag: KI treibt Microsofts Patchday auf Rekordniveau
- Linux Foundation startet Akrites: Schützt das Bündnis Open Source vor KI?
- Postgres in Rust neu geschrieben: KI-Klon besteht jetzt 100 Prozent der Regressionstests
- GEA ersetzt Windows durch Linux und stellt seine Anlagensteuerung unter die neuen EU-Cyberregeln
- Cybersecurity Grundlagen: Was KMU 2026 können müssen
- Cybersecurity-Glossar 2026: 99 Begriffe von BSI bis Zero Trust für Entscheider
