Společnost Anthropic představila výsledky experimentů využívající AI modely pro formální verifikaci spolehlivosti a bezpečnosti již existujících projektů. Během experimentu byly pomocí AI modelů generovány matematické důkazy absence chyb při práci s paměťovými prostory pro 123 otevřených knihoven, testovaných v infrastruktuře OSS Fuzz.
Ověření probíhalo na úrovni zkompilovaného assemblerového kódu pro architekturu RISC-V. Celkový objem vygenerovaných důkazů činil přibližně 180 milionů řádků kódu pro systém verifikace Rocq Prover (asi 600 tisíc řádků na binární soubor s 18 tisíci instrukcemi RISC-V). Důkazy byly vytvářeny automatickým převodem existujících fuzzingových testů na formální specifikace, po kterých AI model Claude dokázal, že při jakýchkoli vstupních datech o velikosti až 64 MB v programu nedochází k haváriím.
Během vytváření důkazů dokázal AI model odhalit a připravit opravy pro stovky chyb, které nebyly dříve zaznamenány při fuzzingovém testování. Mezi jinými byly odhaleny zranitelnosti vedoucí k přetečení vyrovnávací paměti při zpracování určitých vstupních dat (například CVE-2026-56132 v libexpat), stejně jako logické chyby. Kromě toho byl AI model použit k prokázání shody implementace algoritmu zlib v jádru Linux se specifikací RFC 1950.
Také byl v jazyce Rust vygenerován interpreter pro podmnožinu jazyka Python, pro kterou bylo pomocí nástrojů Verus připraveno formální důkazní osvědčení odpovídající semantice CPython. Pro porovnání chování s CPython bylo vykonáno více než 1,7 milionu náhodně generovaných Python programů. Ve 99,95 % případů se výsledky provádění těchto programů v nové implementaci a v CPython shodovaly, přičemž zjištěné rozdíly se ukázaly jako známé hraniční případy.
Prováděná formální verifikace zaručuje shodu se specifikací, ale zcela nevylučuje vznik problémů s bezpečností, jelikož zůstávají neformálně zmapována rizika vyplývající z problémů s vícevláknovostí, dynamickým spojováním a anomálním chováním skutečného hardwaru. Klíčovou výhodou navrhovaného přístupu je práce přímo s binárními soubory, což eliminuje potřebu přepisování stávajícího kódu do formálně verifikovatelných jazyků.
Zdroj: opennet.ru
