Anthropic afirmă că Claude a demonstrat proprietăți de securitate pentru 123 de biblioteci

Pe 22 octombrie 2026, Anthropic a publicat un studiu în care a raportat că, în colaborare cu Theorem, Claude a produs demonstrații formale verificate automat ale unor proprietăți de securitate la nivelul codului de asamblare RISC-V pentru 239 de puncte de intrare ale testelor de fuzzing din 123 de biblioteci open-source.

Potrivit Anthropic, Claude a remediat erorile găsite, apoi a demonstrat că programele se vor încheia întotdeauna în mod normal, fără să declanșeze erori de siguranță a memoriei sau să eșueze la verificarea aserțiunilor, pentru orice intrare mai mică de 64 MB și pentru orice răspuns al sistemului de operare Linux și orice configurație a memoriei modelate. Demonstrațiile presupun că programul rulează ca binar static cu un singur fir de execuție, cu o cantitate fixă de memorie disponibilă, pe un procesor RISC-V care folosește Linux. Anthropic a declarat că demonstrațiile însumează aproximativ 180 de milioane de linii de cod Rocq, iar o demonstrație tipică are aproximativ 600.000 de linii și acoperă binare cu o lungime mediană de 18.000 de instrucțiuni RISC-V. Compania a afirmat că, din câte știe, acesta este primul efort de amploare în care IA este folosită pentru a aplica verificarea formală unui software de producție la nivelul codului de asamblare.

O parte dintre demonstrații, împreună cu semantica RISC-V și a sistemului de operare pe care se bazează, este publicată pe GitHub. Anthropic a spus că publică și componentele de încredere construite pentru proiect care nu erau deja disponibile public, demonstrațiile complete pentru testele de fuzzing care nu au necesitat remedieri și specificațiile testelor de fuzzing pe care nu le-a putut demonstra, dar că nu publică demonstrațiile care ar putea dezvălui o eroare neremediată.

Transformarea testelor de fuzzing în demonstrații formale

Metoda transformă testul de fuzzing existent și compilabil al fiecărei biblioteci într-o specificație formală care codifică o singură regulă: testul nu se blochează pentru nicio intrare mai mică de 64 MB. Specificația este definită pentru instrucțiunile RISC-V compilate, folosind semantica formală a setului de instrucțiuni RISC-V și a proceselor Linux elaborată de Theorem, iar verificatorul de demonstrații Rocq verifică fiecare demonstrație finalizată în raport cu specificația. Anthropic afirmă că astfel rămân doar trei componente în care dezvoltatorii trebuie să aibă încredere: modelele formale pentru RISC-V și procesele Linux, enunțurile exacte ale teoremelor și verificatorul Rocq însuși.

Anthropic a declarat că a aplicat acest proces la sute de proiecte din inițiativa OSS-Fuzz a Google, care oferă testare continuă prin fuzzing pentru proiectele open-source eligibile și instrumentează automat programele C și C++ cu AddressSanitizer, un instrument care provoacă blocarea programului ori de câte ori memoria este accesată necorespunzător. O anexă datată 22 octombrie 2026 prezintă teorema completă demonstrată: pentru toate intrările mai mici de 64 MiB și toate configurațiile memoriei, nici binarul instrumentat cu ASan, nici cel neinstrumentat nu generează erori de execuție, nu se opresc forțat și nu manifestă comportamente nemodelate; în plus, ambele produc trasee identice de citire și scriere, au același comportament la ieșire și lasă sistemul de fișiere în aceeași stare finală.

Anexa precizează că, pe parcursul efortului, Claude a scris aproximativ un miliard de linii de cod Rocq, dintre care aproximativ 180 de milioane au trecut de verificatorul de demonstrații; punctul de intrare al analizatorului cJSON, alcătuit din 391 de linii, a primit o demonstrație de 630.000 de linii, în timp ce fftw3, cu 51.000 de linii incluse, a primit o demonstrație de 480.000 de linii. Întrucât Claude a avut permisiunea să modifice codul înainte de finalizarea unei demonstrații, Anthropic a penalizat modificările, a oferit un bonus suplimentar pentru demonstrarea intrărilor afectate de o modificare și a înregistrat și auditat modificările pentru a descuraja exploatarea mecanismului de recompensare.

Erori descoperite în timpul încercărilor de demonstrare

Anthropic relatează că încercările de demonstrare au scos la iveală sute de erori, multe dintre ele greu de găsit prin fuzzing. În timp ce demonstra proprietățile punctului de intrare al unei biblioteci, Claude a descoperit o scădere sub limita inferioară a contorului într-un program de decomprimare, care provoca o scriere în afara limitelor, dar numai pentru intrări de aproximativ 20 MB cu o configurație rară și specifică. Printre celelalte descoperiri s-au numărat o citire în afara limitelor într-un decodor de imagini, pentru care era necesară o intrare de 64 MB și peste 2 GB de memorie; o citire în afara limitelor care necesita o anumită secvență de apeluri prin două handle-uri către același fișier; și redescoperirea vulnerabilității CVE-2026-56132 din libexpat, care necesita o intrare imbricată profund.

