L'exécution symbolique (symbolic execution) est une technique d'analyse de programme qui explore systématiquement l'ensemble des chemins d'exécution possibles en remplaçant les valeurs concrètes par des valeurs symboliques. Plutôt que de lancer un binaire avec une entrée précise, le moteur représente chaque octet d'entrée comme une variable mathématique et accumule, à chaque branchement conditionnel, des contraintes sur ces variables. Un solveur SMT tel que Z3 résout ensuite ces systèmes de contraintes pour déterminer quelles entrées atteignent un état donné : une branche non couverte, un dépassement de tampon ou une primitive d'écriture arbitraire. Cette approche est au cœur des frameworks modernes de symbolic execution angr triton, largement employés en rétro-ingénierie, en désobfuscation et en recherche de vulnérabilités. Nous détaillons ici leurs architectures respectives, leurs limites — notamment l'explosion combinatoire des chemins — et leur usage concret dans la découverte d'exploits.

En bref

  • L'exécution symbolique explore systématiquement TOUS les chemins en utilisant des valeurs symboliques et un solveur SMT
  • angr est le framework standard : chargement binaire, émulation, exploration et résolution de contraintes
  • Triton combine instrumentation dynamique et exécution symbolique — plus précis mais plus lent
  • La génération automatique d'exploits cible les états où RIP est symbolique (contrôle du flux)
  • L'explosion de chemins est le problème majeur — les techniques hybrides (fuzzing + symbolic) le mitigent
  • Le concolic testing (QSYM, SymCC) est l'approche la plus efficace en pratique

En bref

  • Théorie de l'exécution symbolique : valeurs symboliques, contraintes de chemin, solveurs SMT
  • angr : architecture, projet, états, exploration stratégies et exemples pratiques
  • Triton : instrumentation dynamique symbolique avec Pin/Unicorn
  • Applications offensives : découverte automatique de vulnérabilités et génération d'exploits
  • Limitations : path explosion, environnement modeling, et techniques de mitigation
Exécution Symbolique — Technique d'analyse de programme qui exécute le code avec des variables symboliques au lieu de valeurs concrètes, accumulant des contraintes mathématiques le long de chaque chemin d'exécution. Un solveur SMT (Satisfiability Modulo Theories) détermine les valeurs d'entrée satisfaisant ces contraintes.

Principes de l'Exécution Symbolique

L'exécution symbolique repose sur trois composants fondamentaux :

ComposantRôleImplémentation
Symbolic StateÉtat complet du programme (registres, mémoire, contraintes)SimState dans angr
Path ConstraintsContraintes accumulées le long du cheminFormules SMT (bitvectors)
SMT SolverRésolution des contraintes pour trouver des entrées concrètesZ3, CVC5, Boolector

angr : Framework d'Analyse Binaire

angr est le framework d'exécution symbolique le plus utilisé en sécurité offensive. Développé par le groupe Shellphish (UC Santa Barbara), il combine l'exécution symbolique avec l'analyse statique, l'émulation concrète et la résolution de contraintes :

⚡

Retour terrain

Dans l'analyse de code malveillant, la règle que j'applique avant toute décompilation : analyser le comportement dans une sandbox avant d'ouvrir IDA ou Ghidra. Les malwares modernes incluent fréquemment des mécanismes anti-analyse qui se déclenchent en environnement de débogage — timers, vérification de breakpoints, détection de machines virtuelles. Sur les 3 derniers RATs que j'ai analysés, tous avaient au moins une technique d'anti-debug active.

#!/usr/bin/env python3
# angr — Résolution automatique d'un crackme
import angr, claripy

# Charger le binaire
proj = angr.Project('./crackme', auto_load_libs=False)

# Créer un état initial avec une entrée symbolique
password_len = 16
password = claripy.BVS('password', password_len * 8) # 16 octets symboliques

state = proj.factory.entry_state(
 args=['./crackme'],
 stdin=angr.SimFile('/dev/stdin', content=password)
)

# Configurer l'exploration
simgr = proj.factory.simulation_manager(state)

# Explorer : trouver le chemin vers "Access Granted" (0x401234)
# en évitant "Access Denied" (0x401256)
simgr.explore(find=0x401234, avoid=0x401256)

if simgr.found:
 found_state = simgr.found[0]
 solution = found_state.solver.eval(password, cast_to=bytes)
 print(f"Password: {solution}")
else:
 print("No solution found")

Génération Automatique d'Exploits avec angr

angr peut automatiser la découverte de vulnérabilités et la génération d'exploits. En configurant l'exploration pour atteindre des états dangereux (déréférence de pointeur contrôlé, appel à system(), écriture dans la GOT), le solveur SMT génère les entrées déclenchant la vulnérabilité :

# Découverte automatique de buffer overflow
import angr
from angr import sim_options as so

proj = angr.Project('./vuln_binary')

# État initial avec options de détection
state = proj.factory.entry_state(
 add_options={so.SYMBOL_FILLS_UNCONSTRAINED_MEMORY,
 so.SYMBOL_FILLS_UNCONSTRAINED_REGISTERS}
)

simgr = proj.factory.simulation_manager(state)

