Resumo Técnico: Verificação de Modelos Agênticos

Declaração do Problema

A verificação de código de sistemas gerado por Modelos de Linguagem Grandes (LLMs) apresenta desafios únicos que agravam as dificuldades existentes na verificação formal. Embora os LLMs possam gerar corpos substanciais de código para sistemas operacionais, compiladores e drivers em linguagens como C e Rust, as bases de código resultantes frequentemente carecem de especificações formais explícitas. Além disso, os contratos de segurança no código gerado por LLMs são frequentemente codificados implicitamente nos locais de chamada em vez de serem aplicados nas fronteiras das funções.

Essa codificação implícita leva a um modo de falha específico: funções auxiliares (por exemplo, leitores de indexação por bytes, escritores de aritmética de deslocamento) frequentemente carecem de guardas de limites e estouro, dependendo da lógica do chamador circundante para manter invariantes. Consequentemente, o código funciona corretamente em entrada bem-formada, mas falha em entrada adversária ou elaborada. Ferramentas de verificação tradicionais lutam aqui porque ou super-reportam (sinalizando auxiliares como quebrados sem contexto) ou sub-reportam (perdendo bugs porque os chamadores atuais não os acionam). Adicionalmente, abordagens existentes de verificação baseadas em LLM frequentemente carecem de solidez para segurança aritmética e de memória, enquanto verificadores dedutivos tradicionais lutam com a escala e a natureza pesada de loops do código de sistemas e carecem da capacidade de gerar contraexemplos concretos.

Metodologia: Verificação de Modelos Agênticos

Os autores propõem a Verificação de Modelos Agênticos, um paradigma de verificação que acopla agentes LLM a um backend de verificação de modelo limitado (BMC) sob o princípio: "Agentes propõem, solucionadores verificam."

O sistema, instanciado como BMC-Agent, opera através de um pipeline onde agentes LLM lidam com tarefas que exigem julgamento semântico, enquanto um backend BMC determinístico (CBMC para C, Kani para Rust) descarta todas as decisões relevantes para a solidez.

Compromissos Arquiteturais Principais

1. Inferência de Especificação Top-Down:

   • Agentes inferem pré-condições e pós-condições por função de cima para baixo a partir do contexto do chamador.
   • Especificações são geradas em uma Linguagem de Domínio Específico (DSL) restrita que traduz deterministicamente nas primitivas nativas assume/assert do backend.
   • O sistema gera especificações de correção funcional (por exemplo, expressões de equivalência de referência, identidades algébricas) além de verificações defensivas de ausência de pânico, elevando a verificação da mera evitação de falhas à fidelidade comportamental.

2. Verificação Composicional:

   • A verificação é decomposta por função. Cada função é verificada isoladamente contra sua especificação inferida.
   • Funções chamadas (callees) são substituídas por stubs constrangidos por suas pós-condições. Isso implementa uma disciplina assume-guarantee onde a pós-condição de um callee torna-se a premissa para o chamador.
   • Essa abordagem previne a explosão de estado de todo o programa, permitindo que a verificação escale com o tamanho do espaço de estado de uma única função em vez de todo o programa.

3. Validação de Contraexemplo Multi-Estágio:

   • Contraexemplos BMC não são tratados como relatórios de bugs imediatos. Eles passam por um pipeline de validação rigoroso para distinguir falhas ativas na árvore de código de falhas latentes ou artefatos de modelagem:
     • Alcançabilidade de Entrada: Propagando entradas de testemunha para cima no grafo de chamadas para determinar se um chamador pode fornecer os valores.
     • Viabilidade do Callee: Re-executando BMC com corpos de callee reais para garantir que a testemunha seja alcançável através de implementações reais.
     • Reprodução Dinâmica: Compilando um harness para executar a testemunha em um sistema hospedeiro, capturando sinais (SIGSEGV, SIGABRT, etc.) para confirmar falhas dinâmicas.
     • Auditoria de Realismo: Um agente LLM revisa o contexto completo (especificação, harness, estado da testemunha) para classificar a descoberta como realista ou irrealista, filtrando artefatos invariantes de framework (por exemplo, globais não inicializados, estados de hardware impossíveis).

4. Loop de Refinamento Adaptativo (CEGAR no Nível de Especificação):

   • Quando um contraexemplo é classificado como espúrio (por exemplo, um artefato de desenrolamento de loop), o sistema não o suprime simplesmente. Em vez disso, um LLM propõe refinamentos (estreitando pré-condições, fortalecendo contratos de callee ou ajustando parâmetros do solucionador).
   • Um guarda de solidez garante que esses refinamentos não mascarem bugs reais.
   • Refinamentos aceitos são persistidos em uma base de conhecimento (armazenamento de especificações e biblioteca de padrões) e propagados para todos os chamadores, efetivamente estendendo o CEGAR da abstração de predicados para o nível de especificação com propagação composicional.

Contribuições Principais

O artigo delineia seis contribuições primárias:

