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

Sintesi Tecnica: Dalle Euristiche ai Transformer: Un'analisi esaustiva dell'inferenza dei tipi da binari privi di simboli

Definizione del Problema
Il recupero delle informazioni sui tipi ad alto livello da binari privi di simboli (stripped)—eseguibili privi di tabelle dei simboli e informazioni di debug (es. DWARF)—rimane una sfida fondamentale nel reverse engineering del software, nell'analisi delle vulnerabilità e nella decompilazione. La compilazione è una trasformazione con perdita di informazioni (lossy), dove astrazioni di alto livello come i tipi di dati vengono rimosse, lasciando un "deserto semantico" di istruzioni assembly grezze. Nei binari privi di simboli, questa perdita è esacerbata dalla rimozione dei metadati di debug. Di conseguenza, distinguere tra puntatori e interi, identificare strutture dati complesse (array, struct, union) e comprendere il flusso di controllo diventa intrinsecamente difficile. Questa asimmetria tra l'intento del codice sorgente e la realtà del codice macchina ostacola le applicazioni di sicurezza automatizzate, come il Control-Flow Integrity (CFI), che si basano su firme di tipo precise per mitigare attacchi come il Return-Oriented Programming (ROP).

Evoluzione Metodologica
La survey traccia l'evoluzione della Binary Type Inference (BTI) attraverso tre distinti paradigmi, analizzando come il campo si sia spostato dai sistemi manuali basati su regole ai modelli di deep learning guidati dai dati:

1. Era delle Euristiche e della Risoluzione dei Vincoli: I primi approcci si affidavano alla conoscenza manuale degli esperti e al "duck typing" basato su regole (es. se una variabile è usata come indice, allora è un puntatore). Strumenti come IDA Pro e Ghidra utilizzano queste euristiche. Successivamente, sistemi come BinSub e Retypd hanno formalizzato la BTI come un problema di soddisfacimento di vincoli su un reticolo di tipi (type lattice). Questi metodi algebrici utilizzano la logica simbolica per derivare "tipi principali" basati sul comportamento delle istruzioni (es. mov eax, [ebx+8] implica che ebx è un puntatore). Sebbene formalmente corretti, questi metodi sono fragili, faticano di fronte a ottimizzazioni aggressive del compilatore (es. Frame Pointer Omission) e con le "variabili orfane" prive di sufficienti vincoli di data flow.
2. Modelli Neurali Sequenziali: Ispirata al Natural Language Processing (NLP), questa ondata tratta le istruzioni assembly come sequenze testuali. Sistemi come BITY (utilizzando SVM), EKLAVYA (utilizzando RNN) e CATI (utilizzando CNN) mappano gli opcode e gli operandi in spazi vettoriali per catturare i contesti di utilizzo locale (Variable Usage Context - VUC). Sebbene questi modelli migliorino la robustezza su dati sparsi, soffrono del problema della scomparsa del gradiente (vanishing gradient) e faticano a catturare dipendenze a lungo raggio all'interno di grandi funzioni.
3. Architetture Strutturali e basate su Transformer: Lo stato dell'arte attuale sfrutta le Graph Neural Networks (GNN) e i Transformer. Modelli come TYGR costruiscono Data-Flow Graphs (DFG) per catturare le dipendenze topologiche, permettendo la propagazione delle caratteristiche strutturali (es. pattern di dereferenziazione) attraverso il grafo. SeeType utilizza architetture Transformer con meccanismi di Self-Attention per modellare simultaneamente le dipendenze globali, superando i limiti sequenziali delle RNN. Questi approoli introducono anche la "Tokenizzazione Consapevole dei Numeri" (Numeric-Aware Tokenization), trattando specifici offset (es. 0x8, 0x10) come indizi strutturali espliciti piuttosto che come token generici, aiutando significativamente il recupero del layout.

Contributi Chiave

