Convert Figma logo to code with AI

JonathanSalwan logoTriton

Triton is a dynamic binary analysis library. Build your own program analysis tools, automate your reverse engineering, perform software verification or just emulate code.

3,470
527
3,470
29
View on GitHub

Top Related Projects

unicorn-engine's avatar

unicorn

7,468

Unicorn CPU emulator framework (ARM, AArch64, M68K, Mips, Sparc, PowerPC, RiscV, S390x, TriCore, X86)

angr's avatar

angr

7,457

A powerful and user-friendly binary analysis platform!

capstone-engine's avatar

capstone

7,334

Capstone disassembly/disassembler framework for ARM, ARM64 (ARMv8), Alpha, BPF, Ethereum VM, HPPA, LoongArch, M68K, M680X, Mips, MOS65XX, PPC, RISC-V(rv32G/rv64G), SH, Sparc, SystemZ, TMS320C64X, TriCore, Webassembly, XCore and X86.

radareorg's avatar

radare2

20,310

UNIX-like reverse engineering framework and command-line toolset

Z3Prover's avatar

z3

10,140

The Z3 Theorem Prover

Quick Overview

Triton is a dynamic binary analysis framework based on a symbolic execution engine. It is designed to assist researchers and security engineers with reverse engineering, software verification, and vulnerability discovery.

Pros

  • Powerful Symbolic Execution Engine: Triton's symbolic execution engine allows for in-depth analysis of program behavior, enabling the discovery of complex vulnerabilities and the generation of test cases.
  • Cross-Platform Compatibility: Triton supports multiple architectures, including x86, x86-64, ARMv7, and ARMv8, making it a versatile tool for analyzing a wide range of software.
  • Extensive API and Scripting Capabilities: Triton provides a comprehensive API that allows users to extend its functionality and automate various analysis tasks.
  • Active Development and Community: The Triton project is actively maintained, with regular updates and a growing community of contributors and users.

Cons

  • Steep Learning Curve: Triton's powerful features and flexibility can make it challenging for beginners to get started, requiring a significant investment of time and effort to master.
  • Performance Overhead: Symbolic execution can be computationally intensive, and Triton's performance may be a concern for large or complex programs.
  • Limited Documentation: While the project has a growing community, the documentation could be more comprehensive, making it harder for new users to get started.
  • Potential Compatibility Issues: As a cross-platform tool, Triton may encounter compatibility issues with certain software or environments, requiring additional configuration or workarounds.

Code Examples

Here are a few examples of how to use Triton's API:

  1. Symbolic Execution of a Simple Function:
from triton import TritonContext, ARCH, Instruction, MemoryAccess, CPUSIZE

# Create a Triton context
ctx = TritonContext(ARCH.X86_64)

# Define the function to analyze
function = [
    b"\x48\x83\xec\x08",  # sub rsp, 8
    b"\x48\x89\x7c\x24\x00",  # mov [rsp+0x0], rdi
    b"\x48\x8b\x7c\x24\x00",  # mov rdi, [rsp+0x0]
    b"\x48\x83\xc4\x08",  # add rsp, 8
    b"\xc3",  # ret
]

# Process the function instruction by instruction
for inst in function:
    ctx.processing(Instruction(inst))

# Get the symbolic variable representing the function's return value
ret_value = ctx.getSymbolicRegister(ctx.registers.rax)
print(ret_value)
  1. Taint Analysis:
from triton import TritonContext, ARCH, Instruction, MemoryAccess, CPUSIZE

# Create a Triton context
ctx = TritonContext(ARCH.X86_64)

# Define the program to analyze
program = [
    b"\x48\x89\xd8",  # mov rax, rbx
    b"\x48\x31\xc0",  # xor rax, rax
    b"\x48\x83\xc0\x01",  # add rax, 1
    b"\xc3",  # ret
]

# Process the program instruction by instruction
for inst in program:
    ctx.processing(Instruction(inst))

# Taint the input register (rbx)
ctx.taintRegister(ctx.registers.rbx)

# Check which registers and memory locations are tainted
tainted_regs = ctx.getTaintedRegisters()
tainted_mems = ctx.getTaintedMemory()
print(tainted_regs, tainted_mems)
  1. Constraint Solving:
from triton import TritonContext, ARCH, Instruction, MemoryAccess, CPUSIZE

