Ettevõte Anthropic esitles katsete tulemusi AI-mudelite kasutamisest olemasolevate projektide usaldusväärsuse ja ohutuse formaalseks kinnitamiseks. Katse käigus genereeriti AI-mudelite abil 123 avatud raamatukogu, mis olid testitud OSS Fuzzi infrastruktuuris, matemaatilised tõendid mäluga seotud vigade puudumise kohta.
Kontroll viidi läbi RISC-V arhitektuuri kompileeritud assembleri koodi tasandil. Kokku genereeriti umbes 180 miljonit tõendit Rocq Proveri verifitseerimise süsteemi jaoks (umbes 600 tuhat rida binaarfaili kohta koos 18 tuhande RISC-V käsuga). Tõendid loodi olemasolevate fuzzing-testide automaatse üleviimise kaudu formaalsetesse spetsifikatsioonidesse, mille järel AI mudel Claude tõendas, et kõigi kuni 64 MB suuruste sisendandmete korral ei esine programmis tõrkeid.
Tõendite koostamise käigus suutis AI-mudel tuvastada ja ette valmistada parandusi sadadele vigadele, mis olid varem fuzzing-testimise käigus tähelepanuta jäänud. Muuhulgas avastati haavatavusi, mis põhjustavad puhverülekannet teatud sisendandmete töötlemisel (nt CVE-2026-56132 libexpatis), samuti loogilisi vigu. Lisaks kasutati AI-mudelit zlib algoritmi rakenduse vastavuse tõendamiseks Linuxi tuumas spetsifikatsioonile RFC 1950.
Rust'i keeles genereeriti ka Python'i keele alamkogumi tõlgendaja, mille jaoks koostati Verus'i tööriistade abil formaalne tõend vastavusest CPython'i semantikaga. CPython'i käitumise võrdlemiseks viidi läbi üle 1.7 miljoni juhuslikult genereeritud Python'i programmi. 99,95% juhtudest olid nende programmide tulemused uues rakenduses ja CPython'is identsed, samas kui avastatud erinevused osutusid tuntud äärmisteks juhtudeks.
Teostatud formaalne verifikatsioon tagab vastavuse spetsifikatsioonile, kuid ei välista täielikult turvaprobleemide tekkimist, kuna formaalseteks ei jää riskid, mis on seotud mitme lõime, dünaamilise sidumise ja reaalse riistvara ebanormaalse käitumisega. Pakutava lähenemise peamine eelis on otsene töötamine binaarfailidega, mis võimaldab vältida olemasoleva koodi ümberkirjutamist formaalselt verifitseeritavates keeltes.
Allikas: opennet.ru
