Anthropic je predstavio rezultate eksperimenata korištenjem AI modela za formalnu provjeru pouzdanosti i sigurnosti postojećih projekata. Tokom eksperimenta, AI modeli su korišteni za generiranje matematičkih dokaza o odsustvu memorijskih grešaka za 123 biblioteke otvorenog koda testirane u OSS Fuzz infrastrukturi.
Verifikacija je izvršena na nivou kompajliranog asemblerskog koda za RISC-V arhitekturu. Ukupna količina generisanih dokaza iznosila je približno 180 miliona linija koda za Rocq Prover sistem verifikacije (približno 600 linija po binarnoj datoteci sa 18 RISC-V instrukcija). Dokazi su generisani automatskim pretvaranjem postojećih fuzzing testova u formalne specifikacije, nakon čega je Claude AI model dokazao da je program bez grešaka za bilo koje ulazne podatke do 64 MB.
Tokom procesa izgradnje dokaza, AI model je bio u stanju identificirati i pripremiti ispravke za stotine grešaka koje prethodno nisu otkrivene fuzz testiranjem. Između ostalog, to je uključivalo ranjivosti prelijevanja bafera prilikom obrade određenih ulaznih podataka (npr. CVE-2026-56132 u libexpatu), kao i logičke greške. Nadalje, AI model je korišten za dokazivanje usklađenosti implementacije zlib algoritma u kernelu. Linux RFC 1950 specifikacije.
Interpreter za podskup Pythona je također generiran u Rustu, za koji je pripremljen formalni dokaz usklađenosti sa CPython semantikom korištenjem Verus alata. Za poređenje ponašanja sa CPython-om, izvršeno je preko 1.7 miliona nasumično generiranih Python programa. U 99.95% slučajeva, rezultati izvršavanja ovih programa u novoj implementaciji i u CPython-u su se poklapali, a sve pronađene razlike su bile poznati granični slučajevi.
Formalna verifikacija garantuje usklađenost sa specifikacijama, ali ne eliminiše u potpunosti sigurnosne probleme, jer rizici uzrokovani problemima višenitnosti, dinamičkim povezivanjem i anomalnim ponašanjem na stvarnom hardveru ostaju neformalizovani. Ključna prednost predloženog pristupa je što radi direktno sa binarnim datotekama, eliminišući potrebu za prepisivanjem postojećeg koda u formalno proverljivim jezicima.
izvor: opennet.ru
