Symbolic Execution : Angr, Triton et Exploits

L'exécution symbolique (symbolic execution) est une technique d'analyse de programme qui explore systématiquement tous les chemins d'exécution possibles en utilisant des valeurs symboliques au lieu de valeurs concrètes. Au lieu d'exécuter un programme avec des entrées spécifiques, le moteur d'exécution symbolique représente les entrées comme des variables mathématiques et résout les contraintes de chemin pour déterminer quelles entrées atteignent un état particulier — comme un crash, un buffer overflow, ou un appel à system(). Les outils angr, Triton et KLEE automatisent la découverte de vulnérabilités et la génération d'exploits dans les binaires compilés. Les chercheurs en rétro-ingénierie, les développeurs d'exploits et les analystes de vulnérabilités trouveront ici une méthodologie complète pour l'analyse automatisée de programmes et la découverte d'exploits avec des exemples de code pratiques.

Principes de l'Exécution Symbolique

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

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 :

#!/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.

FAQ — Questions Fréquentes