Anthropic utvecklar tekniker för formell verifiering av befintlig programvara med hjälp av AI

Företaget Anthropic har presenterat resultaten av experiment med AI-modeller för formell verifiering av tillförlitlighet och säkerhet hos redan existerande projekt. Under experimentet genererades matematiska bevis för avsaknad av minnesfel med hjälp av AI-modeller för 123 öppna bibliotek som testades i OSS Fuzz-infrastrukturen.

Verifikationen utfördes på nivån av den kompilerade assemblerkoden för RISC-V-arkitekturen. Den totala volymen av genererade bevis uppgick till cirka 180 miljoner kodrader för verifieringssystemet Rocq Prover (cirka 600 000 rader för en binärfil med 18 000 RISC-V-instruktioner). Bevisen bildades genom automatisk omvandling av befintliga fuzzing-tester till formella specifikationer, varefter AI-modellen Claude bevisade att programmet inte kraschar med alla ingångar upp till 64 MB.

Under processen för att bygga upp bevis kunde AI-modellen identifiera och förbereda korrigeringar för hundratals fel som tidigare inte upptäckts vid fuzzing-testning. Bland annat identifierades sårbarheter som ledde till buffertöverflöd vid bearbetning av vissa indata (t.ex. CVE-2026-56132 i libexpat), samt logiska fel. Dessutom användes AI-modellen för att bevisa att implementeringen av zlib-algoritmen i Linux-kärnan överensstämmer med specifikationen RFC 1950.

Dessutom har en tolk för en delmängd av Python-språket genererats i Rust, för vilken ett formellt bevis har förberetts med hjälp av verktyget Verus för att överensstämma med CPython-semantiken. För att jämföra beteendet med CPython kördes mer än 1,7 miljoner slumpmässigt genererade Python-program. I 99,95% av fallen stämde resultaten från dessa program i den nya implementeringen och i CPython överens, och de identifierade avvikelserna visade sig vara kända gränsfall.

Genomförd formell verifiering garanterar överensstämmelse med specifikationen, men utesluter inte helt uppkomsten av säkerhetsproblem, eftersom risker orsakade av flertrådighet, dynamisk länkning och avvikande beteende hos den verkliga hårdvaran förblir oformulerade. En betydande fördel med den föreslagna metoden är att den arbetar direkt med binärfiler, vilket gör det möjligt att undvika behovet av att skriva om befintlig kod i formellt verifierbara språk.

Källa: opennet.ru