How to use Manticore to find bugs in smart contracts

solidity

smart contracts

security

testing

formal verification

advanced

️Trailofbits

Building secure contracts

January 13, 2020

6 一分钟阅读

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-toolbox
docker 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.11
cd /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 insigh of how DSE works, consider the following example:

1function f(uint a){
2
3  if (a == 65) {
4      // A bug is present
5  }
6
7}
8
 复制

As f() contains two paths, a DSE will construct two differents 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, 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 protection
3  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 constraitns 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:

1pragma solidity >=0.4.24 <0.6.0;
2
3contract 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 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
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 warnings
test_XXXXX.summary: coverage, last instruction, account balances per test case
test_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 ManticoreEVM
2
3m = ManticoreEVM()
4
 复制

A non-contract account is created using m.create_account:

1user_account = m.create_account(balance=1000)
2
 复制

A Solidity contract can be deployed using m.solidity_create_contract:

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 contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
显示全部
 复制

Summary

You can create user and contract accounts with m.create_account and [m.solidity_create_contract](https://manticore.readthedocs.io/en/latest/api.html#manticore.ethereum.ManticoreEVM.solidity_create_contract.

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:

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 creates a symbolic value.
m.make_symbolic_buffer(size) 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 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(). 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 ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("Results are in {}".format(m.workspace))
15m.finalize() # stop the exploration
16
显示全部
 复制

All the code above you can find in the example_run.py

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:

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}
9
 复制

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: the list of states that are ready (they did not execute a REVERT/INVALID)
m.killed_states: the list of states that are killed
m.all_states: all the states

1for state in m.all_states:
2    # do something with state
3
 复制

You can access state information. For example:

state.platform.get_balance(account.address): the balance of the account
state.platform.transactions: the list of transactions
state.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_data
2data = ABI.deserialize("uint", data)
3
 复制

How to generate testcase

Use m.generate_testcase(state, name) to generate testcase:

1m.generate_testcase(state, 'BugFound')
2
 复制

Summary

You can iterate over the state with m.all_states
state.platform.get_balance(account.address) returns the account’s balance
state.platform.transactions returns the list of transactions
transaction.return_data is the data returned
m.generate_testcase(state, name) generate inputs for the state

Summary: Getting Throwing Path

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## Check if an execution ends with a REVERT or INVALID
15for 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')
20
显示全部
 复制

All the code above you can find into the example_run.py

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:

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}
9
 复制

Operators

The Operators 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 Operators
2
 复制

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)
2
 复制

Constraints

You can use constraints globally or for a specific state.

Global constraint

Use m.constrain(constraint) to add a global cosntraint. 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)
7
 复制

State constraint

Use state.constrain(constraint) 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 feasible
4
 复制

Summary: Adding Constraints

Adding constraint to the previous code, we obtain:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## Check if an execution ends with a REVERT or INVALID
20for 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 == 65
24        condition = symbolic_var != 65
25        if m.generate_testcase(state, name="BugFound", only_if=condition):
26            print(f'Bug found, results are in {m.workspace}')
27            no_bug_found = False
28
29if no_bug_found:
30    print(f'No bug found')
31
显示全部
 复制

All the code above you can find into the example_run.py

上次编辑: , Invalid DateTime

Edit page

帮助翻译此页面

How to use Manticore to find bugs in smart contracts

Installation

Manticore through docker

Manticore through pip

Running a script

Introduction to dynamic symbolic execution

Dynamic Symbolic Execution in a Nutshell

Path Predicate Example

Verifying properties

Running under Manticore

Run a standalone exploration

Manipulate a smart contract through the API

Creating Accounts

Summary

Executing transactions

Raw transaction

Named transaction

Summary

Workspace

Terminate the Exploration

Summary: Running under Manticore

Getting throwing paths

Using state information

How to generate testcase

Summary

Summary: Getting Throwing Path

Adding constraints

Operators

Constraints

Global constraint

State constraint

Checking Constraint

Summary: Adding Constraints