Compania Anthropic a prezentat rezultatele experimentelor privind utilizarea modelelor AI pentru verificarea formală a fiabilității și securității proiectelor existente. În cadrul experimentului, cu ajutorul modelelor AI, au fost generate dovezi matematice privind absența erorilor în gestionarea memoriei pentru 123 de biblioteci open-source testate în infrastructura OSS Fuzz.
Verificarea a fost efectuată la nivelul codului de asamblare compilat pentru arhitectura RISC-V. Volumul total de dovezi generate a fost de aproximativ 180 de milioane de linii de cod pentru sistemul de verificare Rocq Prover (aproximativ 600 de mii de linii pentru un fișier binar cu 18 mii de instrucțiuni RISC-V). Dovezile au fost generate prin transformarea automată a testelor existente fuzzing în specificații formale, după care modelul AI Claude a demonstrat că, pentru orice date de intrare de până la 64 MB, programul nu suferă eșecuri.
În procesul de construire a dovezilor, modelul AI a reușit să identifice și să pregătească remedieri pentru sute de erori, care anterior nu fuseseră observate în testarea fuzzing. Printre altele, au fost identificate vulnerabilități care duc la depășirea buffer-ului la procesarea anumitor date de intrare (de exemplu, CVE-2026-56132 în libexpat), precum și erori logice. În plus, modelul AI a fost utilizat pentru a demonstra conformitatea implementării algoritmului zlib în nucleul Linux cu specificația RFC 1950.
De asemenea, un interpret pe limbajul Rust a fost generat pentru un subset al limbajului Python, pentru care, cu ajutorul instrumentului Verus, a fost pregătită o dovadă formală a conformității cu semantica CPython. Pentru a compara comportamentele cu CPython, au fost efectuate peste 1,7 milioane de programe Python generate aleatoriu. În 99,95% din cazuri, rezultatele execuției acestor programe în noua implementare și în CPython s-au coincis, iar discrepanțele observate s-au dovedit a fi cazuri limită cunoscute.
Verificarea formală efectuată garantează conformitatea cu specificația, dar nu elimină complet apariția problemelor de securitate, deoarece riscurile cauzate de problemele de multitasking, legarea dinamică și comportamentul anormal al echipamentului real rămân neachitate. Principalul avantaj al abordării propuse este lucrul direct cu fișierele binare, ceea ce elimină necesitatea de a rescrie codul existent în limbaje formal verificate.
Sursa: opennet.ro
