Anthropic und Theorem melden KI-Beweise für Open-Source-Fuzzing-Ziele

Anthropic hat am 22. Oktober Forschung mit Theorem veröffentlicht. Dem veröffentlichten Bericht zufolge hat Claude formale Sicherheitsbeweise für 239 Fuzzing-Einstiegspunkte in 123 quelloffenen Bibliotheken erstellt. Die Arbeit überführt vorhandene Tests in mathematische Aussagen über kompilierte Programme und lässt die erzeugten Argumente von einem unabhängigen Beweisprüfer kontrollieren. Dabei fand und behob das Modell auch Fehler, die verhindert hatten, dass diese Aussagen gelten.

Die Garantien gelten innerhalb einer festgelegten Ausführungsumgebung. Die RISC-V-Binärdateien sind statisch gegen musl gelinkt und werden jeweils mit nur einem Thread ausgeführt. Sie laufen in einem Modell von Linux-Prozessen, das feste Speicherbudgets voraussetzt. Der technische Anhang nennt Eingaben unter 64 MiB. Theorems Treiberdokumentation erklärt, dass Dateien ab dieser Größe abgewiesen werden. Die Voraussetzungen des Theorems legen außerdem fest, welche Betriebssystemantworten, Speicheranordnungen und Ressourcenbedingungen abgedeckt sind.

Der Ablauf verwendet das bestehende Fuzzing-Testgerüst einer Bibliothek. Dessen Zusicherungen können Eigenschaften wie erfolgreiche Kompression und Dekompression ausdrücken. Er vergleicht normale Binärdateien mit Versionen, die Sanitizer-Prüfungen enthalten, und argumentiert über ihr beobachtbares Verhalten. Im Anhang umfassen Abstürze Speicher- beziehungsweise Ausführungsfehler, Abbrüche und Verhalten, das im Prozessmodell fehlt. Claude erstellt die Argumente in Rocq; dessen Kern prüft, ob sie die geforderten Aussagen beweisen.

Die Vertrauensgrenze bleibt auf die formalen Maschinen- und Prozessmodelle, die genauen Theoremaussagen sowie den Prüfer selbst konzentriert, einschließlich der Hilfswerkzeuge und der Umgebung zur Prüfung jeder Binärdatei. Die Abdeckung folgt dem Code, der über den gewählten Einstiegspunkt erreichbar ist, und den Prüfungen in der Binärdatei. Eigenschaften außerhalb dieser Prüfungen sowie Unterschiede zwischen Modell und eingesetzter Hardware oder Betriebssystemen bleiben relevant, wenn Ergebnisse auf produktiv eingesetzte Software angewandt werden.

Patches brachten eine weitere Herausforderung mit sich: Ein Agent könnte eine Absturzfreiheit leicht beweisbar machen, indem er sinnvolles Programmverhalten entfernt. Laut Anthropic wurde im Experiment jeder Patch bestraft. Zusatzpunkte gab es für den Beweis, welche Eingaben eine Änderung betrifft und wie klein diese Menge ist. Die Forschenden protokollierten und überprüften Patches außerdem auf solche Abkürzungen. Nach einer Änderung wurde die Spezifikation neu erzeugt, und das Modell versuchte die Aussage über das überarbeitete Programm zu beweisen.

Das öffentliche Material ist eine Teilmenge der Forschungsergebnisse. Als die öffentlich zugänglichen Materialien geprüft wurden, führte das Beweisrepository von Theorem 60 Einstiegspunkte in 25 Bibliotheken auf, geprüft mit Rocq 9.2.0. Es legt die kompilierten Binärdateien fest und dokumentiert zugehörige Aussagen und Annahmen. Die veröffentlichte Fassung enthält Übereinstimmungsbeweise, die Verhalten vergleichen und bestimmte Fehler ausschließen. Solche Beweise können dennoch eine endlos laufende Ausführung zulassen. Für Terminierung ist ein gesondertes Theorem erforderlich.

Die fachliche Diskussion in Anthropics Anhang beschreibt deutlich ausführlichere Beweise, als menschliche Spezialisten üblicherweise schreiben würden. Die Agenten führten Registerinhalte, Speicheradressen und Ausführungszweige wiederholt im Detail aus, entwickelten aber auch einige bekannte Abstraktionen. Die Analyse betrachtet bessere modulare Strukturen als offene Frage für die Übertragung auf komplexere Programme. Sie trennt die mathematische Gültigkeit eines Beweises von Effizienz und Organisation seiner Erstellung.

Theorem bietet seinen OSS-Verify-Ablauf außerdem kostenlos für geeignete Open-Source-Projekte an. Die Eignung wird einzeln anhand von Wartung, Nutzung, Lizenzierung und der Rolle an Sicherheitsgrenzen oder als Grundlage anderer Software geprüft. Das Programm priorisiert weitverbreitete Infrastruktur und meldet entdeckte Fehler vertraulich an die Verantwortlichen. Laut Dokumentation können Beweise mehrere Tage benötigen und nach Abschluss aktualisiert werden. Jedes Ergebnis ist dabei an bestimmte Programmbuilds gebunden.