Résumé Technique : Veritas

Énoncé du Problème

La détection des vulnérabilités de corruption de mémoire (MCV) dans les binaires dépouillés présente un défi fondamental de reconstruction sémantique. Contrairement à l'analyse du code source, l'analyse binaire doit reconstruire la manière dont les objets mémoire sont alloués, propagés, contraints et accédés à travers les fonctions, à partir d'artefacts ayant perdu leur structure de haut niveau, leurs limites d'objets et leur flux de contrôle explicite en raison de la compilation et du dépouillement.

Les approches récentes basées sur les grands modèles de langage (LLM) ont amélioré la compréhension du code mais peinent à détecter les MCV dans les binaires pour trois raisons principales :

1. Suivi de l'État Partagé : Les vulnérabilités résultent souvent d'hypothèses incohérentes concernant des régions de mémoire partagées à travers des fonctions disjointes dépourvues d'arêtes de chaîne d'appel directes. L'expansion standard du graphe d'appel échoue à capturer ces dépendances.
2. Perte Sémantique : Les représentations reconstruites sont fragmentées. Le LLVM IR remonté préserve les motifs d'accès mémoire de bas niveau mais est obscurci par les artefacts du compilateur (variables SSA, castes), tandis que le C décompilé fournit une structure de haut niveau mais réduit les opérations mémoire à des expressions d'offset génériques, effaçant l'identité des objets.
3. Vérification des Contraintes : L'analyse statique ne peut souvent pas déterminer si un accès suspect est atteignable sous des conditions de chemin réalisables. Sans preuve exécutable, les LLM s'appuient sur des proxies syntaxiques plutôt que sur une preuve de la propagation des données contrôlées par l'attaquant vers des opérations sensibles à la mémoire, conduisant à un raisonnement fragile et à un taux élevé de faux positifs.

Les cadres d'agents existants conçus pour le code source (reposant sur la synthèse ou l'expansion du graphe d'appel) ne résolvent pas le problème de récupération sémantique posé par les binaires dépouillés, où la structure sémantique requise est partiellement absente par construction.

Méthodologie

Veritas est un cadre d'agents hybride et ancré sémantiquement conçu pour contraindre le raisonnement des LLM à des sémantiques de programme vérifiables et à un comportement exécutable. Il organise l'analyse en trois étapes alignées sur deux couches d'ancrage : Ancrage Statique (faits de programme reconstruits) et Ancrage Exécutif (preuves d'exécution concrète).

1. Sliceur de Contexte Piloté par la Sémantique (Ancrage Statique)

Le Sliceur opère sans LLM pour extraire des flux source-à-sink compacts, étayés par des témoins, à partir du LLVM IR remonté.

