Das Unternehmen Anthropic hat die Ergebnisse von Experimenten zur Verwendung von KI-Modellen zur formalen Verifizierung der Zuverlässigkeit und Sicherheit bestehender Projekte vorgestellt. Im Rahmen des Experiments wurden für 123 Open-Source-Bibliotheken, die in der OSS Fuzz-Infrastruktur getestet wurden, mathematische Beweise für das Fehlen von Fehlern im Umgang mit dem Speicher generiert.
Die Überprüfung wurde auf der Ebene des kompilierten Assemblers für die RISC-V-Architektur durchgeführt. Insgesamt wurden etwa 180 Millionen Codezeilen für das Verifikationssystem Rocq Prover generiert (etwa 600.000 Zeilen für die Binärdatei mit 18.000 RISC-V-Befehlen). Die Beweise wurden durch die automatische Umwandlung vorhandener Fuzzing-Tests in formale Spezifikationen erstellt, wonach das KI-Modell Claude bewies, dass es bei beliebigen Eingaben von bis zu 64 MB in dem Programm zu keinen Abstürzen kam.
Im Prozess des Aufbaus der Beweise konnte das KI-Modell Hunderte von Fehlern identifizieren und Korrekturen für diese vorbereiten, die zuvor beim Fuzzing-Testing nicht erkannt wurden. Unter anderem wurden Schwachstellen identifiziert, die zu Pufferüberläufen bei der Verarbeitung bestimmter Eingabedaten führen (zum Beispiel CVE-2026-56132 in libexpat) sowie logische Fehler. Darüber hinaus wurde das KI-Modell verwendet, um die Konformität der Implementierung des zlib-Algorithmus im Linux-Kernel mit der RFC 1950-Spezifikation zu beweisen.
Außerdem wurde in Rust ein Interpreter für eine Teilmenge der Programmiersprache Python generiert, für den mit Hilfe des Werkzeugs Verus ein formaler Beweis für die Übereinstimmung mit der Semantik von CPython erstellt wurde. Um das Verhalten im Vergleich zu CPython zu überprüfen, wurden über 1,7 Millionen zufällig generierte Python-Programme ausgeführt. In 99,95 % der Fälle stimmten die Ergebnisse der Ausführung dieser Programme in der neuen Implementierung und in CPython überein, während die gefundenen Abweichungen bekannte Grenzfälle darstellten.
Die durchgeführte formale Verifikation gewährleistet die Übereinstimmung mit der Spezifikation, schließt jedoch nicht vollständig die Möglichkeit von Sicherheitsproblemen aus, da die Risiken, die durch Mehrfachverarbeitung, dynamisches Binden und anomales Verhalten von tatsächlicher Hardware verursacht werden, nicht formalisiert bleiben. Ein wesentlicher Vorteil des vorgeschlagenen Ansatzes ist die direkte Arbeit mit Binärdateien, was eine Neuschreibung des bestehenden Codes in formal verifizierbaren Sprachen überflüssig macht.
Quelle: opennet.ru
