Tutorial: Getting Throwing Path

Getting Throwing Path

Table of contents:

• Introduction
• How to use state information
• How to generate testcase
• Summary: Getting Throwing Path

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 now improve the previous example and generate specific inputs for the paths raising an exception in f(). The target is still 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 use state information

Each path executed has its state of the blockchain. A state is either alive or it is terminated, meaning that it reaches a THROW or REVERT instruction. You can access the list of alive states through m.running_states. The list of terminated states (e.g: states that reached an error) you can access using m.terminated_states. The list of all the states you can access using m.all_states. To change the state data you must use the loop:

for state in m.all_states:
    # do something with state

From a specific state, information can be accessed. For example:

• state.platform.transactions: the list of transactions
• state.platform.transactions[-1].return_data: the data returned by the last transaction

On a transaction, transaction.result returns the result of the transaction, which can be 'RETURN', 'STOP', 'REVERT', 'THROW' or 'SELFDESTRUCT'. transaction.data return the data of the transaction.

How to generate testcase

To generate a testcase from a state you should use m.generate_testcase(state, name) as shown below:

m.generate_testcase(state, 'BugFound')

Summary: Getting Throwing Path

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)

## Check if an execution ends with a REVERT or INVALID
for state in m.terminated_states:
    last_tx = state.platform.transactions[-1]
    if last_tx.result in ['REVERT', 'INVALID']:
        print('Throw found {}'.format(m.workspace))
        m.generate_testcase(state, 'ThrowFound')

All the code above you can find into the examples/example_throw.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.