A maior parte dos softwares está repleta de bugs, e a IA agora consegue encontrá-los e explorá-los com facilidade. As defesas padrão contra ataques cibernéticos já não são suficientes, por isso os desenvolvedores precisam de formas de provar que o código está livre de bugs. A verificação formal de software poderia oferecer essa garantia, mas historicamente exigiu anos de esforço especializado, tornando-a impraticável para a maioria dos projetos do mundo real.
Em uma colaboração com a Theorem, os pesquisadores mostram que isso está mudando. Os LLMs agora conseguem produzir provas formais em larga escala, possibilitando novos fluxos de desenvolvimento que incluem garantias de segurança comprovadas. Usando o Claude, a equipe provou propriedades de segurança no nível do código assembly (RISC-V) em mais de 100 bibliotecas de software de código aberto do mundo real. Até onde sabem, este é o primeiro esforço em larga escala a usar IA para aplicar verificação formal a software de produção nesse nível. Ao escrever as provas, o Claude também revelou bugs que haviam escapado à detecção por anos, apesar de trilhões de execuções de teste.
A abordagem se baseia em um método de longa data: os desenvolvedores traduzem o código para um modelo matemático e tentam provar que ele sempre segue regras de segurança definidas. Provas que falham apontam para prováveis bugs. Tradicionalmente, as provas podem ser muitas vezes maiores que o código original e exigem habilidades raras e especializadas. Construir o kernel seL4 levou dois anos-pessoa, mas verificá-lo levou 20.
Para testar a abordagem, o Claude provou que 123 programas de código aberto sempre terminarão normalmente, sem erros de segurança de memória ou asserções falhas, para qualquer entrada abaixo de 64 MB, sob premissas declaradas sobre o ambiente de execução. Os pesquisadores reconhecem que isso está longe de corrigir todos os bugs possíveis, mas afirmam que oferece um roteiro. Um subconjunto das provas está sendo publicado para que outros possam verificá-las e reutilizá-las.
Fonte: Hacker News · Resumido por HeadlinesBriefing