Triton is a dynamic binary analysis framework. It provides internal components like a dynamic symbolic execution engine, a dynamic taint analysis engine, AST representation of the x86, x86-64, ARM32 and AArch64 ISA semantic, an expressions synthesis engine, some SMT simplification passes, SMT solver interface to Z3 and Bitwuzla and, the last but not least, Python bindings. Based on these components, you are able to build your program analysis tools, automate reverse engineering, perform software verification or just emulate code.

<img src="http://triton.quarkslab.com/files/triton_v09_architecture.svg" width="80%"/>


<img src="http://triton.quarkslab.com/files/triton_multi_os.png"/>

As Triton is a kind of a part-time project, please, don't blame us if it is not fully reliable. Open issues or pull requests are always better than trolling =). However, you can follow the development on twitter @qb_triton.

Quick start

• Installation
• Python API
• C++ API
• Python Examples
• They already used Triton

Getting started

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'

Install

Triton relies on the following dependencies:

* libboost                   >= 1.68
* libpython                  >= 3.6
* libcapstone                >= 4.0.x   https://github.com/capstone-engine/capstone
* libz3         (optional)   >= 4.6.0   https://github.com/Z3Prover/z3
* libbitwuzla   (optional)   n/a        https://github.com/bitwuzla/bitwuzla
* llvm          (optional)   >= 12

Linux and OS X

$ git clone https://github.com/JonathanSalwan/Triton
$ cd Triton
$ mkdir build ; cd build
$ cmake ..
$ make -j3
$ sudo make install

Windows

You can use cmake to generate the .sln file of 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-4.0.2-win64/include" \
  -DCAPSTONE_LIBRARIES="C:/Users/jonathan/Works/Tools/capstone-4.0.2-win64/capstone.lib" ..

However, if you prefer to directly download the precompiled library, check out our AppVeyor's artefacts. Note that if you use AppVeyor's artefacts, you probably have to install the Visual C++ Redistributable packages for Visual Studio 2012.

Contributors

Triton is strongly powered by Quarkslab for years but also by several strong contributors:

• Alberto Garcia Illera - Cruise Automation
• Alexey Vishnyakov - ISP RAS
• Black Binary - 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

They already used Triton

Tools

• Ponce: IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
• QSynthesis: Greybox Synthesizer geared for deobfuscation of assembly instructions.
• Pimp: Triton based R2 plugin for concolic execution and total control.
• Exrop: Automatic ROPChain Generation.

Papers and conference

