Kompania Anthropic prezantoi rezultatet e eksperimenteve për përdorimin e modeleve AI për verifikimin formal të besueshmërisë dhe sigurisë së projekteve ekzistuese. Gjatë eksperimentit, përmes modeleve AI për 123 biblioteka të hapura, të testuara në infrastrukturën OSS Fuzz, u gjeneruan prova matematikore për mungesën e gabimeve gjatë punës me memorien.
Kontrolli u krye në nivelin e kodit të kompiluar të assembler-it për arkitekturën RISC-V. Sasia totale e provave të gjeneruara arriti rreth 180 milion rreshta kodi për sistemin e verifikimit Rocq Prover (rreth 600 mijë rreshta për skedarin binar me 18 mijë instruksione RISC-V). Provat u formuan përmes automatizimit të transformimit të testeve ekzistuese të fuzzing në specifikime formale, pas të cilave modeli AI Claude provonte se, për të gjitha të dhënat hyrëse deri në 64 MB, programi nuk kishte dështime.
Gjatë procesit të ndërtimit të provave, modeli AI ishte në gjendje të identifikonte dhe përgatiste korrigjime për qindra gabime që më parë nuk ishin vërtetuar gjatë testimit të fuzzing. Midis të tjerash, u identifikuan vulnerabilitete që çonin në mbushjen e tamponit gjatë përpunimit të të dhënave të caktuara hyrëse (p.sh., CVE-2026-56132 në libexpat), si edhe gabime logjike. Përveç kësaj, modeli AI u përdor për të provuar përputhshmërinë e zbatimit të algoritmit zlib në bërthamën Linux me specifikimin RFC 1950.
Po ashtu, në gjuhën Rust u gjenerua një interpretues për një nëngrup të gjuhës Python, për të cilin, me ndihmën e veglave Verus, u përgatit një provë formale për përputhshmërinë me semantikën e CPython. Për krahasimin e sjelljes me CPython, u ekzekutuan më shumë se 1.7 milion programe Python të gjeneruara rastësisht. Në 99.95% të rasteve, rezultatet e ekzekutimit të këtyre programeve në implementimin e ri dhe në CPython përputheshin, ndërsa diferencat e identifikuara ishin raste të njohura kufitare.
Verifikimi formal i kryer garanton përputhshmërinë me specifikimin, por nuk përjashton plotësisht shfaqjen e problemeve me sigurinë, pasi risqet e shkaktuara nga problemet me multithreading, lidhjen dinamike dhe sjelljen anormale të pajisjeve reale nuk mbeten të formalizuara. Avantazhi kyç i qasjes së propozuar është puna direkt me skedarët binarë, e cila lejon shmangien e nevojës për të ribërë kodin ekzistues në gjuhët e verifikueshme formalisht.
Burimi: opennet.ru
