Votre suite de tests a 94 % de couverture et zéro échec. Un moteur d’exécution symbolique trouve un crash dans votre code en moins de trois secondes.

Le test n’est pas cassé. La métrique de couverture ne ment pas. Le problème est que le testing vérifie le comportement à des points spécifiques. L’exécution symbolique vérifie le comportement sur des régions entières de l’espace d’entrées. Peu importe combien d’exemples vous écrivez si le bug vit dans l’intervalle entre deux d’entre eux.

Ce que fait réellement l’exécution symbolique

L’exécution symbolique est une technique d’analyse de programme qui exécute votre code sur des variables symboliques au lieu de valeurs concrètes. Un test normal passe x = 5 dans une fonction. Un moteur d’exécution symbolique passe x = α, où α représente chaque entier possible.

Alors que le code s’exécute, le moteur suit les contraintes. Quand il atteint une branche comme if (x > 0), il ne choisit pas une direction. Il fork l’exécution. Un chemin porte la contrainte α > 0. L’autre porte α ≤ 0. Les deux chemins continuent indépendamment.

Quand un chemin atteint une assertion, un accès mémoire, ou un site de crash potentiel, le moteur demande à un solveur SMT une question simple : existe-t-il une valeur de α qui satisfait toutes les contraintes sur ce chemin et viole aussi cette propriété de sécurité ? Si le solveur dit oui, il rend un contre-exemple concret. Vous avez maintenant une entrée spécifique qui déclenche un bug pour lequel vous n’avez jamais écrit de test.

Le bug que vos tests unitaires n’attraperont pas

Considérez une fonction qui valide les limites de tableau avant de copier :

int copy_slice(const char *src, size_t src_len,
               size_t offset, size_t count) {
    if (offset > src_len) return -1;
    if (count > 1024) return -1;

    size_t end = offset + count;
    if (end > src_len) return -1;

    char dst[1024];
    memcpy(dst, src + offset, count);
    return 0;
}

Votre suite de tests semble raisonnable :

void test_copy_slice_normal() {
    assert(copy_slice("hello", 5, 1, 3) == 0);
}

void test_copy_slice_too_long() {
    assert(copy_slice("hi", 2, 0, 1025) == -1);
}

void test_copy_slice_bad_offset() {
    assert(copy_slice("hi", 2, 5, 1) == -1);
}

Tout est vert. Mais offset et count sont des size_t, des entiers non signés. Sur un système 64 bits, offset + count peut faire un wrap autour vers un petit nombre si les deux sont grands. Si offset = 0xFFFFFFFFFFFFFFFF et count = 1, alors end = 0, qui n’est pas supérieur à src_len. La vérification des limites passe. memcpy lit depuis une adresse invalide.

Aucun développeur raisonnable n’écrit un cas de test avec offset = 2^64 - 1. L’espace d’entrées est incompréhensiblement grand. L’exécution symbolique n’a pas besoin que vous deviniez la mauvaise entrée. Elle explore le chemin où le wraparound se produit et demande au solveur de trouver des valeurs qui satisfont la contrainte end ≤ src_len pendant que offset + count overflow. Le solveur retourne le contre-exemple en millisecondes.

Comment le moteur explore les chemins

Le mécanisme central est la collecte de contraintes et le forking de chemins. Chaque instruction conditionnelle dans votre code devient un point de branchement. Le moteur maintient une contrainte de chemin, une formule booléenne représentant toutes les conditions qui doivent être vraies pour que l’exécution atteigne le point actuel.

À chaque branche, le moteur interroge le solveur :

  1. La contrainte de chemin actuelle plus la condition de branche vraie est-elle satisfaisable ?
  2. La contrainte de chemin actuelle plus la condition de branche fausse est-elle satisfaisable ?

Si les deux sont satisfaisables, le moteur fork. Il met les deux chemins en file d’attente pour exploration. C’est ainsi que l’exécution symbolique atteint une couverture exhaustive des chemins pour des programmes bornés.

Quand un chemin atteint un crash, un accès hors limites, ou une assertion échouée, le moteur demande au solveur une affectation satisfaisante pour les entrées symboliques sous la contrainte de chemin actuelle. Cette affectation est votre entrée déclenchant le bug.

Vous pouvez voir l’étape de résolution de contraintes directement avec Z3, le solveur SMT qui alimente de nombreux moteurs d’exécution symbolique :

from z3 import Solver, BitVec, UGT, ULT, ULE, simplify

solver = Solver()

# Model 32-bit unsigned size_t values
offset = BitVec('offset', 32)
count = BitVec('count', 32)
src_len = BitVec('src_len', 32)

# Path constraints: offset <= src_len, count <= 1024
solver.add(ULE(offset, src_len))
solver.add(ULE(count, 1024))

# We want to find a case where offset + count wraps around
# and the end check passes incorrectly
end = offset + count
solver.add(UGT(end, src_len))  # This should trigger the return -1

# But what if we look for the overflow case where end wraps?
solver2 = Solver()
solver2.add(ULE(offset, src_len))
solver2.add(ULE(count, 1024))
solver2.add(ULT(offset + count, offset))  # unsigned overflow
solver2.add(ULE(offset + count, src_len))  # bogus check passes

if solver2.check() == solver2.sat:
    model = solver2.model()
    print(f"offset={model[offset]}, count={model[count]}")
    # offset=4294967295, count=1 on a 32-bit model

Le solveur retourne des valeurs concrètes qui satisfont la contrainte d’overflow. C’est le coeur mathématique de l’exécution symbolique. Le moteur fait ça automatiquement à travers chaque branche dans votre programme.

Les compromis qui l’empêchent de remplacer votre suite de tests

L’exécution symbolique n’est pas gratuite. Il y a trois coûts qui limitent où elle est pratique.

