Getting Throwing Path

Table of contents:

Getting Throwing Path

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 (example.sol):

pragma solidity >=0.4.24 <0.6.0;

contract Simple {
    function f(uint256 a) public payable {
        if (a == 65) {
            revert();
        }
    }
}

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

for state in m.all_states:
    # 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:

data = state.platform.transactions[0].return_data
data = ABI.deserialize("uint256", data)

How to generate testcase

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

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

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()

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

user_account = m.create_account(balance=1*10**18)
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 example_throw.py

The next step is to add constraints to the state.

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.

Building Secure Contracts