Symbolic Execution Tool – Manticore

Last Release: 06/06/2019     Last Commit: 06/18/2019

Symbolic Execution Tool – Manticore

Introduction

Manticore is a prototyping tool for dynamic binary analysis, with support for symbolic execution, taint analysis, and binary instrumentation. It comes with easy-to-use CLI (Command Line Tool) which allows you to quickly generate new program test cases with symbolic execution.

Manticore Logo

Manticore: Symbolic Execution Tool for Binary Analysis and Smart Contracts

Manticore is a symbolic execution tool with command line interface which can be used to easily symbolically execute a supported program/smart contract. It’s capable of input generation, crash discovery, execution tracing and has a programmatic interface (via a Python API). In addition, it can also analyse Ethereum smart contracts (EVM bytecode) and Linux ELF binaries (x86, x86_64 and ARMv7).

Features:

  • Automatically generates inputs that trigger unique code paths
  • Discovers inputs that crash programs via memory safety violations
  • Records an instruction-level trace of execution for each generated input
  • Exposes programmatic access to its analysis engine via a Python API

Requirements:

  • Python 3.6+
  • Ubuntu 18.04 (recommended)
  • solc program in your $PATH (for Ethereum smart contract analysis)

Manticore Install

Linux

First you’ll need to install dependencies:

$ sudo apt-get update && sudo apt-get install python3 python3-pip -y

Then grab the Manticore and install its dependencies:

$ git clone https://github.com/trailofbits/manticore.git && cd manticore/examples/linux
$ sudo pip3 install manticore

To build the examples run:

$ make

Installation via Docker

Run container with a shared examples/directory:

$ docker run --rm -it trailofbits/manticore bash
Note: --rm will make the container be deleted if you exit it (if you want to persa from the container, use docker volumes).

Change the example directory, run:

$ cd manticore/examples/linux/

To build the examples:

$ make

Mac OS X

Mac OS X users need to install dependencies manually (preferably in a manticore’s python virtual environment):

$ brew install capstone
$ export MACOS_UNIVERSAL=no && pip install capstone

$ brew install unicorn
$ UNICORN_QEMU_FLAGS="--python=`whereis python`" pip install unicorn

1. User install:

Requires ~/.local/bin in your PATH:

$ echo "PATH=\$PATH:~/.local/bin" >> ~/.profile
$ source ~/.profile
$ pip3 install --user manticore

2. System install:

$ sudo pip3 install manticore

3. Docker install:

$ docker pull trailofbits/manticore

Usage

Manticore has a command line interface which can be used to easily symbolically execute a supported program or smart contract. Analysis results will be placed into a new directory beginning with mcore_Use the CLI to explore possible states in Ethereum smart contracts. This solidity analyzing tool includes detectors that flag potentially vulnerable code in discovered states. Solidity smart contracts must have a .sol extension for Manticore analysis.

To use the Manticore CLI, run:

$ manticore basic
$ cat mcore_*/*0.stdin | ./basic
$ cat mcore_*/*1.stdin | ./basic

Manticore CLI Usage Example

It also has a Python programming interface which you can use to implement custom analyses. For Ethereum smart contracts, you can use it for detailed verification of arbitrary contract properties.

To use the Manticore API, run:

$ cd ../script
$ python3 count_instructions.py ../linux/helloworld
Documentation Box
Download Box