Dynamic Binary Analysis Tool: Manticore

ID N0WHERE:171569
Type n0where
Reporter N0where
Modified 2018-09-02T05:52:53


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?


  • 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)


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.

Dynamic Binary Analysis Tool: Manticore Wiki

Dynamic Binary Analysis Tool: Manticore Downlaod