diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index d41b24c0..37b5a0de 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -1,4 +1,4 @@ -from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE +from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE, Optimize from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, @@ -6,12 +6,17 @@ from mythril.laser.ethereum.transaction.transaction_models import ( import logging -def get_model(constraints): - s = Solver() +def get_model(constraints, minimize=(), maximize=()): + s = Optimize() s.set("timeout", 100000) for constraint in constraints: s.add(constraint) + for e in minimize: + s.minimize(e) + for e in maximize: + s.maximize(e) + result = s.check() if result == sat: return s.model() @@ -62,6 +67,7 @@ def get_transaction_sequence(global_state, constraints): txs = {} creation_tx_ids = [] tx_constraints = constraints.copy() + minimize = [] for transaction in transaction_sequence: tx_id = str(transaction.id) @@ -74,12 +80,14 @@ def get_transaction_sequence(global_state, constraints): UGE(max_calldatasize, transaction.call_data.calldatasize) ) + minimize.append(transaction.call_data.calldatasize) + txs[tx_id] = tx_template.copy() else: creation_tx_ids.append(tx_id) - model = get_model(tx_constraints) + model = get_model(tx_constraints, minimize=minimize) for transaction in transaction_sequence: if not isinstance(transaction, ContractCreationTransaction): @@ -105,7 +113,7 @@ def get_transaction_sequence(global_state, constraints): if "caller" in name: # caller is 'creator' for creation transactions tx_id = name.replace("caller", "") - caller = "0x" + ("%x" % model[d].as_long()).zfill(64) + caller = "0x" + ("%x" % model[d].as_long()).zfill(40) txs[tx_id]["caller"] = caller diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index edefece9..cc340c2e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -417,7 +417,11 @@ class Instruction: environment = global_state.environment op0 = state.stack.pop() - state.stack.append(environment.calldata.get_word_at(op0)) + value, constraints = environment.calldata.get_word_at(op0) + + state.stack.append(value) + state.constraints.extend(constraints) + return [global_state] @StateTransition() @@ -497,7 +501,10 @@ class Instruction: new_memory = [] for i in range(size): - new_memory.append(environment.calldata[i_data]) + value, constraints = environment.calldata[i_data] + new_memory.append(value) + state.constraints.extend(constraints) + i_data = ( i_data + 1 if isinstance(i_data, int) else simplify(i_data + 1) ) diff --git a/mythril/laser/ethereum/natives.py b/mythril/laser/ethereum/natives.py index 3091c963..bb741929 100644 --- a/mythril/laser/ethereum/natives.py +++ b/mythril/laser/ethereum/natives.py @@ -1,6 +1,5 @@ # -*- coding: utf8 -*- -import copy import hashlib import logging @@ -8,7 +7,8 @@ from ethereum.utils import ecrecover_to_pub from py_ecc.secp256k1 import N as secp256k1n from rlp.utils import ALL_BYTES -from mythril.laser.ethereum.util import bytearray_to_int, sha3 +from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int +from z3 import Concat, simplify class NativeContractException(Exception): @@ -70,7 +70,16 @@ def ripemd160(data): def identity(data): - return copy.copy(data) + # Group up into an array of 32 byte words instead + # of an array of bytes. If saved to memory, 32 byte + # words are currently needed, but a correct memory + # implementation would be byte indexed for the most + # part. + return data + result = [] + for i in range(0, len(data), 32): + result.append(simplify(Concat(data[i : i + 32]))) + return result def native_contracts(address, data): @@ -79,4 +88,11 @@ def native_contracts(address, data): """ functions = (ecrecover, sha256, ripemd160, identity) - return functions[address - 1](data.starting_calldata) + + try: + data = [get_concrete_int(e) for e in data._calldata] + except TypeError: + # Symbolic calldata + data = data._calldata + + return functions[address - 1](data) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 20c17c62..9c739308 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -4,16 +4,15 @@ from z3 import ( BitVecRef, BitVecNumRef, BitVecSort, - Solver, ExprRef, Concat, sat, simplify, Array, ForAll, - Solver, - UGT, Implies, + UGE, + UGT, ) from z3.z3types import Z3Exception from mythril.disassembler.disassembly import Disassembly @@ -45,7 +44,7 @@ class Calldata: :param starting_calldata: byte array representing the concrete calldata of a transaction """ self.tx_id = tx_id - if starting_calldata: + if not starting_calldata is None: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) self.concrete = True @@ -56,32 +55,21 @@ class Calldata: self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256) self.concrete = False - self.starting_calldata = starting_calldata or [] - - @property - def constraints(self): - constraints = [] if self.concrete: - for calldata_byte in self.starting_calldata: + for calldata_byte in starting_calldata: if type(calldata_byte) == int: self._calldata.append(BitVecVal(calldata_byte, 8)) else: self._calldata.append(calldata_byte) - constraints.append(self.calldatasize == len(self.starting_calldata)) - else: - x = BitVec("x", 256) - constraints.append( - ForAll(x, Implies(self[x] != 0, UGT(self.calldatasize, x))) - ) - return constraints def concretized(self, model): result = [] - for i in range( get_concrete_int(model.eval(self.calldatasize, model_completion=True)) ): - result.append(get_concrete_int(model.eval(self[i], model_completion=True))) + result.append( + get_concrete_int(model.eval(self._calldata[i], model_completion=True)) + ) return result @@ -103,15 +91,23 @@ class Calldata: except Z3Exception: raise IndexError("Invalid Calldata Slice") - return simplify(Concat(dataparts)) + values, constraints = zip(*dataparts) + result_constraints = [] + for c in constraints: + result_constraints.extend(c) + return (simplify(Concat(values)), result_constraints) if self.concrete: try: - return self._calldata[get_concrete_int(item)] + return (self._calldata[get_concrete_int(item)], ()) except IndexError: - return BitVecVal(0, 8) + return (BitVecVal(0, 8), ()) else: - return self._calldata[item] + constraints = [ + Implies(self._calldata[item] != 0, UGT(self.calldatasize, item)) + ] + + return (self._calldata[item], constraints) class Storage: diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 4aee343f..3cc1afac 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -91,9 +91,6 @@ class MessageCallTransaction: global_state = GlobalState(self.world_state, environment, None) global_state.environment.active_function_name = "fallback" - global_state.mstate.constraints.extend( - global_state.environment.calldata.constraints - ) return global_state @@ -173,9 +170,6 @@ class ContractCreationTransaction: global_state = GlobalState(self.world_state, environment, None) global_state.environment.active_function_name = "constructor" - global_state.mstate.constraints.extend( - global_state.environment.calldata.constraints - ) return global_state diff --git a/tests/laser/state/calldata_test.py b/tests/laser/state/calldata_test.py index c2d76c81..e93799c3 100644 --- a/tests/laser/state/calldata_test.py +++ b/tests/laser/state/calldata_test.py @@ -2,7 +2,7 @@ import pytest from mythril.laser.ethereum.state import Calldata from z3 import Solver, simplify from z3.z3types import Z3Exception - +from mock import MagicMock uninitialized_test_data = [ ([]), # Empty concrete calldata @@ -17,10 +17,12 @@ def test_concrete_calldata_uninitialized_index(starting_calldata): solver = Solver() # Act - value = calldata[100] - value2 = calldata.get_word_at(200) + value, constraint1 = calldata[100] + value2, constraint2 = calldata.get_word_at(200) + + solver.add(constraint1) + solver.add(constraint2) - solver.add(calldata.constraints) solver.check() model = solver.model() @@ -38,7 +40,6 @@ def test_concrete_calldata_calldatasize(): solver = Solver() # Act - solver.add(calldata.constraints) solver.check() model = solver.model() @@ -54,11 +55,11 @@ def test_symbolic_calldata_constrain_index(): solver = Solver() # Act - constraint = calldata[100] == 50 + value, calldata_constraints = calldata[100] + constraint = value == 50 - value = calldata[100] + solver.add([constraint] + calldata_constraints) - solver.add(calldata.constraints + [constraint]) solver.check() model = solver.model() @@ -76,9 +77,10 @@ def test_concrete_calldata_constrain_index(): solver = Solver() # Act - constraint = calldata[2] == 3 + value, calldata_constraints = calldata[2] + constraint = value == 3 - solver.add(calldata.constraints + [constraint]) + solver.add([constraint] + calldata_constraints) result = solver.check() # Assert @@ -88,14 +90,18 @@ def test_concrete_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act constraints = [] - constraints.append(calldata[51] == 1) + value, calldata_constraints = calldata[51] + constraints.append(value == 1) constraints.append(calldata.calldatasize == 50) - solver.add(calldata.constraints + constraints) + solver.add(constraints + calldata_constraints) + result = solver.check() # Assert diff --git a/tests/laser/transaction/symbolic_test.py b/tests/laser/transaction/symbolic_test.py index 5c18d190..2ca12f63 100644 --- a/tests/laser/transaction/symbolic_test.py +++ b/tests/laser/transaction/symbolic_test.py @@ -10,9 +10,6 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state import WorldState, Account import unittest.mock as mock from unittest.mock import MagicMock -from mythril.laser.ethereum.transaction.symbolic import ( - _setup_global_state_for_execution, -) def _is_message_call(_, transaction): @@ -70,25 +67,3 @@ def test_execute_contract_creation(mocked_setup: MagicMock): # laser_evm.exec.assert_called_once() assert laser_evm.exec.call_count == 1 assert len(laser_evm.open_states) == 0 - - -def test_calldata_constraints_in_transaction(): - # Arrange - laser_evm = LaserEVM({}) - world_state = WorldState() - - correct_constraints = [MagicMock(), MagicMock(), MagicMock()] - - transaction = MessageCallTransaction( - world_state, Account("ca11ee"), Account("ca114") - ) - transaction.call_data = MagicMock() - transaction.call_data.constraints = correct_constraints - - # Act - _setup_global_state_for_execution(laser_evm, transaction) - - # Assert - state = laser_evm.work_list[0] - for constraint in correct_constraints: - assert constraint in state.environment.calldata.constraints