Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
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.
