{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/de\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic entwickelt Technologien zur formalen Verifizierung vorhandener Software mithilfe von KI","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Das Unternehmen Anthropic hat die Ergebnisse von Experimenten zur Verwendung von KI-Modellen zur formalen Verifizierung der Zuverl\u00e4ssigkeit und Sicherheit bestehender Projekte vorgestellt. Im Rahmen des Experiments wurden f\u00fcr 123 Open-Source-Bibliotheken, die in der OSS Fuzz-Infrastruktur getestet wurden, mathematische Beweise f\u00fcr das Fehlen von Fehlern im Umgang mit dem Speicher generiert. <\/p>\n
Die \u00dcberpr\u00fcfung wurde auf der Ebene des kompilierten Assemblers f\u00fcr die RISC-V-Architektur durchgef\u00fchrt. Insgesamt wurden etwa 180 Millionen Codezeilen f\u00fcr das Verifikationssystem Rocq Prover generiert (etwa 600.000 Zeilen f\u00fcr die Bin\u00e4rdatei 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\u00fcrzen kam. <\/p>\n
Im Prozess des Aufbaus der Beweise konnte das KI-Modell Hunderte von Fehlern identifizieren und Korrekturen f\u00fcr diese vorbereiten, die zuvor beim Fuzzing-Testing nicht erkannt wurden. Unter anderem wurden Schwachstellen identifiziert, die zu Puffer\u00fcberl\u00e4ufen bei der Verarbeitung bestimmter Eingabedaten f\u00fchren (zum Beispiel CVE-2026-56132 in libexpat) sowie logische Fehler. Dar\u00fcber hinaus wurde das KI-Modell verwendet, um die Konformit\u00e4t der Implementierung des zlib-Algorithmus im Linux-Kernel mit der RFC 1950-Spezifikation zu beweisen.<\/p>\n
Au\u00dferdem wurde in Rust ein Interpreter f\u00fcr eine Teilmenge der Programmiersprache Python generiert, f\u00fcr den mit Hilfe des Werkzeugs Verus ein formaler Beweis f\u00fcr die \u00dcbereinstimmung mit der Semantik von CPython erstellt wurde. Um das Verhalten im Vergleich zu CPython zu \u00fcberpr\u00fcfen, wurden \u00fcber 1,7 Millionen zuf\u00e4llig generierte Python-Programme ausgef\u00fchrt. In 99,95 % der F\u00e4lle stimmten die Ergebnisse der Ausf\u00fchrung dieser Programme in der neuen Implementierung und in CPython \u00fcberein, w\u00e4hrend die gefundenen Abweichungen bekannte Grenzf\u00e4lle darstellten.<\/p>\n
Die durchgef\u00fchrte formale Verifikation gew\u00e4hrleistet die \u00dcbereinstimmung mit der Spezifikation, schlie\u00dft jedoch nicht vollst\u00e4ndig die M\u00f6glichkeit von Sicherheitsproblemen aus, da die Risiken, die durch Mehrfachverarbeitung, dynamisches Binden und anomales Verhalten von tats\u00e4chlicher Hardware verursacht werden, nicht formalisiert bleiben. Ein wesentlicher Vorteil des vorgeschlagenen Ansatzes ist die direkte Arbeit mit Bin\u00e4rdateien, was eine Neuschreibung des bestehenden Codes in formal verifizierbaren Sprachen \u00fcberfl\u00fcssig macht. \n Quelle: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"