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

Résumé Technique : Des heuristiques aux Transformers : Une étude exhaustive de l'inférence de types à partir de binaires dépouillés

Énoncé du problème
La récupération d'informations de type de haut niveau à partir de binaires dépouillés — des exécutables dépourvus de tables de symboles et d'informations de débogage (par exemple, DWARF) — demeure un défi fondamental dans la rétro-ingénierie de logiciels, l'analyse de vulnérabilités et la décompilation. La compilation est une transformation destructrice où les abstractions de haut niveau comme les types de données sont supprimées, laissant derrière elles un « désert sémantique » d'instructions assembleur brutes. Dans les binaires dépouillés, cette perte est exacerbée par la suppression des métadonnées de débogage. Par conséquent, distinguer les pointeurs des entiers, identifier des structures de données complexes (tableaux, structures, unions) et comprendre le flux de contrôle devient intrinsèquement difficile. Cette asymétrie entre l'intention du code source et la réalité du code machine entrave les applications de sécurité automatisées, telles que l'intégrité du flux de contrôle (CFI), qui reposent sur des signatures de types précises pour atténuer des attaques comme le Return-Oriented Programming (ROP).

Évolution méthodologique
L'étude retrace l'évolution de l'inférence de type binaire (BTI) à travers trois paradigmes distincts, analysant comment le domaine est passé de systèmes manuels basés sur des règles à des architectures d'apprentissage profond fondées sur les données :

1. L'ère des heuristiques et de la résolution de contraintes : Les premières approches reposaient sur l'expertise manuelle et le « duck typing » basé sur des règles (par exemple, si une variable est utilisée comme un index, c'est un pointeur). Des outils comme IDA Pro et Ghidra utilisent ces heuristiques. Plus tard, des systèmes comme BinSub et Retypd ont formalisé la BTI comme un problème de satisfaction de contraintes sur un treillis de types. Ces méthodes algébriques utilisent la logique symbolique pour dériver des « types principaux » basés sur le comportement des instructions (par exemple, mov eax, [ebx+8] implique que ebx est un pointeur). Bien que formellement rigoureuses, ces méthodes sont fragiles, peinant face aux optimisations agressives du compilateur (par exemple, l'omission du pointeur de trame ou FPO) et les « variables orphelines » manquant de contraintes de flux de données suffisantes.
2. Modèles neuronaux séquentiels : Inspirée par le traitement du langage naturel (NLP), cette vague traite les instructions assembleur comme des séquences textuelles. Des systèmes comme BITY (utilisant des SVM), EKLAVYA (utilisant des RNN) et CATI (utilisant des CNN) projettent les opcodes et les opérandes dans des espaces vectoriels pour capturer les contextes d'utilisation locale (Variable Usage Context - VUC). Bien que ces modèles améliorent la robustesse sur des données éparses, ils souffrent du problème de disparition du gradient et peinent à capturer les dépendances à longue portée au sein des grandes fonctions.
3. Architectures structurelles et basées sur les Transformers : L'état de l'art actuel exploite les réseaux de neurones sur graphes (GNN) et les Transformers. Des modèles comme TYGR construisent des graphes de flux de données (DFG) pour capturer les dépendances topologiques, permettant la propagation de caractéristiques structurelles (par exemple, les motifs de déréférencement) à travers le graphe. SeeType utilise des architectures Transformer avec des mécanismes d'auto-attention (Self-Attention) pour modéliser simultanément les dépendances globales, dépassant les limitations séquentielles des RNN. Ces approches introduisent également une « tokenisation sensible aux nombres » (Numeric-Aware Tokenization), traitant les décalages spécifiques (par exemple, 0x8, 0x10) comme des indices structurels explicites plutôt que comme des jetons génériques, ce qui aide considérablement la récupération de la disposition (layout).

Contributions clés

