Tutorial: Adding Constraints

Adding Constraints

Table of contents:

• Introduction
• Operators
• Constraints
• Checking Constraint
• Summary: Adding Constraints

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

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

Operators

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

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

last_return = Operators.CONCAT(256, *last_return)

Constraints

You can use constraints globally or for a specific state.

Global constraint

To constraint all the current state with the boolean constraint you should use m.constrain(constraint). For example, you can call a contract from a symbolic address, and restraint this address to be specific values:

symbolic_address = m.make_symbolic_value()
m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
m.transaction(caller=user_account,
              address=contract_account,
              data=m.make_symbolic_buffer(320),
              value=0)

State constraint

To constrain the state with the boolean constraint you should use state.constrain(constraint). It can be used to constrain the state after its exploration to check some property on it.

Checking Constraint

To check if the constraints of a state are still feasible you should use solver.check(state.constraints). For example, the following will constraint symbolic_value to be different from 65 and check if the state is still feasible:

state.constrain(symbolic_var != 65)
if solver.check(state.constraints):
    # state is feasible

Summary: Adding Constraints

Adding constraint to the previous code, we obtain:

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

solver = Z3Solver.instance()

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"]:
        # We don't consider the path were a == 65
        state.constrain(symbolic_var != 65)
        if solver.check(state.constraints):
            print("Bug found in {}".format(m.workspace))
            m.generate_testcase(state, "BugFound")

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