A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs

Este artigo apresenta o Preguss, um framework modular que combina análise estática e modelos de linguagem para automatizar a geração e refinamento de especificações formais, permitindo a verificação de programas de grande escala com mais de 1000 linhas de código e reduzindo o esforço humano em até 88,9%.

O essencial

Imagine que você tem um livro de receitas gigante, com mais de 1.000 páginas, escrito por um chef que às vezes comete erros de digitação perigosos (como esquecer de colocar sal ou, pior, tentar usar uma faca sem cabo). Se alguém tentar seguir essa receita, a cozinha pode explodir ou a comida ficar venenosa. No mundo dos computadores, esse "livro de receitas" é um programa de software, e os "erros de digitação" são falhas que podem fazer o computador travar, perder dados ou até causar acidentes graves (como em satélites ou carros autônomos).

O problema é que esses livros são tão grandes e complexos que nenhum humano consegue ler tudo e achar todos os erros manualmente. E os robôs (inteligências artificiais) que tentam ajudar, muitas vezes, ficam confusos porque o livro é grande demais para a "memória" deles, ou eles inventam regras que não fazem sentido.

Aqui entra o Preguss, o protagonista desta história. O nome é um trocadilho com "1001", sugerindo que ele consegue lidar com histórias (códigos) enormes.

O Que é o Preguss? (A Metáfora do Detetive Especializado)

Pense no Preguss como um detetive de crimes digitais que usa uma estratégia inteligente para não se afogar em detalhes. Em vez de tentar ler o livro inteiro de uma vez (o que deixaria qualquer detetive, humano ou robô, tonto), o Preguss divide o trabalho em duas fases principais:

Fase 1: O Mapa do Crime (Dividir)

Antes de começar a investigar, o Preguss usa uma ferramenta de "raio-X" (chamada análise estática) para olhar o código e dizer: "Ei, aqui na página 45, na linha 10, parece que alguém vai tentar dividir por zero! Isso é perigoso!".

Essa ferramenta marca todos os pontos onde algo pode dar errado. O Preguss então pega esses pontos de perigo e cria pequenos casos de investigação (chamados de "Unidades de Verificação"). Ele organiza esses casos em uma fila, como se fosse um detetive anotando: "Vamos resolver o problema do elevador primeiro, depois o do freio, e só depois o do rádio". Isso evita que o robô tente resolver tudo de uma vez e trave.

Fase 2: O Interrogatório Inteligente (Conquistar)

Agora, o Preguss chama a Inteligência Artificial (o "LLM", que é como um robô muito inteligente, mas que às vezes alucina) para ajudar a resolver cada caso da fila, um por um.

Aqui está a mágica:

1. O Detetive dá a pista: O Preguss mostra para a IA apenas a página específica onde o erro pode acontecer e diz: "Olhe aqui. O sistema de raio-X disse que pode haver um erro de divisão por zero. O que precisamos escrever nas regras (especificações) para garantir que isso não aconteça?"
2. A IA sugere uma regra: A IA tenta inventar uma regra, como "O número nunca pode ser zero".
3. O Juiz verifica: O Preguss pega essa regra e a testa em um tribunal rigoroso (o verificador formal).
   • Se o juiz disser "Certo!", ótimo! O caso está resolvido.
   • Se o juiz disser "Não, isso não funciona" e der uma dica do porquê (ex: "Você esqueceu de dizer que o número também não pode ser negativo"), o Preguss pega essa dica e manda a IA tentar de novo, ajustando a regra.

Se a IA não conseguir resolver um caso específico, o Preguss não desiste. Ele marca aquele caso como "Suspeito, mas precisamos de um humano para olhar de perto" e segue para o próximo. Isso é crucial: em vez de tentar forçar a IA a resolver tudo (o que geraria erros), ele isola o que precisa de ajuda humana.

Por que isso é revolucionário?

1. Não tenta ser um herói solitário: Métodos antigos tentavam dar o livro inteiro para a IA ler de uma vez. O Preguss sabe que a IA tem "memória curta" para textos longos. Então, ele entrega apenas o pedaço necessário, como se fosse dar a um aluno apenas a página do livro que ele precisa estudar, e não a biblioteca inteira.
2. Aprende com os erros: Se a IA inventa uma regra que é "muito estrita" (ex: "O número deve ser 5" quando poderia ser qualquer número positivo), o Preguss percebe que isso gera falsos alarmes e corrige a regra.
3. Economiza tempo de ouro: Em testes reais, o Preguss conseguiu verificar programas gigantes (como o sistema de controle de um satélite) com 80% a 88% menos esforço humano. Antes, especialistas teriam que passar meses revisando cada linha. Agora, o Preguss faz o trabalho pesado e deixa apenas os casos mais difíceis para os humanos.

