Axel Tillequin

https://github.com/bdcht/amoco

Amoco is a python package dedicated to the (static) analysis of binaries.
It features:
- a generic framework for decoding instructions, developed to reduce the time needed to implement support for new architectures.
- a symbolic algebra module which allows to describe the semantics of every instructions and compute a functional representation of instruction blocks.
- a generic execution model wich provides an abstract memory model to deal with concrete or symbolic values transparently, and other system-dependent features.
- various classes implementing usual disassembly techniques like linear sweep, recursive traversal, or more elaborated techniques like path-predicate which relies on SAT/SMT solvers to proceed with discovering the control flow graph or even to implement techniques like DARE (Directed Automated Random Exploration).
- various generic "helpers" and arch-dependent pretty printers to allow custom look-and-feel configurations (think AT&T vs. Intel syntax, absolute vs. relative offsets, decimal or hex immediates, etc).

AmocoPlugin
look_for_gadgets_with_equations.py

???

???

http://angr.io/

angr is a framework for analyzing binaries. It focuses on both static and dynamic symbolic ("concolic") analysis, making it applicable to a variety of tasks

???

???

Jonas Zaddach

Luca Bruno

http://www.s3.eurecom.fr/tools/avatar/

S²E

Avatar is an event-based arbitration framework that orchestrates the communication between an emulator and a target physical device. Avatar's goal is to enable complex dynamic analysis of embedded firmware in order to assist in a wide range of security-related activities including (but not limited to) reverse engineering, malware analysis, vulnerability discovery, vulnerability assessment, backtrace acquisition and root-cause analysis of known test cases.

???

???

pySMT

https://github.com/pysmt/pysmt

pySMT: A library for SMT formulae manipulation and solving http://www.pysmt.org

???

???

feliam

https://github.com/feliam/pysmtlib

Z3

A python layer to interface with several SMTLIBv2 enabled SMT solvers.

???

???

Jonathan Salwan

https://github.com/JonathanSalwan/Triton

PIN

Triton is 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 instructions into the SMT2-LIB representation, a Z3 interface to solve constraints and Python bindings.

???

Code coverage using a dynamic symbolic execution
Dynamic Binary Analysis and Obfuscated Codes

Sascha Böhme

http://www4.in.tum.de/~boehmes/z3-python.html

Z3

This is a Python binding to the SMT solver Z3. Since it is based on Python's dynamic foreign function interface ctypes, no compilation is required. Z3 is a high-performance theorem prover being developed at Microsoft Research. Z3 supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, SAGE, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.

???

site Z3

Microsoft Research

http://research.microsoft.com/en-us/um/redmond/projects/z3/

Z3

Python interface for Z3. It covers all main features in the Z3 API. Z3 is a high-performance theorem prover being developed at Microsoft Research.

SEA
BARF
look_for_gadgets_with_equations.py
rop_compiler

guide