Triton est une bibliothèque d'analyse binaire dynamique. Il fournit des composants internes qui vous permettent de créer vos outils d'analyse de programme, d'automatiser l'ingénierie inverse, d'effectuer une vérification des logiciels ou simplement d'imiter le code.
- Exécution symbolique dynamique
- Analyse de souillure dynamique
- Représentation AST des x86 , x86-64 , arm32 , aarch64 et RISC-V 32/64 Isa Semantic
- Synthèse des expressions
- Passe de simplification SMT
- Levage vers LLVM ainsi que Z3 et retour
- Interface SMT Solver à Z3 et Bitwuzla
- API C ++ et Python
Comme Triton est une sorte de projet à temps partiel, s'il vous plaît, ne nous blâmez pas s'il n'est pas entièrement fiable. Les problèmes ouverts ou les demandes de traction sont toujours meilleurs que la pêche à la traîne =). Cependant, vous pouvez suivre le développement sur Twitter @QB_Triton.
Démarrage rapide
- Installation
- API Python
- API C ++
- Exemples Python
- Ils ont déjà utilisé Triton
Commencer
from triton import *
> >> # Create the Triton context with a defined architecture
>> > ctx = TritonContext ( ARCH . X86_64 )
> >> # Define concrete values (optional)
>> > ctx . setConcreteRegisterValue ( ctx . registers . rip , 0x40000 )
> >> # Symbolize data (optional)
>> > ctx . symbolizeRegister ( ctx . registers . rax , 'my_rax' )
> >> # Execute instructions
>> > ctx . processing ( Instruction ( b" x48 x35 x34 x12 x00 x00 " )) # xor rax, 0x1234
> >> ctx . processing ( Instruction ( b" x48 x89 xc1 " )) # mov rcx, rax
> >> # Get the symbolic expression
>> > rcx_expr = ctx . getSymbolicRegister ( ctx . registers . rcx )
> >> print ( rcx_expr )
( define - fun ref ! 8 () ( _ BitVec 64 ) ref ! 1 ) ; MOV operation - 0x40006 : mov rcx , rax
>> > # Solve constraint
>> > ctx . getModel ( rcx_expr . getAst () == 0xdead )
{ 0 : my_rax : 64 = 0xcc99 }
>> > # 0xcc99 XOR 0x1234 is indeed equal to 0xdead
>> > hex ( 0xcc99 ^ 0x1234 )
'0xdead' Installer
Triton s'appuie sur les dépendances suivantes:
* libcapstone >= 5.0.x https://github.com/capstone-engine/capstone
* libboost (optional) >= 1.68
* libpython (optional) >= 3.6
* libz3 (optional) >= 4.6.0 https://github.com/Z3Prover/z3
* libbitwuzla (optional) >= 0.4.x https://github.com/bitwuzla/bitwuzla
* llvm (optional) >= 12
Linux et macOS
$ git clone https://github.com/JonathanSalwan/Triton
$ cd Triton
$ mkdir build ; cd build
$ cmake ..
$ make -j3
$ sudo make install
Par défaut, LLVM et Bitwuzla ne sont pas compilés. Si vous voulez profiter de toute la puissance de Triton, la compilation Cmake est:
$ cmake -DLLVM_INTERFACE=ON -DCMAKE_PREFIX_PATH= $( llvm-config --prefix ) -DBITWUZLA_INTERFACE=ON ..
MacOS M1 Remarque:
Dans le cas où vous obtenez des erreurs de compilation comme:
Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)
Essayez de spécifier PYTHON_EXECUTABLE , PYTHON_LIBRARIES et PYTHON_INCLUDE_DIRS pour votre version Python spécifique:
cmake -DCMAKE_INSTALL_PREFIX=/opt/homebrew/
-DPYTHON_EXECUTABLE=/opt/homebrew/bin/python3
-DPYTHON_LIBRARIES=/opt/homebrew/Cellar/[email protected]/3.10.8/Frameworks/Python.framework/Versions/3.10/lib/libpython3.10.dylib
-DPYTHON_INCLUDE_DIRS=/opt/homebrew/opt/[email protected]/Frameworks/Python.framework/Versions/3.10/include/python3.10/
.. Ces informations que vous pouvez retirer de cet extrait:
from sysconfig import get_paths
info = get_paths ()
print ( info )
Fenêtre
Vous pouvez utiliser CMake pour générer le fichier .sln de libtriton.
> git clone https://github.com/JonathanSalwan/Triton.git
> cd Triton
> mkdir build
> cd build
> cmake -G " Visual Studio 14 2015 Win64 "
-DBOOST_ROOT="C:/Users/jonathan/Works/Tools/boost_1_61_0"
-DPYTHON_INCLUDE_DIRS="C:/Python36/include"
-DPYTHON_LIBRARIES="C:/Python36/libs/python36.lib"
-DZ3_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/include"
-DZ3_LIBRARIES="C:/Users/jonathan/Works/Tools/z3-4.6.0-x64-win/bin/libz3.lib"
-DCAPSTONE_INCLUDE_DIRS="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/include"
-DCAPSTONE_LIBRARIES="C:/Users/jonathan/Works/Tools/capstone-5.0.1-win64/capstone.lib" ..
Cependant, si vous préférez télécharger directement la bibliothèque précompilée, consultez les artefacts de notre appveyor. Notez que si vous utilisez les artefacts d'Appveyor, vous devez probablement installer les packages redistribuables visuels C ++ pour Visual Studio 2012.
Installation à partir de VCPKG
Le port de Triton de VCPKG est tenu à jour par les membres de l'équipe Microsoft et les contributeurs communautaires. L'URL de VCPKG est: https://github.com/microsoft/vcpkg. Vous pouvez télécharger et installer Triton à l'aide du gestionnaire de dépendance VCPKG:
$ git clone https://github.com/Microsoft/vcpkg.git
$ cd vcpkg
$ ./bootstrap-vcpkg.sh # ./bootstrap-vcpkg.bat for Windows
$ ./vcpkg integrate install
$ ./vcpkg install triton
Si la version est obsolète, veuillez créer une demande de problème ou d'extraction sur le référentiel VCPKG.
Contributeurs
- Alberto Garcia ILERA - Cruise Automation
- Alexey Vishnyakov - ISP Ras
- Binaire noir - n / a
- Christian Heitman - Quarkslab
- Daniil Kuts - ISP Ras
- Jessy Campos - N / A
- Matteo F. - N / A
- Pierrick Brunet - Quarkslab
- Pixelrick - n / a
- Romain Thomas - Quarkslab
- Et bien d'autres
Ils ont déjà utilisé Triton
Outils
- EXROP: Génération automatique de Ropchain.
- Pimp: Plugin R2 basé sur Triton pour l'exécution conforme et le contrôle total.
- PONCE: Gagnant du concours de plugin IDA 2016! Exécution symbolique à un seul clic!
- QSynthesis: Synthétiseur Greybox destiné à la désobfuscation des instructions d'assemblage.
- Tritondse: bibliothèque DSE basée sur Triton avec des capacités de chargement et d'exploration.
- Titan: Titan est un Devirtualzer VMProtect utilisant Triton.
Documents et conférence
- Sydr-Fuzz: Fuzzing hybride continu et analyse dynamique pour le cycle de vie du développement de la sécurité
Talk AT : Ivannikov ISP RAS Open Conference, Moscou, Russie, 2022. [Papier] [Slide]
Auteurs : Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Feotov A.
Résumé : De nos jours, les cadres d'analyse dynamique automatisés pour les tests continus sont très demandés pour garantir la sécurité des logiciels et satisfaire aux exigences du cycle de vie du développement de la sécurité (SDL). L'efficacité de chasse aux insectes de sécurité des techniques de fuzzing hybride de pointe surpasse la fuzzage guidé de couverture largement utilisée. Nous proposons un pipeline d'analyse dynamique amélioré pour tirer parti de la productivité de la détection automatisée de bogues en fonction du fuzzing hybride. Nous mettons en œuvre le pipeline proposé dans le Sydr-Fuzz de Sydr-Fuzz d'outils de fuzzage continu qui est alimenté par un orchestrateur de fuzzing hybride, intégrant notre outil DSE SYDR avec Libfuzzer et AFL ++. SYDR-Fuzz intègre également les vérificateurs des prédicats de sécurité, l'outil de triage de crash CASR et les services publics pour la minimisation du corpus et la collecte de couverture. L'analyse comparative de notre fuzzer hybride contre des solutions de pointe alternatives démontre sa supériorité sur les fuzzers guidés par la couverture tout en restant au même niveau avec des fuzzers hybrides avancés. En outre, nous approuvons la pertinence de notre approche en découvrant 85 nouveaux défauts de logiciels réels dans le projet OSS-Sydr-Fuzz. Enfin, nous ouvrons le code source CASR à la communauté pour faciliter l'examen des accidents existants.
- Forte résolution optimiste pour l'exécution symbolique dynamique
Talk AT : Ivannikov Memorial Workshop, Kazan, Russie, 2022. [Papier] [Diapositive]
Auteurs : Parygina D., Vishnyakov A., Fedotov A.
Résumé : L'exécution symbolique dynamique (DSE) est une méthode efficace pour les tests de programme automatisés et la détection de bogues. Il augmente la couverture du code par l'exploration complexe des branches pendant le fuzzing hybride. Les outils DSE inversent les branches le long d'un chemin d'exécution et aident Fuzzer à examiner les pièces de programme non disponibles auparavant. Le DSE fait souvent face à des problèmes de sur et de contrainte. La première conduit à une complication d'analyse significative tandis que la seconde provoque une exécution symbolique inexacte. Nous proposons une forte méthode de résolution optimiste qui élimine les contraintes de prédicat de chemin non pertinentes pour l'inversion de la branche cible. Nous éliminons ces contraintes symboliques dont la branche cible ne dépend pas du contrôle. De plus, nous gérons 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 parent, par exemple le retour, le goto, la rupture, etc. Nous implémentons la méthode proposée dans notre outil d'exécution symbolique dynamique SYDR. Nous évaluons la forte stratégie optimiste, 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 de stratégies aide à augmenter la couverture du code, soit le nombre moyen de branches correctement inversées par minute. Il est optimal d'appliquer les deux stratégies en contraste avec d'autres configurations.
- Synthèse du programme Greybox: une nouvelle approche pour attaquer l'obscurcissement du flux de données
Talk at : Blackhat USA, Las Vegas, Nevada, 2021. [Diapositive]
Auteurs : Robin David
Résumé : Ce discours présente les dernières avancées de la synthèse des programmes appliquées pour la désobfuscation. Il vise à démystifier cette technique d'analyse en montrant comment elle peut être mise en œuvre sur l'obscurcissement. En particulier la mise en œuvre de la QSynthesis publiée pour ce talk-talk montre un flux de travail complet de bout en bout pour désobfusquer les instructions d'assemblage dans les instructions optimisées (désobfuscées) réassemblées dans le binaire.
- Du code source au cas de test de bisser via l'automatisation des tests de logiciels
Talk at : C & ESAR, Rennes, France, 2021. [Papier] [Diapositive]
Auteurs : Robin David, Jonathan Salwan, Justin Bourroux
Résumé : Cet article présente une approche automatisant le processus de test logiciel d'un code source aux tests dynamiques du programme compilé. Plus précisément, à partir d'un rapport d'analyse statique indiquant des alertes sur les lignes source, il permet aux tests de couvrir ces lignes de vérification dynamique et de manière opportuniste si elles peuvent ou non déclencher un crash. Le résultat est un corpus d'essai permettant de couvrir les alertes et de les déclencher s'ils se trouvent être de vrais positifs. Cet article discute de la méthodologie utilisée pour retrouver les alertes dans le binaire compilé, le processus de sélection des moteurs de test et les résultats obtenus sur une implémentation de pile TCP / IP pour les systèmes intégrés et IoT.
- Prédicats de sécurité symbolique: faiblesse du programme Hunt
Talk at : Ivannikov ISP RAS Open Conference, Moscou, Russie, 2021. [Paper] [Diapositive]
Auteurs : A.vishnyakov, V.logunova, E.Kobrin, D.Kuts, D.Parygina, A.fedotov
Résumé : L'exécution symbolique dynamique (DSE) est une méthode puissante pour l'exploration de chemin pendant le fuzzing hybride et la détection automatique des bogues. Nous proposons des prédicats de sécurité pour détecter efficacement le comportement non défini et les erreurs de violation de l'accès à la mémoire. Initialement, nous exécutons symboliquement le programme sur des chemins qui ne déclenchent aucune erreur (Hybrid Fuzzing 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 impliquer la déréférence du pointeur nul, la division par zéro, l'accès hors limites ou les faiblesses de débordement entières. Contrairement à l'analyse statique, l'exécution symbolique dynamique ne rapporte pas seulement 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 sémantique des fonctions pour les fonctions de bibliothèque standard C / C ++ communes. Nous visons à modéliser le flux de contrôle à l'intérieur d'une fonction avec une seule formule symbolique. Cela aide à la détection des bogues, accélère l'exploration du chemin et surmonte les sur-contraintes du 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 des prédicats 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 des désinfections. Nous évaluons la précision SYDR pour 11 CWE de Juliet Test Suite. SYDR montre une précision globale de 95,59%. Nous mettons publiquement les artefacts d'évaluation SYDR pour faciliter la reproductibilité des résultats.
- Vers le raisonnement de pointeurs symboliques dans l'exécution symbolique dynamique
Talk at : Ivannikov Memorial Workshop, Nizhny Novgorod, Russie, 2021. [Paper] [Diapositive]
Auteurs : Daniil Kuts
Résumé : L'exécution symbolique dynamique est une technique largement utilisée pour les tests de logiciels automatisés, conçus pour l'exploration des chemins d'exécution et la détection des erreurs de programme. Une approche hybride s'est récemment répandue, lorsque l'objectif principal de l'exécution symbolique est d'aider Fuzzer à augmenter la couverture du programme. Plus l'exécuteur symbolique des branches peut inverser, plus il est utile pour Fuzzer. Un flux de contrôle de programme dépend souvent des valeurs de mémoire, qui sont obtenues par les index d'adresses informatiques à partir de l'entrée utilisateur. Cependant, la plupart des outils DSE ne prennent pas en charge de telles dépendances, ils manquent donc certaines succursales de programme souhaitées. Nous implémentons le raisonnement d'adresses symboliques sur les lectures de mémoire dans notre outil d'exécution symbolique dynamique SYDR. Les régions d'accès à la mémoire possibles sont déterminées soit en analysant les expressions symboliques de l'adresse mémoire, soit une recherche binaire avec SMT-solver. Nous proposons une technique de linéarisation améliorée pour modéliser les accès à la mémoire. Différentes méthodes de modélisation de la mémoire sont comparées sur l'ensemble des 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.
- QSYNTH: Une approche basée sur la synthèse du programme pour la déobfuscation du code binaire
Talk at : Bar, San Diego, Californie, 2020. [Papier]
Auteurs : Robin David, Luigi Coniglio, Mariano Ceccato
Résumé : Nous présentons une approche générique tirant parti de la synthèse du DSE et du programme pour synthétiser avec succès les programmes obscurcis avec des arithmétiques mixtes-arithmétiques, du codage des données ou de la virtualisation. L'algorithme de synthèse proposé est une primitive de synthèse d'énumération hors ligne guidée par une recherche de haut en bas. Nous montrons son efficacité contre un obfuscateur de pointe et son évolutivité car il remplace d'autres approches similaires basées sur la synthèse. Nous montrons également son efficacité en présence d'obscurcissement composite (combinaison de diverses techniques). Ce travail en cours éclaire l'efficacité de la synthèse pour cibler certains types d'obfuscations et ouvre la voie à des algorithmes plus robustes et à des stratégies de simplification.
- SYDR: exécution symbolique dynamique de pointe
Talk at : Ivannikov ISP Ras Open Conference, Moscou, Russie, 2020. [Paper] [Slide] [VIDEO]
Auteurs : A.vishnyakov, A.fedotov, D.Kuts, A.Novikov, D.Parygina, E.Kobrin, V.logunova, P.Belecky, S.Kurmangaleev
Résumé : L'exécution symbolique dynamique (DSE) possède une énorme quantité d'applications dans la sécurité informatique (fuzzing, découverte de vulnérabilité, inverse, etc.). Nous proposons plusieurs améliorations de performances et de précision pour l'exécution symbolique dynamique. Sauter des instructions non symboliques permet de construire un prédicat de chemin 1,2-3,5 fois plus rapide. Le moteur symbolique simplifie les formules lors de l'exécution symbolique. Le découpage des prédicats de chemin élimine les conjoints non pertinents à partir de requêtes de solveur. Nous gérons chaque table de saut (instruction Switch) en tant que branches multiples et décrivons la méthode d'exécution symbolique des programmes multithreads. Les solutions proposées ont été mises en œuvre dans l'outil SYDR. SYDR effectue l'inversion des branches dans le prédicat de chemin. SYDR combine l'outil d'instrumentation binaire dynamique Dynamorio avec le moteur symbolique Triton.
- Déobfuscation symbolique: du code virtualisé à l'original
Talk at : Dimva, Paris-Saclay, France, 2018. [Papier] [Diapositive]
Auteurs : Jonathan Salwan, Sébastien Bardin, Marie-Laure Pote
Résumé : 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 l'ingénierie inverse 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 de chemin symbolique, la souillure et la recompilation permettant de récupérer, à partir d'un code virtualisé, un code déviptualisé sémantiquement identique à l'original et de clôture. Nous définissons les critères et les mesures pour évaluer la pertinence des résultats désobfusés en termes d'exactitude et de précision. Enfin, nous proposons une configuration open source permettant d'évaluer l'approche proposée contre plusieurs formes de virtualisation.
- Déobfuscation de la protection logicielle basée sur la machine virtuelle
Talk at : Sstic, Rennes, France, 2017. [Papier français] [diapositive anglaise] [Vidéo française]
Auteurs : Jonathan Salwan, Sébastien Bardin, Marie-Laure Pote
Résumé : Dans cette présentation, nous décrivons une approche qui consiste à analyser automatiquement les protections de logiciels basées sur la machine et qui recompiles une nouvelle version du binaire sans de telles protections. Cette approche automatisée repose sur un guide d'exécution symbolique par une analyse de souillure et certaines politiques de concrétisation, puis sur une réécriture binaire en utilisant la transition LLVM.
- Comment Triton peut aider à inverser les protections logicielles basées sur la machine virtuelle
Talk at : CSAW SOS, NYC, New York, 2016. [Slide]
Auteurs : Jonathan Salwan, Romain Thomas
Résumé : La première partie de la conversation sera une introduction au cadre de Triton pour exposer ses composants et expliquer comment ils fonctionnent ensemble. Ensuite, la deuxième partie comprendra des démonstrations sur la façon dont il est possible d'inverser les protections virtuelles basées sur la machine en utilisant l'analyse de souillure, l'exécution symbolique, les simplifications SMT et les optimisations LLVM-IR.
- Analyse binaire dynamique et codes obscurcis
Talk at : St'hack, Bordeaux, France, 2016. [Slide]
Auteurs : Jonathan Salwan, Romain Thomas
Résumé : Lors de cette présentation, nous parlerons de la façon dont un DBA (analyse binaire dynamique) peut aider un ingénieur à la recherche de code obscurci. Nous introduirons d'abord certaines techniques d'obscuscations de base, puis exposerons comment il est possible de briser certaines choses (en utilisant notre framework DBA open-source - Triton) comme détecter les prédicats opaques, reconstruire CFG, trouver l'algorithme d'origine, isoler les données sensibles et bien d'autres ... Ensuite, nous terminerons par une démo et peu de mots sur nos travaux futurs.
- Comment Triton peut aider à analyser les binaires obscurcis
Publication à : Misc Magazine 82, 2015. [Article français]
Auteurs : Jonathan Salwan, Romain Thomas
Résumé : L'obscurcissement binaire est utilisé pour protéger la propriété intellectuelle du logiciel. Il existe différents types d'évolution mais à peu près, il transforme une structure binaire en une autre structure binaire en préservant le même sémantique. L'objectif de l'obscurcissement est de s'assurer que les informations d'origine sont «noyées» dans des informations inutiles qui rendront la rétro-ingénierie plus difficile. Dans cet article, nous montrerons comment nous pouvons analyser un programme OFFcalisé et briser certains obuscations en utilisant le cadre Triton.
- Triton: un cadre d'exécution conforme
Talk at : Sstic, Rennes, France, 2015. [Papier français] [diapositive anglaise détaillée]
Auteurs : Jonathan Salwan, Florent Saudel
Résumé : Ce discours concerne la publication de Triton, un cadre d'exécution concocable basé sur PIN. Il fournit des composants comme un moteur de souillure, un moteur d'exécution symbolique dynamique, un moteur instantané, une traduction de l'instruction x64 à SMT2, une interface Z3 pour résoudre les contraintes et les liaisons Python. Sur la base de ces composants, Triton offre la possibilité de créer des outils pour la recherche sur les vulnérabilités ou l'assistance à l'ingénierie inverse.
- Analyse du comportement dynamique utilisant l'instrumentation binaire
Talk at : St'hack, Bordeaux, France, 2015. [Diapositive]
Auteurs : Jonathan Salwan
Résumé : Ce discours peut être considéré comme la partie 2 de notre discours à Securityday. Dans la partie précédente, nous avons expliqué comment il était possible de couvrir une fonction ciblée en mémoire en utilisant l'approche DSE (dynamique symbolic exécution). Couvrir une fonction (ou ses états) ne signifie pas trouver toutes les vulnérabilités, une certaine vulnérabilité ne plante pas le programme. C'est pourquoi nous devons implémenter une analyse spécifique pour trouver des bogues spécifiques. Ces analyses sont basées sur l'instrumentation binaire et l'analyse du comportement d'exécution du programme. Dans cette conférence, nous verrons comment il est possible de trouver ces types de bogues suivants: off-by-by-by-by, pile / tas débordement, use-après-libre, chaîne de format et {écrire, lire} -What-where.
- Couvrant une fonction à l'aide d'une approche d'exécution symbolique dynamique
Talk at : Security Day, Lille, France, 2015. [Diapion]
Auteurs : Jonathan Salwan
Résumé : Ce discours concerne l'analyse binaire et l'instrumentation. Nous verrons comment il est possible de cibler une fonction spécifique, instantanée la mémoire / registre de contexte avant la fonction, traduire l'instrumentation en une représentation intermédiaire, appliquer une analyse de souillure en fonction de cette valeur IR, de construire / maintenir des formules pour un chemin spécifique dynamique, de restaurer la mémoire de contexte et de générer un autre concret de concret pour parcourir un autre chemin à parcourir la fonction de la mémoire de contexte.
Citer Triton
@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},
}