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 import solver

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