manticore

Symbolic execution tool

https://github.com/trailofbits/manticore

Science Score: 64.0%

This score indicates how likely this project is to be science-related based on various indicators:

✓
CITATION.cff file
Found CITATION.cff file
✓
codemeta.json file
Found codemeta.json file
✓
.zenodo.json file
Found .zenodo.json file
○
DOI references
✓
Academic publication links
Links to: arxiv.org
✓
Committers with academic emails
8 of 99 committers (8.1%) from academic institutions
○
Institutional organization owner
○
JOSS paper metadata
○
Scientific vocabulary similarity
Low similarity (18.0%) to scientific vocabulary

Keywords

binary-analysis blockchain emulation ethereum program-analysis python security smt symbolic-execution testing z3

Keywords from Contributors

academic-papers conference-presentations security-reviews solidity vulnerability-detection distribution sequences interactive optim fake

Last synced: 4 months ago · JSON representation ·

Repository

Symbolic execution tool

Basic Info

Host: GitHub
Owner: trailofbits
License: agpl-3.0
Language: Python
Default Branch: master
Homepage: https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/
Size: 43.5 MB

Statistics

Stars: 3,783
Watchers: 128
Forks: 481
Open Issues: 272
Releases: 19

Topics

binary-analysis blockchain emulation ethereum program-analysis python security smt symbolic-execution testing z3

Created almost 9 years ago · Last pushed 4 months ago

Metadata Files

Readme Changelog Contributing License Citation Codeowners

:warning: Project is in Maintenance Mode :warning:

This project is no longer internally developed and maintained. However, we are happy to review and accept small, well-written pull requests by the community. We will only consider bug fixes and minor enhancements.

Any new or currently open issues and discussions shall be answered and supported by the community.

Manticore

Manticore is a symbolic execution tool for the 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:

bash pip install manticore

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

bash pip install "manticore[native]"

Option 3: Installing a nightly development build:

bash pip install --pre "manticore[native]"

Option 4: Installing from the master branch:

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

Option 5: Install via Docker:

bash 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:

bash $ 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 simplifies 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:

```bash $ 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, and then review discovered states to ensure invariants for a contract hold.

Click to expand:

```python 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()

useraccount = m.createaccount(balance=10000000) contractaccount = m.soliditycreatecontract(contractsrc, owner=useraccount, balance=0) value = m.makesymbolic_value()

contract_account.incremented(value)