O Resultado na Vida Real

Os autores testaram o Preguss em programas reais, incluindo um sistema de controle de navegação para uma espaçonave. O resultado?

• O Preguss conseguiu provar que o software estava livre de erros perigosos na grande maioria dos casos.
• Mais impressionante ainda: ele encontrou 6 erros reais que os desenvolvedores não tinham percebido, como tentativas de acessar memória não inicializada. Isso é como o detetive encontrar uma bomba que estava escondida antes que ela explodisse.

Resumo em uma frase

O Preguss é um sistema que ensina a Inteligência Artificial a agir como um detetive organizado: em vez de tentar resolver o mistério do mundo inteiro de uma vez, ele divide o caso em pequenos pedaços, usa pistas de ferramentas automáticas para guiar a IA, e só pede ajuda humana quando o caso realmente fica complicado, tornando a verificação de softwares gigantes rápida, segura e quase automática.

Resumo técnico

1. Problema e Motivação

A verificação formal automática de grandes sistemas de software e hardware é considerada o "Santo Graal" dos métodos formais. No entanto, a verificação de programas em larga escala (com milhares de linhas de código - LoC) enfrenta desafios significativos, especialmente no que tange à garantia de ausência de erros de tempo de execução (RTEs), como divisão por zero, overflow de buffer/numérico e dereferência de ponteiro nulo.

Os principais obstáculos identificados são:

• Limitações de Contexto dos LLMs: Modelos de Linguagem de Grande Escala (LLMs) atuais têm dificuldade em processar programas inteiros devido a janelas de contexto limitadas e à incapacidade de localizar informações precisas em um único passo ("one-shot").
• Complexidade de Especificações Interprocedurais: A verificação de grandes programas exige a síntese de especificações que cruzam limites de funções (pré-condições, pós-condições, invariantes de laço). Abordagens existentes frequentemente falham em distinguir entre pré e pós-condições ou geram especificações "super-constrangidas" (over-constrained), gerando falsos positivos.
• Dependência de Esforço Humano: Ferramentas de verificação dedutiva (como Frama-C/Wp) exigem especificações formais precisas, cuja síntese automática ainda depende fortemente de especialistas humanos, especialmente para projetos grandes.

O objetivo do trabalho é superar essas limitações criando um framework que automatize a síntese de especificações formais para verificar a ausência de RTEs em programas reais com mais de 1.000 LoC.

2. Metodologia: O Framework Preguss

O artigo apresenta o Preguss, um framework modular e de granularidade fina que sinergiza análise estática e verificação dedutiva utilizando LLMs. A abordagem segue uma estratégia de "dividir e conquistar" em duas fases principais:

Fase 1: Construção e Priorização de Unidades de Verificação (Divide)

• Guia por Erros Potenciais (RTE-Guided): Em vez de tentar verificar o programa inteiro de uma vez, o sistema utiliza um analisador estático baseado em interpretação abstrata (ex: Frama-C/Eva) para gerar asserções de RTE que indicam potenciais comportamentos indefinidos (UBs).
• Unidades de Verificação (V-Units): O problema monolítico é decomposto em unidades gerenciáveis. Cada V-Unit consiste em uma "asserção guarda" (o RTE a ser provado ou descartado) e um "fatia de contexto" mínima necessária para sua validação (a função hospedeira e suas chamadas diretas/indiretas).
• Ordenação Bottom-Up: As V-Units são organizadas em uma fila com base na hierarquia de chamadas. A verificação ocorre de baixo para cima (das funções chamadas para as chamadoras), garantindo que as especificações das funções internas estejam disponíveis antes de verificar as chamadoras. Isso mitiga o problema de contexto longo dos LLMs.

Fase 2: Síntese Fina de Especificações Interprocedurais (Conquer)

