Anthropic: Claude escreveu provas verificadas por máquina para o código compilado de 123 bibliotecas de código aberto
A Frontier Red Team da Anthropic e a empresa de métodos formais Theorem usaram o Claude para provar que 239 pontos de entrada de testes de fuzzing em 123 bibliotecas do OSS-Fuzz não podem falhar com entradas inferiores a 64 MB num ambiente modelado. O trabalho revelou bugs que anos de fuzzing não tinham detetado, mas as provas têm ressalvas importantes.
A Anthropic publicou uma investigação em que a sua Frontier Red Team, juntamente com a empresa de métodos formais Theorem, usou o Claude para verificar formalmente propriedades de segurança de 123 bibliotecas de código aberto do projeto OSS-Fuzz da Google, abrangendo 239 pontos de entrada de fuzzing. As provas incidem sobre código máquina RISC-V compilado, não sobre o código-fonte.
Como funcionou
Cada teste de fuzzing existente foi transformado numa especificação formal: o teste compilado não pode falhar (por exemplo, por um erro de memória detetado pelo AddressSanitizer ou uma asserção falhada) com nenhuma entrada inferior a 64 MB num ambiente modelado. A Theorem forneceu modelos formais do conjunto de instruções RISC-V e do comportamento de processos Linux; o Claude escreveu as provas e o verificador Rocq validou-as. Segundo a DevOps.com, o Claude produziu cerca de 180 milhões de linhas de provas em poucas semanas.
Bugs que o fuzzing não viu
O Claude podia corrigir os bugs que encontrava, e surgiram centenas. Entre os exemplos, um underflow de contador num descompressor que só causava escrita fora dos limites com entradas de cerca de 20 MB, e um erro de leitura num descodificador de imagens que exigia 64 MB. A Anthropic diz ter penalizado patches grandes e auditado-os para que o modelo não reescrevesse programas que trivialmente nunca falham.
Limites
A Anthropic sublinha que “verificado formalmente” não significa “sem bugs”. As provas pressupõem binários RISC-V de uma só thread, ligados estaticamente com musl libc, enquanto a maior parte do software Linux corre em x86 ou ARM com glibc; o AddressSanitizer não apanha todos os erros de memória e nem todos os pontos de entrada foram verificados. O custo é outra limitação: as provas podem consumir centenas de milhões de tokens. Os ganhos de eficiência dos novos modelos Claude vêm de testes internos da Anthropic. Parte das provas foi publicada no GitHub.
Também disponível em: EnglishСаха тылаРусскийEspañol中文العربية