Triton is a dynamic binary analysis (DBA) framework. It provides internal components like a Dynamic Symbolic Execution (DSE) engine, a dynamic taint engine, AST representations of the x86, x86-64, ARM32 and AArch64 Instructions Set Architecture (ISA), SMT simplification passes, 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 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.
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")) # xor 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'- Jonathan Salwan - Lead dev, Quarkslab
- Christian Heitman - Core dev, Quarkslab
- Pierrick Brunet - Core dev, Quarkslab
- Romain Thomas - Core dev, Quarkslab
- Florent Saudel - Core dev, Bordeaux University
@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},
}