• Síntese Iterativa Guiada por Feedback: Para cada V-Unit, um LLM é instruído a gerar especificações candidatas. O processo é iterativo:
  1. O verificador dedutivo tenta provar a asserção guarda usando as especificações atuais.
  2. Se falhar (status "unknown"), o feedback do verificador (obrigações de prova, erros de sintaxe, lógica não resolvida) é enviado de volta ao LLM.
  3. O LLM refina as especificações com base nesse feedback.
• Estratégias Diferenciadas:
  • Função Hospedeira: O LLM gera pré-condições e invariantes de laço apenas para a função local, evitando gerar pré-condições para funções chamadas (o que causaria especificações super-constrangidas).
  • Funções Chamadas (Callees): O LLM gera exclusivamente pós-condições e invariantes para as funções chamadas, permitindo que o contexto interprocedural seja construído corretamente sem violar a terminação do processo.
• Validação de Sintaxe e Semântica: Um mecanismo de correção automática verifica se as especificações geradas são sintaticamente válidas e semanticamente satisfatórias, descartando aquelas que induziriam falsos negativos.

3. Principais Contribuições

1. Síntese Guiada por RTE Potencial: Formalização de um novo paradigma onde asserções de erros de tempo de execução (geradas por análise estática) guiam a síntese de especificações, focando apenas no necessário para provar a ausência de RTEs.
2. Framework Preguss: A primeira abordagem automatizada capaz de provar a ausência de RTEs em programas reais com mais de 1.000 LoC com esforço humano marginal. O framework integra análise estática e verificação dedutiva de forma terminante e sonora.
3. Dataset Aberto: Construção de um conjunto de dados com programas C do mundo real anotados com especificações geradas pelo Preguss e validadas por especialistas.
4. Desempenho Superior: Demonstração de que o Preguss supera significativamente as abordagens baseadas em LLMs do estado da arte (como AutoSpec) em taxa de sucesso de verificação e eficiência.

4. Resultados Experimentais

Os experimentos foram conduzidos em benchmarks pequenos (Frama-C-Problems) e quatro projetos reais de grande escala:

• Contiki (544 LoC), X509-parser (1.199 LoC), SAMCODE (1.280 LoC, sistema de controle de espaçonave) e Atomthreads (1.451 LoC).

Principais Métricas:

• Taxa de Sucesso: O Preguss alcançou uma taxa de sucesso média de 79,7% no benchmark Frama-C-Problems, superando o AutoSpec (32,7%) e o AutoSpecRte (41,8%).
• Projetos Reais: Nos projetos grandes, o Preguss verificou automaticamente entre 78,1% e 94,7% das unidades de verificação (V-Units).
• Redução de Esforço Humano: O framework reduziu o esforço de verificação humana em 80,6% a 88,9% (medido pelo número de especificações que precisaram de intervenção manual) em comparação com a verificação manual completa.
• Descoberta de Bugs Reais: No sistema de controle de espaçonave SAMCODE, o Preguss ajudou a identificar 6 RTEs confirmados (acessos a variáveis não inicializadas) que foram posteriormente validados pelos desenvolvedores.
• Custo e Tempo: Embora o custo de inferência do LLM seja maior que o das abordagens basais devido à estratégia de refinamento iterativo, o tempo total de execução e o custo financeiro permanecem viáveis, com uma redução drástica no tempo de verificação manual.

5. Significado e Impacto

O trabalho Preguss representa um avanço significativo na escalabilidade da verificação formal:

• Viabilidade Industrial: Demonstra que é possível automatizar a verificação de segurança (ausência de RTEs) em sistemas críticos de grande porte, algo que anteriormente exigia meses de trabalho manual de especialistas.
• Sinergia de Ferramentas: Estabelece um novo padrão de integração onde a análise estática (rápida, mas com falsos positivos) e a verificação dedutiva (precisa, mas exigente em especificações) se complementam, com o LLM atuando como o "cérebro" que traduz os alertas estáticos em especificações formais refinadas.
• Abordagem de Granularidade Fina: A estratégia de decompor o problema em V-Units e usar feedback iterativo resolve o dilema do "contexto longo" dos LLMs, permitindo que eles foquem em contextos semânticos relevantes sem se perderem na complexidade do código inteiro.

Em resumo, o Preguss oferece um caminho viável para a verificação quase totalmente automatizada de grandes sistemas de software, reduzindo drasticamente a barreira de entrada para métodos formais na indústria de software crítico.