From Heuristics to Transformers: A Comprehensive Survey of Type Inference from Stripped Binaries

Resumo Técnico: De Heurísticas a Transformers: Um Levantamento Abrangente da Inferência de Tipos em Binários Sem Símbolos

Declaração do Problema
A recuperação de informações de tipos de alto nível a partir de binários sem símbolos — executáveis desprovidos de tabelas de símbolos e informações de depuração (ex: DWARF) — permanece um desafio fundamental na engenharia reversa de software, análise de vulnerabilidades e descompilação. A compilação é uma transformação com perda, onde abstrações de alto nível como tipos de dados são removidas, deixando um "deserto semântico" de instruções de assembly puras. Em binários sem símbolos, essa perda é exacerbada pela remoção de metadados de depuração. Consequentemente, distinguir ponteiros de inteiros, identificar estruturas de dados complexas (arrays, structs, unions) e compreender o fluxo de controle torna-se inerentemente difícil. Essa assimetria entre a intenção do código fonte e a realidade do código de máquina dificulta aplicações de segurança automatizadas, como a Integridade de Fluxo de Controle (CFI), que dependem de assinaturas de tipos precisas para mitigar ataques como Return-Oriented Programming (ROP).

Evolução Metodológica
O levantamento traça a evolução da Inferência de Tipo Binário (BTI) através de três paradigmas distintos, analisando como o campo mudou de sistemas manuais baseados em regras para arquiteturas de aprendizado profundo orientadas a dados:

1. Era das Heurísticas e Resolução de Restrições: As abordagens iniciais dependiam de conhecimento especializado manual e "duck typing" baseado em regras (ex: se uma variável é usada como índice, ela é um ponteiro). Ferramentas como IDA Pro e Ghidra utilizam essas heurísticas. Posteriormente, sistemas como BinSub e Retypd formalizaram a BTI como um problema de satisfação de restrições sobre um reticulado de tipos (type lattice). Esses métodos algébricos usam lógica simbólica para derivar "tipos principais" baseados no comportamento da instrução (ex: mov eax, [ebx+8] implica que ebx é um ponteiro). Embora formalmente consistentes, esses métodos são frágeis, enfrentando dificuldades com otimizações agressivas de compiladores (ex: Omissão de Ponteiro de Quadro/Frame Pointer Omission) e "variáveis órfãs" que carecem de restrições de fluxo de dados suficientes.
2. Modelos Neurais Sequenciais: Inspirada pelo Processamento de Linguagem Natural (NLP), esta onda trata as instruções de assembly como sequências textuais. Sistemas como BITY (usando SVMs), EKLAVYA (usando RNNs) e CATI (usando CNNs) mapeiam opcodes e operandos em espaços vetoriais para capturar contextos de uso local (Variable Usage Context - VUC). Embora esses modelos melhorem a robustez em dados esparsos, eles sofrem com o problema do desaparecimento do gradiente (vanishing gradient) e têm dificuldade em capturar dependências de longo alcance dentro de grandes funções.
3. Arquiteturas Estruturais e Baseadas em Transformers: O estado da arte atual aproveita Redes Neurais de Grafos (GNNs) e Transformers. Modelos como o TYGR constroem Grafos de Fluxo de Dados (DFGs) para capturar dependências topológicas, permitindo a propagação de características estruturais (ex: padrões de desreferência) através do grafo. O SeeType utiliza arquiteturas Transformer com mecanismos de Auto-Atenção (Self-Attention) para modelar dependências globais simultaneamente, superando as limitações sequenciais das RNNs. Essas abordagens também introduzem a "Tokenização Consciente de Numéricos" (Numeric-Aware Tokenization), tratando offsets específicos (ex: 0x8, 0x10) como dicas estruturais explícitas em vez de tokens genéricos, auxiliando significativamente na recuperação de layout.

Principais Contribuições

