Anthropic prezentēja eksperimentu rezultātus, izmantojot mākslīgā intelekta modeļus, lai formāli pārbaudītu esošo projektu uzticamību un drošību. Eksperimenta laikā mākslīgā intelekta modeļi tika izmantoti, lai ģenerētu matemātiskus pierādījumus par atmiņas kļūdu neesamību 123 atvērtā pirmkoda bibliotēkām, kas tika testētas OSS Fuzz infrastruktūrā.
Verifikācija tika veikta kompilētā assemblera koda līmenī RISC-V arhitektūrai. Kopējais ģenerēto pierādījumu apjoms Rocq Prover verifikācijas sistēmai sasniedza aptuveni 180 miljonus koda rindiņu (aptuveni 600 000 rindiņu katrā binārajā failā ar 18 000 RISC-V instrukcijām). Pierādījumi tika ģenerēti, automātiski konvertējot esošos neskaidros testus formālās specifikācijās, pēc kā Claude AI modelis pierādīja, ka programma ir bez kļūdām jebkuriem ievades datiem līdz 64 MB.
Pārbaudes procesa laikā mākslīgā intelekta modelis spēja identificēt un sagatavot labojumus simtiem kļūdu, kuras iepriekš nebija atklātas ar izplūdušo (fuzz) testēšanu. Cita starpā tās ietvēra bufera pārpildes ievainojamības, apstrādājot noteiktus ievades datus (piemēram, CVE-2026-56132 libexpat versijā), kā arī loģiskas kļūdas. Turklāt mākslīgā intelekta modelis tika izmantots, lai pierādītu kodola zlib algoritma implementācijas atbilstību. Linux RFC 1950 specifikācijas.
Arī Rust valodā tika ģenerēts Python apakškopas interpretētājs, kuram, izmantojot Verus rīkkopa, tika sagatavots formāls atbilstības CPython semantikai pierādījums. Lai salīdzinātu darbību ar CPython, tika izpildītas vairāk nekā 1.7 miljoni nejauši ģenerētu Python programmu. 99.95% gadījumu šo programmu izpildes rezultāti jaunajā ieviešanā un CPython sakrita, un visas atrastās neatbilstības bija zināmi robežgadījumi.
Formāla verifikācija garantē atbilstību specifikācijām, taču tā pilnībā nenovērš drošības problēmas, jo riski, ko rada daudzpavedienu problēmas, dinamiskā saistīšana un anomāla uzvedība reālā aparatūrā, paliek neformalizēti. Piedāvātās pieejas galvenā priekšrocība ir tā, ka tā darbojas tieši ar binārajiem failiem, novēršot nepieciešamību pārrakstīt esošo kodu formāli verificējamās valodās.
Avots: opennet.ru