# Create a Triton context
ctx = TritonContext(ARCH.X86_64)

# Define the program to analyze
program = [
    b"\x48\x31\xc0",  # xor r

Competitor Comparisons

unicorn-engine logo

unicorn

7,468

Unicorn CPU emulator framework (ARM, AArch64, M68K, Mips, Sparc, PowerPC, RiscV, S390x, TriCore, X86)

Pros of Unicorn

  • Wider architecture support, including x86, ARM, MIPS, and more
  • Faster emulation speed, suitable for large-scale fuzzing and dynamic analysis
  • Simpler API, making it easier to integrate into existing projects

Cons of Unicorn

  • Less focus on symbolic execution and formal verification
  • Limited built-in analysis capabilities compared to Triton
  • Lacks advanced features like taint analysis and abstract interpretation

Code Comparison

Unicorn example:

from unicorn import *

# Initialize emulator in X86-32bit mode
mu = Uc(UC_ARCH_X86, UC_MODE_32)

# Map 2MB memory for this emulation
mu.mem_map(ADDRESS, 2 * 1024 * 1024)

# Write machine code to be emulated to memory
mu.mem_write(ADDRESS, X86_CODE32)

Triton example:

from triton import *

ctx = TritonContext()
ctx.setArchitecture(ARCH.X86_64)

# Define symbolic variables
sym_x = ctx.symbolizeRegister(ctx.registers.rax)
sym_y = ctx.symbolizeRegister(ctx.registers.rbx)

# Define constraints
ctx.setConcreteRegisterValue(ctx.registers.rax, 2)
ctx.setConcreteRegisterValue(ctx.registers.rbx, 3)

Both Unicorn and Triton are powerful tools for binary analysis and emulation, but they serve different purposes. Unicorn excels in pure emulation and performance, while Triton focuses on symbolic execution and advanced program analysis techniques.

angr logo

angr

7,457

A powerful and user-friendly binary analysis platform!

Pros of angr

  • More comprehensive framework for binary analysis, including symbolic execution and program slicing
  • Larger community and ecosystem with extensive documentation and tutorials
  • Supports a wider range of architectures and file formats

Cons of angr

  • Steeper learning curve due to its complexity and extensive features
  • Can be slower for certain types of analysis compared to Triton
  • Requires more system resources, especially for large-scale analyses

Code Comparison

angr example:

import angr

proj = angr.Project('binary')
state = proj.factory.entry_state()
simgr = proj.factory.simulation_manager(state)
simgr.explore(find=0x400000)

Triton example:

from triton import *

ctx = TritonContext()
ctx.setArchitecture(ARCH.X86_64)
ctx.setMode(MODE.SYMBOLIC_EXECUTION, True)
ctx.loadBinary('binary')

Both frameworks provide powerful binary analysis capabilities, but angr offers a more comprehensive suite of tools at the cost of increased complexity, while Triton focuses on efficient symbolic execution and taint analysis with a simpler API.

capstone-engine logo

capstone

7,334

Capstone disassembly/disassembler framework for ARM, ARM64 (ARMv8), Alpha, BPF, Ethereum VM, HPPA, LoongArch, M68K, M680X, Mips, MOS65XX, PPC, RISC-V(rv32G/rv64G), SH, Sparc, SystemZ, TMS320C64X, TriCore, Webassembly, XCore and X86.

Pros of Capstone

  • Wider architecture support (x86, ARM, MIPS, PowerPC, etc.)
  • Lightweight and faster disassembly
  • More mature and widely adopted in the industry

Cons of Capstone

  • Limited to disassembly only, no advanced analysis features
  • Less focus on symbolic execution and dynamic analysis
  • Requires additional tools for more complex reverse engineering tasks

Code Comparison

Capstone (disassembly):

cs_insn *insn;
size_t count = cs_disasm(handle, code, code_size, address, 0, &insn);
for (size_t j = 0; j < count; j++) {
    printf("0x%"PRIx64":\t%s\t\t%s\n", insn[j].address, insn[j].mnemonic, insn[j].op_str);
}

Triton (symbolic execution):

instruction = Instruction()
instruction.setOpcode(opcode)
instruction.setAddress(address)
processing(instruction)
print(instruction)

Summary

Capstone is a lightweight, fast disassembler with broad architecture support, making it ideal for basic reverse engineering tasks. Triton, on the other hand, offers more advanced features like symbolic execution and dynamic binary analysis, making it better suited for complex reverse engineering and vulnerability research. While Capstone is more widely adopted and mature, Triton provides a more comprehensive toolkit for in-depth analysis of binary code.

radareorg logo

radare2

20,310

UNIX-like reverse engineering framework and command-line toolset

Pros of radare2

  • More comprehensive reverse engineering framework with a wider range of features
  • Larger community and ecosystem, with more plugins and extensions available
  • Better suited for general-purpose reverse engineering tasks

Cons of radare2

  • Steeper learning curve due to its extensive feature set
  • Can be more resource-intensive for certain operations
  • Less focused on symbolic execution and dynamic binary analysis

Code Comparison

radare2:

r_core_cmd(core, "aaa", 0);
r_core_cmd(core, "pdf @main", 0);
r_core_cmd(core, "afx", 0);

Triton:

inst = Instruction()
inst.setOpcode(opcode)
inst.setAddress(addr)
ProcessingPyTriton().processing(inst)

Summary

radare2 is a more comprehensive reverse engineering framework with a broader range of features and a larger community. It's better suited for general-purpose reverse engineering tasks but has a steeper learning curve. Triton, on the other hand, is more focused on symbolic execution and dynamic binary analysis, making it more specialized but potentially easier to use for specific tasks.

Z3Prover logo

z3

10,140

The Z3 Theorem Prover

Pros of z3

  • More mature and widely adopted SMT solver with extensive documentation
  • Supports a broader range of theories and logics
  • Offers bindings for multiple programming languages

Cons of z3

  • Steeper learning curve for beginners
  • Less focused on specific use cases like binary analysis
  • May require more setup and configuration for specialized tasks

Code Comparison

z3:

from z3 import *

x = Int('x')
y = Int('y')
s = Solver()
s.add(x + y > 5)
s.add(x > 1, y > 1)
print(s.check())
print(s.model())

Triton:

from triton import *

ctx = TritonContext()
ctx.setArchitecture(ARCH.X86_64)

x = ctx.symbolizeRegister(ctx.registers.rax)
y = ctx.symbolizeRegister(ctx.registers.rbx)

ast = ctx.getAstContext()
expr = ast.land([
    ast.bvadd(x, y) > ast.bv(5, 64),
    x > ast.bv(1, 64),
    y > ast.bv(1, 64)
])

model = ctx.getModel(expr)
print(model)

The code examples demonstrate basic constraint solving in both z3 and Triton. While z3 provides a more general-purpose SMT solving approach, Triton focuses on symbolic execution in the context of binary analysis, offering built-in support for CPU architectures and registers.

Convert Figma logo designs to code with AI

Visual Copilot

Introducing Visual Copilot: A new AI model to turn Figma designs to high quality code using your components.

Try Visual Copilot

README

Triton is a dynamic binary analysis library. It provides internal components that allow you to build your program analysis tools, automate reverse engineering, perform software verification or just emulate code.

  • Dynamic symbolic execution
  • Dynamic taint analysis
  • AST representation of the x86, x86-64, ARM32, AArch64 and RISC-V 32/64 ISA semantic
  • Expressions synthesis
  • SMT simplification passes
  • Lifting to LLVM as well as Z3 and back
  • SMT solver interface to Z3 and Bitwuzla
  • C++ and Python API


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.

      Codecov      

Quick start

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:

* 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 and MacOS

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

By default, LLVM and Bitwuzla are not compiled. If you want to enjoy the full power of Triton, the cmake compile is:

$ cmake -DLLVM_INTERFACE=ON -DCMAKE_PREFIX_PATH=$(llvm-config --prefix) -DBITWUZLA_INTERFACE=ON ..

MacOS M1 Note:

In case if you get compilation errors like:

Could NOT find PythonLibs (missing: PYTHON_LIBRARIES PYTHON_INCLUDE_DIRS)

Try to specify PYTHON_EXECUTABLE, PYTHON_LIBRARIES and PYTHON_INCLUDE_DIRS for your specific Python version:

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/ \
      ..

This information you can get out from this snippet:

from sysconfig import get_paths
info = get_paths()
print(info)

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-5.0.1-win64/include" \
  -DCAPSTONE_LIBRARIES="C:/Users/jonathan/Works/Tools/capstone-5.0.1-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.

Installing from vcpkg

The Triton port in vcpkg is kept up to date by Microsoft team members and community contributors. The url of vcpkg is: https://github.com/Microsoft/vcpkg. You can download and install Triton using 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

If the version is out of date, please create an issue or pull request on the vcpkg repository.

Contributors

They already used Triton

Tools

  • Exrop: Automatic ROPChain Generation.
  • Pimp: Triton based R2 plugin for concolic execution and total control.
  • Ponce: IDA 2016 plugin contest winner! Symbolic Execution just one-click away!
  • QSynthesis: Greybox Synthesizer geared for deobfuscation of assembly instructions.
  • TritonDSE: Triton-based DSE library with loading and exploration capabilities.
  • Titan: Titan is a VMProtect devirtualizer using Triton.

Papers and conference

  • Sydr-Fuzz: Continuous Hybrid Fuzzing and Dynamic Analysis for Security Development Lifecycle
    Talk at: Ivannikov ISP RAS Open Conference, Moscow, Russia, 2022. [paper] [slide]
    Authors: Vishnyakov A., Kuts D., Logunova V., Parygina D., Kobrin E., Savidov G., Fedotov A.
    Abstract: Nowadays automated dynamic analysis frameworks for continuous testing are in high demand to ensure software safety and satisfy the security development lifecycle (SDL) requirements. The security bug hunting efficiency of cutting-edge hybrid fuzzing techniques outperforms widely utilized coverage-guided fuzzing. We propose an enhanced dynamic analysis pipeline to leverage productivity of automated bug detection based on hybrid fuzzing. We implement the proposed pipeline in the continuous fuzzing toolset Sydr-Fuzz which is powered by hybrid fuzzing orchestrator, integrating our DSE tool Sydr with libFuzzer and AFL++. Sydr-Fuzz also incorporates security predicate checkers, crash triaging tool Casr, and utilities for corpus minimization and coverage gathering. The benchmarking of our hybrid fuzzer against alternative state-of-the-art solutions demonstrates its superiority over coverage-guided fuzzers while remaining on the same level with advanced hybrid fuzzers. Furthermore, we approve the relevance of our approach by discovering 85 new real-world software flaws within the OSS-Sydr-Fuzz project. Finally, we open Casr source code to the community to facilitate examination of the existing crashes.

  • Strong Optimistic Solving for Dynamic Symbolic Execution
    Talk at: Ivannikov Memorial Workshop, Kazan, Russia, 2022. [paper] [slide]
    Authors: Parygina D., Vishnyakov A., Fedotov A.
    Abstract: Dynamic symbolic execution (DSE) is an effective method for automated program testing and bug detection. It is increasing the code coverage by the complex branches exploration during hybrid fuzzing. DSE tools invert the branches along some execution path and help fuzzer examine previously unavailable program parts. DSE often faces over- and underconstraint problems. The first one leads to significant analysis complication while the second one causes inaccurate symbolic execution. We propose strong optimistic solving method that eliminates irrelevant path predicate constraints for target branch inversion. We eliminate such symbolic constraints that the target branch is not control dependent on. Moreover, we separately handle symbolic branches that have nested control transfer instructions that pass control beyond the parent branch scope, e.g. return, goto, break, etc. We implement the proposed method in our dynamic symbolic execution tool Sydr. We evaluate the strong optimistic strategy, the optimistic strategy that contains only the last constraint negation, and their combination. The results show that the strategies combination helps increase either the code coverage or the average number of correctly inverted branches per one minute. It is optimal to apply both strategies together in contrast with other configurations.

  • 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 path predicate 1.2--3.5 times faster. Symbolic engine simplifies formulas during symbolic execution. Path predicate slicing eliminates irrelevant conjuncts from solver queries. We handle each jump table (switch statement) as multiple branches and describe the method for symbolic execution of multi-threaded programs. The proposed solutions were implemented in Sydr tool. Sydr performs inversion of branches in path predicate. Sydr combines DynamoRIO dynamic binary instrumentation tool with Triton symbolic engine.

  • Symbolic Deobfuscation: From Virtualized Code Back to the Original
    Talk at: DIMVA, Paris-Saclay, France, 2018. [paper] [slide]
    Authors: Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet
    Abstract: Software protection has taken an important place during the last decade in order to protect legit software against reverse engineering or tampering. Virtualization is considered as one of the very best defenses against such attacks. We present a generic approach based on symbolic path exploration, taint and recompilation allowing to recover, from a virtualized code, a devirtualized code semantically identical to the original one and close in size. We define criteria and metrics to evaluate the relevance of the deobfuscated results in terms of correctness and precision. Finally we propose an open-source setup allowing to evaluate the proposed approach against several forms of virtualization.

  • Deobfuscation of VM based software protection
    Talk at: SSTIC, Rennes, France, 2017. [french paper] [english slide] [french video]
    Authors: Jonathan Salwan, Sébastien Bardin, Marie-Laure Potet
    Abstract: In this presentation we describe an approach which consists to automatically analyze virtual machine based software protections and which recompiles a new version of the binary without such protections. This automated approach relies on a symbolic execution guide by a taint analysis and some concretization policies, then on a binary rewriting using LLVM transition.

  • How Triton can help to reverse virtual machine based software protections
    Talk at: CSAW SOS, NYC, New York, 2016. [slide]
    Authors: Jonathan Salwan, Romain Thomas
    Abstract: The first part of the talk is going to be an introduction to the Triton framework to expose its components and to explain how they work together. Then, the second part will include demonstrations on how it's possible to reverse virtual machine based protections using taint analysis, symbolic execution, SMT simplifications and LLVM-IR optimizations.

  • Dynamic Binary Analysis and Obfuscated Codes
    Talk at: St'Hack, Bordeaux, France, 2016. [slide]
    Authors: Jonathan Salwan, Romain Thomas
    Abstract: At this presentation we will talk about how a DBA (Dynamic Binary Analysis) may help a reverse engineer to reverse obfuscated code. We will first introduce some basic obfuscation techniques and then expose how it's possible to break some stuffs (using our open-source DBA framework - Triton) like detect opaque predicates, reconstruct CFG, find the original algorithm, isolate sensible data and many more... Then, we will conclude with a demo and few words about our future work.

  • How Triton may help to analyse obfuscated binaries
    Publication at: MISC magazine 82, 2015. [french article]
    Authors: Jonathan Salwan, Romain Thomas
    Abstract: Binary obfuscation is used to protect software's intellectual property. There exist different kinds of obfucation but roughly, it transforms a binary structure into another binary structure by preserving the same semantic. The aim of obfuscation is to ensure that the original information is "drown" in useless information that will make reverse engineering harder. In this article we will show how we can analyse an ofbuscated program and break some obfuscations using the Triton framework.

  • Triton: A Concolic Execution Framework
    Talk at: SSTIC, Rennes, France, 2015. [french paper] [detailed english slide]
    Authors: Jonathan Salwan, Florent Saudel
    Abstract: This talk is about the release of Triton, a concolic execution framework based on Pin. It provides components like a taint engine, a dynamic symbolic execution engine, a snapshot engine, translation of x64 instruction to SMT2, a Z3 interface to solve constraints and Python bindings. Based on these components, Triton offers the possibility to build tools for vulnerabilities research or reverse-engineering assistance.

  • Dynamic Behavior Analysis Using Binary Instrumentation
    Talk at: St'Hack, Bordeaux, France, 2015. [slide]
    Authors: Jonathan Salwan
    Abstract: This talk can be considered like the part 2 of our talk at SecurityDay. In the previous part, we talked about how it was possible to cover a targeted function in memory using the DSE (Dynamic Symbolic Execution) approach. Cover a function (or its states) doesn't mean find all vulnerabilities, some vulnerability doesn't crashes the program. That's why we must implement specific analysis to find specific bugs. These analysis are based on the binary instrumentation and the runtime behavior analysis of the program. In this talk, we will see how it's possible to find these following kind of bugs : off-by-one, stack / heap overflow, use-after-free, format string and {write, read}-what-where.

  • Covering a function using a Dynamic Symbolic Execution approach
    Talk at: Security Day, Lille, France, 2015. [slide]
    Authors: Jonathan Salwan
    Abstract: This talk is about binary analysis and instrumentation. We will see how it's possible to target a specific function, snapshot the context memory/registers before the function, translate the instrumentation into an intermediate representation,apply a taint analysis based on this IR, build/keep formulas for a Dynamic Symbolic Execution (DSE), generate a concrete value to go through a specific path, restore the context memory/register and generate another concrete value to go through another path then repeat this operation until the target function is covered.

Cite 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},
}