Claude di Anthropic scrive codice e ne prova automaticamente la sicurezza
Anthropic, in collaborazione con il partner Theorem, ha utilizzato il modello Claude per verificare matematicamente codici software esistenti e generare prove formali della loro correttezza. Questo approccio affronta un problema fondamentale del software generato da AI, ma presenta anche limiti pratici rigorosi.
Verifica formale del codice
Provare che un software funzioni senza errori in tutte le circostanze è sempre stato un processo costoso e dispendioso in termini di tempo. Ad esempio, un team di specialisti ha impiegato 20 anni-persona solo per verificare formalmente il piccolo kernel del sistema operativo seL4. Pertanto, questo metodo è stato riservato a casi estremi come il software avionico di Airbus.
Anthropic ha utilizzato il suo modello Claude per prendere in carico il lavoro di verifica. In poche settimane, Claude ha prodotto circa 180 milioni di righe di codice di prova matematica, basandosi su programmi di test di 123 librerie open-source del progetto di sicurezza OSS-Fuzz di Google.
Processo di verifica
Invece di scrivere nuovo codice, Claude ha verificato il software esistente traducendo i test di crash in problemi matematici, analizzando il codice macchina compilato e producendo prove estese. Un programma di verifica indipendente chiamato Rocq controlla automaticamente queste prove, e secondo Anthropic, il processo richiede quasi nessuna revisione umana. I ricercatori lo definiscono "generazione di prove completamente autonoma", anche se gli strumenti e le basi formali sono stati costruiti da umani presso Theorem.
Scoperta di bug
Mentre generava le prove, Claude ha riscontrato centinaia di bug e ha potuto correggerli da solo. Molti di questi bug sarebbero sfuggiti ai test convenzionali perché si manifestano solo in condizioni molto specifiche, come file di input insolitamente grandi o una particolare sequenza di accessi, affermano i ricercatori.
Ad esempio, durante un tentativo di verificare un lettore PDF ampiamente utilizzato, il team ha trovato tanti bug di sicurezza in una settimana quanti ne vengono tipicamente segnalati per quel software in un intero anno. In un'altra applicazione, Claude ha rilevato un errore logico che era rimasto non rilevato per oltre un decennio. Anche quando una prova completa fallisce, Anthropic afferma che il tentativo rivela comunque bug reali.
Limiti della verifica formale
Anthropic riconosce che "verificato formalmente" non significa "senza errori". Le prove valgono solo in condizioni rigorose: una specifica architettura del processore, programmi single-threaded e input inferiori a 64 MB. In pratica, queste librerie funzionano su hardware diverso e in diverse configurazioni.
Il costo computazionale è elevato, con singole prove che arrivano a centinaia di milioni di token. Anthropic non riporta i costi totali del progetto. Tuttavia, se l'AI può verificare il proprio codice, gli sviluppatori possono fare maggiore affidamento sul software generato dall'AI e spendere meno tempo a revisionarlo. Questo risparmia costi non solo sulla verifica, ma sull'intero processo di codifica. Una prova più piccola ha anche dimostrato che le prove sono riutilizzabili e che i modelli più recenti stanno diventando più efficienti: Opus 5.5 risolve la metà delle prove con circa il 40% in meno di token rispetto a Opus 5.
Implicazioni per l'automazione del software
Il progetto rafforza il caso per l'automazione del software. Se l'AI può scrivere codice e garantirne la correttezza in condizioni definite, la domanda passa da "L'AI può programmare?" a "L'AI può provare che il codice che scrive è sicuro?". Se la risposta è sì, le conseguenze potrebbero andare ben oltre gli attuali strumenti di codifica.
Ad esempio, Anthropic si aspetta che la verifica formale con l'AI diventi presto pratica quanto il test standard, e la roadmap di Theorem mira già alle infrastrutture critiche come glibc, OpenSSL e cURL.