Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

Título: Desativando Bombas Lógicas na Execução Simbólica com Código Fantasma Gerado por LLMs

Autores: Dimitrios Stamatios Bouras e Sergey Mechtaev (Peking University)

1. O Problema

A execução simbólica é uma técnica poderosa de análise de programas que executa código com entradas abstratas, codifica o comportamento em restrições lógicas e utiliza solucionadores SMT (Satisfiability Modulo Theories) para analisar esses caminhos. No entanto, sua eficácia é fundamentalmente limitada por três fatores principais:

1. Fragmentos hostis ao solucionador: Cálculos complexos (aritmética não linear, funções trigonométricas) geram restrições SMT difíceis ou indecidíveis.
2. Modelagem de ambiente: Dificuldade em modelar com precisão chamadas de sistema, comunicação de rede ou bibliotecas externas.
3. Estruturas de heap ilimitadas: O uso de alocação de memória dinâmica e ponteiros causa uma explosão de caminhos devido às inúmeras configurações possíveis de estruturas de dados (aliasing).

Abordagens recentes tentaram substituir solucionadores SMT por Modelos de Linguagem Grandes (LLMs) para contornar essas limitações. Contudo, essas técnicas puramente baseadas em LLMs falham em analisar bases de código reais quando o objetivo está profundamente aninhado, exigindo consistência global entre muitas restrições interconectadas que os LLMs têm dificuldade em manter.

2. Metodologia: O Framework Gordian

O trabalho propõe o Gordian, um framework híbrido de execução simbólica que integra seletivamente LLMs para gerar código fantasma (ghost code) leve. O objetivo não é substituir o solucionador SMT, mas auxiliá-lo a lidar com fragmentos de código hostis, preservando a capacidade de raciocínio global e preciso do solucionador.

O Gordian opera em três etapas principais para lidar com fragmentos difíceis, selecionando o tipo de código fantasma com base no contexto:

A. Inversão de Fragmentos Difíceis (Ghost Inversion)

• Problema: O LLM identifica um fragmento de código difícil (ex: sin(x), cos(x)) e gera um procedimento de inversão (ex: uma busca por seção áurea para encontrar x dado sin(x)).
• Mecanismo: O sistema executa o programa simbolicamente, substituindo o fragmento difícil por variáveis simbólicas frescas. Em seguida, utiliza a propagação bidirecional de restrições:
  1. O solucionador SMT resolve as restrições do sufixo (pós-fragmento) para obter valores candidatos.
  2. O código fantasma inverso executa esses valores "para trás" para inferir valores candidatos para a entrada.
  3. Um otimizador encontra o valor de entrada mais próximo que satisfaz as restrições do prefixo (pré-fragmento).
• Resultado: Permite navegar por caminhos que dependem de operações matemáticas complexas sem depender puramente do solucionador SMT para resolver a equação direta.

B. Modelagem por Surrogados (Surrogate Models)

• Problema: Alguns fragmentos não podem ser invertidos (ex: perdem informação, dependem de estado externo).
• Mecanismo: O LLM gera um modelo substituto (surrogate) que aproxima o comportamento do fragmento original, mas traduzido para uma teoria amigável ao solucionador (ex: aritmética linear ou vetores de bits), preservando o comportamento relevante para o controle de fluxo.
• Validação: Como o modelo é aproximado, qualquer entrada gerada é validada executando o programa original para garantir a correção (preservação da soundness).

C. Particionamento Semântico de Heap (Semantic Heap Partitioning)

• Problema: Estruturas de dados dinâmicas (como listas ligadas ou árvores) causam explosão de caminhos devido às muitas formas possíveis de configuração de memória.
• Mecanismo: O LLM gera código fantasma que restringe o heap a um pequeno conjunto de topologias semânticas relevantes (ex: "lista encadeada de tamanho >= 3", "anel válido", "cadeia quebrada").
• Benefício: Em vez de explorar todas as combinações de ponteiros, o sistema explora apenas as formas estruturais significativas para o domínio do problema, mantendo os valores dos dados como simbólicos.

3. Contribuições Principais

1. Abordagem Híbrida Inovadora: Integração de LLMs para gerar código fantasma que auxilia solucionadores SMT, em vez de substituí-los, mantendo o raciocínio global preciso.
2. Três Variantes de Código Fantasma: Definição prática de inversão, surrogados e particionamento de heap, com prompts e algoritmos de integração específicos.
3. Implementação e Avaliação Abrangente: Implementação sobre o motor KLEE e avaliação em benchmarks sintéticos ("LogicBombs"), uma biblioteca matemática real (FDLibM) e programas de entrada estruturada (libexpat, jq, bc).

4. Resultados Experimentais

O Gordian foi comparado com execução simbólica tradicional (KLEE com STP, Z3, KLEE-Float) e técnicas baseadas em LLMs (ConcoLLMic, Cottontail).

• Cobertura de Código:
  • LogicBombs (Sintético): Gordian aumentou a cobertura em 52–84% em comparação com a execução simbólica tradicional e 86–419% em relação às técnicas baseadas em LLMs.
  • FDLibM (Matemática): Melhorou a cobertura média em 22,09% sobre a melhor configuração KLEE e 183,5% sobre o ConcoLLMic.
  • Programas Estruturados (libexpat, jq, bc): Aumentou a cobertura total em até 108,55% sobre o KLEE e cobriu 9,7 vezes mais linhas de código que o ConcoLLMic.
• Eficiência de Tokens (Custo):
  • O uso de LLMs no Gordian é altamente eficiente, pois é invocado apenas em fragmentos específicos.
  • Redução no uso de tokens de 90% a 96% em comparação com abordagens puramente baseadas em LLMs (que consultam o modelo continuamente).
  • Exemplo: No benchmark FDLibM, o Gordian reduziu o uso de tokens em 23x comparado ao ConcoLLMic.

5. Significado e Conclusão

O trabalho demonstra que a combinação de raciocínio global preciso (via SMT) com conhecimento de domínio e geração de código (via LLM) supera as limitações de ambas as abordagens isoladas.

• Praticidade: O uso de "código fantasma" permite que o sistema lide com "bombas lógicas" e restrições complexas sem sacrificar a correção formal, pois os resultados são sempre validados contra o programa original.
• Escalabilidade: A abordagem é escalável para bases de código reais e grandes, resolvendo problemas de explosão de caminhos e restrições indecidíveis que paralisam ferramentas tradicionais.
• Futuro: O artigo sugere que a integração nativa desses módulos de LLM dentro dos motores de execução simbólica (em vez de orquestração externa) pode ser um caminho futuro para reduzir a complexidade de engenharia e melhorar o desempenho.

Em resumo, o Gordian representa um avanço significativo na análise de software, transformando LLMs de "substitutos de solucionadores" (que falham em consistência global) em "assistentes especializados" que desbloqueiam caminhos de execução anteriormente inalcançáveis.