The Pulse
Anthropic usa Claude per produrre dimostrazioni relative a 239 test in 123 librerie
Anthropic afferma che Claude e la società di verifica Theorem hanno prodotto dimostrazioni verificate automaticamente per 239 punti d’ingresso dei fuzz test in 123 librerie open source. Le dimostrazioni riguardano specifici binari RISC-V e
AI.info Team · Scritto con l’IA · verificato ·
Anthropic afferma che Claude ha contribuito a dimostrare che 239 punti d’ingresso dei test software in 123 librerie open source non possono causare crash nelle condizioni specificate. La società ha pubblicato i risultati il 22 ottobre, descrivendo un lavoro svolto con la società di verifica formale Theorem nell’arco di alcune settimane, durante il quale sono stati individuati anche bug che gli sviluppatori possono correggere.
«Nell’arco di alcune settimane, Claude ha corretto i bug che aveva trovato e poi ha dimostrato che nessun input (fino a 64 MB) provoca crash in 239 punti d’ingresso distribuiti tra 123 diverse librerie OSS-Fuzz». Keane Lucas, Aengus Lynch e altri, Anthropic Frontier Red Team
Le dimostrazioni riguardano programmi RISC-V compilati
Il gruppo è partito dai punti d’ingresso dei fuzz test di OSS-Fuzz di Google, un programma che sottopone continuamente a test i progetti open source idonei. I fuzzer generano grandi quantità di input alla ricerca di crash, ma non possono provare ogni input possibile. Anthropic e Theorem hanno invece chiesto a Claude di dimostrare che ciascun test selezionato non avrebbe causato crash con nessun input inferiore a 64 MB.
Le conclusioni riguardano binari RISC-V compilati, non direttamente il codice sorgente o ogni funzione di una libreria. I programmi rappresentati nel modello sono binari a thread singolo, collegati staticamente, che girano su Linux con un limite di memoria fisso. Claude ha scritto le dimostrazioni in Rocq, un assistente alla dimostrazione il cui kernel verifica che ciascuna dimostrazione soddisfi la relativa specifica formale.
Anthropic riferisce di aver prodotto in totale circa 180 milioni di righe di codice di dimostrazione in Rocq. Una dimostrazione tipica contava all’incirca 600.000 righe e riguardava un binario con una lunghezza mediana di 18.000 istruzioni RISC-V. La società afferma che pubblicherà una parte delle dimostrazioni, insieme ai modelli formali dei processi RISC-V e Linux.
Il tentativo di dimostrare la sicurezza ha portato alla luce dei bug
Secondo Anthropic, il lavoro sulle dimostrazioni ha permesso anche di trovare centinaia di bug. In un caso, Claude ha individuato un underflow di un contatore che causava una scrittura fuori dai limiti, ma solo con input di circa 20 MB disposti secondo una configurazione rara. Un’altra lettura fuori dai limiti richiedeva un input di 64 MB e più di 2 GB di memoria.
Alcuni dei problemi individuati non erano bug che causavano crash. Anthropic afferma che Claude ha trovato anche errori logici, tra cui un caso in cui una funzionalità pensata per limitare i file caricabili da un’applicazione non veniva sempre applicata. La società afferma di aver lasciato che Claude correggesse i bug scoperti e poi rigenerasse la specifica prima di tentare una nuova dimostrazione.
«Verificato» ha comunque un significato circoscritto
Una dimostrazione stabilisce che un determinato binario soddisfa una determinata specifica nell’ambito di un determinato modello della macchina. Non stabilisce che la specifica comprenda tutti i rischi del mondo reale, né che un’intera libreria sia priva di bug. Anthropic osserva che il lavoro non ha riguardato tutti i punti d’ingresso dei test e che AddressSanitizer, uno dei controlli utilizzati, non rileva tutti i bug di sicurezza della memoria.
Contano anche le ipotesi relative all’hardware e al sistema operativo. Le dimostrazioni si basano su modelli di RISC-V e Linux, mentre molti programmi in uso girano su sistemi x86 o ARM e adottano modalità di collegamento diverse. Anthropic afferma che le differenze tra questi ambienti e il modello formale possono lasciare alcuni comportamenti fuori dall’ambito della dimostrazione.
Theorem apre la procedura ai manutentori
Theorem afferma di offrire gratuitamente il suo servizio OSS Verify ai progetti open source idonei. I manutentori possono richiedere la verifica degli obiettivi dei fuzz test, anche se i progetti devono soddisfare i criteri di ammissibilità del servizio e il suo processo di compilazione richiede attualmente binari RISC-V collegati staticamente.
I risultati di Anthropic sostengono una tesi circoscritta: per i binari e i test verificati, nelle condizioni rappresentate dal modello, gli input esaminati non producono i crash specificati. Le dimostrazioni e le specifiche pubblicate consentono ad altri di esaminare questa tesi, ma non certificano tutte le 123 librerie per ogni piattaforma o utilizzo.