for state in m.readystates: print("can value be 1? {}".format(state.canbetrue(value == 1))) print("can value be 200? {}".format(state.canbe_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:

```python # 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:

```python 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 command-line 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 in academic work, consider applying to the Crytic $10k Research Prize.

Demo Video from ASE 2019

Tool Integrations

MATE: Merged Analysis To prevent Exploits
- Mantiserve: REST API interaction with Manticore to start, kill, and check Manticore instance
- Dwarfcore: Plugins and detectors for use within Mantiserve engine during exploration
- Under-constrained symbolic execution Interface for symbolically exploring single functions with Manticore

Owner

Name: Trail of Bits
Login: trailofbits
Kind: organization
Email: opensource@trailofbits.com
Location: New York, New York

Website: https://www.trailofbits.com
Twitter: trailofbits
Repositories: 125
Profile: https://github.com/trailofbits

More code: binary lifters @lifting-bits, blockchain @crytic, forks @trail-of-forks

Citation (CITATION.cff)

# YAML 1.2
---
abstract: "An effective way to maximize code coverage in software tests is through dynamic symbolic execution-a technique that uses constraint solving to systematically explore a program's state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients."
authors: 
  -
    affiliation: "Trail of Bits"
    family-names: Mossberg
    given-names: Mark
  -
    affiliation: "Trail of Bits"
    family-names: Manzano
    given-names: Felipe
  -
    affiliation: "Trail of Bits"
    family-names: Hennenfent
    given-names: Eric
  -
    affiliation: "Trail of Bits"
    family-names: Groce
    given-names: Alex
  -
    affiliation: "Trail of Bits"
    family-names: Greico
    given-names: Gustavo
  -
    affiliation: "Trail of Bits"
    family-names: Feist
    given-names: Josselin
  -
    affiliation: "Trail of Bits"
    family-names: Brunson
    given-names: Trent
  -
    affiliation: "Trail of Bits"
    family-names: Dinaburg
    given-names: Artem
cff-version: "1.1.0"
date-released: 2019-11-11
doi: "10.1109/ASE.2019.00133"
keywords: 
  - "symbolic execution"
  - "binary analysis"
  - ethereum
license: "AGPL-3.0"
message: "If you use this software in an academic work, please cite our paper."
repository-code: "https://github.com/trailofbits/manticore"
title: "Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts"
...

GitHub Events

Total

Issues event: 8
Watch event: 108
Delete event: 23
Issue comment event: 5
Push event: 46
Pull request review event: 3
Pull request review comment event: 3
Pull request event: 17
Fork event: 17
Create event: 8

Last Year

Issues event: 8
Watch event: 108
Delete event: 23
Issue comment event: 5
Push event: 46
Pull request review event: 3
Pull request review comment event: 3
Pull request event: 17
Fork event: 17
Create event: 8

Committers

Last synced: 8 months ago

All Time

Total Commits: 1,094
Total Committers: 99
Avg Commits per committer: 11.051
Development Distribution Score (DDS): 0.814

Past Year

Commits: 0
Committers: 0
Avg Commits per committer: 0.0
Development Distribution Score (DDS): 0.0

Top Committers

Name	Email	Commits
Mark Mossberg	m**g@g**m	204
feliam	f**o@g**m	137
Disconnect3d	d**a@g**m	79
Eric Kilmer	e**r@g**m	69
Yan	y****n	68
Eric Hennenfent	e**t@t**m	67
JP Smith	j**h@i**u	60
ggrieco-tob	3****b	31
defunct	d**t@d**o	26
Samuel E. Moelius	3****s	20
kokrui	k**g@g**m	20
Catena cyber	3****r	19
Brad Larsen	b**n@t**m	18
Nikita Karetnikov	n**a@k**g	17
Paul Kehrer	p**r@g**m	15
Dan Guido	d**n@t**m	14
Feist Josselin	j**n@t**m	12
Theofilos Petsios	t**s@c**u	11
dependabot[bot]	4****]	10
Alex A	n**r@h**r	9
Eric Hennenfent	e**e@g**m	9
Boyan MILANOV	b**v@t**m	9
Srinivas P G	s**9@n**u	9
Arun John Kuruvilla	a**a@g**m	8
sschriner	6****r	8
Alan	e**s@c**h	7
Stephan Tolksdorf	st@q****m	7
Pierre Pronchery	k**n@d**g	6
Garret Reece	G****e	6
William Woodruff	w**m@t**m	6
and 69 more...

Committer Domains (Top 20 + Academic)

trailofbits.com: 6 nyu.edu: 2 ilstu.edu: 1 defunct.io: 1 karetnikov.org: 1 cs.columbia.edu: 1 codemuch.tech: 1 quanttec.com: 1 defora.org: 1 samuel-gross.com: 1 sultanik.com: 1 onicsla.bz: 1 watson.org: 1 sobolevn.me: 1 dinaburg.org: 1 devtty1er.com: 1 mimisbrunnr.net: 1 iress.com: 1 xternet.dev: 1 sjtu.edu.cn: 1 imsa.edu: 1 kth.se: 1 imperial.ac.uk: 1

Issues and Pull Requests

Last synced: 7 months ago

All Time

Total issues: 42
Total pull requests: 83
Average time to close issues: 29 days
Average time to close pull requests: 25 days
Total issue authors: 31
Total pull request authors: 19
Average comments per issue: 3.43
Average comments per pull request: 0.92
Merged pull requests: 48
Bot issues: 0
Bot pull requests: 33

Past Year

Issues: 10
Pull requests: 1
Average time to close issues: N/A
Average time to close pull requests: N/A
Issue authors: 1
Pull request authors: 1
Average comments per issue: 0.0
Average comments per pull request: 2.0
Merged pull requests: 0
Bot issues: 0
Bot pull requests: 0

View more stats

Top Authors

Issue Authors

sam-xif (9)
dguido (6)
ekilmer (2)
PavanKumarChaparla (2)
teknogeek (1)
gsalzer (1)
krypston104 (1)
0-wiz-0 (1)
Pet3ris (1)
anhdungle93 (1)
christiankakesa (1)
patelvishal1401 (1)
Lokizzle (1)
anudit (1)
SunBeomSo (1)

Pull Request Authors

dependabot[bot] (38)
ekilmer (17)
ehennenfent (7)
feliam (5)
sschriner (5)
Yustynn (2)
gustavo-grieco (2)
wolflo (2)
Boyan-MILANOV (1)
xternet (1)
artemdinaburg (1)
zarifpour (1)
PavanKumarChaparla (1)
omahs (1)
montyly (1)

Top Labels

Issue Labels

bug (35) idea (2) help wanted (2) good first issue (2) Hacktoberfest (1) ethereum (1)

Pull Request Labels

dependencies (38) github_actions (5) native models (2) api (1) ux (1) ci (1) ethereum (1)

Packages

Total packages: 1
Total downloads:
- pypi 36,234 last-month
Total docker downloads: 38

Total dependent packages: 1
Total dependent repositories: 23
Total versions: 1,222
Total maintainers: 2

pypi.org: manticore

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

Homepage: https://github.com/trailofbits/manticore
Documentation: https://manticore.readthedocs.io/
License: GNU Affero General Public License v3
Latest release: 0.3.7
published almost 4 years ago

Versions: 1,222
Dependent Packages: 1
Dependent Repositories: 23
Downloads: 36,234 Last month
Docker Downloads: 38

Rankings

Stargazers count: 1.3%

Forks count: 2.4%

Dependent repos count: 3.0%

Average: 3.0%

Downloads: 3.1%

Docker downloads count: 3.7%

Dependent packages count: 4.8%

Maintainers (2)

trailofbits disconnect3d_tob

Last synced: 12 months ago

Dependencies

docs/requirements.txt pypi

Sphinx ==4.3.0

setup.py pypi

crytic-compile >=0.2.2
dataclasses *
evm *
intervaltree *
ply *
prettytable *
protobuf *
pyevmasm >=0.2.3
pysha3 *
pyyaml *
rlp *
wasm *

.github/workflows/ci.yml actions

actions/checkout v3 composite
actions/setup-node v3 composite
actions/setup-python v4 composite
coverallsapp/github-action 1.1.3 composite
pypa/gh-action-pypi-publish v1.6.4 composite

.github/workflows/osx.yml actions

actions/checkout v3 composite
actions/setup-node v3 composite
actions/setup-python v4 composite

.github/workflows/pip-audit.yml actions

actions/checkout v3 composite
actions/setup-python v4 composite
pypa/gh-action-pip-audit v1.0.4 composite

.github/workflows/release.yml actions

actions/checkout v3 composite
actions/setup-node v3 composite
actions/setup-python v4 composite
pypa/gh-action-pypi-publish v1.6.4 composite

Dockerfile docker

ubuntu 20.04 build

server/setup.py pypi

manticore *

manticore

Science Score: 64.0%

Keywords

Keywords from Contributors

Repository

Basic Info

Statistics

Topics

Metadata Files

README.md

:warning: Project is in Maintenance Mode :warning:

Manticore

Features

Installation

Usage

CLI

EVM

Manticore-verifier

Native

API

EVM

Native

WASM

Requirements

Compiling Smart Contracts

Using a different solver (Yices, Z3, CVC4)

Installing CVC4

Installing Yices

Getting Help

License

Publications

Demo Video from ASE 2019

Tool Integrations

Owner

Citation (CITATION.cff)

GitHub Events

Total

Last Year

Committers

All Time

Past Year

Top Committers

Committer Domains (Top 20 + Academic)

Issues and Pull Requests

All Time

Past Year

Top Authors

Issue Authors

Pull Request Authors

Top Labels

Issue Labels

Pull Request Labels

Packages

pypi.org: manticore

Rankings

Maintainers (2)

Dependencies