Tutorial: Exercise

Exercise

Table of contents:

• Targeted contract
• Exercise to solve
• Proposed scenario
• Solution

Join the team on Slack at: https://empireslacking.herokuapp.com/ #ethereum

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

Targeted contract

We will test the following contract exercises/overflow.sol:

pragma solidity >=0.4.24 <0.6.0;

contract Overflow {
    uint public sellerBalance=0;

    function add(uint value) public returns (bool){
        sellerBalance += value; // complicated math, possible overflow
    }
}

Exercise to solve

Exercise corresponds to automatically find a vulnerability with a Manticore script. Once the vulnerability is found, Manticore can be applied to a fixed version of the contract, to demonstrate that the bug is effectively fixed.

Use Manticore to find if an overflow is possible in Overflow.add. Propose a fix of the contract, and test your fix using your Manticore script.

Proposed scenario

The solution will be based on the proposed scenario, but other solutions are possible.

Proposed scenario:

• Generate one user account
• Generate the contract account
• Call two times add with two symbolic values
• Call sellerBalance()
• Check if it is possible for the value returned by sellerBalance() to be lower than the first input.

Hints:

Recall from Getting Throwing Path that the value returned by the last transaction can be accessed through:

state.platform.transactions[-1].return_data

Recall from Adding Constraints, return_data needs to be concatened:

last_return = Operators.CONCAT(256, *last_return)

Recall from Adding Constraints, to add a constraint a > b on two unsigned integers use:

state.constrain(Operators.UGT(a, b))

Solution

This solution can be found in /exercises/overflow_solution.py or click here

from manticore.ethereum import ManticoreEVM
from manticore.core.smtlib import Operators
from manticore.core.smtlib.solver import Z3Solver

solver = Z3Solver.instance()

m = ManticoreEVM()  # initiate the blockchain
with open("overflow.sol") as f:
    source_code = f.read()

# Generate the accounts
user_account = m.create_account(balance=1000)
contract_account = m.solidity_create_contract(
    source_code, owner=user_account, balance=0
)

# First add won't overflow uint256 representation
value_0 = m.make_symbolic_value()
contract_account.add(value_0, caller=user_account)
# Potential overflow
value_1 = m.make_symbolic_value()
contract_account.add(value_1, caller=user_account)
contract_account.sellerBalance(caller=user_account)

for state in m.ready_states:
    # Check if input0 > sellerBalance

    # last_return is the data returned
    last_return = state.platform.transactions[-1].return_data
    # retrieve last_return and input0 in a similar format
    last_return = Operators.CONCAT(256, *last_return)

    state.constrain(Operators.UGT(value_0, last_return))

    if solver.check(state.constraints):
        print("Overflow found! see {}".format(m.workspace))
        m.generate_testcase(state, "OverflowFound")