• Taxonomia Unificada: O artigo fornece uma categorização abrangente das metodologias de BTI, mapeando a transição da subtipagem algébrica para modelos sequenciais de NLP e, finalmente, para GNNs estruturais e Transformers.
• Análise Anatômica: Ele desconstrói o pipeline de BTI em quatro componentes fundamentais: Identificação de Variáveis (lidando com registradores, offsets de pilha e heap), Elevação para Representação Intermediária (IR) (ex: VEX, LLVM-IR), Extração de Características (características de fluxo de dados, contextuais e estruturais) e o Mecanismo de Resolução de Tipos (solvers lógicos vs. modelos probabilísticos).
• Identificação de Desafios Críticos: O levantamento sintetiza quatro obstáculos primários enfrentados pela BTI moderna:
  • Perda de Semântica sob Otimização: Otimizações agressivas de compilador (ex: -O3, FPO) distorcem a anatomia do programa, reordenando instruções e reutilizando registradores, o que quebra suposições heurísticas.
  • Lacuna de Literacia Numérica: Modelos tradicionais frequentemente mascaram valores numéricos, cegando o sistema para pistas estruturais críticas contidas em offsets.
  • Ambiguidade Topológica: Tipos complexos (structs vs. unions) frequentemente exibem sobreposição topológica na forma binária, tornando a reconstrução detalhada de membros difícil sem análise interprocedural.
  • Integridade de Dataset: A prevalência de funções duplicadas em datasets padrão leva os modelos a "memorizar" em vez de generalizar, inflando métricas de precisão.
• Roteiro Futuro: Os autores propõem três direções de pesquisa de alto impacto:
  1. Modelos de Fundação Binária: Desenvolver modelos de auto-supervisão pré-treinados em bilhões de linhas de assembly não rotulado para aprender uma "gramática de assembly universal", permitindo inferência zero-shot entre diferentes arquiteturas.
  2. Integração Neuro-Simbólica: Combinar a intuição estatística de geradores neurais (ex: SeeType) com a verificação formal de motores de lógica simbólica (ex: BinSub) para garantir que os outputs sejam tanto estatisticamente prováveis quanto logicamente consistentes.
  3. Síntese de Estrutura Automatizada: Ir além da classificação para a predição generativa de arquivos de cabeçalho completos, contabilizando alinhamento, preenchimento (padding) e ponteiros aninhados.

Resultados e Desempenho
O artigo observa que, embora o aprendizado profundo tenha elevado significativamente o teto de precisão para a inferência de tipos, particularmente na reconstrução de tipos de structs detalhados, nenhum método é perfeito.

• Solvers de Restrições oferecem alta precisão verificável quando as restrições são completas, mas falham em dados esparsos.
• Modelos Sequenciais melhoram a robustez, mas lutam com dependências de longo alcance.
• GNNs e Transformers alcançam resultados de estado da arte ao capturar formas de fluxo de dados globais e dependências de longo alcance. No entanto, eles incorrem em custos computacionais mais altos e ainda enfrentam desafios na reconstrução da árvore interna de membros aninhados e offsets.
• Capacidades Generativas: O artigo destaca um estudo de caso onde um LLM (GPT-5) reconstruiu com sucesso código C legível a partir de assembly, demonstrando um "salto generativo" ao agrupar acessos à memória e inferir definições de structs, embora permaneça propenso a alucinações e careça de garantias de correção formal.

Significância
O artigo posiciona-se como uma ponte crítica entre a intuição de "caixa-preta" das redes neurais modernas e a lógica rigorosa da análise de programas tradicional. Argumenta que o futuro da inferência de tipos binários não reside em escolher um paradigma sobre o outro, mas sim na integração neuro-simbólica. Ao combinar a cobertura de modelos neurais para "variáveis órfãs" com a correção formal de solvers algébricos, o campo pode avançar para a reconstrução totalmente automatizada da intenção de alto nível. Esta evolução é apresentada como essencial para o avanço de sistemas de segurança autônomos, permitindo que analistas naveguem pela ambiguidade semântica de binários otimizados e sem símbolos com uma clareza sem precedentes.