Manticore

0.3.7 verified Sat May 09 auth: no python

Manticore is a symbolic execution tool for analysis of binaries and smart contracts. Current version 0.3.7 (2022-10-06), released by Trail of Bits. Active development with major refactors in 0.3.x; Ethereum features use crytic-compile.

pip install manticore

Common errors

error ImportError: cannot import name 'Manticore' from 'manticore' ↓

cause Old import path used before 0.3.0 rewrites.

fix

Use 'from manticore import Manticore' for the top-level class.

error ModuleNotFoundError: No module named 'crytic_compile' ↓

cause Missing crytic-compile dependency for Ethereum analysis.

fix

pip install crytic-compile, or reinstall manticore with pip install manticore[evm]

error OSError: libunicorn.so.1: cannot open shared object file ↓

cause Missing Unicorn emulator library for native binary analysis.

fix

Install Unicorn engine: pip install unicorn, or on Ubuntu: apt-get install libunicorn-dev

Warnings

breaking Manticore 0.3.0+ requires Python >=3.7 and rewrites the executor API. Old scripts using manticore.core.xxx will break. ↓

fix Replace 'manticore.core.xxx' with 'manticore.xxx' as per new API.

deprecated The old Ethereum API (ManticoreEVM) is deprecated in favor of EthereumManticore (import from manticore.ethereum). ↓

fix Use 'from manticore.ethereum import EthereumManticore' instead.

gotcha Manticore may hang or crash in multiprocessing mode due to Z3 SMT solver issues. Use single process (m = Manticore(procs=1)) for troubleshooting. ↓

fix Set procs=1 in Manticore constructor.

Install

pip install manticore[native]

Imports

Manticore

wrong

from manticore.core import Manticore

correct

from manticore import Manticore

Old import path from <0.3.0

EthereumManticore

wrong

from manticore import EthereumManticore

correct

from manticore.ethereum import EthereumManticore

Common mistake

ManticoreBase

wrong

from manticore import ManticoreBase

correct

from manticore.core.smtlib import ManticoreBase

Not top-level

Quickstart

Basic native binary symbolic execution. For Ethereum, use EthereumManticore.

from manticore import Manticore

m = Manticore('/bin/ls')
m.run()
for state in m.running_states:
    print(state.solve_one())