• Tassonomia Unificata: Il documento fornisce una categorizzazione completa delle metodologie BTI, mappando la transizione dal sottotipaggio algebrico ai modelli NLP sequenziali e, infine, alle GNN strutturali e ai Transformer.
• Analisi Anatomica: Decostruisce la pipeline BTI in quattro componenti fondamentali: Identificazione delle Variabili (gestione di registri, offset dello stack e heap), Lifting della Rappresentazione Intermedia (IR) (es. VEX, LLVM-IR), Estrazione delle Caratteristiche (caratteristiche di data-flow, contestuali e strutturali) e il Motore di Risoluzione dei Tipi (solutori logici vs modelli probabilistici).
• Identificazione delle Sfide Critiche: La survey sintetizza quattro ostacoli primari che affrontano la moderna BTI:
  • Perdita di Semantica sotto Ottimizzazione: Le ottimizzazioni aggressive del compilatore (es. -O3, FPO) distorcono l'anatomia del programma, riordinando le istruzioni e riutilizzando i registri, il che rompe le assunzioni euristiche.
  • Gap di Alfabetismo Numerico: I modelli tradizionali spesso mascherano i valori numerici, accecando il sistema rispetto ai critici indizi strutturali contenuti negli offset.
  • Ambiguità Topologica: I tipi complessi (struct vs union) spesso presentano una sovrapposizione topologica nella forma binaria, rendendo difficile la ricostruzione fine dei membri senza un'analisi inter-procedurale.
  • Integrità dei Dataset: La prevalenza di funzioni duplicate nei dataset standard porta i modelli a "memorizzare" piuttosto che generalizzare, gonfiando le metriche di accuratezza.
• Roadmap Futura: Gli autori propongono tre direzioni di ricerca ad alto impatto:
  1. Modelli di Fondazione per i Binari: Sviluppare modelli auto-supervisionati pre-addestrati su miliardi di righe di assembly non etichettate per apprendere una "grammatica assembly universale", consentendo l'inferenza zero-shot tra diverse architetture.
  2. Integrazione Neuro-Simbolica: Combinare l'intuizione statistica dei generatori neurali (es. SeeType) con la verifica formale dei motori di logica simbolica (es. BinSub) per garantire che gli output siano sia statisticamente probabili che logicamente consistenti.
  3. Sintesi Automatica delle Strutture: Passare dalla classificazione alla predizione generativa di file header completi, tenendo conto di allineamento, padding e puntatori annidati.

Risultati e Prestazioni
Il documento nota che, sebbene il deep learning abbia alzato significativamente il tetto dell'accuratezza per l'inferenza dei tipi, in particolare per la ricostruzione di tipi di struct granulari, nessun approccio è perfetto.

• I Solutori di Vincoli offrono un'alta accuratezza verificabile quando i vincoli sono completi, ma falliscono su dati sparsi.
• I Modelli Sequenziali migliorano la robustezza ma faticano con le dipendenze a lungo raggio.
• GNN e Transformer raggiungono risultati allo stato dell'arte catturando le forme globali del data-flow e le dipendenze a lungo raggio. Tuttavia, comportano costi computazionali più elevati e affrontano ancora sfide nella ricostruzione dell'albero interno di membri annidati e offset.
• Capacità Generative: La paper evidenzia un caso di studio in cui un LLM (GPT-5) ha ricostruito con successo codice C leggibile dal codice assembly, dimostrando un "salto generativo" nel raggruppare gli accessi alla memoria e inferire definizioni di struct, sebbene rimanga incline alle allucinazioni e privo di garanzie di correttezza formale.

Significatività
Il documento posiziona la ricerca come un ponte critico tra l'intuizione "black-box" dei moderni modelli neurali e il rigore logico dell'analisi tradizionale dei programmi. Argomenta che il futuro dell'inferenza dei tipi binari non risiede nella scelta di un paradigma rispetto a un altro, ma nell'integrazione neuro-simbolica. Combinando la copertura dei modelli neurali per le "variabili orfane" con la correttezza formale dei solutori algebrici, il campo può muoversi verso una ricostruzione completamente automatizzata dell'intento di alto livello. Questa evoluzione è presentata come essenziale per far avanzare i sistemi di sicurezza autonomi, consentendo agli analisti di navigare l'ambiguità semantica dei binari ottimizzati e privi di simboli con una chiarezza senza precedenti.