Anthropic presenterade resultaten av experiment med AI-modeller för att formellt verifiera tillförlitligheten och säkerheten hos befintliga projekt. Under experimentet användes AI-modeller för att generera matematiska bevis på frånvaron av minnesfel för 123 bibliotek med öppen källkod som testats i OSS Fuzz-infrastrukturen.
Verifieringen utfördes på kompilerad assemblerkodnivå för RISC-V-arkitekturen. Den totala volymen genererade bevis uppgick till cirka 180 miljoner kodrader för Rocq Prover-verifieringssystemet (cirka 600 000 rader per binärfil med 18 000 RISC-V-instruktioner). Bevisen genererades genom att automatiskt konvertera befintliga fuzzingtester till formella specifikationer, varefter Claude AI-modellen bevisade att programmet är felfritt för indata upp till 64 MB.
Under bevisbyggandeprocessen kunde AI-modellen identifiera och förbereda korrigeringar för hundratals buggar som tidigare inte upptäckts genom fuzztestning. Bland annat inkluderade dessa sårbarheter för buffertöverflöde vid bearbetning av viss indata (t.ex. CVE-2026-56132 i libexpat), samt logiska fel. Dessutom användes AI-modellen för att bevisa överensstämmelse hos kärnans implementering av zlib-algoritmen. Linux RFC 1950-specifikationer.
En tolk för en delmängd av Python genererades också i Rust, för vilken ett formellt bevis på överensstämmelse med CPython-semantik utarbetades med hjälp av Verus-verktygslådan. För att jämföra beteendet med CPython kördes över 1.7 miljoner slumpmässigt genererade Python-program. I 99.95 % av fallen matchade resultaten av att köra dessa program i den nya implementeringen och i CPython, och eventuella avvikelser som hittades var kända edge-fall.
Formell verifiering garanterar specifikationsefterlevnad, men den eliminerar inte helt säkerhetsproblem, eftersom risker orsakade av multitrådningsproblem, dynamisk länkning och avvikande beteende på verklig hårdvara förblir oformaliserade. En viktig fördel med den föreslagna metoden är att den fungerar direkt med binära filer, vilket eliminerar behovet av att skriva om befintlig kod i formellt verifierbara språk.
Källa: opennet.ru
