Manticore : Symbolic Execution Tool

Manticore is a symbolic execution tool for analysis of binaries and smart contracts. Beginning with version 0.2.0, Python 3.6+ is required.

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

Also ReadInvisi-Shell : Hide Your Powershell Script In Plain Sight(Bypass all Powershell security features)

Usage

CLI

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. Manticore includes detectors that flag potentially vulnerable code in discovered states. Solidity smart contracts must have a .sol extension for analysis by Manticore.

$ manticore ./path/to/contract.sol  # runs, and creates a mcore_* directory with analysis results
$ manticore --detect-reentrancy ./path/to/contract.sol  # Above, but with reentrancy detection enabled
$ manticore --detect-all ./path/to/contract.sol  # Above, but with all detectors enabled

The command line can also be used to simply explore a Linux binary:

$ 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

API

Manticore has a Python programming interface which can be used to implement custom analyses.

For Ethereum smart contracts, it can be used for detailed verification of arbitrary contract properties. Set starting conditions, execute symbolic transactions, then review discovered states to ensure invariants for your contract hold.

from manticore.ethereum import ManticoreEVM
contract_src="""
contract Adder {
    function incremented(uint value) public returns (uint){
        if (value == 1)
            revert();
        return value + 1;
    }
}
"""
m = ManticoreEVM()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(contract_src,
                                              owner=user_account,
                                              balance=0)
value = m.make_symbolic_value()

contract_account.incremented(value)

for state in m.running_states:
    print("can value be 1? {}".format(state.can_be_true(value == 1)))
    print("can value be 200? {}".format(state.can_be_true(value == 200)))

It is also possible to use the API to create custom analysis tools for Linux binaries.

# example Manticore script
from manticore import Manticore

hook_pc = 0x400ca0

m = Manticore('./path/to/binary')

@m.hook(hook_pc)
def hook(state):
  cpu = state.cpu
  print('eax', cpu.EAX)
  print(cpu.read_int(cpu.ESP))

  m.terminate()  # tell Manticore to stop

m.run()

Quickstart

Install and try Manticore in a few shell commands:

# Install system dependencies
sudo apt-get update && sudo apt-get install python3 python3-pip -y

# Install Manticore and its dependencies
sudo pip3 install manticore

# Download the examples
git clone https://github.com/trailofbits/manticore.git && cd manticore/examples/linux

# Build the examples
make

# Use the Manticore CLI
manticore basic
cat mcore_*/*0.stdin | ./basic
cat mcore_*/*1.stdin | ./basic

# Use the Manticore API
cd ../script
python3 count_instructions.py ../linux/helloworld

You can also use Docker to quickly install and try Manticore:

# Run container with a shared examples/ directory
# Note that `--rm` will make the container be deleted if you exit it
# (if you want to persist data from the container, use docker volumes)
$ docker run --rm -it trailofbits/manticore bash

# Change to examples directory
manticore@8d456f662d0f:~$ cd manticore/examples/linux/

# Build the examples
manticore@8d456f662d0f:~/manticore/examples/linux$ make

# Use the Manticore CLI
manticore@8d456f662d0f:~/manticore/examples/linux$ manticore basic


manticore@8d456f662d0f:~/manticore/examples/linux$ cat mcore_*/*0.stdin | ./basic
manticore@8d456f662d0f:~/manticore/examples/linux$ cat mcore_*/*1.stdin | ./basic

# Use the Manticore API
manticore@8d456f662d0f:~/manticore/examples/linux$ cd ../script
manticore@8d456f662d0f:~/manticore/examples/script$ python3 count_instructions.py ../linux/helloworld

Installation

NOTE: If you use Mac OS X you 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

Option 1: Perform a user install (requires ~/.local/bin in your PATH).

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

Option 2: Use a virtual environment.

sudo pip3 install virtualenvwrapper
echo "source /usr/local/bin/virtualenvwrapper.sh" >> ~/.profile
source ~/.profile
mkvirtualenv manticore
sudo ./manticore/bin/pip3 install manticore

Option 3: Perform a system install.

sudo pip3 install manticore

Option 4: Install via Docker.

docker pull trailofbits/manticore

Once installed, the manticore CLI tool and Python API will be available.

You can follow us on LinkedinTwitterFacebook for daily Cybersecurity updates also you can take the Best Cybersecurity courses online to keep your self-updated.

R K

Recent Posts

Bash Arrays Explained Simply: Beginner’s Guide with Examples

If you’re learning Bash scripting, one of the most useful features you’ll come across is…

11 hours ago

Bash For Loop Examples Explained Simply for Beginners

If you are new to Bash scripting or Linux shell scripting, one of the most…

22 hours ago

How Does a Firewall Work Step by Step

How Does a Firewall Work Step by Step? What Is a Firewall and How Does…

2 days ago

ROADTools: The Modern Azure AD Exploration Framework

ROADTools is a powerful framework designed for exploring and interacting with Microsoft Azure Active Directory…

6 days ago

How to Enumerate Microsoft 365 Groups Using PowerShell and Python

Microsoft 365 Groups (also known as M365 Groups or Unified Groups) are at the heart…

6 days ago

SeamlessPass: Using Kerberos Tickets to Access Microsoft 365

SeamlessPass is a specialized tool designed to leverage on-premises Active Directory Kerberos tickets to obtain…

7 days ago