Claude a găsit și erori logice care nu provoacă niciodată blocarea programului, inclusiv o restricție privind fișierele pe care le poate încărca o aplicație, care nu este aplicată întotdeauna. Anthropic a declarat că încercările de verificare a mai multor aplicații critice, utilizate pe scară largă, au scos la iveală o eroare logică necunoscută anterior, care rămăsese latentă mai bine de un deceniu, și că, în timpul unui efort de verificare a unui cititor PDF utilizat pe scară largă, a găsit într-o săptămână tot atâtea erori de securitate câte sunt raportate de obicei într-un an.

Experimente suplimentare și constatări privind eficiența

Dincolo de OSS-Fuzz, Anthropic i-a cerut lui Claude să redacteze o specificație formală pentru RFC 1950, documentul tehnic care definește formatul de comprimare zlib, apoi să demonstreze că implementarea zlib din nucleul Linux îl implementează corect. Claude a demonstrat direct proprietățile binarului compilat pentru x86, folosind semantica formală a setului de instrucțiuni x86 generată de Claude, iar Anthropic a declarat că a repetat procesul pentru alte șase biblioteci utilizate pe scară largă și a găsit erori minore, imposibil de exploatat, în cazuri-limită, care sunt raportate proiectelor din amonte. Compania a mai raportat că generarea semanticii x86 a identificat sute de greșeli în documentația oficială de referință și un număr mai mic de erori chiar în hardware și că executarea pas cu pas a semanticii poate porni un mediu de utilizator Ubuntu pe un nucleu Linux.

Într-un alt experiment, Claude a construit în Rust un interpretor pentru o mare parte din limbajul Python și a demonstrat, folosind instrumentul de verificare Verus, că acesta respectă semantica CPython descrisă într-un articol academic. Anexa tehnică precizează că au fost demonstrate toate cele 17 niveluri ale interpretorului, teorema stabilind că „Ori de câte ori interpretorul returnează un rezultat, acesta este cel prescris de semantica formală”. Anthropic a declarat că testarea empirică a 1,7 milioane de programe Python generate aleatoriu a relevat un comportament identic cu cel al CPython în 99,95% dintre teste; dintre cele șapte erori introduse intenționat, cinci au trecut nedetectate la testarea aleatorie, în timp ce toate șapte au invalidat demonstrația.

Pentru a măsura eficiența, Anthropic a creat 36 de sarcini mici de verificare, reducând puncte de intrare reale din OSS-Fuzz și obținând programe cu 283–2.491 de instrucțiuni, ale căror intrări erau limitate la 64 de octeți, iar AddressSanitizer era înlocuit cu un mediu de execuție „mini-ASan” de aproximativ 100 de instrucțiuni. Anthropic relatează că Opus 5.5 demonstrează jumătate dintre sarcini folosind cu aproximativ 40% mai puține tokenuri decât Opus 5. Anthropic mai relatează că agenții cărora li s-a permis să copieze demonstrațiile unii de la alții într-un spațiu de lucru comun au avut nevoie de cu 17% mai puține tokenuri decât agenții care au lucrat singuri, că unii au reușit după ce eșuaseră anterior când lucrau individual și că agenții care au lucrat singuri nu au reușit să finalizeze două dintre demonstrații. Compania a declarat că același efect de reutilizare s-a manifestat la scară largă în timpul efortului OSS-Fuzz, când echipele de agenți au copiat demonstrații finalizate și le-au adaptat, deoarece o mare parte din fiecare demonstrație vizează codul comun de inițializare pentru mediul de execuție C și AddressSanitizer.

Limitările declarate și programul OSS Verify

Anthropic precizează că demonstrațiile nu înseamnă că bibliotecile nu conțin erori: erorile rămase s-ar putea afla în componentele considerate de încredere sau în afara domeniului acoperit de demonstrații. Demonstrațiile vizează binare RISC-V statice, cu execuție pe un singur fir și legate cu musl libc, în timp ce majoritatea utilizatorilor rulează aceste biblioteci pe x86 sau ARM și le leagă dinamic cu glibc; în plus, AddressSanitizer nu detectează toate erorile de siguranță a memoriei. Compania a declarat că se așteaptă ca aceste limitări să poată fi depășite pe măsură ce modelele se îmbunătățesc.

Theorem oferă gratuit aceeași conductă de procesare proiectelor open-source eligibile, prin programul său OSS Verify. Înscrierea se face printr-o cerere de integrare care adaugă fișierele project.yaml, Dockerfile și build.sh în depozitul programului, iar Theorem afirmă că evaluează proiectele după criterii similare celor folosite de OSS-Fuzz, acordând prioritate infrastructurii critice utilizate pe scară largă. Potrivit Theorem, administratorii proiectelor primesc o demonstrație Rocq, verificată de nucleul Rocq, care atestă că fiecare țintă de fuzzing nu se blochează la nicio intrare de până la 64 MiB; erorile descoperite în timpul procesului de demonstrare sunt comunicate în mod privat administratorilor prin e-mail, fără un termen-limită pentru divulgare, iar producerea demonstrațiilor poate dura mai multe zile. Foaia de parcurs a Theorem vizează verificarea întregului ecosistem Nix, inclusiv a infrastructurii critice precum glibc, OpenSSL și cURL.