Natural Language based Specification and Verification

Resumo Técnico: Especificação e Verificação Baseadas em Linguagem Natural (NLForge)

Declaração do Problema
Violações de segurança de memória em programas C e C++ — como desreferenciações inválidas, uso após liberação e acesso fora dos limites — permanecem uma fonte primária de vulnerabilidades de software. Esses erros frequentemente decorrem de interações interprocedurais complexas envolvendo alocação, liberação, inicialização e aliasing, que ferramentas tradicionais de análise estática têm dificuldade em verificar em escala. Embora os Modelos de Linguagem de Grande Escala (LLMs) tenham demonstrado capacidades robustas na identificação de bugs, enfrentam desafios significativos em prevenir a introdução de novas vulnerabilidades por meio de verificação formal. Pipelines de verificação existentes tipicamente exigem especificações em linguagens formais rígidas (por exemplo, invariantes de loop, pré/pós-condições), criando uma alta carga de anotação. Tentativas anteriores de usar LLMs para sintetizar essas especificações formais mostraram sucesso limitado. Além disso, benchmarks recentes indicam que o desempenho dos LLMs cai precipitadamente ao migrar da verificação de função única para raciocínio composicional e multifuncional, devido em grande parte às limitações da janela de contexto e à dificuldade de manter consistência semântica global.

Metodologia: NLForge
Os autores propõem o NLForge, um framework de verificação composicional que aproveita LLMs para gerar e raciocinar sobre especificações em linguagem natural em vez de artefatos formais rígidos. O sistema opera em uma análise ascendente, priorizando os chamados (callee-first), sobre o grafo de chamadas do programa.

1. Arquitetura do Pipeline:

   • Pré-processamento: O sistema extrai definições de funções, assinaturas e locais de chamada do código C/C++ para construir um grafo de chamadas. Chamadas não resolvidas são tratadas por meio de stubs externos.
   • Análise Ascendente: O framework executa uma sequência de passes de análise sobre o grafo de chamadas em ordem topológica (processando os chamados antes dos chamadores).
   • Resumos em Linguagem Natural: Em vez de gerar lógica formal, o LLM produz resumos estruturados em linguagem natural (codificados como JSON tipado com descrições em linguagem natural) para propriedades específicas:
     • Alocação/Liberação/Inicialização: Resumindo a criação de objetos no heap, efeitos de liberação e inicialização de parâmetros de saída.
     • Contratos de Segurança de Memória: Inferindo pré-condições (por exemplo, não-nulo, não-liberado, tamanho do buffer) e pós-condições.
     • Resumos de Vazamento e Inteiros: Rastreando obrigações não resolvidas e riscos de overflow de inteiros.
   • Verificação Composicional: No passe final de verificação, o LLM analisa uma função usando suas próprias pré-condições inferidas e os resumos em linguagem natural de seus chamados. O modelo atua como um agente de raciocínio que mantém um estado de execução latente, verificando requisitos de segurança contra contratos de chamados sem incorporar (inlining) a implementação completa do chamado.

2. Racional de Design:
   A abordagem é motivada pela observação de que LLMs, treinados em código e documentação, podem gerar, interpretar e refinar resumos em linguagem natural de forma mais consistente do que notações formais rígidas. Este design visa decompor o problema de verificação em resumos semânticos reutilizáveis, permitindo que o modelo raciocine sobre uma função sob suposições explicitamente declaradas sobre seus chamados, em vez de reanalisar o código-fonte bruto para cada chamador.

Principais Contribuições

• Framework Composicional: Um framework de verificação interprocedural ascendente para C/C++ que utiliza LLMs para inferir e verificar propriedades de segurança de memória.
• Representação Intermediária em Linguagem Natural: A introdução de resumos semânticos em linguagem natural como representação intermediária para verificação, contrastando com trabalhos anteriores focados na geração de especificações formais para verificadores simbólicos externos.
• Pipeline de Análise Estagiada: Uma decomposição do raciocínio de segurança de memória em resumos reutilizáveis (alocação, liberação, inicialização e obrigações do lado do chamador) que são alimentados de volta ao LLM em estágios subsequentes.
• Avaliação Empírica: Um estudo comparativo de raciocínio composicional versus uma linha de base de prompt de programa inteiro não composicional nos benchmarks SV-COMP 2026.

Resultados
Os autores avaliaram o NLForge em um subconjunto dos benchmarks de segurança de memória SV-COMP 2026 usando quatro backbones de LLM (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite e Qwen3.5-27B-UD-Q4) e os compararam com verificadores tradicionais (CPAchecker, Symbiotic, Ultimate Automizer).

• RQ1 (LLMs como Verificadores): A análise baseada em LLMs demonstra alta recall e cobertura, identificando a maioria dos verdadeiros positivos (por exemplo, o Sonnet-4.6 alcançou 99,8% de recall em valid-memsafety). No entanto, eles produzem significativamente mais falsos positivos do que ferramentas tradicionais e ainda não podem servir como verificadores autônomos e sound. Ferramentas tradicionais frequentemente retornam "Desconhecido" (UNK) para casos difíceis para evitar falsos positivos, enquanto LLMs fornecem respostas definitivas com taxas de erro mais altas.
• RQ2 (Verificação Composicional): A abordagem composicional supera significativamente a linha de base não composicional, particularmente em benchmarks complexos do mundo real de fluxo de controle e estrutura de dados.
  • As execuções composicionais aumentaram os Verdadeiros Positivos de 3.390 para 3.476 e reduziram os Falsos Negativos de 301 para 216 em todos os modelos.
  • A melhoria foi mais pronunciada para modelos menores (por exemplo, o Qwen3.5-27B-Q4 viu os Falsos Negativos cair de 218 para 97) e em benchmarks que exigem forte raciocínio interprocedural.
  • Os ganhos foram menos consistentes em testes sintéticos e localizados do Juliet, onde modelos não composicionais podiam explorar padrões locais diretamente.

Significado e Alegações
O artigo argumenta por uma mudança na forma como os LLMs são utilizados na verificação: migrar de tratá-los exclusivamente como geradores de artefatos formais para motores externos para usá-los como agentes de raciocínio sobre resumos estruturados e reutilizáveis em linguagem natural.

• Praticidade: A linguagem natural serve como uma camada de especificação intermediária prática que habilita a verificação composicional, particularmente para tarefas onde o prompt de programa inteiro excede o orçamento de raciocínio do modelo ou a janela de contexto.
• Limitações: Os autores reconhecem que a informalidade da linguagem natural leva a problemas de calibração (maiores falsos positivos) e que a abordagem é sensível à qualidade dos resumos gerados; erros nos resumos podem se propagar e amplificar.
• Perspectiva Futura: O trabalho sugere que, embora os LLMs ainda não sejam um substituto para a verificação formal sound, eles oferecem uma direção promissora para verificação escalável de detecção de bugs. Trabalhos futuros devem focar em melhorar a calibração, combinar resumos com verificações simbólicas e lidar com recursos complexos como chamadas indiretas e invariantes de heap de forma mais robusta.

O estudo conclui que a questão não é meramente se os LLMs podem verificar a segurança de memória, mas sob quais representações e decomposições eles se tornam mais confiáveis, destacando que a linguagem natural pode efetivamente preencher a lacuna entre a estrutura modular do programa e as capacidades de raciocínio dos LLMs.