Spoločnosť Anthropic predstavila výsledky experimentov s využitím AI modelov na formálnu verifikáciu spoľahlivosti a bezpečnosti existujúcich projektov. Počas experimentu boli pomocou AI modelov generované matematické dôkazy o absencii chýb pri práci s pamäťou pre 123 otvorených knižníc, testovaných v prostredí OSS Fuzz.
Kontrola sa vykonávala na úrovni skompilovaného assemblerového kódu pre architektúru RISC-V. Celkový objem generovaných dôkazov dosiahol približne 180 miliónov riadkov kódu pre systém verifikácie Rocq Prover (približne 600 tisíc riadkov na binárny súbor s 18 tisícami RISC-V inštrukcií). Dôkazy sa vytvárali automatickým prevodom existujúcich fuzzing testov na formálne špecifikácie, po čom AI model Claude dokazoval, že pri akýchkoľvek vstupných údajoch do 64 MB v programe nevznikajú výpadky.
Počas tvorby dôkazov AI model dokázal odhaliť a pripraviť opravy pre stovky chýb, ktoré neboli predtým zaznamenané pri fuzzing testovaní. Medzi nimi boli zistené zraniteľnosti vedúce k pretečeniu zásobníka pri spracovaní určitých vstupných údajov (napríklad CVE-2026-56132 v libexpat), ako aj logické chyby. Okrem toho bol AI model použitý na dôkaz súladu implementácie algoritmu zlib v jadre Linuxu so špecifikáciou RFC 1950.
Taktiež bol v jazyku Rust generovaný interpretátor pre podmnožinu jazyka Python, pre ktorú bolo pomocou nástrojov Verus pripravené formálne dôkazové súlad s semantikou CPython. Na porovnanie správania s CPython bolo vykonaných viac ako 1,7 milióna náhodne generovaných Python programov. V 99,95 % prípadov sa výsledky vykonania týchto programov v novej implementácii a v CPython zhodovali, pričom zistené rozdiely sa ukázali ako známe hraničné prípady.
Provedená formálna verifikácia zabezpečuje súlad so špecifikáciou, ale úplne nevylučuje vznik bezpečnostných problémov, pretože formálne nie sú zohľadnené riziká spôsobené problémami s viacerými vláknami, dynamickým prepojením a anomálnym správaním skutočného hardvéru. Kľúčovou výhodou navrhnutého prístupu je práca priamo s binárnymi súbormi, čo umožňuje obísť potrebu prepisovania existujúceho kódu na formálne overiteľných jazykoch.
Zdroj: opennet.ru
