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