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-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:

1. They are constructed using constraints on the program's input.
2. 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){
2
3  if (a == 65) {
4      // A bug is present
5  }
6
7}
 複製

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 protection
3  return c;
4}
 複製

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}
 複製

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;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
顯示全部
 複製

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...
顯示全部

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):

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()
 複製

A non-contract account is created using m.create_account(opens in a new tab):

1user_account = m.create_account(balance=1000)
 複製

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 contract
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
顯示全部
 複製

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)
 複製

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)
 複製

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)
 複製

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))
 複製

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 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
顯示全部
 複製

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}
 複製

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 state
 複製

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)
 複製

How to generate testcase

Use m.generate_testcase(state, name)(opens in a new tab) to generate testcase:

1m.generate_testcase(state, 'BugFound')
 複製

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')
顯示全部
 複製

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}
 複製

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 Operators
 複製

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)
 複製

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)
 複製

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 feasible
 複製

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')
顯示全部
 複製

All the code above you can find into the example_run.py(opens in a new tab)