Triton: Dynamic Binary Analysis (DBA) framework

by do son · Published · Updated

Triton

Triton is a dynamic binary analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a Taint Engine, AST representations of the x86 and the x86-64 instructions set semantics, SMT simplification passes, and an SMT Solver Interface, and, the last but not least, Python bindings.

Based on these components, you are able to build program analysis tools, automate reverse engineering and perform software verification. As Triton is still a young project, please, don’t blame us if it is not yet reliable.

Engines and Components

  • Spread Taint
    Taint analysis is used to know at each program point what part of memory or register are controllable by the user input. According to the instruction semantics, the taint is spread over the execution. Read more
  • Dynamic Symbolic Execution
    The symbolic execution engine transforms the control flow and the data flow of the program into symbolic expressions. These expressions may be used to know at each program point what values can hold a register or part of memory. Read more
  • SMT Solver Interface
    This component allows you to solve symbolic expressions. As all expressions are on the SMT2-LIB representation, you can plug any SMT solver which supports this format. By default, Triton is interfaced with the Z3 SMT solver. Read more
  • AST Representations of Semantics
    Triton converts the x86 and the x86-64 instruction set semantics into AST representations which allows you to perform precise analysis and allow you to build and modify your own symbolic expressions.
  • SMT simplification passes
    Triton allows you to optimize or translate all SMT AST nodes before the assignment to a register, a memory, or a volatile symbolic expression. This feature allows you to deobfuscate some expressions.
  • Python Bindings
    Build your own tools through a high-level language and communicate with the Pin API and Triton’s components via Python bindings.

Changelog v0.9

  • Better dealing with path constraints
  • Lifting To SMT file
  • Lifting to Python file
  • Lifting to LLVM file
  • Lifting to LLVM IR and back
  • Python from 3.6 to 3.9 comparability
  • Add new AST optimizations
  • Add new instructions
  • Add FPU specification
  • Add support for Thumb IT instructions
  • Add the Bitwuzla solver interface
  • Add a synthesis expression engine
  • Fix semantics
  • Fix optimizations
  • And so many more

Download & Tutorial

Copyright:

* Jonathan Salwan (Quarkslab)
* Pierrick Brunet (Quarkslab)
* Romain Thomas (Quarkslab)
* Florent Saudel (Bordeaux University)

Tags: Triton