Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery

1. O Problema

A detecção automatizada de vulnerabilidades em grandes bases de código C/C++ (milhões de linhas) enfrenta um dilema entre escalabilidade e precisão:

• Análise Estática (SA): Escala bem para grandes códigos, mas gera altas taxas de falsos positivos e não consegue confirmar se uma vulnerabilidade é explorável.
• Fuzzing: Eficaz para encontrar bugs, mas luta para atingir estados profundos de bibliotecas internas que exigem configurações complexas de estado do programa.
• Execução Simbólica (SE): Oferece alta precisão e gera entradas concretas (testes) que confirmam formalmente violações de propriedades. No entanto, a SE não é escalável diretamente em grandes projetos devido à explosão de caminhos e dependências de ambiente. O principal gargalo é a construção manual de "harnesses" (programas de teste que configuram o estado simbólico, criam stubs para dependências e definem asserções), o que exige conhecimento profundo do código e da engine de SE, limitando sua adoção prática.
• LLMs (Modelos de Linguagem): Podem gerar código, mas carecem de garantias formais de correção e frequentemente falham ao tentar analisar contextos de código massivos sem execução real.

2. Metodologia: O Pipeline Sailor

O Sailor (Static Analysis Informed and LLM-Orchestrated Symbolic Execution) é uma pipeline totalmente automatizada que integra três fases para superar as limitações individuais das técnicas acima.

Fase 1: Geração de Alvos Informada por Análise Estática

• Objetivo: Identificar locais candidatos a vulnerabilidades e gerar especificações estruturadas.
• Processo:
  1. Utiliza CodeQL para escanear o código-fonte usando uma suíte de 34 consultas (padrões de segurança e regras personalizadas para vazamentos de memória, uso após liberação, etc.).
  2. Gera "fatos" (localização, descrição, rastreamento de fluxo de dados).
  3. Enriquece os fatos com contexto (chamadas suspeitas, variáveis de ponteiro, dicas de limites e contexto de compilação).
  4. Cria uma Especificação de Vulnerabilidade (JSON) que define o local alvo, a função de entrada (entrypoint), um modelo de asserção de segurança e filtros para remover código irrelevante (testes, exemplos).

Fase 2: Execução Simbólica Orquestrada por LLM

• Objetivo: Sintetizar automaticamente o harness de execução simbólica para cada especificação gerada na Fase 1.
• Processo:
  1. Um LLM (GPT-5 no estudo) atua como orquestrador em um ciclo iterativo de "planejar, agir, receber feedback".
  2. Exploração de Fonte: O LLM lê definições de tipos e assinaturas de funções para entender a estrutura do projeto.
  3. Síntese do Harness: O LLM gera três componentes:
     • Driver: Configura o estado inicial simbólico (aloca memória, define variáveis simbólicas).
     • Stubs: Substitui dependências externas e caminhos de código não relevantes para reduzir a explosão de caminhos.
     • Asserções: Codifica a propriedade de segurança a ser verificada (ex: klee_assert(0) após uma chamada vulnerável).
  4. Refinamento Iterativo: O harness é compilado e executado no KLEE (engine de SE).
     • Se houver erro de compilação, o LLM corrige o código.
     • Se a SE não atingir o alvo ou não encontrar o bug, o feedback (cobertura de caminhos, erros de execução) é enviado ao LLM para refinar o driver e os stubs.
     • O ciclo continua até um limite de iterações (60 voltas) ou até que um bug seja disparado.

Fase 3: Validação Concreta

• Objetivo: Eliminar falsos positivos gerados por harnesses irreais ou erros do LLM.
• Processo:
  1. As entradas concretas (witnesses) geradas pelo KLEE são usadas para criar um driver de reprodução.
  2. O código original do projeto é compilado com AddressSanitizer (ASan).
  3. O driver é executado contra a biblioteca instrumentada.
  4. Apenas se o ASan relatar um crash real no código do projeto (e não no código do harness), a vulnerabilidade é marcada como confirmada.

3. Principais Contribuições

1. Técnica Automatizada de Ponta a Ponta: Primeira abordagem que transforma automaticamente código-fonte em alvos de SE, sintetiza harnesses via LLM e valida resultados via execução concreta, sem intervenção humana na escrita de harnesses.
2. Implementação Sailor: Integração funcional de CodeQL, LLM, KLEE e ASan.
3. Escalabilidade e Precisão: Demonstração de que a combinação dessas técnicas permite escalar a SE para projetos com até 1,84 milhão de linhas de código (como o Binutils), algo inviável manualmente.
4. Conjunto de Dados: Avaliação em 10 projetos open-source (6,8 milhões de linhas de código), resultando em 379 vulnerabilidades únicas previamente desconhecidas.

4. Resultados da Avaliação

O Sailor foi testado em 10 projetos (libpng, libtiff, libxml2, curl, SELinux, mupdf, FFmpeg, binutils, OpenSSL, SQLite).

• Descobertas:
  • 379 vulnerabilidades únicas confirmadas (421 crashes totais).
  • 60% dos crashes confirmados foram reproduzidos via fuzzing (LibFuzzer) usando as sementes geradas pelo KLEE.
  • Tipos de bugs encontrados: Heap-buffer-overflow (68%), Use-after-free (13%), Segmentation fault (13%).
• Comparação com Baselines (Linha de Base):
  • O Sailor superou significativamente todas as abordagens de comparação.
  • O baseline mais forte (um agente LLM autônomo com acesso total ao código e interações ilimitadas) encontrou apenas 12 vulnerabilidades.
  • Abordagens puras de SE com harnesses manuais ou gerados por LLM sem iteração falharam em compilar ou encontrar bugs reais.
• Estudo de Ablação (Importância de cada componente):
  • Sem Análise Estática (A1): A descoberta de bugs caiu 12,2 vezes (de 379 para 31), mostrando que o direcionamento do LLM é crucial.
  • Sem Refinamento Iterativo (B2): Se o LLM gera o harness de uma só vez sem feedback de compilação/SE, 0 vulnerabilidades são confirmadas.
  • Sem Execução Simbólica (B3-B5): Abordagens puramente baseadas em LLM (mesmo com SA) não conseguem confirmar mais do que 12 vulnerabilidades, devido à alta taxa de falsos positivos.

5. Significado e Conclusão

O trabalho demonstra que nenhuma técnica isolada é suficiente para a descoberta de vulnerabilidades em escala industrial:

• A Análise Estática fornece o "onde" (alvos).
• O LLM fornece o "como" (sintetiza a lógica complexa do harness e explora o contexto do código).
• A Execução Simbólica fornece o "se" (garantia formal de que o caminho é viável e gera entradas).
• A Validação Concreta fornece a "verdade" (elimina falsos positivos).

O Sailor estabelece um novo paradigma onde o LLM não substitui a execução simbólica, mas atua como um orquestrador inteligente que supera as barreiras de engenharia (escrita de harnesses) que impediam a aplicação prática da SE em grandes sistemas. Isso permite a descoberta de bugs críticos de segurança em bibliotecas fundamentais que antes eram consideradas intransponíveis para análise automatizada profunda.