Manticore – Dynamic Binary Analysis Tool

Manticore comes with an easy-to-use command line tool that quickly generates new program “test cases” (or sample inputs) with symbolic execution. Each test case results in a unique outcome when running the program, like a normal process exit or crash (e.g., invalid program counter, invalid memory read/write).

The command line tool satisfies some use cases, but practical use requires more flexibility. That’s why we created a Python API for custom analyses and application-specific optimizations. Manticore’s expressive and scriptable Python API can help you answer questions like:

• At point X in execution, is it possible for variable Y to be a specified value?
• Can the program reach this code at runtime?
• What is a program input that will cause execution of this code?
• Is user input ever used as a parameter to this libc function?
• How many times does the program execute this function?
• How many instructions does the program execute if given this input?

Features

• Input Generation: Manticore automatically generates inputs that trigger unique code paths
• Crash Discovery: Manticore discovers inputs that crash programs via memory safety violations
• Execution Tracing: Manticore records an instruction-level trace of execution for each generated input
• Programmatic Interface: Manticore exposes programmatic access to its analysis engine via a Python API

Manticore can analyze the following types of programs:

• Ethereum smart contracts (EVM bytecode)
• Linux ELF binaries (x86, x86_64 and ARMv7)

Requirements

Manticore is supported on Linux and requires Python 2.7, pip 7.1.0 or higher, and the Z3 Theorem Prover. Ubuntu 16.04 is strongly recommended.