Explosion de chemins. Chaque instruction if double le nombre de chemins. Une fonction avec 20 branches indépendantes a plus d’un million de chemins. La plupart des moteurs abandonnent après un timeout ou un budget de chemins. Les boucles aggravent ça. Une boucle qui itère symboliquement sur une plage non bornée crée infiniment de chemins. Les moteurs déroulent généralement les boucles un nombre fixe de fois et passent à la suite.

État externe et appels système. L’exécution symbolique fonctionne mieux sur des fonctions pures. Quand votre code lit depuis un fichier, fait une requête réseau, ou interroge une base de données, le moteur n’a aucune idée de quelle valeur reviendra. Certains outils modélisent les appels de bibliothèque communs de manière heuristique. D’autres exigent que vous écriviez des modèles de mock. C’est fastidieux et sujet aux erreurs.

Timeouts du solveur. Les formules de contraintes pour du code réel sont complexes. Les tableaux, les bitvectors, l’arithmétique en virgule flottante, et les mathématiques non linéaires peuvent pousser un solveur SMT dans un temps exponentiel. Un chemin qui prend des microsecondes à exécuter concrètement peut prendre des minutes à résoudre symboliquement. Les moteurs abandonnent ces chemins et les rapportent comme non résolus.

À cause de ces limites, l’exécution symbolique est un complément au testing, pas un remplacement. Elle trouve les cas limites profonds. Vos tests vérifient les cas courants et le comportement d’intégration.

Trois façons de l’essayer sur du code réel

Vous n’avez pas besoin d’un doctorat pour exécuter de l’exécution symbolique. Les outils modernes cachent la plupart de la complexité.

Pour C/C++ : KLEE. KLEE est le moteur d’exécution symbolique open source classique construit sur LLVM. Vous compilez votre code en LLVM bitcode avec clang -emit-llvm, puis exécutez klee sur le résultat. KLEE a trouvé des bugs sérieux dans GNU coreutils, SQLite, et d’autres codebase C largement utilisés.

clang -emit-llvm -c -g copy_slice.c -o copy_slice.bc
klee --max-time=60 copy_slice.bc

KLEE sort des fichiers .ktest pour chaque bug qu’il trouve. Vous pouvez les rejouer avec un petit runtime pour voir les entrées exactes.

Pour Python et les binaires : angr. angr est un framework Python pour l’exécution symbolique, l’analyse binaire, et le reverse engineering. Il fonctionne sur des binaires compilés, donc vous n’avez pas besoin de code source. Vous écrivez un script Python pour configurer des registres symboliques et de la mémoire, puis laissez angr explorer.

import angr

proj = angr.Project("./copy_slice")
state = proj.factory.entry_state()
sm = proj.factory.simulation_manager(state)
sm.explore(find=lambda s: b"crash" in s.posix.dumps(1))

angr est plus lent que KLEE mais gère des binaires du monde réel avec toutes leurs conventions d’appel chaotiques et dépendances de bibliothèque.

Pour Rust : Kani. Kani est un vérificateur spécifique à Rust construit sur CBMC. Vous annotez une fonction avec #[kani::proof] et exécutez cargo kani. Il vérifie les overflows arithmétiques, les accès hors limites, et les échecs d’assertion en utilisant l’exécution symbolique sous le capot.

#[kani::proof]
fn check_copy_slice() {
    let src = kani::any_slice::<u8, 1024>();
    let offset: usize = kani::any();
    let count: usize = kani::any();
    kani::assume(count <= 1024);
    let _ = copy_slice(src, src.len(), offset, count);
}

Kani est la rampe d’accès la plus facile si vous êtes déjà dans l’écosystème Rust. Il s’intègre avec cargo et vous donne des traces d’erreur dans un format familier.

Questions fréquemment posées

L’exécution symbolique remplace-t-elle le fuzzing ?

Non. Le fuzzing génère des entrées aléatoires et observe les crashes. L’exécution symbolique raisonne sur les chemins et trouve des entrées qui satisfont des contraintes spécifiques. Le fuzzing passe à l’échelle pour de grands programmes et des exécutions longues. L’exécution symbolique trouve des bugs plus profonds dans des régions plus petites. Les deux techniques fonctionnent bien ensemble. Des outils comme Driller et QSYM les combinent, utilisant le fuzzing pour la couverture et l’exécution symbolique pour les branches difficiles à atteindre.

L’exécution symbolique peut-elle prouver que mon code n’a pas de bugs ?

Seulement pour des programmes bornés sans boucles non bornées et sans dépendances externes. Pour la plupart du code de production, l’exécution symbolique peut prouver l’absence de certaines classes de bugs jusqu’à une limite de profondeur de chemin. Elle ne peut pas prouver la correction totale.

Combien de temps ça prend à exécuter ?

De minutes à des heures pour de petites fonctions. L’exécution symbolique n’est pas un démon de vitesse en CI. Exécutez-la sur des fonctions de sécurité critiques, des parsers, et du code de vérification de limites. N’essayez pas d’exécuter symboliquement tout votre framework web.

Commencez par une fonction

Vous n’avez pas besoin d’exécuter symboliquement tout votre codebase. Choisissez une fonction où un bug ferait mal. Un parser. Une vérification d’autorisation. Une copie de buffer.

Écrivez un harnais KLEE, un script angr, ou une preuve Kani. Exécutez-le. Regardez-le trouver une entrée pour laquelle vous n’auriez jamais écrit de test. Corrigez le bug. Dormez mieux.

L’objectif n’est pas de remplacer vos tests. L’objectif est d’arrêter de prétendre que 94 % de couverture signifie 94 % de sécurité. L’exécution symbolique trouve les intervalles. Vos tests ne le feront jamais.