Pre-release

This release is a pre-release and may not be stable for production use.

Manticore

Manticore is a symbolic execution tool for analysis of smart contracts and binaries.

Features

Program Exploration: Manticore can execute a program with symbolic inputs and explore all the possible states it can reach
Input Generation: Manticore can automatically produce concrete inputs that result in a given program state
Error Discovery: Manticore can detect crashes and other failure cases in binaries and smart contracts
Instrumentation: Manticore provides fine-grained control of state exploration via event callbacks and instruction hooks
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, aarch64, and ARMv7)
WASM Modules

Installation

Note: We recommend installing Manticore in a virtual environment to prevent conflicts with other projects or packages

Option 1: Installing from PyPI:

pip install manticore

Option 2: Installing from PyPI, with extra dependencies needed to execute native binaries:

pip install "manticore[native]"

Option 3: Installing a nightly development build:

pip install --pre "manticore[native]"

Option 4: Installing from the master branch:

git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"

Option 5: Install via Docker:

docker pull trailofbits/manticore

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

For a development installation, see our wiki.

Usage

CLI

Manticore has a command line interface which can perform a basic symbolic analysis of a binary or smart contract. Analysis results will be placed into a workspace directory beginning with mcore_. For information about the workspace, see the wiki.

EVM

Manticore CLI automatically detects you are trying to test a contract if (for ex.) the contract has a .sol or a .vy extension. See a demo.

Click to expand:

$ manticore examples/evm/umd_example.sol 
 [9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
 [9921] m.e.manticore:INFO: Starting symbolic create contract
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 0
 [9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 1
 [9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx

Manticore-verifier

An alternative CLI tool is provided that simplifys contract testing and allows writing properties methods in the same high-level language the contract uses. Checkout manticore-verifier documentation. See a demo

Native

Click to expand:

$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973

API

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

EVM

For Ethereum smart contracts, the API can be used for detailed verification of arbitrary contract properties. Users can set the starting conditions, execute symbolic transactions, then review discovered states to ensure invariants for a contract hold.

Click to expand:

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=10000000)
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.ready_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)))

Native

It is also possible to use the API to create custom analysis tools for Linux binaries. Tailoring the initial state helps avoid state explosion problems that commonly occur when using the CLI.

Click to expand:

# example Manticore script
from manticore.native import Manticore

m = Manticore.linux('./example')

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

  m.kill()  # tell Manticore to stop

m.run()

WASM

Manticore can also evaluate WebAssembly functions over symbolic inputs for property validation or general analysis.

Click to expand:

from manticore.wasm import ManticoreWASM

m = ManticoreWASM("collatz.wasm")

def arg_gen(state):
    # Generate a symbolic argument to pass to the collatz function.
    # Possible values: 4, 6, 8
    arg = state.new_symbolic_value(32, "collatz_arg")
    state.constrain(arg > 3)
    state.constrain(arg < 9)
    state.constrain(arg % 2 == 0)
    return [arg]


# Run the collatz function with the given argument generator.
m.collatz(arg_gen)

# Manually collect return values
# Prints 2, 3, 8
for idx, val_list in enumerate(m.collect_returns()):
    print("State", idx, "::", val_list[0])

Requirements

Manticore requires Python 3.7 or greater
Manticore officially supports the latest LTS version of Ubuntu provided by Github Actions
- Manticore has experimental support for EVM and WASM (but not native Linux binaries) on MacOS
We recommend running with increased stack size. This can be done by running ulimit -s 100000 or by passing --ulimit stack=100000000:100000000 to docker run

Compiling Smart Contracts

Ethereum smart contract analysis requires the solc program in your $PATH.
Manticore uses crytic-compile to build smart contracts. If you're having compilation issues, consider running crytic-compile on your code directly to make it easier to identify any issues.
We're still in the process of implementing full support for the EVM Istanbul instruction semantics, so certain opcodes may not be supported. In a pinch, you can try compiling with Solidity 0.4.x to avoid generating those instructions.

Using a different solver (Yices, Z3, CVC4)

Manticore relies on an external solver supporting smtlib2. Currently Z3, Yices and CVC4 are supported and can be selected via commandline or configuration settings. If Yices is available, Manticore will use it by default. If not, it will fall back to Z3 or CVC4. If you want to manually choose which solver to use, you can do so like this: manticore --smt.solver Z3

Installing CVC4

For more details go to https://cvc4.github.io/. Otherwise just get the binary and use it.

    sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
    sudo chmod +x /usr/bin/cvc4

Installing Yices

Yices is incredibly fast. More details here https://yices.csl.sri.com/

    sudo add-apt-repository ppa:sri-csl/formal-methods
    sudo apt-get update
    sudo apt-get install yices2

Getting Help

Feel free to stop by our #manticore slack channel in Empire Hacking for help using or extending Manticore.

Documentation is available in several places:

The wiki contains information about getting started with Manticore and contributing
The API reference has more thorough and in-depth documentation on our API
The examples directory has some small examples that showcase API features
The manticore-examples repository has some more involved examples, including some real CTF problems

If you'd like to file a bug report or feature request, please use our issues page.

For questions and clarifications, please visit the discussion page.

License

Manticore is licensed and distributed under the AGPLv3 license. Contact us if you're looking for an exception to the terms.

Publications

Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts, Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg - ASE 19

If you are using Manticore on an academic work, consider applying to the Crytic $10k Research Prize.

Demo Video from ASE 2019

Metadata

Release files for manticore 0.3.7.dev220121

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for manticore 0.3.7.dev220121
File	Size	Uploaded	Provenance
manticore-0.3.7.dev220121.tar.gz	381.2 kB	Jan 21, 2022	Without provenance	Details

Built distribution (wheel)

Table of built distributions (wheels) for manticore 0.3.7.dev220121
File	Interpreter	ABI	Platform	Reset
manticore-0.3.7.dev220121-py3-none-any.whl 416.6 kB Jan 21, 2022 Without provenance	Python 3	none	any	Details

Total release size: 797.9 kB

Release files / manticore-0.3.7.dev220121.tar.gz

Download URL	manticore-0.3.7.dev220121.tar.gz
Size	381.2 kB
Tags	Source
SHA-256 checksum How to use checksums	`7a1e55f8f64e962ce4da2b572718d6f22c1ec79c49453179d94ffd79984772ea`
BLAKE2b-256 checksum How to use checksums	`78f473c6ad276d0de7060fc9a7ebbae95407b3f0601c689270691740af662ecc`
Upload date	Jan 21, 2022
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`twine/3.7.1 importlib_metadata/4.10.1 pkginfo/1.8.2 requests/2.27.1 requests-toolbelt/0.9.1 tqdm/4.62.3 CPython/3.8.12`

Release files / manticore-0.3.7.dev220121-py3-none-any.whl

Download URL	manticore-0.3.7.dev220121-py3-none-any.whl
Size	416.6 kB
Tags	Python 3
SHA-256 checksum How to use checksums	`9127edcd5f08f7e57e8d25723b0ca61d602d5089d5e71a5c5acc4c4a3ade31d3`
BLAKE2b-256 checksum How to use checksums	`64accd29f5a22c2f8f71b3e66c8f7df234a5729721ad57e1ab197fa82ea56578`
Upload date	Jan 21, 2022
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`twine/3.7.1 importlib_metadata/4.10.1 pkginfo/1.8.2 requests/2.27.1 requests-toolbelt/0.9.1 tqdm/4.62.3 CPython/3.8.12`

Security for manticore 0.3.7.dev220121

Report project as malware

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.