## Install via pip

Triton peut être installé via `pip` :```console
pip install triton-library

### Linux et MacOS```console
$ git clone https://github.com/JonathanSalwan/Triton
$ cd Triton
$ mkdir build ; cd build
$ cmake ..
$ make -j3
$ sudo make install

#### Note pour MacOS M1 :

Dans le cas où vous obtenez des erreurs de compilation comme :```
Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)

Ces informations que vous pouvez obtenir à partir de cet extrait :```python
from sysconfig import get_paths
info = get_paths()
print(info)

Vous pouvez utiliser setup.py pour générer la version debug de triton.pyd sous Windows.```console
> git clone https://github.com/JonathanSalwan/Triton.git
> cd Triton
> $env:COMPILER_DIR="C:/deps/llvm/llvm2116r/bin"
> $env:CMAKE_PREFIX_PATH="C:/deps/llvm/llvm-project-21.1.6.src/install/lib/cmake/llvm;C:/code/cxx-common-cmake/build/install"
> python_d -m build --wheel
> python_d -m pip install (Get-ChildItem .\dist\triton_library*)

Si la version est obsolète, veuillez [créer un problème ou une pull request](https://github.com/Microsoft/vcpkg) sur le dépôt vcpkg.


# Contributeurs

* [**Alberto Garcia Illera**](https://twitter.com/algillera) - Cruise Automation
* [**Alexey Vishnyakov**](https://vishnya.xyz/) - ISP RAS
* [**Black Binary**](https://github.com/black-binary) - n/a
* [**Christian Heitman**](https://github.com/cnheitman) - Quarkslab
* [**Daniil Kuts**](https://github.com/apach301) - ISP RAS
* [**Jessy Campos**](https://github.com/ek0) - n/a
* [**Matteo F.**](https://twitter.com/fvrmatteo) - n/a
* [**Pierrick Brunet**](https://github.com/pbrunet) - Quarkslab
* [**PixelRick**](https://github.com/PixelRick) - n/a
* [**Romain Thomas**](https://twitter.com/rh0main) - Quarkslab
* [**Et bien d'autres**](https://github.com/JonathanSalwan/Triton/graphs/contributors)


## Ils ont déjà utilisé Triton

### Outils

* [Exrop](https://github.com/d4em0n/exrop): Génération automatique de chaînes ROP.
* [Pimp](https://github.com/kamou/pimp): Plugin R2 basé sur Triton pour l'exécution concolique et le contrôle total.
* [Ponce](https://github.com/illera88/Ponce): Gagnant du concours de plugins IDA 2016 ! L'exécution symbolique à un clic !
* [QSynthesis](https://github.com/quarkslab/qsynthesis): Synthétiseur Greybox conçu pour le désobfuscation des instructions assembleur.
* [TritonDSE](https://github.com/quarkslab/tritondse): Bibliothèque DSE basée sur Triton avec capacités de chargement et d'exploration.
* [Titan](https://github.com/archercreat/titan): Titan est un dévirtualiseur VMProtect utilisant Triton.

### Articles et conférences<ul dir="auto">
<li>
<b>Sydr-Fuzz : Hybrid Fuzzing continu et analyse dynamique pour le cycle de développement sécurisé</b><br />
 <b>Présenté à</b> : Ivannikov ISP RAS Open Conference, Moscou, Russie, 2022. [<a href="publications/ISPOPEN2022-sydr-fuzz.pdf">article</a>] [<a href="publications/ISPOPEN2022-slide-sydr-fuzz-vishnyakov.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Fedotov A.<br />
 <b>Résumé</b> : <em>De nos jours, les cadres d'analyse dynamique automatisée pour les tests continus sont très demandés pour garantir la sécurité des logiciels et satisfaire les exigences du cycle de développement sécurisé (SDL). L'efficacité de la chasse aux bogues de sécurité du fuzzy hybride de pointe surpasse celle du fuzzy guidé par couverture largement utilisé. Nous proposons un pipeline d'analyse dynamique amélioré pour tirer parti de la productivité de la détection automatisée de bogues basée sur le fuzzy hybride. Nous implémentons le pipeline proposé dans l'ensemble d'outils de fuzzy continu Sydr-Fuzz, qui est propulsé par un orchestrateur de fuzzy hybride, intégrant notre outil DSE Sydr avec libFuzzer et AFL++. Sydr-Fuzz intègre également des vérificateurs de prédicats de sécurité, l'outil de triage de crash Casr, et des utilitaires pour la minimisation du corpus et la collecte de couverture. L'évaluation comparative de notre fuzzzer hybride par rapport à d'autres solutions de pointe démontre sa supériorité sur les fuzzers guidés par couverture, tout en restant au même niveau que les fuzzers hybrides avancés. De plus, nous confirmons la pertinence de notre approche en découvrant 85 nouvelles failles logicielles réelles dans le cadre du projet OSS-Sydr-Fuzz. Enfin, nous ouvrons le code source de Casr à la communauté pour faciliter l'examen des crashs existants.</em>
</li><br/>
<li>
<b>Résolution optimiste forte pour l'exécution symbolique dynamique</b><br />
 <b>Présenté à</b> : Ivannikov Memorial Workshop, Kazan, Russie, 2022. [<a href="publications/IVMEM2022-strong-optimistic-parygina.pdf">article</a>] [<a href="publications/IVMEM2022-slide-strong-optimistic-parygina.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Parygina D., Vishnyakov A., Fedotov A.<br />
 <b>Résumé</b> : <em>L'exécution symbolique dynamique (DSE) est une méthode efficace pour les tests de programmes automatisés et la détection de bogues. Elle augmente la couverture de code en explorant des branches complexes lors du fuzzy hybride. Les outils DSE inversent les branches le long d'un chemin d'exécution et aident le fuzzer à examiner des parties du programme auparavant inaccessibles. La DSE est souvent confrontée à des problèmes de sur-contrainte et de sous-contrainte. Le premier conduit à une complication significative de l'analyse tandis que le second provoque une exécution symbolique imprécise.
 Nous proposons une méthode de résolution optimiste forte qui élimine les contraintes de prédicat de chemin non pertinentes pour l'inversion de branche cible. Nous éliminons les contraintes symboliques dont la branche cible ne dépend pas du contrôle. De plus, nous traitons séparément les branches symboliques qui ont des instructions de transfert de contrôle imbriquées qui passent le contrôle au-delà de la portée de la branche parente, par exemple return, goto, break, etc. Nous implémentons la méthode proposée dans notre outil d'exécution symbolique dynamique Sydr.
 Nous évaluons la stratégie optimiste forte, la stratégie optimiste qui ne contient que la dernière négation de contrainte, et leur combinaison. Les résultats montrent que la combinaison des stratégies permet d'augmenter soit la couverture de code, soit le nombre moyen de branches correctement inversées par minute. Il est optimal d'appliquer les deux stratégies ensemble contrairement aux autres configurations.</em>
</li><br/>
<li>
<b>Synthèse de programmes Greybox : une nouvelle approche pour attaquer l'obfuscation du flux de données</b><br />
 <b>Présenté à</b> : Blackhat USA, Las Vegas, Nevada, 2021. [<a href="publications/BHUSA2021-David-Greybox-Program-Synthesis.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Robin David<br />
 <b>Résumé</b> : <em>Cette présentation expose les dernières avancées en matière de synthèse de programmes appliquée à la désobfuscation. Elle vise à démystifier cette technique d'analyse en montrant comment elle peut être mise en œuvre sur de l'obfuscation. En particulier, l'implémentation Qsynthesis publiée pour cette présentation montre un workflow complet de bout en bout pour désobfusquer des instructions assembleur en instructions optimisées (désobfusquées) réassemblées dans le binaire.</em>
</li><br/>
<li>
<b>Du code source au cas de test de crash via l'automatisation des tests logiciels</b><br />
 <b>Présenté à</b> : C&ESAR, Rennes, France, 2021. [<a href="publications/CESAR2021_robin-david-paper.pdf">article</a>] [<a href="publications/CESAR2021_robin-david-slide.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Robin David, Jonathan Salwan, Justin Bourroux<br />
 <b>Résumé</b> : <em>Cet article présente une approche automatisant le processus de test logiciel depuis un code source jusqu'au test dynamique du programme compilé. Plus précisément, à partir d'un rapport d'analyse statique indiquant des alertes sur des lignes de code source, il permet de tester pour couvrir ces lignes dynamiquement et de vérifier de manière opportuniste si elles peuvent ou non déclencher un crash. Le résultat est un corpus de test permettant de couvrir les alertes et de les déclencher si elles s'avèrent être de vrais positifs. Cet article discute de la méthodologie employée pour suivre les alertes dans le binaire compilé, du processus de sélection des moteurs de test et des résultats obtenus sur une implémentation de pile TCP/IP pour les systèmes embarqués et IoT.</em>
</li><br/>
<li>
<b>Prédicats de sécurité symboliques : chasser les faiblesses des programmes</b><br />
 <b>Présenté à</b> : Ivannikov ISP RAS Open Conference, Moscou, Russie, 2021. [<a href="publications/ISPOPEN2021-security-predicates-vishnyakov.pdf">article</a>] [<a href="publications/ISPOPEN2021-slide-security-predicates-vishnyakov.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : A.Vishnyakov, V.Logunova, E.Kobrin, D.Kuts, D.Parygina, A.Fedotov<br />
 <b>Résumé</b> : <em>L'exécution symbolique dynamique (DSE) est une méthode puissante pour l'exploration de chemins lors du fuzzy hybride et la détection automatique de bogues. Nous proposons des prédicats de sécurité pour détecter efficacement les comportements indéfinis et les erreurs de violation d'accès mémoire. Initialement, nous exécutons symboliquement le programme sur des chemins qui ne déclenchent aucune erreur (le fuzzy hybride peut explorer ces chemins). Ensuite, nous construisons un prédicat de sécurité symbolique pour vérifier une condition d'erreur. Ainsi, nous pouvons modifier le flux de données du programme pour entraîner des faiblesses de déréférencement de pointeur nul, de division par zéro, d'accès hors limites ou de débordement d'entier. Contrairement à l'analyse statique, l'exécution symbolique dynamique ne se contente pas de signaler les erreurs mais génère également de nouvelles données d'entrée pour les reproduire. De plus, nous introduisons la modélisation de la sémantique des fonctions pour les fonctions courantes des bibliothèques standard C/C++. Nous visons à modéliser le flux de contrôle à l'intérieur d'une fonction avec une seule formule symbolique. Cela facilite la détection de bogues, accélère l'exploration de chemins et surmonte les sur-contraintes dans le prédicat de chemin. Nous implémentons les techniques proposées dans notre outil d'exécution symbolique dynamique Sydr. Ainsi, nous utilisons des méthodes puissantes de Sydr telles que le découpage de prédicat de chemin qui élimine les contraintes non pertinentes.
 Nous présentons Juliet Dynamic pour mesurer la précision des outils de détection de bogues dynamiques. Le système de test vérifie également que les entrées générées déclenchent les sanitizers. Nous évaluons la précision de Sydr pour 11 CWEs de la suite de tests Juliet. Sydr montre une précision globale de 95,59 %. Nous rendons publics les artefacts d'évaluation de Sydr pour faciliter la reproductibilité des résultats.</em>
</li><br/>
<li>
<b>Vers un raisonnement sur les pointeurs symboliques dans l'exécution symbolique dynamique</b><br />
 <b>Présenté à</b> : Ivannikov Memorial Workshop, Nizhny Novgorod, Russie, 2021. [<a href="publications/IVMEM2021-symbolic-pointers-kuts.pdf">article</a>] [<a href="publications/IVMEM2021-slide-symbolic-pointers-kuts.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Daniil Kuts<br />
 <b>Résumé</b> : <em>L'exécution symbolique dynamique est une technique largement utilisée pour les tests logiciels automatisés, conçue pour l'exploration de chemins d'exécution et la détection d'erreurs de programme. Une approche hybride s'est récemment répandue, où l'objectif principal de l'exécution symbolique est d'aider le fuzzer à augmenter la couverture du programme. Plus l'exécuteur symbolique peut inverser de branches, plus il est utile pour le fuzzer. Le flux de contrôle d'un programme dépend souvent des valeurs mémoire, qui sont obtenues en calculant des index d'adresse à partir de l'entrée utilisateur. Cependant, la plupart des outils DSE ne prennent pas en charge ces dépendances, ils manquent donc certaines branches de programme souhaitées. Nous implémentons le raisonnement sur les adresses symboliques lors des lectures mémoire dans notre outil d'exécution symbolique dynamique Sydr. Les régions d'accès mémoire possibles sont déterminées soit en analysant les expressions symboliques d'adresse mémoire, soit par recherche binaire avec un solveur SMT. Nous proposons une technique de linéarisation améliorée pour modéliser les accès mémoire. Différentes méthodes de modélisation mémoire sont comparées sur un ensemble de programmes. Notre évaluation montre que la gestion des adresses symboliques permet de découvrir de nouvelles branches symboliques et d'augmenter la couverture du programme.</em>
</li><br/>
<li>
<b>QSynth : une approche basée sur la synthèse de programmes pour la désobfuscation de code binaire</b><br />
 <b>Présenté à</b> : BAR, San Diego, Californie, 2020. [<a href="publications/BAR2020-qsynth-robin-david.pdf">article</a>]<br />
 <b>Auteurs</b> : Robin David, Luigi Coniglio, Mariano Ceccato<br />
 <b>Résumé</b> : <em>Nous présentons une approche générique tirant parti à la fois de la DSE et de la synthèse de programmes pour synthétiser avec succès des programmes obfusqués avec Mixed-Boolean-Arithmetic, Data-Encoding ou Virtualization. L'algorithme de synthèse proposé est une synthèse par énumération hors ligne guidée par une recherche en largeur d'abord descendante. Nous montrons son efficacité contre un obfusqueur de pointe et sa scalabilité car il surpasse d'autres approches similaires basées sur la synthèse. Nous montrons également son efficacité en présence d'obfuscation composite (combinaison de plusieurs techniques). Ce travail en cours éclaire l'efficacité de la synthèse pour cibler certains types d'obfuscation et ouvre la voie à des algorithmes plus robustes et des stratégies de simplification.</em>
</li><br/>
<li>
<b>Sydr : exécution symbolique dynamique de pointe</b><br />
 <b>Présenté à</b> : Ivannikov ISP RAS Open Conference, Moscou, Russie, 2020. [<a href="publications/ISPRAS2020-sydr.pdf">article</a>] [<a href="publications/ISPOPEN2020-slide-sydr-vishnyakov.pdf">diapositives</a>] [<a href="https://www.ispras.ru/conf/2020/video/compiler-technology-11-december.mp4#t=6021">vidéo</a>]<br />
 <b>Auteurs</b> : A.Vishnyakov, A.Fedotov, D.Kuts, A.Novikov, D.Parygina, E.Kobrin, V.Logunova, P.Belecky, S.Kurmangaleev<br />
 <b>Résumé</b> : <em>L'exécution symbolique dynamique (DSE) a une énorme quantité d'applications en sécurité informatique (fuzzing, découverte de vulnérabilités, rétro-ingénierie, etc.). Nous proposons plusieurs améliorations de performance et de précision pour l'exécution symbolique dynamique. Le saut d'instructions non symboliques permet de construire un prédicat de chemin 1,2 à 3,5 fois plus rapidement. Le moteur symbolique simplifie les formules pendant l'exécution symbolique. Le découpage de prédicat de chemin élimine les conjonctions non pertinentes des requêtes du solveur. Nous traitons chaque table de saut (instruction switch) comme plusieurs branches et décrivons la méthode pour l'exécution symbolique de programmes multi-threadés. Les solutions proposées ont été implémentées dans l'outil Sydr. Sydr effectue l'inversion de branches dans le prédicat de chemin. Sydr combine l'outil d'instrumentation binaire dynamique DynamoRIO avec le moteur symbolique Triton.</em>
</li><br/>
<li>
<b>Désobfuscation symbolique : du code virtualisé à l'original</b><br />
 <b>Présenté à</b> : DIMVA, Paris-Saclay, France, 2018. [<a href="publications/DIMVA2018-deobfuscation-salwan-bardin-potet.pdf">article</a>] [<a href="publications/DIMVA2018-slide-deobfuscation-salwan-bardin-potet.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet<br />
 <b>Résumé</b> : <em>La protection des logiciels a pris une place importante au cours de la dernière décennie afin de protéger les logiciels légitimes contre la rétro-ingénierie ou la falsification. La virtualisation est considérée comme l'une des meilleures défenses contre de telles attaques. Nous présentons une approche générique basée sur l'exploration symbolique de chemins, le marquage et la recompilation permettant de récupérer, à partir d'un code virtualisé, un code dévirtualisé sémantiquement identique à l'original et de taille proche. Nous définissons des critères et des métriques pour évaluer la pertinence des résultats désobfusqués en termes de correction et de précision. Enfin, nous proposons une configuration open source permettant d'évaluer l'approche proposée contre plusieurs formes de virtualisation.</em>
</li><br/>
<li>
<b>Désobfuscation de protections logicielles basées sur VM</b><br />
 <b>Présenté à</b> : SSTIC, Rennes, France, 2017. [<a href="publications/SSTIC2017-French-Article-desobfuscation_binaire_reconstruction_de_fonctions_virtualisees-salwan_potet_bardin.pdf">article en français</a>] [<a href="publications/SSTIC2017_Deobfuscation_of_VM_based_software_protection.pdf">diapositives en anglais</a>] [<a href="https://static.sstic.org/videos2017/SSTIC_2017-06-07_P08.mp4">vidéo en français</a>]<br />
 <b>Auteurs</b> : Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet<br />
 <b>Résumé</b> : <em>Dans cette présentation, nous décrivons une approche qui consiste à analyser automatiquement les protections logicielles basées sur machine virtuelle et qui recompile une nouvelle version du binaire sans ces protections. Cette approche automatisée repose sur une exécution symbolique guidée par une analyse de marquage et des politiques de concrétisation, puis sur une réécriture binaire utilisant la transition LLVM.</em>
</li><br/>
<li>
<b>Comment Triton peut aider à inverser les protections logicielles basées sur machine virtuelle</b><br />
 <b>Présenté à</b> : CSAW SOS, NYC, New York, 2016. [<a href="publications/CSAW2016-SOS-Virtual-Machine-Deobfuscation-RThomas_JSalwan.pdf">diapositives</a>]<br />
 <b>Auteurs</b> : Jonathan Salwan, Romain Thomas<br />
 <b>Résumé</b> : <em>La première partie de l'exposé sera une introduction au framework Triton pour exposer ses composants et expliquer comment ils fonctionnent ensemble. Ensuite, la deuxième partie comprendra des démonstrations sur la manière dont il est possible d'inverser des protections basées sur machine virtuelle en utilisant l'analyse de marquage, l'exécution symbolique, les simplifications SMT et les optimisations LLVM-IR.</em>
</li><br/>
<li>
<b>Analyse binaire dynamique et codes obfusqués</b><br  />
 <b>Présenté à</b> : St'Hack, Bordeaux, France, 2016. [<a href="publications/StHack2016_Dynamic_Binary_Analysis_and_Obfuscated_Codes_RThomas_JSalwan.pdf">diapositives</a>]<br  />
 <b>Auteurs</b> : Jonathan Salwan, Romain Thomas<br />
 <b>Résumé</b> : <em>Dans cette présentation, nous parlerons de la manière dont une DBA (Dynamic Binary Analysis) peut aider un ingénieur en rétro-ingénierie à inverser du code obfusqué. Nous présenterons d'abord quelques techniques d'obfuscation de base, puis nous exposerons comment il est possible de briser certaines choses (en utilisant notre framework DBA open source - Triton) comme détecter des prédicats opaques, reconstruire le CFG, trouver l'algorithme original, isoler des données sensibles et bien d'autres... Ensuite, nous conclurons par une démo et quelques mots sur nos travaux futurs.</em>
</li><br/>
<li>
<b>Comment Triton peut aider à analyser des binaires obfusqués</b><br  />
 <b>Publication dans</b> : magazine MISC 82, 2015. [<a href="publications/MISC-82_French_Paper_How_Triton_may_help_to_analyse_obfuscated_binaries_RThomas_JSalwan.pdf">article en français</a>]<br  />
 <b>Auteurs</b> : Jonathan Salwan, Romain Thomas<br />
 <b>Résumé</b> : <em>L'obfuscation binaire est utilisée pour protéger la propriété intellectuelle des logiciels. Il existe différents types d'obfuscation mais grosso modo, elle transforme une structure binaire en une autre structure binaire en préservant la même sémantique. Le but de l'obfuscation est de garantir que l'information originale est « noyée » dans des informations inutiles qui rendront la rétro-ingénierie plus difficile. Dans cet article, nous montrerons comment analyser un programme obfusqué et briser certaines obfuscations en utilisant le framework Triton.</em>
</li><br/>
<li>
<b>Triton : un cadre d'exécution concolique</b><br  />
 <b>Présenté à</b> : SSTIC, Rennes, France, 2015. [<a href="publications/SSTIC2015_French_Paper_Triton_Framework_dexecution_Concolique_FSaudel_JSalwan.pdf">article en français</a>] [<a href="publications/SSTIC2015_English_slide_detailed_version_Triton_Concolic_Execution_FrameWork_FSaudel_JSalwan.pdf">diapositives détaillées en anglais</a>] <br />
 <b>Auteurs</b> : Jonathan Salwan, Florent Saudel<br />
 <b>Résumé</b> : <em>Cette présentation concerne la publication de Triton, un cadre d'exécution concolique basé sur Pin. Il fournit des composants tels qu'un moteur de marquage, un moteur d'exécution symbolique dynamique, un moteur de snapshot, la traduction d'instructions x64 en SMT2, une interface Z3 pour résoudre des contraintes et des liaisons Python. Basés sur ces composants, Triton offre la possibilité de construire des outils pour la recherche de vulnérabilités ou l'assistance à la rétro-ingénierie.</em>
</li><br/>
<li>
<b>Analyse de comportement dynamique à l'aide de l'instrumentation binaire</b><br  />
 <b>Présenté à</b> : St'Hack, Bordeaux, France, 2015. [<a href="publications/StHack2015_Dynamic_Behavior_Analysis_using_Binary_Instrumentation_Jonathan_Salwan.pdf">diapositives</a>]<br  />
 <b>Auteurs</b> : Jonathan Salwan<br />
 <b>Résumé</b> : <em>Cette présentation peut être considérée comme la partie 2 de notre exposé à SecurityDay. Dans la partie précédente, nous avons parlé de la manière dont il était possible de couvrir une fonction ciblée en mémoire en utilisant l'approche DSE (Dynamic Symbolic Execution). Couvrir une fonction (ou ses états) ne signifie pas trouver toutes les vulnérabilités ; certaines vulnérabilités ne font pas crasher le programme. C'est pourquoi nous devons implémenter des analyses spécifiques pour trouver des bogues spécifiques. Ces analyses sont basées sur l'instrumentation binaire et l'analyse du comportement en cours d'exécution du programme. Dans cette conférence, nous verrons comment trouver les types de bogues suivants : off-by-one, débordement de pile / tas, use-after-free, chaîne de format et {write, read}-what-where.</em>
</li><br/>
<li>
<b>Couverture d'une fonction à l'aide d'une approche d'exécution symbolique dynamique</b><br  />
 <b>Présenté à</b> : Security Day, Lille, France, 2015. [<a href="publications/SecurityDay2015_dynamic_symbolic_execution_Jonathan_Salwan.pdf">diapositives</a>]<br  />
 <b>Auteurs</b> : Jonathan Salwan<br />
 <b>Résumé</b> : <em>Cette présentation concerne l'analyse et l'instrumentation binaires. Nous verrons comment cibler une fonction spécifique, prendre un instantané du contexte mémoire/registres avant la fonction, traduire l'instrumentation en une représentation intermédiaire, appliquer une analyse de marquage basée sur cette RI, construire/conserver des formules pour une exécution symbolique dynamique (DSE), générer une valeur concrète pour passer par un chemin spécifique, restaurer le contexte mémoire/registres et générer une autre valeur concrète pour passer par un autre chemin, puis répéter cette opération jusqu'à ce que la fonction cible soit couverte.</em>
</li>
</ul>


## Cite Triton```latex
@inproceedings{SSTIC2015-Saudel-Salwan,
  author    = {Saudel, Florent and Salwan, Jonathan},
  title     = {Triton: A Dynamic Symbolic Execution Framework},
  booktitle = {Symposium sur la s{\'{e}}curit{\'{e}} des technologies de l'information
               et des communications},
  series    = {SSTIC},
  pages     = {31--54},
  address   = {Rennes, France},
  month     = jun,
  year      = {2015},
}