Resumo Técnico: Veritas

Declaração do Problema

Detectar vulnerabilidades de corrupção de memória (MCVs) em binários desprovidos de símbolos apresenta um desafio fundamental de reconstrução semântica. Diferentemente da análise de código-fonte, a análise de binários deve recuperar como objetos de memória são alocados, propagados, restringidos e acessados através de funções a partir de artefatos que perderam a estrutura de alto nível, os limites dos objetos e o fluxo de controle explícito devido à compilação e ao stripping.

Abordagens recentes baseadas em Modelos de Linguagem de Grande Escala (LLMs) melhoraram a compreensão de código, mas lutam com a detecção de MCVs em binários por três razões principais:

1. Rastreamento de Estado Compartilhado: As vulnerabilidades frequentemente surgem de suposições inconsistentes sobre regiões de memória compartilhadas através de funções disjuntas que carecem de arestas diretas na cadeia de chamadas. A expansão padrão do grafo de chamadas falha em capturar essas dependências.
2. Perda Semântica: As representações recuperadas são fragmentadas. A IR LLVM elevada preserva padrões de acesso à memória de baixo nível, mas é obscurecida por artefatos do compilador (variáveis SSA, casts), enquanto o C descompilado fornece estrutura de alto nível, mas colapsa operações de memória em expressões de deslocamento genéricas, apagando a identidade do objeto.
3. Verificação de Restrições: A análise estática frequentemente não consegue determinar se um acesso suspeito é alcançável sob condições de caminho viáveis. Sem evidência executável, os LLMs dependem de proxies sintáticos em vez de prova de como dados controlados pelo atacante se propagam para operações sensíveis à memória, levando a raciocínio frágil e altas taxas de falsos positivos.

Frameworks de agentes existentes projetados para código-fonte (baseados em sumarização ou expansão de grafo de chamadas) não resolvem o problema de recuperação semântica imposto por binários desprovidos de símbolos, onde a estrutura semântica necessária está parcialmente ausente por construção.

Metodologia

O Veritas é um framework agentic híbrido e semanticamente fundamentado, projetado para restringir o raciocínio do LLM a semânticas de programa verificáveis e comportamento executável. Ele organiza a análise em três estágios alinhados com duas camadas de fundamentação: Fundamentação Estática (fatos do programa recuperados) e Fundamentação em Tempo de Execução (evidência de execução concreta).

1. Cortador de Contexto Orientado a Semântica (Fundamentação Estática)

O Cortador opera sem LLMs para extrair fluxos compactos, apoiados por testemunhas, de fontes a sumidouros a partir da IR LLVM elevada.

• Grafo de Propagação Interprocedural: Ele eleva o binário para IR LLVM usando o RetDec e constrói um grafo de propagação interprocedural tipado ($G_P$) codificando chamadas, retornos e dependências globais. Este grafo rastreia como valores relevantes para contaminação (ponteiros, deslocamentos, comprimentos) se propagam através das funções.
• Extração de Fluxo Baseada em Testemunhas: Em vez de tratar todos os pares fonte-sumidouro alcançáveis como significativos, o Cortador verifica testemunhas interprocedurais limitadas. Ele rastreia tokens contaminados desde fontes de entrada (ex: fread) até sumidouros de risco de memória (ex: argumentos de APIs perigosas), validando a propagação em cada limite de função usando cadeias de definição-uso e metadados.
• Construção de Objeto de Fluxo: As testemunhas aceitas são convertidas em objetos de fluxo compactos contendo funções ordenadas, tokens relevantes para contaminação e "pistas de âncora" (classes de proveniência e anotações de ponto final). Isso substitui o binário completo por um contexto pequeno e semanticamente completo para análise a jusante.

2. Detector de Vulnerabilidades de Visão Dupla (Raciocínio Controlado do LLM)

O Detector realiza raciocínio passo a passo sobre os fluxos apoiados por testemunhas, usando uma representação de entrada de visão dupla para superar a perda semântica.

• Representação de Visão Dupla: Para funções de fonte e sumidouro, o LLM recebe tanto o código C descompilado (para raciocínio de fluxo de controle) quanto a IR LLVM elevada (para desambiguar operações de memória e semântica do sumidouro). Para funções intermediárias, ele usa principalmente código descompilado, guiado por pistas de âncora.
• Raciocínio Passo a Passo: O LLM analisa o fluxo uma função de cada vez, mantendo um estado de raciocínio acumulado (inventário de valores propagados, aliases e limites). Ele atualiza esse estado com base em atribuições e decisões de fluxo de controle, evitando os limites de contexto de processar todo o fluxo de uma só vez.
• Memorização Baseada em Trie: Para reduzir redundância, o sistema memoriza estados de raciocínio para prefixos de fluxo compartilhados, invocando o LLM apenas no sufixo único de um fluxo.
• Verificação de Consistência: Antes de relatar um candidato, o Detector realiza uma verificação final sensível ao caminho para garantir que o valor contaminado permaneça relevante para a vulnerabilidade e que o acesso ao sumidouro viole a segurança da memória sob condições viáveis.

