Symbolic execution tool for analysis of binaries and smart contracts.
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
Usage:-
$ manticore ./path/to/binary # runs, and creates a mcore_* directory with analysis results
$ manticore ./path/to/binary ab cd # use concrete strings "ab", "cd" as program arguments
$ manticore ./path/to/binary ++ ++ # use two symbolic strings of length two as program arguments
$ manticore ./path/to/contract.sol # runs, and creates a mcore_* directory with analysis results