Triton Dynamic Binary Analysis Library

Triton is used as a foundation for several specialized security and reverse-engineering tools. If you are looking for specific implementations of concolic execution, deobfuscation, or binary analysis, consider these projects:

• Exrop: Automatic ROPChain Generation.
• Pimp: An R2 plugin for concolic execution and total control.
• Ponce: An IDA 2016 plugin for one-click symbolic execution.
• QSynthesis: A greybox synthesizer for deobfuscating assembly instructions.
• TritonDSE: A Dynamic Symbolic Execution (DSE) library with loading and exploration capabilities.
• Titan: A VMProtect devirtualizer.

To build from source, clone the repository and use cmake. To enable full functionality including LLVM and Bitwuzla support, use the specific CMake flags provided below.

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

# Build with LLVM and Bitwuzla support
$ cmake -DLLVM_INTERFACE=ON -DCMAKE_PREFIX_PATH=$(llvm-config --prefix) -DBITWUZLA_INTERFACE=ON ..

Triton is available via the vcpkg dependency manager.

$ git clone https://github.com/Microsoft/vcpkg.git
$ cd vcpkg
$ ./bootstrap-vcpkg.sh  # ./bootstrap-vcpkg.bat for Windows
$ ./vcpkg integrate install
$ ./vcpkg install triton

Triton allows you to perform dynamic symbolic execution by creating a TritonContext for a specific architecture. You can set concrete register values, symbolize registers, execute instructions, and solve constraints using an SMT solver interface.

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)

# Solve constraint
ctx.getModel(rcx_expr.getAst() == 0xdead)

If a binary is packed (e.g., it shows no strings or has dynamic jumps in IDA), you can unpack it by dumping the process memory while it is running and waiting for input.

1. Run the binary in gdb.
2. When the binary reaches the input prompt (e.g., Citizen Access ID:), interrupt it with Ctrl-C.
3. Identify the memory maps using cat /proc/<PID>/maps (where <PID> is the process ID obtained via getpid).
4. Use the dump memory command in GDB to save the specific memory range to a file.

The easiest way to install Triton for Python development is via pip.

pip install triton-library

When performing binary emulation, you can hijack specific libc routines (like getchar) to symbolize their return values. This allows you to treat user input as symbolic variables.

To optimize the analysis of large binaries or virtual machines:

1. Symbolize Input: During emulation, when a target function like getchar is called, symbolize its return value.
2. Filter Instructions: Generate a sub-trace by printing only instructions that contain symbolic variables. This significantly reduces the instruction count by focusing only on code paths linked to the input.
3. Constraint Solving: Use Triton's symbolic engine to apply constraints to flags (e.g., setting zf to 1 for conditional jumps) to explore specific execution paths.

If you encounter Could NOT find PythonLibs errors on MacOS M1, manually specify the Python paths in your cmake command. You can find the required paths using sysconfig.get_paths() in Python.

cmake -DCMAKE_INSTALL_PREFIX=/opt/homebrew/ \
      -DPYTHON_EXECUTABLE=/opt/homebrew/bin/python3 \
      -DPYTHON_LIBRARIES=/opt/homebrew/Cellar/python@3.10/3.10.8/Frameworks/Python.framework/Versions/3.10/lib/libpython3.10.dylib \
      -DPYTHON_INCLUDE_DIRS=/opt/homebrew/opt/python@3.10/Frameworks/Python.framework/Versions/3.10/include/python3.10/ \
      ..

You can reconstruct the logic of a binary by lifting the path predicate generated during emulation into LLVM Intermediate Representation (IR). This is useful for recovering the underlying mathematical constraints or source-like logic of a program.

Use ctx.getPathPredicate() to retrieve the current path predicate and ctx.liftToLLVM() to convert it into an LLVM module.

def lifting2llvm(ctx):
   predicate = ctx.getPathPredicate()
   M = ctx.liftToLLVM(predicate, fname="mars_analytica", optimize=True)
   print(M)
   return