Glossary
Exécution symbolique
Technique d'analyse qui exécute le code avec des valeurs symboliques au lieu d'entrées concrètes, explorant plusieurs chemins à la fois.
L'exécution symbolique est une technique d'analyse de programme qui exécute le code en utilisant des valeurs symboliques plutôt que concrètes — chaque entrée inconnue est représentée par un symbole mathématique. Le moteur suit les contraintes sur ces symboles (par exemple « le symbole X doit être > 0 pour que cette branche soit prise ») et recourt à un solveur SMT (comme Z3) pour trouver des entrées concrètes satisfaisant n'importe quelle condition de chemin souhaitée. En reverse engineering, l'exécution symbolique sert à résoudre automatiquement des crackmes, à contourner les vérifications de licence, à trouver des entrées déclenchant des bugs et à désobfusquer du code. Parmi les frameworks populaires figurent angr (Python), Triton et Manticore. Elle passe mal à l'échelle sur les gros binaires — un problème connu sous le nom d'explosion des chemins.