Manticore is a symbolic execution tool for analysis of binaries and smart contracts.
Manticore is a symbolic execution tool for analysis of smart contracts and binaries.
Manticore can analyze the following types of programs:
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.
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.
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.
$ 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
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
$ 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
Manticore provides a Python programming interface which can be used to implement powerful custom analyses.
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.
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)))
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.
# 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()
Manticore can also evaluate WebAssembly functions over symbolic inputs for property validation or general analysis.
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])
ulimit -s 100000 or by passing --ulimit stack=100000000:100000000 to docker runsolc program in your $PATH.crytic-compile on your code directly to make it easier to identify any issues.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
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
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
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.
Manticore is licensed and distributed under the AGPLv3 license. Contact us if you're looking for an exception to the terms.
If you are using Manticore on an academic work, consider applying to the Crytic $10k Research Prize.
FAQs
Manticore is a symbolic execution tool for analysis of binaries and smart contracts.
We found that manticore demonstrated a healthy version release cadence and project activity because the last version was released less than a year ago. It has 2 open source maintainers collaborating on the project.
Did you know?
Socket for GitHub automatically highlights issues in each pull request and monitors the health of all your open source dependencies. Discover the contents of your packages and block harmful activity before you install or update your dependencies.
Security News
PyPI confirms no security flaws were exploited in the Ultralytics supply chain attack and highlights improvements for safer package publishing.
Security News
Research
The Socket Research Team breaks down a malicious wrapper package that uses obfuscation to harvest credentials and exfiltrate sensitive data.
Research
Security News
Attackers used a malicious npm package typosquatting a popular ESLint plugin to steal sensitive data, execute commands, and exploit developer systems.