• Graphe de Propagation Interprocédural : Il remonte le binaire vers le LLVM IR en utilisant RetDec et construit un graphe de propagation interprocédural typé ($G_P$) codant les dépendances d'appel, de retour et globales. Ce graphe suit la propagation des valeurs pertinentes pour la taint (pointeurs, offsets, longueurs) à travers les fonctions.
• Extraction de Flux Basée sur les Témoins : Au lieu de traiter toutes les paires source-sink atteignables comme significatives, le Sliceur vérifie des témoins interprocéduraux bornés. Il trace les jetons taintés depuis les sources d'entrée (par exemple fread) jusqu'aux sinks à risque mémoire (par exemple, arguments d'API dangereux), validant la propagation à chaque frontière de fonction à l'aide de chaînes def-use et de métadonnées.
• Construction d'Objets de Flux : Les témoins acceptés sont convertis en objets de flux compacts contenant des fonctions ordonnées, des jetons pertinents pour la taint et des « indices d'ancrage » (classes de provenance et annotations de point de terminaison). Cela remplace le binaire complet par un contexte petit et sémantiquement complet pour l'analyse en aval.

2. Détecteur de Vulnérabilités à Double Vue (Raisonnement Contrôlé par LLM)

Le Détecteur effectue un raisonnement étape par étape sur les flux étayés par des témoins, utilisant une représentation d'entrée à double vue pour surmonter la perte sémantique.

• Représentation à Double Vue : Pour les fonctions source et sink, le LLM reçoit à la fois le code C décompilé (pour le raisonnement sur le flux de contrôle) et le LLVM IR remonté (pour désambiguïser les opérations mémoire et la sémantique des sinks). Pour les fonctions intermédiaires, il utilise principalement le code décompilé, guidé par les indices d'ancrage.
• Raisonnement Étape par Étape : Le LLM analyse le flux une fonction à la fois, maintenant un état de raisonnement accumulé (inventaire des valeurs propagées, alias et bornes). Il met à jour cet état en fonction des affectations et des décisions de flux de contrôle, évitant ainsi les limites de contexte liées au traitement du flux entier en une seule fois.
• Mémoïsation Basée sur les Arbres de Préfixes (Trie) : Pour réduire la redondance, le système mémoïse les états de raisonnement pour les préfixes de flux partagés, n'invocant le LLM que sur le suffixe unique d'un flux.
• Vérification de Cohérence : Avant de signaler un candidat, le Détecteur effectue une vérification finale sensible au chemin pour s'assurer que la valeur taintée reste pertinente pour la vulnérabilité et que l'accès au sink viole la sécurité de la mémoire dans des conditions réalisables.

3. Validateur Automatique de Vulnérabilités (Ancrage Exécutif)

Le Validateur traduit les hypothèses du détecteur en vérifications exécutables pour confirmer ou réfuter les candidats.

• Préparation des Artefacts : Il mappe les hypothèses du détecteur vers des coordonnées exécutables (RVA, symboles) en utilisant Radare2, comblant le fossé entre les vues du décompilateur et le débogage exécutif.
• Collaboration Multi-Agents : Trois agents orchestrent la validation :
  • Stratège : Planifie la validation, sélectionnant les cibles d'instrumentation, les points d'arrêt et les modalités de déclenchement (fichier, réseau, CLI).
  • Vérificateur : Exécute le plan, génère des Preuves de Concept (PoC) et exécute le binaire sous des débogueurs (Radare2) ou des vérificateurs de mémoire (Valgrind) pour observer les plantages ou les accès invalides.
  • Explorateur : Si les preuves initiales sont insuffisantes, il sonde des états alternatifs ou des fonctions connexes pour trouver des preuves de soutien.
• Confirmation : Une vulnérabilité est confirmée uniquement lorsque des preuves concrètes d'exécution (par exemple, une violation de segment, une erreur Valgrind ou un état mémoire spécifique) corroborent le sink signalé, le motif d'accès et la cause racine.

Contributions Clés

1. Cadre Veritas : Un cadre d'agents ancré sémantiquement qui unifie l'analyse statique de programme et la validation exécutif pour détecter la corruption de mémoire dans les binaires dépouillés.
2. Architecture en Trois Étapes :
   • Un Sliceur qui extrait des flux étayés par des témoins à partir d'IR remonté sans LLM.
   • Un Détecteur à Double Vue qui raisonne sur les flux en utilisant un support IR sélectif pour résoudre l'ambiguïté sémantique.
   • Un Validateur qui confirme les hypothèses en utilisant des artefacts visibles par le débogueur et une exécution concrète.
3. Benchmark Finement Granulaire : Un ensemble de données curaté de 20 cas réels de corruption de mémoire binaire avec une vérité de terrain au niveau des traces, construit pour évaluer la détection binaire ancrée.
4. Performance : L'évaluation montre que Veritas atteint un rappel de 90 % sur le benchmark, surpassant significativement les analyseurs statiques (0 % de rappel), le fuzzing (10 % de rappel) et les bases de référence d'agents (25–35 % de rappel). Il a produit zéro faux positif lors d'une validation exhaustive de 623 candidats et seulement 2 faux positifs dans un audit échantillonné plus large.
5. Découverte Réelle : Veritas a découvert une lecture hors limites zero-day inconnue précédemment dans la bibliothèque Universal Scene Description d'Apple (libusd_ms.dylib), qui a été confirmée et attribuée un CVE.

Résultats et Signification

L'article soutient que l'efficacité de la découverte de vulnérabilités basée sur les LLM ne dépend pas uniquement de la capacité intrinsèque du modèle, mais de la capacité de l'infrastructure environnante à reconstruire la structure sémantique requise pour le raisonnement.

• Ancrage Sémantique comme Principe de Conception : Les résultats soutiennent l'ancrage sémantique comme principe de conception opérationnel. En contraignant le raisonnement des LLM à des faits explicites pertinents pour la mémoire (ancrage statique) et en validant les conclusions contre un comportement exécutable (ancrage exécutif), Veritas évite la fragilité des spéculations de modèles non contraints.
• Supériorité sur les Bases de Référence : Les outils traditionnels échouent en raison d'un manque d'ancrage sémantique à travers les fonctions. Les bases de référence d'agents échouent car elles manquent de modèles explicites des cycles de vie des objets mémoire et s'appuient sur une exploration non guidée ou des motifs syntaxiques. Veritas comble ce fossé en utilisant une analyse déterministe pour pré-calculer la propagation et des LLM pour interpréter des sémantiques complexes, suivis d'une confirmation exécutif rigoureuse.
• Compromis Coût-Précision : Bien que la validation exécutif soit le principal goulot d'étranglement en termes de coûts (nécessitant la génération de PoC et le débogage), le cadre démontre qu'une haute précision est réalisable dans l'analyse de binaires dépouillés uniquement par des preuves exécutables. Le système privilégie la fiabilité de la détection au débit, un compromis nécessaire pour l'analyse binaire critique pour la sécurité.

L'article conclut que pour la détection pratique de vulnérabilités binaires, le raisonnement doit être ancré à la fois dans les sémantiques de programme reconstruites et les preuves exécutables, un principe que Veritas met en œuvre grâce à son architecture hybride et modulaire.