L'azienda Anthropic ha presentato i risultati di esperimenti sull'uso dei modelli AI per la verifica formale dell'affidabilità e sicurezza di progetti esistenti. Durante l'esperimento, utilizzando modelli AI, sono state generate dimostrazioni matematiche dell'assenza di errori nella gestione della memoria per 123 librerie open source, testate nell'infrastruttura OSS Fuzz.
Il controllo è stato effettuato a livello di codice assembly compilato per l'architettura RISC-V. Il volume totale delle dimostrazioni generate ha raggiunto circa 180 milioni di righe di codice per il sistema di verifica Rocq Prover (circa 600.000 righe per un file binario contenente 18.000 istruzioni RISC-V). Le dimostrazioni sono state create convertendo automaticamente i test di fuzzing esistenti in specifiche formali, dopodiché il modello AI Claude ha dimostrato che con qualsiasi input fino a 64 MB non si verificano malfunzionamenti nel programma.
Nel processo di costruzione delle dimostrazioni, il modello AI è stato in grado di rilevare e preparare correzioni per centinaia di errori precedentemente non notati durante i test di fuzzing. Tra l'altro, sono state identificate vulnerabilità che portano a overflow del buffer durante l'elaborazione di determinate input (ad esempio, CVE-2026-56132 in libexpat), così come errori logici. Inoltre, il modello AI è stato utilizzato per dimostrare la conformità dell'implementazione dell'algoritmo zlib nel kernel Linux alla specifica RFC 1950.
È stato inoltre generato un interprete in Rust per un sottoinsieme del linguaggio Python, per il quale è stata preparata una dimostrazione formale di conformità alla semantica CPython utilizzando gli strumenti di Verus. Per confrontare il comportamento con CPython, sono stati eseguiti oltre 1,7 milioni di programmi Python generati casualmente. Nel 99,95% dei casi, i risultati dell'esecuzione di questi programmi nella nuova implementazione e in CPython sono stati coincidenti, e le discrepanze osservate si sono rivelate casi limite noti.
La verifica formale effettuata garantisce la conformità alle specifiche, ma non elimina completamente il rischio di problemi di sicurezza, poiché non rimangono formalizzati i rischi causati da problemi di multithreading, linking dinamico e comportamenti anomali dell'hardware reale. Il principale vantaggio dell'approccio proposto è il lavoro diretto con i file binari, che consente di evitare la necessità di riscrivere il codice esistente in linguaggi formalmente verificabili.
Fonte: opennet.ru
