{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/it\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic sta sviluppando una tecnica per la verifica formale del software esistente utilizzando l'IA","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
L'azienda Anthropic ha presentato i risultati di esperimenti sull'uso dei modelli AI per la verifica formale dell'affidabilit\u00e0 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. <\/p>\n
Il controllo \u00e8 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\u00e9 il modello AI Claude ha dimostrato che con qualsiasi input fino a 64 MB non si verificano malfunzionamenti nel programma. <\/p>\n
Nel processo di costruzione delle dimostrazioni, il modello AI \u00e8 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\u00e0 che portano a overflow del buffer durante l'elaborazione di determinate input (ad esempio, CVE-2026-56132 in libexpat), cos\u00ec come errori logici. Inoltre, il modello AI \u00e8 stato utilizzato per dimostrare la conformit\u00e0 dell'implementazione dell'algoritmo zlib nel kernel Linux alla specifica RFC 1950.<\/p>\n
\u00c8 stato inoltre generato un interprete in Rust per un sottoinsieme del linguaggio Python, per il quale \u00e8 stata preparata una dimostrazione formale di conformit\u00e0 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.<\/p>\n
La verifica formale effettuata garantisce la conformit\u00e0 alle specifiche, ma non elimina completamente il rischio di problemi di sicurezza, poich\u00e9 non rimangono formalizzati i rischi causati da problemi di multithreading, linking dinamico e comportamenti anomali dell'hardware reale. Il principale vantaggio dell'approccio proposto \u00e8 il lavoro diretto con i file binari, che consente di evitare la necessit\u00e0 di riscrivere il codice esistente in linguaggi formalmente verificabili. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"