Anthropic je predstavil rezultate poskusov z uporabo modelov umetne inteligence za formalno preverjanje zanesljivosti in varnosti obstoječih projektov. Med poskusom so bili modeli umetne inteligence uporabljeni za generiranje matematičnih dokazov o odsotnosti napak v pomnilniku za 123 odprtokodnih knjižnic, testiranih v infrastrukturi OSS Fuzz.
Preverjanje je bilo izvedeno na ravni prevedene zbirne kode za arhitekturo RISC-V. Skupna količina ustvarjenih dokazov je znašala približno 180 milijonov vrstic kode za sistem za preverjanje Rocq Prover (približno 600 vrstic na binarno datoteko z 18 instrukcijami RISC-V). Dokazi so bili ustvarjeni z avtomatsko pretvorbo obstoječih fuzzing testov v formalne specifikacije, nakar je model Claude AI dokazal, da je program brezhibno delujoč za vse vhodne podatke do 64 MB.
Med procesom gradnje dokazov je model umetne inteligence sposoben prepoznati in pripraviti popravke za stotine napak, ki jih fuzz testiranje prej ni odkrilo. Med drugim so bile te ranljivosti prelivanja medpomnilnika pri obdelavi določenih vhodnih podatkov (npr. CVE-2026-56132 v libexpatu) ter logične napake. Poleg tega je bil model umetne inteligence uporabljen za dokazovanje skladnosti implementacije algoritma zlib v jedru. Linux Specifikacije RFC 1950.
V Rustu je bil ustvarjen tudi interpreter za podmnožico Pythona, za katerega je bil z uporabo orodja Verus pripravljen formalni dokaz skladnosti s semantiko CPython. Za primerjavo vedenja s CPythonom je bilo izvedenih več kot 1.7 milijona naključno ustvarjenih programov Python. V 99.95 % primerov so se rezultati izvajanja teh programov v novi implementaciji in v CPythonu ujemali, vsa ugotovljena odstopanja pa so bila znani robni primeri.
Formalno preverjanje zagotavlja skladnost s specifikacijami, vendar ne odpravi popolnoma varnostnih težav, saj tveganja, ki jih povzročajo težave z večnitnostjo, dinamično povezovanje in anomalno vedenje na resnični strojni opremi, ostajajo neformalizirana. Ključna prednost predlaganega pristopa je, da deluje neposredno z binarnimi datotekami, kar odpravlja potrebo po prepisovanju obstoječe kode v formalno preverljivih jezikih.
Vir: opennet.ru
