Verifica formale con Claude: dimostrazioni per 123 librerie open source

Il 22 ottobre il Frontier Red Team di Anthropic, insieme alla società Theorem, ha pubblicato uno studio in cui Claude ha scritto dimostrazioni formali di sicurezza per 123 librerie open source del progetto OSS-Fuzz. Le dimostrazioni riguardano il codice RISC-V compilato, non il codice sorgente. Secondo gli autori, è la prima verifica formale di software di produzione a livello assembly con l’aiuto dell’IA su questa scala.

Come funziona la verifica formale con Claude?

La verifica formale è una dimostrazione matematica che un programma ha una certa proprietà per ogni input possibile, non solo per quelli che qualcuno ha testato. Il problema è che finora richiedeva anni di lavoro di esperti. Un confronto dallo studio: la verifica del kernel seL4 ha richiesto circa 20 anni-persona, la sua scrittura due.

La pipeline dello studio è questa:

1. Il punto di partenza sono i test di fuzzing esistenti di OSS-Fuzz (un progetto di Google che bombarda senza sosta le librerie con dati casuali).
2. La libreria, insieme al test, viene compilata in un eseguibile RISC-V.
3. Dalla semantica del processore RISC-V e di un processo Linux sviluppata da Theorem nasce automaticamente una specifica: il programma deve sempre terminare normalmente, senza errori di memoria né asserzioni fallite.
4. Claude scrive la dimostrazione e il verificatore Rocq conferma che soddisfa la specifica.
5. Quando Claude trova un bug, corregge il codice, la specifica viene rigenerata e la dimostrazione viene ricostruita da capo.

La garanzia copre ogni input inferiore a 64 MB e ogni risposta del sistema e disposizione della memoria modellate (assumendo un programma statico e single-thread su RISC-V e Linux).

Quali numeri ha fornito Anthropic?

1. 239 punti di ingresso in 123 librerie.
2. In totale circa 180 milioni di righe di dimostrazioni in Rocq; una dimostrazione tipica ha circa 600.000 righe e riguarda un programma con una mediana di 18.000 istruzioni RISC-V.
3. Il tutto ha richiesto qualche settimana.
4. Su 36 piccoli compiti, Opus 5.5 ne ha dimostrato la metà consumando circa il 40% di token in meno rispetto a Opus 5, e gli agenti che lavoravano in uno spazio condiviso hanno consumato il 17% in meno che da soli.

Curiosamente, la dimostrazione per cpp-httplib ha richiesto di provare che l’albero rosso-nero di libc++ ha una profondità limitata logaritmicamente, perché solo così si poteva escludere uno stack overflow nel distruttore di std::set.

Quali bug ha trovato Claude?

Secondo gli autori, il processo ha scoperto centinaia di bug sopravvissuti ad anni di fuzzing. Esempi dal post:

1. Un underflow di un contatore in un decompressore, che portava a una scrittura fuori dal buffer, ma solo con un input di circa 20 MB dalla struttura rara.
2. Una lettura fuori dal buffer in un decoder di immagini, che richiedeva un input di 64 MB e oltre 2 GB di memoria.
3. Una lettura fuori dal buffer che compariva solo con una specifica sequenza di chiamate su due handle dello stesso file.
4. La riscoperta di CVE-2026-56132 in libexpat (richiedeva un input profondamente annidato).
5. Un bug logico: una funzione che limitava l’accesso ai file non sempre funzionava, anche se nulla andava in crash.

A questo si aggiungono tre esperimenti. Claude ha scritto una specifica formale della RFC 1950 e ha dimostrato su binari x86 che la zlib del kernel Linux la implementa correttamente. Ha anche costruito in Rust un interprete di un sottoinsieme di Python che, su 1,7 milioni di programmi casuali, si è comportato come CPython nel 99,95% dei casi. E un tentativo di verificare un noto lettore PDF ha trovato in una settimana tante vulnerabilità quante se ne segnalano di solito in un anno.

È la stessa direzione di PHP2Shell e di Claude Mythos in Bank of America: i modelli di IA trovano bug che persone e strumenti classici non hanno individuato per anni. Solo che questa volta non finisce solo con una patch, ma con una dimostrazione.

A cosa fare attenzione?

Primo, a che cosa significa «verificato». Gli autori lo scrivono chiaramente: la verifica formale non significa codice privo di bug (in originale «»Formally verified« does not mean »bug-free.«»). Una dimostrazione vale quanto la specifica, i modelli di RISC-V e Linux e lo stesso verificatore Rocq.

Secondo, all’ambito. Le dimostrazioni riguardano binari RISC-V statici e single-thread con musl, mentre la maggior parte di noi esegue codice su x86 o ARM con glibc. Non coprono nemmeno il codice morto né i casi in cui è il programma che chiama la libreria a corrompere la memoria.

Terzo, al costo. Singole dimostrazioni possono consumare centinaia di milioni di token, cosa che gli stessi autori indicano come il limite principale.

Parte delle dimostrazioni è già su GitHub (oss-verify-proofs), insieme alla semantica di RISC-V e Linux. Il resto aspetta, perché potrebbe rivelare bug non ancora corretti.

FAQ

Che cos’è la verifica formale?

È una dimostrazione matematica, controllata da un programma, che il codice ha una certa proprietà per tutti gli input, ad esempio che non scrive mai fuori dal buffer. Test e fuzzing controllano solo casi selezionati.

Le librerie verificate sono prive di bug?

No. La dimostrazione garantisce l’assenza di crash solo nel modello descritto (RISC-V, Linux, input inferiore a 64 MB, un solo thread). I bug possono annidarsi nella specifica, nel modello della macchina o al di fuori di questo ambito.

Posso far verificare il mio progetto?

Theorem gestisce OSS Verify, un programma gratuito per progetti open source selezionati. Il maintainer del progetto si candida con una pull request contenente i file project.yaml, Dockerfile e build.sh, in modo simile a OSS-Fuzz. Bisogna mettere in conto di spostare la build su binari statici riscv64.