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}8Көшіру
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}5Көшіру
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}7Көшіру
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}10Бәрін көрсетуКөшіру
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...11Бәрін көрсету
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()4Көшіру
A non-contract account is created using m.create_account(opens in a new tab):
1user_account = m.create_account(balance=1000)2Көшіру
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)13Бәрін көрсетуКөшіру
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)5Көшіру
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)7Көшіру
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)3Көшіру
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))2Көшіру
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 exploration16Бәрін көрсетуКөшіру
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)