• Taxonomie unifiée : Le document fournit une catégorisation complète des méthodologies de BTI, cartographiant la transition de la sous-typation algébrique vers les modèles de NLP séquentiels, puis vers les GNN structurels et les Transformers.
• Analyse anatomique : Il déconstruit le pipeline de la BTI en quatre composants fondamentaux : l'identification des variables (gestion des registres, des décalages de pile et du tas), l'élévation en représentation intermédiaire (IR) (par exemple, VEX, LLVM-IR), l'extraction de caractéristiques (flux de données, contextuelles et structurelles) et le moteur de résolution de types (solveurs logiques vs modèles probabilistes).
• Identification des défis critiques : L'étude synthétise quatre obstacles principaux faisant face à la BTI moderne :
  • Perte de sémantique sous l'effet de l'optimisation : Les optimisations agressives du compilateur (par exemple, -O3, FPO) déforment l'anatomie du programme, réordonnant les instructions et réutilisant les registres, ce qui brise les hypothèses heuristiques.
  • Écart de littératie numérique : Les modèles traditionnels masquent souvent les valeurs numériques, aveuglant le système aux indices structurels critiques contenus dans les décalages (offsets).
  • Ambiguïté topologique : Les types complexes (structures vs unions) présentent souvent un chevauchement topologique dans la forme binaire, rendant la reconstruction fine des membres difficile sans analyse inter-procédurale.
  • Intégrité des jeux de données : La prévalence de fonctions dupliquées dans les jeux de données standards conduit les modèles à « mémoriser » plutôt qu'à généraliser, gonflant ainsi artificiellement les mesures de précision.
• Feuille de route future : Les auteurs proposent trois directions de recherche à fort impact :
  1. Modèles de fondation binaires : Développer des modèles auto-supervisés pré-entraînés sur des milliards de lignes d'assembleur non étiquetées pour apprendre une « grammaire assembleur universelle », permettant une inférence zero-shot à travers différentes architectures.
  2. Intégration neuro-symbolique : Combiner l'intuition statistique des générateurs neuronaux (ex: SeeType) avec la vérification formelle des moteurs de logique symbolique (ex: BinSub) pour garantir que les résultats sont à la fois statistiquement probables et logiquement cohérents.
  3. Synthèse de structures automatisée : Passer de la classification à la prédiction générative de fichiers d'en-tête complets, en tenant compte de l'alignement, du remplissage (padding) et des pointeurs imbriqués.

Résultats et performances
Le document note que bien que l'apprentissage profond ait considérablement élevé le plafond de précision de l'inférence de type, notamment pour la reconstruction de types de structures fines, aucune approche n'est parfaite.

• Les solveurs de contraintes offrent une haute précision vérifiable lorsque les contraintes sont complètes, mais échouent sur les données éparses.
• Les modèles séquentiels améliorent la robustesse mais peinent avec les dépendances à longue portée.
• Les GNN et Transformers atteignent l'état de l'art en capturant les formes globales de flux de données et les dépendances à longue portée. Cependant, ils entraînent des coûts computationnels plus élevés et font toujours face aux défis de la reconstruction de l'arbre interne des membres imbriqués et de leurs décalages.
• Capacités génératives : Le document met en avant une étude de cas où un LLM (GPT-5) a réussi à reconstruire du code C lisible à partir de l'assembleur, démontant un « saut génératif » dans le regroupement des accès mémoire et l'inférence de définitions de structures, bien qu'il reste sujet aux hallucinations et manque de garanties de correction formelle.

Signification
Le document positionne ce travail comme un pont critique entre l'intuition de type « boîte noire » des réseaux neuronaux modernes et la rigueur logique de l'analyse de programmes traditionnelle. Il soutient que l'avenir de l'inférence de type binaire ne réside pas dans le choix d'un paradigme plutôt qu'un autre, mais dans l'intégration neuro-symbolique. En combinant la couverture des modèles neuronaux pour les « variables orphelines » avec la correction formelle des solveurs algébriques, le domaine peut tendre vers une reconstruction entièrement automatisée de l'intention de haut niveau. Cette évolution est présentée comme essentielle pour faire progresser les systèmes de sécurité autonomes, permettant aux analystes de naviguer dans l'ambiguïté sémantique des binaires optimisés et dépouillés avec une clarté sans précédent.