• Greybox Program Synthesis: A New Approach to Attack Dataflow Obfuscation Talk at: Blackhat USA, Las Vegas, Nevada, 2021. [slide] Authors: Robin David Abstract: This talk presents the latest advances in program synthesis applied for deobfuscation. It aims at demystifying this analysis technique by showing how it can be put into action on obfuscation. Especially the implementation Qsynthesis released for this talk shows a complete end-to-end workflow to deobfuscate assembly instructions back in optimized (deobfuscated) instructions reassembled back in the binary.
• From source code to crash test-case through software testing automation Talk at: C&ESAR, Rennes, France, 2021. [paper] [slide] Authors: Robin David, Jonathan Salwan, Justin Bourroux Abstract: This paper present an approach automating the software testing process from a source code to the dynamic testing of the compiled program. More specifically, from a static analysis report indicating alerts on source lines it enables testing to cover these lines dynamically and opportunistically checking whether whether or not they can trigger a crash. The result is a test corpus allowing to cover alerts and to trigger them if they happen to be true positives. This paper discuss the methodology employed to track alerts down in the compiled binary, the testing engines selection process and the results obtained on a TCP/IP stack implementation for embedded and IoT systems.
• Symbolic Security Predicates: Hunt Program Weaknesses Talk at: Ivannikov ISP RAS Open Conference, Moscow, Russia, 2021. [paper] [slide] Authors: A.Vishnyakov, V.Logunova, E.Kobrin, D.Kuts, D.Parygina, A.Fedotov Abstract: Dynamic symbolic execution (DSE) is a powerful method for path exploration during hybrid fuzzing and automatic bug detection. We propose security predicates to effectively detect undefined behavior and memory access violation errors. Initially, we symbolically execute program on paths that don’t trigger any errors (hybrid fuzzing may explore these paths). Then we construct a symbolic security predicate to verify some error condition. Thus, we may change the program data flow to entail null pointer dereference, division by zero, out-of-bounds access, or integer overflow weaknesses. Unlike static analysis, dynamic symbolic execution does not only report errors but also generates new input data to reproduce them. Furthermore, we introduce function semantics modeling for common C/C++ standard library functions. We aim to model the control flow inside a function with a single symbolic formula. This assists bug detection, speeds up path exploration, and overcomes overconstraints in path predicate. We implement the proposed techniques in our dynamic symbolic execution tool Sydr. Thus, we utilize powerful methods from Sydr such as path predicate slicing that eliminates irrelevant constraints. We present Juliet Dynamic to measure dynamic bug detection tools accuracy. The testing system also verifies that generated inputs trigger sanitizers. We evaluate Sydr accuracy for 11 CWEs from Juliet test suite. Sydr shows 95.59% overall accuracy. We make Sydr evaluation artifacts publicly available to facilitate results reproducibility.
• Towards Symbolic Pointers Reasoning in Dynamic Symbolic Execution Talk at: Ivannikov Memorial Workshop, Nizhny Novgorod, Russia, 2021. [paper] [slide] Authors: Daniil Kuts Abstract: Dynamic symbolic execution is a widely used technique for automated software testing, designed for execution paths exploration and program errors detection. A hybrid approach has recently become widespread, when the main goal of symbolic execution is helping fuzzer increase program coverage. The more branches symbolic executor can invert, the more useful it is for fuzzer. A program control flow often depends on memory values, which are obtained by computing address indexes from user input. However, most DSE tools don't support such dependencies, so they miss some desired program branches. We implement symbolic addresses reasoning on memory reads in our dynamic symbolic execution tool Sydr. Possible memory access regions are determined by either analyzing memory address symbolic expressions, or binary searching with SMT-solver. We propose an enhanced linearization technique to model memory accesses. Different memory modeling methods are compared on the set of programs. Our evaluation shows that symbolic addresses handling allows to discover new symbolic branches and increase the program coverage.
• QSynth: A Program Synthesis based Approach for Binary Code Deobfuscation Talk at: BAR, San Diego, California, 2020. [paper] Authors: Robin David, Luigi Coniglio, Mariano Ceccato Abstract: We present a generic approach leveraging both DSE and program synthesis to successfully synthesize programs obfuscated with Mixed-Boolean-Arithmetic, Data-Encoding or Virtualization. The synthesis algorithm proposed is an offline enumerate synthesis primitive guided by top-down breath-first search. We shows its effectiveness against a state-of-the-art obfuscator and its scalability as it supersedes other similar approaches based on synthesis. We also show its effectiveness in presence of composite obfuscation (combination of various techniques). This ongoing work enlightens the effectiveness of synthesis to target certain kinds of obfuscations and opens the way to more robust algorithms and simplification strategies.
• Sydr: Cutting Edge Dynamic Symbolic Execution Talk at: Ivannikov ISP RAS Open Conference, Moscow, Russia, 2020. [paper] [slide] [video] Authors: A.Vishnyakov, A.Fedotov, D.Kuts, A.Novikov, D.Parygina, E.Kobrin, V.Logunova, P.Belecky, S.Kurmangaleev Abstract: Dynamic symbolic execution (DSE) has enormous amount of applications in computer security (fuzzing, vulnerability discovery, reverse-engineering, etc.). We propose several performance and accuracy improvements for dynamic symbolic execution. Skipping non-symbolic instructions allows to build a pa