💻 computer science

Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

Le papier présente Gordian, un cadre d'exécution symbolique hybride qui améliore significativement la couverture d'analyse et l'efficacité des tokens LLM en générant du code fantôme pour aider les solveurs SMT à surmonter les fragments de code hostiles, tout en préservant leur capacité de raisonnement global.

Auteurs originaux : Dimitrios Stamatios Bouras, Sergey Mechtaev

Publié 2026-03-23

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Dimitrios Stamatios Bouras, Sergey Mechtaev

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous essayez de résoudre un immense labyrinthe géant (le code d'un programme informatique) pour trouver une porte secrète (une fonctionnalité spécifique ou un bug). C'est ce que font les outils d'exécution symbolique : ils essaient de cartographier tous les chemins possibles du labyrinthe en même temps.

Mais il y a trois gros problèmes :

Les murs mathématiques : Certains passages du labyrinthe sont protégés par des énigmes mathématiques si complexes (comme des calculs de trigonométrie ou des nombres à virgule flottante) que le "cerveau" du robot (le solveur) s'y perd et abandonne.
Les pièces qui changent : Le labyrinthe a des murs qui bougent ou des pièces qui apparaissent dans des endroits imprévisibles (la mémoire dynamique), ce qui crée des milliards de chemins possibles. Le robot ne peut pas tous les explorer.
La fatigue : Parfois, le robot s'épuise à essayer de tout calculer seul.

Récemment, des chercheurs ont pensé : "Et si on utilisait une Intelligence Artificielle (une IA très puissante, comme un LLM) pour remplacer le robot ?"
Le problème, c'est que l'IA est comme un génie un peu distrait : elle est brillante pour deviner la solution d'une énigme isolée, mais elle perd le fil quand il faut relier des dizaines d'énigmes entre elles pour traverser tout le labyrinthe. Elle fait des erreurs de logique à grande échelle.

La Solution : Gordian, le "Couteau Suisse"

Les auteurs de cette paper proposent Gordian. Au lieu de remplacer le robot par l'IA, Gordian les fait travailler en équipe.

Imaginez que le robot est un architecte rigoureux qui sait tout calculer parfaitement, mais qui est lent et bloqué par les énigmes trop dures. L'IA est un artiste créatif qui voit les choses différemment, mais qui n'est pas très bon en mathématiques pures.

Gordian utilise l'IA pour créer de la "Code Fantôme" (Ghost Code). C'est comme si l'IA dessinait des ponts temporaires ou des raccourcis pour aider l'architecte à passer les obstacles.

Voici les trois types de "ponts" (ou astuces) que Gordian utilise :

1. Le Pont à Double Sens (Inversion)

Le problème : L'architecte arrive devant un mur avec une porte verrouillée par une formule mathématique compliquée. Il ne sait pas comment tourner la clé pour ouvrir la porte.
L'astuce Gordian : L'IA regarde la porte et dit : "Attends, si je marche à reculons depuis l'autre côté, je vois comment la clé tourne !". Elle écrit un petit programme qui fait l'inverse de l'énigme.
Le résultat : Le robot utilise ce "chemin inverse" pour comprendre comment entrer dans la pièce, puis il vérifie avec ses propres calculs rigoureux si c'est bien possible. C'est comme si l'IA donnait la clé à l'architecte, qui vérifie ensuite si elle ouvre bien la porte.

2. Le Mannequin de Remplacement (Surrogates)

Le problème : Parfois, l'énigme est si complexe (comme un calcul de cryptographie ou une simulation physique) que le robot ne peut pas la résoudre du tout.
L'astuce Gordian : L'IA dit : "On ne va pas résoudre l'énigme exacte, c'est trop dur. On va mettre un mannequin à la place qui se comporte presque pareil, mais qui est facile à comprendre pour le robot."
Le résultat : Le robot traverse le labyrinthe avec ce mannequin simplifié. Une fois qu'il a trouvé un chemin intéressant, il vérifie après coup avec le vrai code pour s'assurer que le mannequin ne l'a pas trompé.

3. Le Tri des Chemins (Partitionnement de la Mémoire)

Le problème : Le labyrinthe a des milliers de pièces vides qui peuvent être remplies de n'importe quoi. Le robot essaie de tout explorer et explose de fatigue (c'est l'explosion de chemins).
L'astuce Gordian : L'IA dit : "Regarde, dans ce type de labyrinthe, les pièces ne sont pas aléatoires. Elles forment soit un cercle, soit une ligne, soit un arbre. On va ne tester que ces trois formes logiques."
Le résultat : Au lieu d'essayer des milliards de configurations, le robot ne teste que les formes qui ont du sens. Cela réduit le travail de 99% tout en gardant les chemins les plus importants.

Pourquoi c'est génial ?

Dans les tests réels (sur des bibliothèques mathématiques complexes et des logiciels de traitement de fichiers), Gordian a été un véritable champion :

Il a trouvé 52% à 84% de chemins en plus que les robots classiques.
Il a trouvé 86% à 419% de chemins en plus que les méthodes qui utilisent uniquement l'IA.
Et le plus important : il a utilisé 90% à 96% moins de "tokens" (c'est-à-dire moins de "pensées" ou de calculs coûteux de l'IA).

En résumé :
Gordian ne remplace pas le cerveau mathématique par un cerveau créatif. Il utilise le cerveau créatif pour construire des échelles et des ponts là où le cerveau mathématique est bloqué, tout en gardant le cerveau mathématique comme gardien final pour s'assurer que tout est exact. C'est une équipe parfaite : l'IA apporte l'intuition, le robot apporte la rigueur.

1. Problématique

L'exécution symbolique est une technique puissante d'analyse de programmes, mais son efficacité est fondamentalement limitée par trois obstacles majeurs :

Fragments hostiles aux solveurs : Les calculs complexes (arithmétique non linéaire, fonctions trigonométriques, nombres à virgule flottante) génèrent des contraintes SMT (Satisfiability Modulo Theories) difficiles ou impossibles à résoudre.
Modélisation de l'environnement : La précision requise pour modéliser les appels système ou les structures de données dynamiques est souvent inatteignable.
Explosion des chemins : La taille infinie de l'espace d'exécution, notamment avec des structures de données dynamiques (tas, pointeurs), rend l'exploration exhaustive impossible.

Les approches récentes tentant de remplacer les solveurs SMT par des Modèles de Langage (LLM) pour générer des tests échouent souvent sur des bases de code réelles. En effet, les LLM peinent à maintenir une cohérence globale sur de longs chemins d'exécution impliquant de multiples fonctions et contraintes interdépendantes, là où les solveurs SMT excellent.

2. Méthodologie : Le Framework Gordian

Les auteurs proposent Gordian, un framework hybride d'exécution symbolique qui n'utilise pas le LLM pour remplacer le solveur, mais pour générer du « code fantôme » (ghost code) léger afin d'aider le solveur SMT à surmonter les fragments hostiles.

Le système fonctionne en trois étapes clés :

Identification : Le LLM analyse le code pour identifier les fragments difficiles (ex: opérations mathématiques complexes, structures de données dynamiques).
Génération de Code Fantôme : Selon le contexte, le LLM génère l'un des trois types de code fantôme suivants :
- Inversion de fragments (Ghost Inversion) : Pour les opérations non inversibles par le solveur (ex: sin(x)), le LLM génère une procédure d'inversion (ex: recherche par section dorée). Cela permet une propagation bidirectionnelle des contraintes : le solveur résout les contraintes de la fin du chemin, et le code fantôme inverse propage ces valeurs vers l'entrée pour satisfaire les contraintes de début.
- Modèles de substitution (Surrogate Models) : Pour les fragments trop complexes, le LLM génère une version simplifiée et « friendly » pour le solveur (ex: remplacer une fonction cryptographique par un stub) qui préserve le comportement logique nécessaire aux branches de contrôle.
- Partitionnement sémantique du tas (Semantic Heap Partitioning) : Pour les structures de données dynamiques, le LLM génère du code qui contraint le tas à des topologies sémantiques spécifiques (ex: une liste chaînée de longueur $\ge$ 3, un cycle valide). Cela réduit l'espace de recherche en évitant l'exploration de formes de tas non pertinentes, tout en laissant les valeurs des nœuds symboliques.
Validation de la justesse (Soundness) : Le code fantôme est considéré comme une aide heuristique. Toute entrée générée est exécutée sur le programme original pour vérifier qu'elle atteint bien la branche cible, garantissant ainsi que les hallucinations du LLM n'affectent pas la validité des résultats.

3. Contributions Clés

Approche Hybride Innovante : Intégration sélective des LLM dans l'exécution symbolique pour générer du code d'assistance, préservant la capacité de raisonnement global et précis des solveurs SMT.
Trois Variations de Code Fantôme : Définition et implémentation de l'inversion, des modèles de substitution et du partitionnement sémantique du tas, accompagnés de prompts et d'algorithmes d'intégration spécifiques.
Évaluation Exhaustive : Une validation rigoureuse sur des benchmarks synthétiques (LogicBombs), une bibliothèque mathématique réelle (FDLibM) et des programmes traitant des entrées structurées (libexpat, jq, bc).

4. Résultats Expérimentaux

Les expériences ont été menées sur le moteur KLEE avec Z3/STP, comparant Gordian aux exécutions symboliques traditionnelles et aux approches purement basées sur les LLM (ConcoLLMic, Cottontail).

Couverture de Code :
- Sur le benchmark LogicBombs, Gordian a déclenché jusqu'à 94,3 % des « bombes logiques », soit une amélioration de 138 % par rapport à KLEE et 47 % par rapport à ConcoLLMic.
- Sur la bibliothèque mathématique FDLibM, Gordian a atteint une couverture moyenne de 91,7 %, surpassant KLEE (+22 %) et ConcoLLMic (+183 %).
- Sur les programmes à entrées structurées (libexpat, jq, bc), Gordian a amélioré la couverture totale de 79 % à 108 % par rapport à KLEE et a couvert 9,7 fois plus de lignes que ConcoLLMic.
Efficacité des Tokens LLM :
- Gordian est extrêmement économe en tokens. Il réduit l'utilisation des tokens LLM de 90 % à 96 % par rapport aux approches purement LLM (ConcoLLMic et Cottontail), car le LLM n'est invoqué que pour générer du code statique et non pour raisonner sur chaque chemin d'exécution.
Analyse de Composantes : L'ablation a montré que les trois techniques de code fantôme sont complémentaires ; leur union (Gordian) couvre presque tous les cas, là où les techniques individuelles ne couvrent que des sous-ensembles distincts.

5. Signification et Impact

Cet article démontre que l'intégration des LLM dans l'exécution symbolique ne doit pas se faire par un remplacement du solveur, mais par une collaboration ciblée.

Pragmatisme : Gordian résout le dilemme entre la précision des solveurs SMT (nécessaire pour les dépendances globales) et la flexibilité des LLM (nécessaire pour les mathématiques complexes et la structure des données).
Passage à l'échelle : La méthode permet d'analyser des bases de code réels et complexes (bibliothèques mathématiques, parseurs XML/JSON) qui étaient auparavant inaccessibles aux outils d'exécution symbolique classiques.
Économie de ressources : En minimisant l'usage des LLM, l'approche rend l'analyse formelle plus viable économiquement et techniquement pour des projets industriels.

En conclusion, Gordian représente une avancée majeure vers l'automatisation de l'analyse de programmes complexes, en « désamorçant » les obstacles logiques grâce à une assistance intelligente et vérifiée par le LLM.