A empresa Anthropic apresentou os resultados de experimentos sobre o uso de modelos de IA para verificação formal da confiabilidade e segurança de projetos já existentes. Durante o experimento, foram geradas provas matemáticas da ausência de erros no gerenciamento de memória utilizando modelos de IA em 123 bibliotecas abertas, testadas na infraestrutura OSS Fuzz.
A verificação foi realizada no nível do código assembly compilado para a arquitetura RISC-V. O volume total de provas geradas foi de cerca de 180 milhões de linhas de código para o sistema de verificação Rocq Prover (aproximadamente 600 mil linhas por arquivo binário com 18 mil instruções RISC-V). As provas foram formadas por meio da conversão automática de testes de fuzzing existentes em especificações formais, após o que o modelo de IA Claude provou que, para quaisquer entradas de até 64 MB, não ocorriam falhas no programa.
No processo de construção das provas, o modelo de IA conseguiu identificar e preparar correções para centenas de erros que anteriormente não foram detectados durante o teste de fuzzing. Entre outros, foram descobertas vulnerabilidades que levam a overflow de buffer ao processar certos dados de entrada (por exemplo, CVE-2026-56132 no libexpat), além de erros lógicos. Além disso, o modelo de IA foi utilizado para provar a conformidade da implementação do algoritmo zlib no núcleo do Linux com a especificação RFC 1950.
Também foi gerador um interpretador em Rust para um subconjunto da linguagem Python, para o qual foi preparada uma prova formal de conformidade com a semântica do CPython utilizando a ferramenta Verus. Para comparar o comportamento com o CPython, mais de 1,7 milhões de programas Python aleatoriamente gerados foram executados. Em 99,95% dos casos, os resultados da execução desses programas na nova implementação e no CPython coincidiram, e as divergências identificadas se mostraram casos extremos conhecidos.
A verificação formal realizada garante conformidade com a especificação, mas não elimina completamente a possibilidade de problemas de segurança, uma vez que não ficam formalizados os riscos causados por problemas de multithreading, vinculação dinâmica e comportamento anômalo do hardware real. A principal vantagem da abordagem proposta é o trabalho diretamente com arquivos binários, o que permite evitar a necessidade de reescrever o código existente em linguagens formalmente verificáveis.
Fonte: opennet.ru