# Explorer jusqu'à un état "unconstrained" (RIP symbolique = contrôle du flux)
simgr.explore(
 find=lambda s: s.solver.symbolic(s.regs.rip), # RIP symbolique !
 avoid=lambda s: b"error" in s.posix.dumps(1)
)

if simgr.unconstrained:
 crash_state = simgr.unconstrained[0]
 # RIP est symbolique — on peut le résoudre vers n'importe quelle adresse
 crash_state.add_constraints(crash_state.regs.rip == 0xdeadbeef)
 exploit_input = crash_state.solver.eval(
 crash_state.posix.stdin.load(0, 200), cast_to=bytes
 )
 print(f"Exploit input (RIP=0xdeadbeef): {exploit_input}")

Triton : Exécution Symbolique Dynamique

Triton (développé par Quarkslab) combine l'instrumentation dynamique (via Pin ou l'émulation Unicorn) avec l'exécution symbolique. Contrairement à angr qui analyse le binaire statiquement puis simule l'exécution, Triton observe l'exécution réelle et construit les contraintes dynamiquement — ce qui évite les problèmes de modélisation de l'environnement.

# Triton — analyse d'un binaire avec instrumentation dynamique
from triton import *

ctx = TritonContext(ARCH.X86_64)

# Charger le binaire en mémoire
binary = open('./target', 'rb').read()
ctx.setConcreteMemoryAreaValue(0x400000, binary)

# Symboliser l'entrée
for i in range(32):
 ctx.symbolizeMemory(MemoryAccess(input_addr + i, 1), f'input_{i}')

# Émuler instruction par instruction
pc = entry_point
while pc:
 inst = Instruction(pc, ctx.getConcreteMemoryAreaValue(pc, 16))
 ctx.processing(inst)
 
 # À chaque branchement, enregistrer la contrainte de chemin
 if inst.isBranch():
 constraint = ctx.getPathPredicate()
 # Inverser la contrainte pour explorer l'autre chemin
 model = ctx.getModel(ctx.getAstContext().lnot(constraint))
 if model:
 print(f"Alternative path input: {model}")
 
 pc = ctx.getConcreteRegisterValue(ctx.registers.rip)

KLEE : Exécution Symbolique sur LLVM IR

KLEE opère sur le bytecode LLVM (IR) plutôt que sur les binaires compilés. Avantages : résolution de type plus précise, meilleure modélisation de l'environnement (libc symbolique), et intégration avec les suites de tests. KLEE a découvert des bugs dans Coreutils (GNU), des bibliothèques open-source, et des firmwares IoT. Limitation : nécessite le code source ou le bytecode LLVM.

Concolic Testing : Le Meilleur des Deux Mondes

Le concolic testing (concrete + symbolic) combine l'exécution concrète avec l'analyse symbolique. Le programme est d'abord exécuté avec une entrée concrète, les contraintes de chemin sont collectées symboliquement, puis le solveur inverse une contrainte pour générer une nouvelle entrée explorant un chemin différent. Cette approche atténue le problème d'explosion de chemins en guidant l'exploration par l'exécution concrète.

Path Explosion et Stratégies de Mitigation

Le problème majeur de l'exécution symbolique est l'explosion de chemins : à chaque branchement conditionnel, le nombre de chemins possibles double. Un programme avec N branches a potentiellement 2^N chemins. Les stratégies de mitigation :

  • Merging : fusionner les états à des points de convergence (réduire le nombre d'états actifs)
  • Pruning : élaguer les chemins qui ne mènent pas vers les cibles (guided exploration)
  • Symbolic summaries : résumer les fonctions fréquemment appelées plutôt que les ré-analyser
  • Veritesting : basculer entre exécution symbolique statique et dynamique selon le contexte
  • Fuzzing hybride : combiner exécution symbolique et fuzzing (AFL+QSYM, SymCC+AFL++)

Fuzzing Hybride : Symbolic + Coverage-Guided

Le fuzzing hybride combine la puissance du fuzzing coverage-guided (AFL++, libFuzzer) avec l'exécution symbolique pour maximiser la couverture de code. Le fuzzer explore rapidement les chemins simples, tandis que l'exécution symbolique résout les contraintes complexes (checksums, magic bytes, comparaisons multi-octets) que le fuzzing seul ne peut pas franchir.

💡 Conseil pratique — Pour débuter avec angr, commencez par les challenges CTF : angr-doc contient des exemples pour chaque type de challenge (crackme, exploitation, reversing). Le mode auto_load_libs=False accélère l'analyse en évitant de symboliser la libc complète.

À retenir

  • L'exécution symbolique explore systématiquement TOUS les chemins en utilisant des valeurs symboliques et un solveur SMT
  • angr est le framework standard : chargement binaire, émulation, exploration et résolution de contraintes
  • Triton combine instrumentation dynamique et exécution symbolique — plus précis mais plus lent
  • La génération automatique d'exploits cible les états où RIP est symbolique (contrôle du flux)
  • L'explosion de chemins est le problème majeur — les techniques hybrides (fuzzing + symbolic) le mitigent
  • Le concolic testing (QSYM, SymCC) est l'approche la plus efficace en pratique

🔗 Références externes