From 85a2926a568e1350e1cef1e9bd5199c1f55e0973 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 31 Oct 2018 13:15:48 -0400 Subject: [PATCH 1/5] related calldata and concretion improvements/fixes --- mythril/analysis/solver.py | 18 ++++++++---- mythril/laser/ethereum/instructions.py | 3 ++ mythril/laser/ethereum/state.py | 39 +++++++++++++++----------- 3 files changed, 38 insertions(+), 22 deletions(-) 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 c31d5f46..53d4d2a0 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -420,6 +420,7 @@ class Instruction: op0 = state.stack.pop() state.stack.append(environment.calldata.get_word_at(op0)) + environment.calldata.update_constraints(state) return [global_state] @StateTransition() @@ -504,6 +505,8 @@ class Instruction: i_data + 1 if isinstance(i_data, int) else simplify(i_data + 1) ) + environment.calldata.update_constraints(state) + for i in range(0, len(new_memory), 32): state.memory[i + mstart] = simplify(Concat(new_memory[i : i + 32])) except IndexError: diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 20c17c62..15b5ac9e 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,6 +44,8 @@ class Calldata: :param starting_calldata: byte array representing the concrete calldata of a transaction """ self.tx_id = tx_id + self._constraints = [] + self._not_yet_added_constraints = [] if starting_calldata: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) @@ -56,28 +57,29 @@ 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 + + @property + def constraints(self): + return self._constraints + + def update_constraints(self, mstate): + """ + Update constraints of a mstate + :param mstate: mstate to add constraints to + """ + mstate.constraints.extend(self._not_yet_added_constraints) + + self._constraints += self._not_yet_added_constraints + self._not_yet_added_constraints = [] def concretized(self, model): result = [] - for i in range( get_concrete_int(model.eval(self.calldatasize, model_completion=True)) ): @@ -111,6 +113,9 @@ class Calldata: except IndexError: return BitVecVal(0, 8) else: + constraints = [Implies(item != 0, UGT(self.calldatasize, item))] + self._not_yet_added_constraints += constraints + return self._calldata[item] From 18c182d5e129223cd6697ed047094330a92b3a74 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 31 Oct 2018 14:05:32 -0400 Subject: [PATCH 2/5] remove now unused code and update unit tests for new Calldata constraints handling --- mythril/laser/ethereum/state.py | 2 +- .../transaction/transaction_models.py | 3 -- tests/laser/state/calldata_test.py | 29 +++++++++++++++---- tests/laser/transaction/symbolic_test.py | 25 ---------------- 4 files changed, 24 insertions(+), 35 deletions(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 15b5ac9e..649837ee 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -46,7 +46,7 @@ class Calldata: self.tx_id = tx_id self._constraints = [] self._not_yet_added_constraints = [] - if starting_calldata: + if not starting_calldata is None: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) self.concrete = True diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 4aee343f..eb85b295 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -173,9 +173,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..2c77a58f 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 @@ -14,13 +14,17 @@ uninitialized_test_data = [ def test_concrete_calldata_uninitialized_index(starting_calldata): # Arrange calldata = Calldata(0, starting_calldata) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act value = calldata[100] value2 = calldata.get_word_at(200) - solver.add(calldata.constraints) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.check() model = solver.model() @@ -38,7 +42,6 @@ def test_concrete_calldata_calldatasize(): solver = Solver() # Act - solver.add(calldata.constraints) solver.check() model = solver.model() @@ -51,6 +54,8 @@ def test_concrete_calldata_calldatasize(): def test_symbolic_calldata_constrain_index(): # Arrange calldata = Calldata(0) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act @@ -58,7 +63,10 @@ def test_symbolic_calldata_constrain_index(): value = calldata[100] - solver.add(calldata.constraints + [constraint]) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.add(constraint) + solver.check() model = solver.model() @@ -73,12 +81,16 @@ def test_symbolic_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9]) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act constraint = calldata[2] == 3 - solver.add(calldata.constraints + [constraint]) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.add(constraint) result = solver.check() # Assert @@ -88,6 +100,8 @@ def test_concrete_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0) + mstate = MagicMock() + mstate.constraints = [] solver = Solver() # Act @@ -95,7 +109,10 @@ def test_concrete_calldata_constrain_index(): constraints.append(calldata[51] == 1) constraints.append(calldata.calldatasize == 50) - solver.add(calldata.constraints + constraints) + calldata.update_constraints(mstate) + solver.add(mstate.constraints) + solver.add(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 From c9f6f8b2f31ccdbd648827fd18368c94803b6605 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 31 Oct 2018 15:04:20 -0400 Subject: [PATCH 3/5] update natives.py to reflect calldata fixes --- mythril/laser/ethereum/natives.py | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) 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) From 28c611fc0697e694e52b9c9431dcfc911d419dcf Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 6 Nov 2018 08:30:54 -0500 Subject: [PATCH 4/5] fix calldata constraint --- mythril/laser/ethereum/state.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 649837ee..0c39fbf1 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -113,7 +113,9 @@ class Calldata: except IndexError: return BitVecVal(0, 8) else: - constraints = [Implies(item != 0, UGT(self.calldatasize, item))] + constraints = [ + Implies(self._calldata[item] != 0, UGT(self.calldatasize, item)) + ] self._not_yet_added_constraints += constraints return self._calldata[item] From 2662ae07544a72185878fc8e76ed5e1fa78d3338 Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 6 Nov 2018 10:59:03 -0500 Subject: [PATCH 5/5] calldata getitem returns tuple with constraints --- mythril/laser/ethereum/instructions.py | 14 ++++--- mythril/laser/ethereum/state.py | 33 ++++++----------- .../transaction/transaction_models.py | 3 -- tests/laser/state/calldata_test.py | 37 +++++++------------ 4 files changed, 33 insertions(+), 54 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 53d4d2a0..8b838aa2 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -419,8 +419,11 @@ class Instruction: environment = global_state.environment op0 = state.stack.pop() - state.stack.append(environment.calldata.get_word_at(op0)) - environment.calldata.update_constraints(state) + value, constraints = environment.calldata.get_word_at(op0) + + state.stack.append(value) + state.constraints.extend(constraints) + return [global_state] @StateTransition() @@ -500,13 +503,14 @@ 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) ) - environment.calldata.update_constraints(state) - for i in range(0, len(new_memory), 32): state.memory[i + mstart] = simplify(Concat(new_memory[i : i + 32])) except IndexError: diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 0c39fbf1..9c739308 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -44,8 +44,6 @@ class Calldata: :param starting_calldata: byte array representing the concrete calldata of a transaction """ self.tx_id = tx_id - self._constraints = [] - self._not_yet_added_constraints = [] if not starting_calldata is None: self._calldata = [] self.calldatasize = BitVecVal(len(starting_calldata), 256) @@ -64,26 +62,14 @@ class Calldata: else: self._calldata.append(calldata_byte) - @property - def constraints(self): - return self._constraints - - def update_constraints(self, mstate): - """ - Update constraints of a mstate - :param mstate: mstate to add constraints to - """ - mstate.constraints.extend(self._not_yet_added_constraints) - - self._constraints += self._not_yet_added_constraints - self._not_yet_added_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 @@ -105,20 +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: constraints = [ Implies(self._calldata[item] != 0, UGT(self.calldatasize, item)) ] - self._not_yet_added_constraints += constraints - return self._calldata[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 eb85b295..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 diff --git a/tests/laser/state/calldata_test.py b/tests/laser/state/calldata_test.py index 2c77a58f..e93799c3 100644 --- a/tests/laser/state/calldata_test.py +++ b/tests/laser/state/calldata_test.py @@ -14,16 +14,14 @@ uninitialized_test_data = [ def test_concrete_calldata_uninitialized_index(starting_calldata): # Arrange calldata = Calldata(0, starting_calldata) - mstate = MagicMock() - mstate.constraints = [] solver = Solver() # Act - value = calldata[100] - value2 = calldata.get_word_at(200) + value, constraint1 = calldata[100] + value2, constraint2 = calldata.get_word_at(200) - calldata.update_constraints(mstate) - solver.add(mstate.constraints) + solver.add(constraint1) + solver.add(constraint2) solver.check() model = solver.model() @@ -54,18 +52,13 @@ def test_concrete_calldata_calldatasize(): def test_symbolic_calldata_constrain_index(): # Arrange calldata = Calldata(0) - mstate = MagicMock() - mstate.constraints = [] solver = Solver() # Act - constraint = calldata[100] == 50 + value, calldata_constraints = calldata[100] + constraint = value == 50 - value = calldata[100] - - calldata.update_constraints(mstate) - solver.add(mstate.constraints) - solver.add(constraint) + solver.add([constraint] + calldata_constraints) solver.check() model = solver.model() @@ -81,16 +74,13 @@ def test_symbolic_calldata_constrain_index(): def test_concrete_calldata_constrain_index(): # Arrange calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9]) - mstate = MagicMock() - mstate.constraints = [] solver = Solver() # Act - constraint = calldata[2] == 3 + value, calldata_constraints = calldata[2] + constraint = value == 3 - calldata.update_constraints(mstate) - solver.add(mstate.constraints) - solver.add(constraint) + solver.add([constraint] + calldata_constraints) result = solver.check() # Assert @@ -106,12 +96,11 @@ def test_concrete_calldata_constrain_index(): # Act constraints = [] - constraints.append(calldata[51] == 1) + value, calldata_constraints = calldata[51] + constraints.append(value == 1) constraints.append(calldata.calldatasize == 50) - calldata.update_constraints(mstate) - solver.add(mstate.constraints) - solver.add(constraints) + solver.add(constraints + calldata_constraints) result = solver.check()