Dynamic Binary Analysis Tool
Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
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 supports binaries of the following formats, operating systems, and architectures. It has been primarily used on binaries compiled from C and C++.
OS/Formats: Linux ELF, Windows Minidump
Architectures: x86, x86_64, ARMv7 (partial)
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.
Quick Start
Install and try Manticore in a few shell commands (see an asciinema):
# Install system dependencies
sudo apt-get update && sudo apt-get install z3 python-pip -y
python -m pip install -U pip
# Install manticore and its dependencies
git clone https://github.com/trailofbits/manticore.git && cd manticore
sudo pip install --no-binary capstone .
# Build the examples
cd examples/linux
make
# Use the Manticore CLI
manticore basic
cat mcore_*/*1.stdin | ./basic
cat mcore_*/*2.stdin | ./basic
# Use the Manticore API
cd ../script
python count_instructions.py ../linux/helloworld
Installation
Make sure that Z3 is installed and available on your PATH. On Ubuntu, this is as simple as sudo apt-get install z3.
Option 1: Perform a user install (requires ~/.local/bin in your PATH).
echo "PATH=\$PATH:~/.local/bin" >> ~/.profile
source ~/.profile
git clone https://github.com/trailofbits/manticore.git && cd manticore
pip install --user --no-binary capstone .
Option 2: Use a virtual environment (requires virtualenvwrapper or similar).
pip install virtualenvwrapper
echo "source /usr/local/bin/virtualenvwrapper.sh" >> ~/.profile
source ~/.profile
git clone https://github.com/trailofbits/manticore.git && cd manticore
mkvirtualenv manticore
pip install --no-binary capstone .
Option 3: Perform a system install.
git clone https://github.com/trailofbits/manticore.git && cd manticore
sudo pip install --no-binary capstone .
Once installed, the manticore CLI tool and its Python API will be available.
Usage
$ manticore ./path/to/binary # runs, and creates a mcore_* directory with analysis results
Docs
Download
Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation.
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 supports binaries of the following formats, operating systems, and architectures. It has been primarily used on binaries compiled from C and C++.
OS/Formats: Linux ELF, Windows Minidump
Architectures: x86, x86_64, ARMv7 (partial)
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.
Quick Start
Install and try Manticore in a few shell commands (see an asciinema):
# Install system dependencies
sudo apt-get update && sudo apt-get install z3 python-pip -y
python -m pip install -U pip
# Install manticore and its dependencies
git clone https://github.com/trailofbits/manticore.git && cd manticore
sudo pip install --no-binary capstone .
# Build the examples
cd examples/linux
make
# Use the Manticore CLI
manticore basic
cat mcore_*/*1.stdin | ./basic
cat mcore_*/*2.stdin | ./basic
# Use the Manticore API
cd ../script
python count_instructions.py ../linux/helloworld
Installation
Make sure that Z3 is installed and available on your PATH. On Ubuntu, this is as simple as sudo apt-get install z3.
Option 1: Perform a user install (requires ~/.local/bin in your PATH).
echo "PATH=\$PATH:~/.local/bin" >> ~/.profile
source ~/.profile
git clone https://github.com/trailofbits/manticore.git && cd manticore
pip install --user --no-binary capstone .
Option 2: Use a virtual environment (requires virtualenvwrapper or similar).
pip install virtualenvwrapper
echo "source /usr/local/bin/virtualenvwrapper.sh" >> ~/.profile
source ~/.profile
git clone https://github.com/trailofbits/manticore.git && cd manticore
mkvirtualenv manticore
pip install --no-binary capstone .
Option 3: Perform a system install.
git clone https://github.com/trailofbits/manticore.git && cd manticore
sudo pip install --no-binary capstone .
Once installed, the manticore CLI tool and its Python API will be available.
Usage
$ manticore ./path/to/binary # runs, and creates a mcore_* directory with analysis results
Docs
Download