Reverse engineering framework in Python

Symbolic execution tool

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.

KLEE Symbolic Execution Engine

Binary Analysis Platform

IDA 2016 plugin contest winner! Symbolic Execution just one-click away!

An open source interactive disassembler

Angora is a mutation-based fuzzer. The main goal of Angora is to increase branch coverage by solving path constraints without symbolic execution.

A unit test-like interface for fuzzing and symbolic execution

A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.

Playing with the Tigress binary protection. Break some of its protections and solve some of its challenges. Automatic deobfuscation using symbolic execution, taint analysis and LLVM.

A static analysis tool for Python that blurs the line between testing and type systems.

yet another tool for analysing binaries

History of symbolic execution (as well as SAT/SMT solving, fuzzing, and taint data tracking)

A lightweight VM for hardware hacking, RE (fuzzing, symEx, exploiting etc) and wargaming tasks

Simple Theorem Prover, an efficient SMT solver for bitvectors

Use angr in the IDA Pro debugger generating a state from the current debug session

SymGDB - symbolic execution plugin for gdb

Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE

Automatic ROPChain Generation

Seeding fuzzers with symbolic execution

Offensive vulnerability scanner for ethereum, and symbolic execution tool for the Ethereum Virtual Machine

A Dynamic Symbolic Execution (DSE) engine for JavaScript. ExpoSE is highly scalable, compatible with recent JavaScript standards, and supports symbolic modelling of strings and regular expressions.

Simplify Ethereum security analysis and testing

Testing Intermediate Representations for Binary Analysis

KLEE-TAINT - Klee with taint analysis support

Tutorial on Symbolic Execution. Hands-on session is based on the angr framework.

CRETE under development

The Symbolic, Mechanized, Observable, Operational SHell: an executable formalization of the POSIX shell standard.

AI based fuzzer based on imitation learning