Selskabet Anthropic har præsenteret resultaterne af eksperimenter vedrørende brugen af AI-modeller til formel verifikation af pålidelighed og sikkerhed i allerede eksisterende projekter. I løbet af eksperimentet blev der med hjælp fra AI-modeller genereret matematiske beviser for fravær af fejl i hukommelseshåndteringen for 123 åbne biblioteker, der blev testet i OSS Fuzz-infrastrukturen.
Verifikationen blev gennemført på niveauet for den komplierede assemblerkode for RISC-V-arkitekturen. Den samlede mængde af genererede beviser udgjorde cirka 180 millioner linjer kode for verifikationssystemet Rocq Prover (cirka 600.000 linjer for en binær fil med 18.000 RISC-V-instruktioner). Beviserne blev dannet ved automatisk at konvertere eksisterende fuzzing-tests til formelle specifikationer, hvorefter AI-modellen Claude beviste, at der under alle inddata op til 64 MB ikke opstår fejl i programmet.
I løbet af opbygningen af beviserne kunne AI-modellen identificere og forberede rettelser til hundredevis af fejl, som tidligere ikke blev bemærket under fuzzing-testning. Blandt andet blev der identificeret sårbarheder, der fører til buffer-overløb ved behandling af visse inddata (f.eks. CVE-2026-56132 i libexpat), samt logiske fejl. Desuden blev AI-modellen brugt til at bevise, at implementeringen af zlib-algoritmen i Linux-kernen overholder specifikationen i RFC 1950.
Derudover blev der genereret en fortolker på Rust til en undergruppe af Python-sproget, for hvilken der ved hjælp af værktøjet Verus blev forberedt et formelt bevis for overensstemmelse med semantikken af CPython. For at sammenligne adfærden med CPython blev der udført mere end 1,7 millioner tilfældigt genererede Python-programmer. I 99,95% af tilfældene stemte resultaterne af eksekveringen af disse programmer i den nye implementering overens med CPython, og de identificerede forskelle viste sig at være kendte grænsetilfælde.
Den udførte formelle verifikation garanterer overensstemmelse med specifikationen, men udelukker ikke fuldstændigt opstående sikkerhedsproblemer, da der stadig er uformelle risici forårsaget af problemer med multitrådning, dynamisk binding og unormel adfærd fra det faktiske udstyr. En nøglefordel ved den foreslåede tilgang er arbejdet direkte med binære filer, hvilket gør det muligt at undgå behovet for at omskrive den eksisterende kode til formelt verificerbare sprog.
Kilde: opennet.ru