1. Paradigma de Verificação de Modelos Agênticos: Um framework onde agentes LLM gerenciam tarefas semânticas (inferência de especificação, seleção de verificação, classificação) enquanto backends BMC garantem solidez, permitindo verificação sem especificação de código C e Rust gerado por LLM.
2. Camada de Especificação Top-Down: Um mecanismo para inferir pré/pós-condições por função e selecionar verificações aritméticas semanticamente justificadas (por exemplo, estouro, verificações de ponteiro) via uma DSL que traduz para CBMC/Kani.
3. Arquitetura de Verificação Composicional: Uma abordagem escalável que verifica funções isoladamente sob contratos assume-guarantee, paralelizando através de camadas do grafo de chamadas.
4. Pipeline de Validação: Um processo de quatro estágios (alcançabilidade, viabilidade, reprodução dinâmica, auditoria de realismo) que categoriza descobertas em níveis de evidência (por exemplo, "confirmado dinâmico", "confirmado entrada de sistema").
5. Loop de Refinamento Multi-Nível: Um sistema que eleva o CEGAR ao nível de especificação, usando contraexemplos espúrios para impulsionar refinamentos composicionais que persistem entre execuções.
6. Implementação e Avaliação do BMC-Agent: Uma ferramenta funcional avaliada em diversos corpora, demonstrando a capacidade de confirmar defeitos reais, produzir verificações limpas limitadas em bibliotecas fuzzadas e provar equivalência funcional.

Resultados da Avaliação

Os autores avaliaram o BMC-Agent em quatro corpora abrangendo C e Rust:

• VibeOS (C): Um kernel ARM64 de 15.000 linhas gerado por LLM. O BMC-Agent confirmou 34 bugs realistas em 12 módulos. Destes, 16 foram reproduzidos dinamicamente (SIGSEGV/SIGABRT), 14 foram confirmados como pontos de entrada de sistema e 4 foram violações de modelo formal.
• Bibliotecas OSS Maduras (C): Avaliado em jq, OpenSSL, libcurl, libxml2 e protobuf upb. A ferramenta divulgou 2 defeitos de comportamento indefinido em jq (arquivados como GHSA) e produziu verificações limpas limitadas em superfícies de parser fortemente fuzzadas (por exemplo, 15/24 funções folha em ASN.1 do OpenSSL verificadas limpas).
• Driver Realtek r8125 (C): Encontrou uma bypass de verificação de limites MMIO acionado por CAP_NET_ADMIN no ioctl da ferramenta rtl8125, acionado ao habilitar verificações de estouro específicas via seletor de flag.
• claudes-c-compiler (Rust): Um compilador C de 50.000 linhas gerado por LLM. O BMC-Agent confirmou 25 bugs reais, principalmente defeitos da classe de pânico em auxiliares de bytes de API pública (OOB de fatia, estouro de inteiros) e uma violação de correção funcional. Também estabeleceu equivalência funcional limitada para auxiliares de hash ELF e escrita de cabeçalho.

Observações Chave dos Resultados:

• A precisão da ferramenta é atribuída aos detectores de estágio de realismo (filtrando artefatos de framework), seleção de flag por função (habilitando verificações desativadas por padrão em configurações padrão) e ao loop de feedback (convertendo padrões recorrentes em invariantes permanentes).
• No caso do compilador Rust, os bugs seguiram um anti-padrão específico: o LLM escreveu funções auxiliares sem verificações de limites, dependendo dos chamadores para manter invariantes. Isso resultou em código que funcionava em entrada bem-formada, mas falhava em entrada adversária, um perfil distinto de erros de lógica de compilador escritos por humanos típicos.

Significado e Alegações

O artigo alega que a Verificação de Modelos Agênticos aborda a "lacuna de especificação" no código de sistemas gerado por LLMs automatizando a inferência de contratos e acoplando-os com verificação de modelo limitada e sólida.

• Solidez vs. Escalabilidade: Ao delegar a solidez ao BMC e usar agentes para julgamento semântico, a abordagem evita a insolididade do raciocínio puro de LLM enquanto supera os limites de escalabilidade da verificação de todo o programa.
• Verificação Acionável: O pipeline de validação multi-estágio garante que os bugs relatados não sejam apenas contraexemplos teóricos, mas sejam classificados por sua alcançabilidade e impacto dinâmico, distinguindo entre falhas ativas e tarefas de endurecimento latentes.
• Propagação Composicional: A capacidade do sistema de refinar especificações e propagá-las através do grafo de chamadas permite que ele aprenda com contraexemplos espúrios, melhorando a qualidade da verificação ao longo do tempo sem intervenção manual.

Os autores permanecem modestos quanto ao trabalho futuro, observando que uma avaliação quantitativa ampla (precisão/recall em escala), análise mais profunda das suposições de correção de especificação e redução de custos via otimização de tokens são os próximos passos necessários. Eles enfatizam que os resultados atuais demonstram a capacidade do pipeline de confirmar defeitos e verificar superfícies limpas, mas não alegam ter resolvido o problema geral de verificar todo o código gerado por LLM sem limitações.