How to use Manticore to find bugs in smart contracts
The aim of this tutorial is to show how to use Manticore to automatically find bugs in smart contracts.
Installation
Manticore requires >= python 3.6. It can be installed through pip or using docker.
Manticore through docker
docker pull trailofbits/eth-security-toolboxdocker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox
The last command runs eth-security-toolbox in a docker that has access to your current directory. You can change the files from your host, and run the tools on the files from the docker
Inside docker, run:
solc-select 0.5.11cd /home/trufflecon/
Manticore through pip
pip3 install --user manticore
solc 0.5.11 is recommended.
Running a script
To run a python script with python 3:
python3 script.py
Introduction to dynamic symbolic execution
Dynamic Symbolic Execution in a Nutshell
Dynamic symbolic execution (DSE) is a program analysis technique that explores a state space with a high degree of semantic awareness. This technique is based on the discovery of "program paths", represented as mathematical formulas called path predicates
. Conceptually, this technique operates on path predicates in two steps:
- They are constructed using constraints on the program's input.
- They are used to generate program inputs that will cause the associated paths to execute.
This approach produces no false positives in the sense that all identified program states can be triggered during concrete execution. For example, if the analysis finds an integer overflow, it is guaranteed to be reproducible.
Path Predicate Example
To get an insight of how DSE works, consider the following example:
1function f(uint a){23 if (a == 65) {4 // A bug is present5 }67}Copy
As f()
contains two paths, a DSE will construct two different path predicates:
- Path 1:
a == 65
- Path 2:
Not (a == 65)
Each path predicate is a mathematical formula that can be given to a so-called SMT solver(opens in a new tab), which will try to solve the equation. For Path 1
, the solver will say that the path can be explored with a = 65
. For Path 2
, the solver can give a
any value other than 65, for example a = 0
.
Verifying properties
Manticore allows a full control over all the execution of each path. As a result, it allows you to add arbitrary constraints to almost anything. This control allows for the creation of properties on the contract.
Consider the following example:
1function unsafe_add(uint a, uint b) returns(uint c){2 c = a + b; // no overflow protection3 return c;4}Copy
Here there is only one path to explore in the function:
- Path 1:
c = a + b
Using Manticore, you can check for overflow, and add constraints to the path predicate:
c = a + b AND (c < a OR c < b)
If it is possible to find a valuation of a
and b
for which the path predicate above is feasible, it means that you have found an overflow. For example the solver can generate the input a = 10 , b = MAXUINT256
.
If you consider a fixed version:
1function safe_add(uint a, uint b) returns(uint c){2 c = a + b;3 require(c>=a);4 require(c>=b);5 return c;6}Copy
The associated formula with overflow check would be:
c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)
This formula cannot be solved; in other world this is a proof that in safe_add
, c
will always increase.
DSE is thereby a powerful tool, that can verify arbitrary constraints on your code.
Running under Manticore
We will see how to explore a smart contract with the Manticore API. The target is the following smart contract example.sol
(opens in a new tab):
1pragma solidity >=0.4.24 <0.6.0;23contract Simple {4 function f(uint a) payable public{5 if (a == 65) {6 revert();7 }8 }9}Show allCopy
Run a standalone exploration
You can run Manticore directly on the smart contract by the following command (project
can be a Solidity File, or a project directory):
$ manticore project
You will get the output of testcases like this one (the order may change):
1...2... m.c.manticore:INFO: Generated testcase No. 0 - STOP3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT6... m.c.manticore:INFO: Generated testcase No. 4 - STOP7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij310...Show all
Without additional information, Manticore will explore the contract with new symbolic transactions until it does not explore new paths on the contract. Manticore does not run new transactions after a failing one (e.g: after a revert).
Manticore will output the information in a mcore_*
directory. Among other, you will find in this directory:
global.summary
: coverage and compiler warningstest_XXXXX.summary
: coverage, last instruction, account balances per test casetest_XXXXX.tx
: detailed list of transactions per test case
Here Manticore founds 7 test cases, which correspond to (the filename order may change):
Transaction 0 | Transaction 1 | Transaction 2 | Result | |
---|---|---|---|---|
test_00000000.tx | Contract creation | f(!=65) | f(!=65) | STOP |
test_00000001.tx | Contract creation | fallback function | REVERT | |
test_00000002.tx | Contract creation | RETURN | ||
test_00000003.tx | Contract creation | f(65) | REVERT | |
test_00000004.tx | Contract creation | f(!=65) | STOP | |
test_00000005.tx | Contract creation | f(!=65) | f(65) | REVERT |
test_00000006.tx | Contract creation | f(!=65) | fallback function | REVERT |
Exploration summary f(!=65) denotes f called with any value different than 65.
As you can notice, Manticore generates an unique test case for every successful or reverted transaction.
Use the --quick-mode
flag if you want fast code exploration (it disable bug detectors, gas computation, ...)
Manipulate a smart contract through the API
This section describes details how to manipulate a smart contract through the Manticore Python API. You can create new file with python extension *.py
and write the necessary code by adding the API commands (basics of which will be described below) into this file and then run it with the command $ python3 *.py
. Also you can execute the commands below directly into the python console, to run the console use the command $ python3
.
Creating Accounts
The first thing you should do is to initiate a new blockchain with the following commands:
1from manticore.ethereum import ManticoreEVM23m = ManticoreEVM()Copy
A non-contract account is created using m.create_account(opens in a new tab):
1user_account = m.create_account(balance=1000)Copy
A Solidity contract can be deployed using m.solidity_create_contract(opens in a new tab):
1source_code = '''2pragma solidity >=0.4.24 <0.6.0;3contract Simple {4 function f(uint a) payable public{5 if (a == 65) {6 revert();7 }8 }9}10'''11# Initiate the contract12contract_account = m.solidity_create_contract(source_code, owner=user_account)Show allCopy
Summary
- You can create user and contract accounts with m.create_account(opens in a new tab) and m.solidity_create_contract(opens in a new tab).
Executing transactions
Manticore supports two types of transaction:
- Raw transaction: all the functions are explored
- Named transaction: only one function is explored
Raw transaction
A raw transaction is executed using m.transaction(opens in a new tab):
1m.transaction(caller=user_account,2 address=contract_account,3 data=data,4 value=value)Copy
The caller, the address, the data, or the value of the transaction can be either concrete or symbolic:
- m.make_symbolic_value(opens in a new tab) creates a symbolic value.
- m.make_symbolic_buffer(size)(opens in a new tab) creates a symbolic byte array.
For example:
1symbolic_value = m.make_symbolic_value()2symbolic_data = m.make_symbolic_buffer(320)3m.transaction(caller=user_account,4 address=contract_address,5 data=symbolic_data,6 value=symbolic_value)Copy
If the data is symbolic, Manticore will explore all the functions of the contract during the transaction execution. It will be helpful to see the Fallback Function explanation in the Hands on the Ethernaut CTF(opens in a new tab) article for understanding how the function selection works.
Named transaction
Functions can be executed through their name.
To execute f(uint var)
with a symbolic value, from user_account, and with 0 ether, use:
1symbolic_var = m.make_symbolic_value()2contract_account.f(symbolic_var, caller=user_account, value=0)Copy
If value
of the transaction is not specified, it is 0 by default.
Summary
- Arguments of a transaction can be concrete or symbolic
- A raw transaction will explore all the functions
- Function can be called by their name
Workspace
m.workspace
is the directory used as output directory for all the files generated:
1print("Results are in {}".format(m.workspace))Copy
Terminate the Exploration
To stop the exploration use m.finalize()(opens in a new tab). No further transactions should be sent once this method is called and Manticore generates test cases for each of the path explored.
Summary: Running under Manticore
Putting all the previous steps together, we obtain:
1from manticore.ethereum import ManticoreEVM23m = ManticoreEVM()45with open('example.sol') as f:6 source_code = f.read()78user_account = m.create_account(balance=1000)9contract_account = m.solidity_create_contract(source_code, owner=user_account)1011symbolic_var = m.make_symbolic_value()12contract_account.f(symbolic_var)1314print("Results are in {}".format(m.workspace))15m.finalize() # stop the explorationShow allCopy
All the code above you can find in the example_run.py
(opens in a new tab)
Getting throwing paths
We will now generate specific inputs for the paths raising an exception in f()
. The target is still the following smart contract example.sol
(opens in a new tab):
1pragma solidity >=0.4.24 <0.6.0;2contract Simple {3 function f(uint a) payable public{4 if (a == 65) {5 revert();6 }7 }8}Copy
Using state information
Each path executed has its state of the blockchain. A state is either ready or it is killed, meaning that it reaches a THROW or REVERT instruction:
- m.ready_states(opens in a new tab): the list of states that are ready (they did not execute a REVERT/INVALID)
- m.killed_states(opens in a new tab): the list of states that are killed
- m.all_states(opens in a new tab): all the states
1for state in m.all_states:2 # do something with stateCopy
You can access state information. For example:
state.platform.get_balance(account.address)
: the balance of the accountstate.platform.transactions
: the list of transactionsstate.platform.transactions[-1].return_data
: the data returned by the last transaction
The data returned by the last transaction is an array, which can be converted to a value with ABI.deserialize, for example:
1data = state.platform.transactions[0].return_data2data = ABI.deserialize("uint", data)Copy
How to generate testcase
Use m.generate_testcase(state, name)(opens in a new tab) to generate testcase:
1m.generate_testcase(state, 'BugFound')Copy
Summary
- You can iterate over the state with m.all_states
state.platform.get_balance(account.address)
returns the account’s balancestate.platform.transactions
returns the list of transactionstransaction.return_data
is the data returnedm.generate_testcase(state, name)
generate inputs for the state
Summary: Getting Throwing Path
1from manticore.ethereum import ManticoreEVM23m = ManticoreEVM()45with open('example.sol') as f:6 source_code = f.read()78user_account = m.create_account(balance=1000)9contract_account = m.solidity_create_contract(source_code, owner=user_account)1011symbolic_var = m.make_symbolic_value()12contract_account.f(symbolic_var)1314## Check if an execution ends with a REVERT or INVALID15for state in m.terminated_states:16 last_tx = state.platform.transactions[-1]17 if last_tx.result in ['REVERT', 'INVALID']:18 print('Throw found {}'.format(m.workspace))19 m.generate_testcase(state, 'ThrowFound')Show allCopy
All the code above you can find into the example_run.py
(opens in a new tab)
Note we could have generated a much simpler script, as all the states returned by terminated_state have REVERT or INVALID in their result: this example was only meant to demonstrate how to manipulate the API.
Adding constraints
We will see how to constrain the exploration. We will make the assumption that the
documentation of f()
states that the function is never called with a == 65
, so any bug with a == 65
is not a real bug. The target is still the following smart contract example.sol
(opens in a new tab):
1pragma solidity >=0.4.24 <0.6.0;2contract Simple {3 function f(uint a) payable public{4 if (a == 65) {5 revert();6 }7 }8}Copy
Operators
The Operators(opens in a new tab) module facilitates the manipulation of constraints, among other it provides:
- Operators.AND,
- Operators.OR,
- Operators.UGT (unsigned greater than),
- Operators.UGE (unsigned greater than or equal to),
- Operators.ULT (unsigned lower than),
- Operators.ULE (unsigned lower than or equal to).
To import the module use the following:
1from manticore.core.smtlib import OperatorsCopy
Operators.CONCAT
is used to concatenate an array to a value. For example, the return_data of a transaction needs to be changed to a value to be checked against another value:
1last_return = Operators.CONCAT(256, *last_return)Copy
Constraints
You can use constraints globally or for a specific state.
Global constraint
Use m.constrain(constraint)
to add a global constraint.
For example, you can call a contract from a symbolic address, and restraint this address to be specific values:
1symbolic_address = m.make_symbolic_value()2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))3m.transaction(caller=user_account,4 address=contract_account,5 data=m.make_symbolic_buffer(320),6 value=0)Copy
State constraint
Use state.constrain(constraint)(opens in a new tab) to add a constraint to a specific state. It can be used to constrain the state after its exploration to check some property on it.
Checking Constraint
Use solver.check(state.constraints)
to know if a constraint is still feasible.
For example, the following will constraint symbolic_value to be different from 65 and check if the state is still feasible:
1state.constrain(symbolic_var != 65)2if solver.check(state.constraints):3 # state is feasibleCopy
Summary: Adding Constraints
Adding constraint to the previous code, we obtain:
1from manticore.ethereum import ManticoreEVM2from manticore.core.smtlib.solver import Z3Solver34solver = Z3Solver.instance()56m = ManticoreEVM()78with open("example.sol") as f:9 source_code = f.read()1011user_account = m.create_account(balance=1000)12contract_account = m.solidity_create_contract(source_code, owner=user_account)1314symbolic_var = m.make_symbolic_value()15contract_account.f(symbolic_var)1617no_bug_found = True1819## Check if an execution ends with a REVERT or INVALID20for state in m.terminated_states:21 last_tx = state.platform.transactions[-1]22 if last_tx.result in ['REVERT', 'INVALID']:23 # we do not consider the path were a == 6524 condition = symbolic_var != 6525 if m.generate_testcase(state, name="BugFound", only_if=condition):26 print(f'Bug found, results are in {m.workspace}')27 no_bug_found = False2829if no_bug_found:30 print(f'No bug found')Show allCopy
All the code above you can find into the example_run.py
(opens in a new tab)
Last edit: @lukassim(opens in a new tab), April 26, 2024