Tutorial: Running under Manticore

Running under Manticore

Table of contents:

• Introduction
• How to run a standalone exploration
• How to manipulate a smart contract through API
• Summary: Running under Manticore

All the paths given in this tutorial are relative to /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore in eth-security-toolbox.

Introduction

We will see how to explore a smart contract with the Manticore API. The target is the following smart contract (examples/example.sol):

pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}

How to run a standalone exploration

You can run Manticore directly on the smart contract by the following command:

$ manticore example.sol

You will get the output of testcases(the order may change) like this one:

...
... m.c.manticore:INFO: Generated testcase No. 0 - STOP
... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
... m.c.manticore:INFO: Generated testcase No. 4 - STOP
... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
...

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 transaction.

How to manipulate a smart contract through 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.

Blockchain and accounts

The first thing you should do is to initiate a new blockchain with the following commands:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

Now we can create a non-contract account. To create a account use m.create_account:

user_account = m.create_account(balance=1000)

To deploy a solidity contract use m.solidity_create_contract:

source_code = '''
pragma solidity >=0.4.24 <0.6.0;
contract Simple {
    function f(uint a) payable public{
        if (a == 65) {
            revert();
        }
    }
}
'''
# Initiate the contract
contract_account = m.solidity_create_contract(source_code, owner=user_account)

Transactions

You can execute a raw transaction using m.transaction:

m.transaction(caller=user_account,
              address=contract_account,
              data=data,
              value=value)

The caller, the address, the data, or the value of the transaction can be either concrete or symbolic. To create a symbolic value use m.make_symbolic_value and to create a symbolic byte array use m.make_symbolic_buffer(size) as shown below:

symbolic_value = m.make_symbolic_value()
symbolic_data = m.make_symbolic_buffer(320)
m.transaction(caller=user_account,
              address=contract_address,
              data=symbolic_data,
              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 article for understanding how the function selection works.

Manticore also allows the user to execute only one specific function. For example, to execute f(uint var) with a symbolic value, from user_account, and with 0 ether, run the following:

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var, caller=user_account, value=0)

If value of the transaction is not specified, it is 0 by default.

Workspace

m.workspace is the directory used as output directory for all the files generated:

print("Results are in {}".format(m.workspace))

Terminate the Exploration

To stop the exploration you should 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:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

with open('example.sol') as f:
    source_code = f.read()

user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(source_code, owner=user_account)

symbolic_var = m.make_symbolic_value()
contract_account.f(symbolic_var)

print("Results are in {}".format(m.workspace))
m.finalize() # stop the exploration

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