3. Validador Automático de Vulnerabilidades (Fundamentação em Tempo de Execução)

O Validador traduz hipóteses do detector em verificações executáveis para confirmar ou refutar candidatos.

• Preparação de Artefatos: Ele mapeia hipóteses do detector para coordenadas executáveis (RVAs, símbolos) usando o Radare2, fazendo a ponte entre as visões do descompilador e a depuração em tempo de execução.
• Colaboração Multi-Agente: Três agentes orquestram a validação:
  • Estrategista: Planeja a validação, selecionando alvos de instrumentação, pontos de interrupção e modalidades de disparo (arquivo, rede, CLI).
  • Verificador: Executa o plano, gerando Provas de Conceito (PoCs) e executando o binário sob depuradores (Radare2) ou verificadores de memória (Valgrind) para observar falhas ou acessos inválidos.
  • Explorador: Se a evidência inicial for insuficiente, ele investiga estados alternativos ou funções relacionadas para encontrar evidências de suporte.
• Confirmação: Uma vulnerabilidade é confirmada apenas quando evidência concreta de tempo de execução (ex: uma violação de segmento, erro do Valgrind ou estado de memória específico) corrobora o sumidouro relatado, o padrão de acesso e a causa raiz.

Principais Contribuições

1. Framework Veritas: Um framework agentic semanticamente fundamentado que unifica análise estática de programas e validação em tempo de execução para detectar corrupção de memória em binários desprovidos de símbolos.
2. Arquitetura de Três Estágios:
   • Um Cortador que extrai fluxos apoiados por testemunhas de IR elevada sem LLMs.
   • Um Detector de Visão Dupla que raciocina sobre fluxos usando suporte seletivo de IR para resolver ambiguidade semântica.
   • Um Validador que confirma hipóteses usando artefatos visíveis ao depurador e execução concreta.
3. Benchmark de Alta Granularidade: Um conjunto de dados curado de 20 casos reais de corrupção de memória em binários com verdade fundamental em nível de trilha, construído para avaliar a detecção fundamentada de binários.
4. Desempenho: A avaliação mostra que o Veritas alcança 90% de recall no benchmark, superando significativamente analisadores estáticos (0% de recall), fuzzing (10% de recall) e baselines agentic (25–35% de recall). Ele produziu zero falsos positivos em uma validação exaustiva de 623 candidatos e apenas 2 falsos positivos em uma auditoria amostral maior.
5. Descoberta no Mundo Real: O Veritas descobriu uma leitura fora dos limites zero-day previamente desconhecida na biblioteca Universal Scene Description da Apple (libusd_ms.dylib), que foi confirmada e recebeu um CVE.

Resultados e Significância

O artigo argumenta que a eficácia da descoberta de vulnerabilidades baseada em LLMs não depende apenas da capacidade intrínseca do modelo, mas da capacidade da infraestrutura circundante de recuperar a estrutura semântica necessária para o raciocínio.

• Fundamentação Semântica como Princípio de Design: Os resultados apoiam a fundamentação semântica como um princípio de design operacional. Ao restringir o raciocínio do LLM a fatos explícitos relevantes para memória (fundamentação estática) e validar conclusões contra comportamento executável (fundamentação em tempo de execução), o Veritas evita a fragilidade da especulação de modelo sem restrições.
• Superioridade sobre Baselines: Ferramentas tradicionais falham devido à falta de fundamentação semântica através de funções. As baselines agentic falham porque carecem de modelos explícitos dos ciclos de vida de objetos de memória e dependem de exploração não guiada ou padrões sintáticos. O Veritas preenche essa lacuna usando análise determinística para pré-computar a propagação e LLMs para interpretar semânticas complexas, seguidos por confirmação rigorosa em tempo de execução.
• Compromisso Custo-Precisão: Embora a validação em tempo de execução seja o principal gargalo de custo (requerendo geração de PoC e depuração), o framework demonstra que alta precisão é alcançável na análise de binários desprovidos de símbolos apenas através de evidência executável. O sistema prioriza a confiabilidade da detecção sobre o rendimento, um compromisso necessário para análise de binários críticos para segurança.

O artigo conclui que, para detecção prática de vulnerabilidades em binários, o raciocínio deve estar ancorado tanto na semântica do programa recuperada quanto na evidência executável, um princípio que o Veritas implementa através de sua arquitetura modular e híbrida.