From 5f24d234385d7b9398574785573c3b35dc21b31c Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sat, 11 May 2019 11:28:19 +0530 Subject: [PATCH 1/4] Storage Refactor --- mythril/laser/ethereum/instructions.py | 130 ++++++++---------- mythril/laser/ethereum/keccak.py | 18 +-- .../laser/ethereum/transaction/symbolic.py | 2 +- .../transaction/transaction_models.py | 2 +- mythril/laser/smt/__init__.py | 8 +- mythril/laser/smt/bitvec.py | 3 + mythril/laser/smt/bitvecfunc.py | 7 +- mythril/laser/smt/bool.py | 3 + mythril/laser/smt/expression.py | 6 + tests/laser/evm_testsuite/evm_test.py | 4 +- .../overflow.sol.o.graph.html | 6 +- .../outputs_expected/overflow.sol.o.json | 13 ++ .../outputs_expected/overflow.sol.o.jsonv2 | 17 +++ .../outputs_expected/overflow.sol.o.markdown | 13 ++ .../outputs_expected/overflow.sol.o.text | 11 ++ .../underflow.sol.o.graph.html | 4 +- .../outputs_expected/underflow.sol.o.json | 13 ++ .../outputs_expected/underflow.sol.o.jsonv2 | 17 +++ .../outputs_expected/underflow.sol.o.markdown | 13 ++ .../outputs_expected/underflow.sol.o.text | 11 ++ 20 files changed, 200 insertions(+), 101 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b6bb61cd..70ffe84c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -945,7 +945,6 @@ class Instruction: ) log.debug("Created BitVecFunc hash.") - keccak_function_manager.add_keccak(result, state.memory[index]) else: keccak = utils.sha3(data.value.to_bytes(length, byteorder="big")) result = symbol_factory.BitVecFuncVal( @@ -1366,42 +1365,37 @@ class Instruction: state = global_state.mstate index = state.stack.pop() log.debug("Storage access at index " + str(index)) + index = simplify(index) - try: - index = util.get_concrete_int(index) + if not keccak_function_manager.is_keccak(index): return self._sload_helper(global_state, index) - except TypeError: - if not keccak_function_manager.is_keccak(index): - return self._sload_helper(global_state, str(index)) + storage_keys = global_state.environment.active_account.storage.keys() + keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys)) - storage_keys = global_state.environment.active_account.storage.keys() - keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys)) + results = [] # type: List[GlobalState] + constraints = [] - results = [] # type: List[GlobalState] - constraints = [] + for keccak_key in keccak_keys: + key_argument = keccak_function_manager.get_argument(keccak_key) + index_argument = keccak_function_manager.get_argument(index) + if key_argument.size() != index_argument.size(): + continue + constraints.append((keccak_key, key_argument == index_argument)) - for keccak_key in keccak_keys: - key_argument = keccak_function_manager.get_argument(keccak_key) - index_argument = keccak_function_manager.get_argument(index) - constraints.append((keccak_key, key_argument == index_argument)) + for (keccak_key, constraint) in constraints: + if constraint in state.constraints: + results += self._sload_helper(global_state, keccak_key, [constraint]) + if len(results) > 0: + return results - for (keccak_key, constraint) in constraints: - if constraint in state.constraints: - results += self._sload_helper( - global_state, keccak_key, [constraint] - ) - if len(results) > 0: - return results + for (keccak_key, constraint) in constraints: + results += self._sload_helper(copy(global_state), keccak_key, [constraint]) - for (keccak_key, constraint) in constraints: - results += self._sload_helper( - copy(global_state), keccak_key, [constraint] - ) - if len(results) > 0: - return results + if len(results) > 0: + return results - return self._sload_helper(global_state, str(index)) + return self._sload_helper(global_state, index) @staticmethod def _sload_helper( @@ -1422,6 +1416,8 @@ class Instruction: if constraints is not None: global_state.mstate.constraints += constraints + if global_state.mstate.constraints.is_possible is False: + return [] global_state.mstate.stack.append(data) return [global_state] @@ -1452,58 +1448,40 @@ class Instruction: state = global_state.mstate index, value = state.stack.pop(), state.stack.pop() log.debug("Write to storage[" + str(index) + "]") - - try: - index = util.get_concrete_int(index) + index = simplify(index) + is_keccak = keccak_function_manager.is_keccak(index) + if not is_keccak: return self._sstore_helper(global_state, index, value) - except TypeError: - is_keccak = keccak_function_manager.is_keccak(index) - if not is_keccak: - return self._sstore_helper(global_state, str(index), value) - - storage_keys = global_state.environment.active_account.storage.keys() - keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys) - - results = [] # type: List[GlobalState] - new = symbol_factory.Bool(False) - - for keccak_key in keccak_keys: - key_argument = keccak_function_manager.get_argument( - keccak_key - ) # type: Expression - index_argument = keccak_function_manager.get_argument( - index - ) # type: Expression - condition = key_argument == index_argument - condition = ( - condition - if type(condition) == bool - else is_true(simplify(cast(Bool, condition))) - ) - if condition: - return self._sstore_helper( - copy(global_state), - keccak_key, - value, - key_argument == index_argument, - ) - results += self._sstore_helper( - copy(global_state), - keccak_key, - value, - key_argument == index_argument, - ) + storage_keys = global_state.environment.active_account.storage.keys() - new = Or(new, cast(Bool, key_argument != index_argument)) + keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys) - if len(results) > 0: - results += self._sstore_helper( - copy(global_state), str(index), value, new - ) - return results + results = [] # type: List[GlobalState] + new = symbol_factory.Bool(False) + + for keccak_key in keccak_keys: + key_argument = keccak_function_manager.get_argument( + keccak_key + ) # type: Expression + index_argument = keccak_function_manager.get_argument( + index + ) # type: Expression + if key_argument.size() != index_argument.size(): + continue + + result = self._sstore_helper( + copy(global_state), keccak_key, value, key_argument == index_argument + ) + if len(result) > 0: + return result - return self._sstore_helper(global_state, str(index), value) + new = Or(new, cast(Bool, key_argument != index_argument)) + results += self._sstore_helper(copy(global_state), index, value, new) + if len(results) > 0: + return results + # results += self._sstore_helper(copy(global_state), index, value) + return self._sstore_helper(copy(global_state), index, value) @staticmethod def _sstore_helper(global_state, index, value, constraint=None): @@ -1531,6 +1509,8 @@ class Instruction: if constraint is not None: global_state.mstate.constraints.append(constraint) + if global_state.mstate.constraints.is_possible is False: + return [] return [global_state] diff --git a/mythril/laser/ethereum/keccak.py b/mythril/laser/ethereum/keccak.py index 47a39ed1..1d838961 100644 --- a/mythril/laser/ethereum/keccak.py +++ b/mythril/laser/ethereum/keccak.py @@ -1,6 +1,7 @@ """This module contains a function manager to deal with symbolic Keccak values.""" -from mythril.laser.smt import Expression +from mythril.laser.smt import Expression, BitVecFunc, BitVec +from typing import cast, Union class KeccakFunctionManager: @@ -16,7 +17,9 @@ class KeccakFunctionManager: :param expression: :return: """ - return str(expression) in self.keccak_expression_mapping.keys() + if not isinstance(expression, BitVecFunc): + return False + return expression.func_name == "keccak256" def get_argument(self, expression: Expression) -> Expression: """ @@ -26,13 +29,4 @@ class KeccakFunctionManager: """ if not self.is_keccak(expression): raise ValueError("Expression is not a recognized keccac result") - return self.keccak_expression_mapping[str(expression)][1] - - def add_keccak(self, expression: Expression, argument: Expression) -> None: - """ - - :param expression: - :param argument: - """ - index = str(expression) - self.keccak_expression_mapping[index] = (expression, argument) + return cast(BitVecFunc, expression).input_ diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index def5048e..f8a131cb 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -73,7 +73,7 @@ def execute_contract_creation( del laser_evm.open_states[:] new_account = laser_evm.world_state.create_account( - 0, concrete_storage=True, dynamic_loader=None, creator=CREATOR_ADDRESS + 0, concrete_storage=False, dynamic_loader=None, creator=CREATOR_ADDRESS ) if contract_name: new_account.contract_name = contract_name diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 3c5aabf4..5a65443e 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -154,7 +154,7 @@ class ContractCreationTransaction(BaseTransaction): super().__init__(*args, **kwargs, init_call_data=False) # type: ignore # TODO: set correct balance for new account self.callee_account = self.callee_account or self.world_state.create_account( - 0, concrete_storage=True + 0, concrete_storage=False ) def initial_global_state(self) -> GlobalState: diff --git a/mythril/laser/smt/__init__.py b/mythril/laser/smt/__init__.py index d849d0c4..c0f2732c 100644 --- a/mythril/laser/smt/__init__.py +++ b/mythril/laser/smt/__init__.py @@ -72,7 +72,7 @@ class SymbolFactory(Generic[T, U]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: Expression = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value. @@ -91,7 +91,7 @@ class SymbolFactory(Generic[T, U]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: Expression = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value. @@ -140,7 +140,7 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: Expression = None, ) -> BitVecFunc: """Creates a new bit vector function with a concrete value.""" raw = z3.BitVecVal(value, size) @@ -152,7 +152,7 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]): func_name: str, size: int, annotations: Annotations = None, - input_: Union[int, "BitVec"] = None, + input_: Expression = None, ) -> BitVecFunc: """Creates a new bit vector function with a symbolic value.""" raw = z3.BitVec(name, size) diff --git a/mythril/laser/smt/bitvec.py b/mythril/laser/smt/bitvec.py index 05081137..67224243 100644 --- a/mythril/laser/smt/bitvec.py +++ b/mythril/laser/smt/bitvec.py @@ -243,6 +243,9 @@ class BitVec(Expression[z3.BitVecRef]): """ return self._handle_shift(other, rshift) + def __hash__(self): + return self.raw.__hash__() + def _comparison_helper( a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool diff --git a/mythril/laser/smt/bitvecfunc.py b/mythril/laser/smt/bitvecfunc.py index f73ef504..54756025 100644 --- a/mythril/laser/smt/bitvecfunc.py +++ b/mythril/laser/smt/bitvecfunc.py @@ -2,6 +2,7 @@ from typing import Optional, Union, cast, Callable import z3 +from mythril.laser.smt.expression import Expression from mythril.laser.smt.bitvec import BitVec, Bool, And, Annotations from mythril.laser.smt.bool import Or @@ -26,6 +27,7 @@ def _arithmetic_helper( union = a.annotations + b.annotations if isinstance(b, BitVecFunc): + # TODO: Find better value to set input and name to in this case? return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union) @@ -79,7 +81,7 @@ class BitVecFunc(BitVec): self, raw: z3.BitVecRef, func_name: Optional[str], - input_: Union[int, "BitVec"] = None, + input_: Expression = None, annotations: Optional[Annotations] = None, ): """ @@ -223,3 +225,6 @@ class BitVecFunc(BitVec): :return The resulting right shifted output: """ return _arithmetic_helper(self, other, operator.rshift) + + def __hash__(self) -> int: + return self.raw.__hash__() diff --git a/mythril/laser/smt/bool.py b/mythril/laser/smt/bool.py index 9fa097e4..41f82d49 100644 --- a/mythril/laser/smt/bool.py +++ b/mythril/laser/smt/bool.py @@ -80,6 +80,9 @@ class Bool(Expression[z3.BoolRef]): else: return False + def __hash__(self) -> int: + return self.raw.__hash__() + def And(*args: Union[Bool, bool]) -> Bool: """Create an And expression.""" diff --git a/mythril/laser/smt/expression.py b/mythril/laser/smt/expression.py index 8e9e697e..ae98cd31 100644 --- a/mythril/laser/smt/expression.py +++ b/mythril/laser/smt/expression.py @@ -45,6 +45,12 @@ class Expression(Generic[T]): def __repr__(self) -> str: return repr(self.raw) + def size(self): + return self.raw.size() + + def __hash__(self) -> int: + return self.raw.__hash__() + G = TypeVar("G", bound=Expression) diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 6227b3ce..fc84d20a 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -2,7 +2,7 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.state.account import Account from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.transaction.concolic import execute_message_call -from mythril.laser.smt import Expression, BitVec +from mythril.laser.smt import Expression, BitVec, symbol_factory from mythril.analysis.solver import get_model from datetime import datetime @@ -139,7 +139,7 @@ def test_vmtest( for index, value in details["storage"].items(): expected = int(value, 16) - actual = account.storage[int(index, 16)] + actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)] if isinstance(actual, Expression): actual = actual.value actual = 1 if actual is True else 0 if actual is False else actual diff --git a/tests/testdata/outputs_expected/overflow.sol.o.graph.html b/tests/testdata/outputs_expected/overflow.sol.o.graph.html index 70210177..a245f3a4 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.graph.html +++ b/tests/testdata/outputs_expected/overflow.sol.o.graph.html @@ -24,8 +24,8 @@ @@ -59,4 +59,4 @@ }); - + \ No newline at end of file diff --git a/tests/testdata/outputs_expected/overflow.sol.o.json b/tests/testdata/outputs_expected/overflow.sol.o.json index 89fdb839..c8d029f7 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.json +++ b/tests/testdata/outputs_expected/overflow.sol.o.json @@ -26,6 +26,19 @@ "sourceMap": null, "swc-id": "101", "title": "Integer Underflow" + }, + { + "address": 725, + "contract": "Unknown", + "debug": "", + "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 78155, + "min_gas_used": 17019, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Overflow" } ], "success": true diff --git a/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 b/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 index dfcc29d5..570fdeba 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 +++ b/tests/testdata/outputs_expected/overflow.sol.o.jsonv2 @@ -34,6 +34,23 @@ "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow" + }, + { + "description": { + "head": "The binary addition can overflow.", + "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." + }, + "extra": { + "discoveryTime": "" + }, + "locations": [ + { + "sourceMap": "725:1:0" + } + ], + "severity": "High", + "swcID": "SWC-101", + "swcTitle": "Integer Overflow and Underflow" } ], "meta": {}, diff --git a/tests/testdata/outputs_expected/overflow.sol.o.markdown b/tests/testdata/outputs_expected/overflow.sol.o.markdown index 8774d894..82642a1e 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/overflow.sol.o.markdown @@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. + +## Integer Overflow +- SWC ID: 101 +- Severity: High +- Contract: Unknown +- Function name: `sendeth(address,uint256)` +- PC address: 725 +- Estimated Gas Usage: 17019 - 78155 + +### Description + +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. diff --git a/tests/testdata/outputs_expected/overflow.sol.o.text b/tests/testdata/outputs_expected/overflow.sol.o.text index 698665d8..e70dda5b 100644 --- a/tests/testdata/outputs_expected/overflow.sol.o.text +++ b/tests/testdata/outputs_expected/overflow.sol.o.text @@ -20,3 +20,14 @@ The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- +==== Integer Overflow ==== +SWC ID: 101 +Severity: High +Contract: Unknown +Function name: sendeth(address,uint256) +PC address: 725 +Estimated Gas Usage: 17019 - 78155 +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. +-------------------- + diff --git a/tests/testdata/outputs_expected/underflow.sol.o.graph.html b/tests/testdata/outputs_expected/underflow.sol.o.graph.html index 62381211..64d31932 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.graph.html +++ b/tests/testdata/outputs_expected/underflow.sol.o.graph.html @@ -24,8 +24,8 @@ diff --git a/tests/testdata/outputs_expected/underflow.sol.o.json b/tests/testdata/outputs_expected/underflow.sol.o.json index 6a2464d5..a0042598 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.json +++ b/tests/testdata/outputs_expected/underflow.sol.o.json @@ -26,6 +26,19 @@ "sourceMap": null, "swc-id": "101", "title": "Integer Underflow" + }, + { + "address": 725, + "contract": "Unknown", + "debug": "", + "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.", + "function": "sendeth(address,uint256)", + "max_gas_used": 52861, + "min_gas_used": 11915, + "severity": "High", + "sourceMap": null, + "swc-id": "101", + "title": "Integer Overflow" } ], "success": true diff --git a/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 b/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 index 94854e04..b6611bdd 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 +++ b/tests/testdata/outputs_expected/underflow.sol.o.jsonv2 @@ -34,6 +34,23 @@ "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow" + }, + { + "description": { + "head": "The binary addition can overflow.", + "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion." + }, + "extra": { + "discoveryTime": "" + }, + "locations": [ + { + "sourceMap": "725:1:0" + } + ], + "severity": "High", + "swcID": "SWC-101", + "swcTitle": "Integer Overflow and Underflow" } ], "meta": {}, diff --git a/tests/testdata/outputs_expected/underflow.sol.o.markdown b/tests/testdata/outputs_expected/underflow.sol.o.markdown index 48399072..acc444d4 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.markdown +++ b/tests/testdata/outputs_expected/underflow.sol.o.markdown @@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. + +## Integer Overflow +- SWC ID: 101 +- Severity: High +- Contract: Unknown +- Function name: `sendeth(address,uint256)` +- PC address: 725 +- Estimated Gas Usage: 11915 - 52861 + +### Description + +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. diff --git a/tests/testdata/outputs_expected/underflow.sol.o.text b/tests/testdata/outputs_expected/underflow.sol.o.text index 16701a04..498ff588 100644 --- a/tests/testdata/outputs_expected/underflow.sol.o.text +++ b/tests/testdata/outputs_expected/underflow.sol.o.text @@ -20,3 +20,14 @@ The binary subtraction can underflow. The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion. -------------------- +==== Integer Overflow ==== +SWC ID: 101 +Severity: High +Contract: Unknown +Function name: sendeth(address,uint256) +PC address: 725 +Estimated Gas Usage: 11915 - 52861 +The binary addition can overflow. +The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion. +-------------------- + From 7bce67d7ae308d6a9c019228dd6cb322325c6253 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 14 May 2019 16:15:12 +0530 Subject: [PATCH 2/4] Refactor the keccakmanager and use concrete storage --- mythril/laser/ethereum/instructions.py | 24 +++++++------------ mythril/laser/ethereum/keccak.py | 14 +++++------ .../laser/ethereum/transaction/symbolic.py | 2 +- .../transaction/transaction_models.py | 2 +- 4 files changed, 17 insertions(+), 25 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 70ffe84c..7c5d099f 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -56,8 +56,6 @@ log = logging.getLogger(__name__) TT256 = 2 ** 256 TT256M1 = 2 ** 256 - 1 -keccak_function_manager = KeccakFunctionManager() - class StateTransition(object): """Decorator that handles global state copy and original return. @@ -901,7 +899,6 @@ class Instruction: :param global_state: :return: """ - global keccak_function_manager state = global_state.mstate op0, op1 = state.stack.pop(), state.stack.pop() @@ -1360,25 +1357,24 @@ class Instruction: :param global_state: :return: """ - global keccak_function_manager state = global_state.mstate index = state.stack.pop() log.debug("Storage access at index " + str(index)) index = simplify(index) - if not keccak_function_manager.is_keccak(index): + if not KeccakFunctionManager.is_keccak(index): return self._sload_helper(global_state, index) storage_keys = global_state.environment.active_account.storage.keys() - keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys)) + keccak_keys = list(filter(KeccakFunctionManager.is_keccak, storage_keys)) results = [] # type: List[GlobalState] constraints = [] for keccak_key in keccak_keys: - key_argument = keccak_function_manager.get_argument(keccak_key) - index_argument = keccak_function_manager.get_argument(index) + key_argument = KeccakFunctionManager.get_argument(keccak_key) + index_argument = KeccakFunctionManager.get_argument(index) if key_argument.size() != index_argument.size(): continue constraints.append((keccak_key, key_argument == index_argument)) @@ -1430,11 +1426,10 @@ class Instruction: :param this_key: :param argument: """ - global keccak_function_manager for keccak_key in keccak_keys: if keccak_key == this_key: continue - keccak_argument = keccak_function_manager.get_argument(keccak_key) + keccak_argument = KeccakFunctionManager.get_argument(keccak_key) yield keccak_argument != argument @StateTransition() @@ -1444,27 +1439,26 @@ class Instruction: :param global_state: :return: """ - global keccak_function_manager state = global_state.mstate index, value = state.stack.pop(), state.stack.pop() log.debug("Write to storage[" + str(index) + "]") index = simplify(index) - is_keccak = keccak_function_manager.is_keccak(index) + is_keccak = KeccakFunctionManager.is_keccak(index) if not is_keccak: return self._sstore_helper(global_state, index, value) storage_keys = global_state.environment.active_account.storage.keys() - keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys) + keccak_keys = filter(KeccakFunctionManager.is_keccak, storage_keys) results = [] # type: List[GlobalState] new = symbol_factory.Bool(False) for keccak_key in keccak_keys: - key_argument = keccak_function_manager.get_argument( + key_argument = KeccakFunctionManager.get_argument( keccak_key ) # type: Expression - index_argument = keccak_function_manager.get_argument( + index_argument = KeccakFunctionManager.get_argument( index ) # type: Expression if key_argument.size() != index_argument.size(): diff --git a/mythril/laser/ethereum/keccak.py b/mythril/laser/ethereum/keccak.py index 1d838961..81f36f14 100644 --- a/mythril/laser/ethereum/keccak.py +++ b/mythril/laser/ethereum/keccak.py @@ -7,11 +7,8 @@ from typing import cast, Union class KeccakFunctionManager: """A keccak function manager for symbolic expressions.""" - def __init__(self): - """""" - self.keccak_expression_mapping = {} - - def is_keccak(self, expression: Expression) -> bool: + @staticmethod + def is_keccak(expression: Expression) -> bool: """ :param expression: @@ -21,12 +18,13 @@ class KeccakFunctionManager: return False return expression.func_name == "keccak256" - def get_argument(self, expression: Expression) -> Expression: + @staticmethod + def get_argument(expression: Expression) -> Expression: """ :param expression: :return: """ - if not self.is_keccak(expression): - raise ValueError("Expression is not a recognized keccac result") + if not KeccakFunctionManager.is_keccak(expression): + raise ValueError("Expression is not a recognized keccak result") return cast(BitVecFunc, expression).input_ diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index f8a131cb..def5048e 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -73,7 +73,7 @@ def execute_contract_creation( del laser_evm.open_states[:] new_account = laser_evm.world_state.create_account( - 0, concrete_storage=False, dynamic_loader=None, creator=CREATOR_ADDRESS + 0, concrete_storage=True, dynamic_loader=None, creator=CREATOR_ADDRESS ) if contract_name: new_account.contract_name = contract_name diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 5a65443e..3c5aabf4 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -154,7 +154,7 @@ class ContractCreationTransaction(BaseTransaction): super().__init__(*args, **kwargs, init_call_data=False) # type: ignore # TODO: set correct balance for new account self.callee_account = self.callee_account or self.world_state.create_account( - 0, concrete_storage=False + 0, concrete_storage=True ) def initial_global_state(self) -> GlobalState: From 7143822ee597132a88c3703dd2cf0ec0d8c9c89b Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 7 Jun 2019 12:59:23 +0530 Subject: [PATCH 3/4] Fix errors based on recent changes --- mythril/laser/ethereum/instructions.py | 4 +--- tests/laser/evm_testsuite/evm_test.py | 5 ++++- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index bf03a6de..6c751564 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1407,9 +1407,7 @@ class Instruction: return self._sload_helper(global_state, index) @staticmethod - def _sload_helper( - global_state: GlobalState, index: Union[str, int], constraints=None - ): + def _sload_helper(global_state: GlobalState, index: Expression, constraints=None): """ :param global_state: diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 2bdcecb2..51b61b30 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -114,6 +114,8 @@ def test_vmtest( post_condition: dict, ) -> None: + if test_name != "JDfromStorageDynamicJump0_jumpdest0": + return # Arrange if test_name in ignored_test_names: return @@ -125,7 +127,8 @@ def test_vmtest( account.code = Disassembly(details["code"][2:]) account.nonce = int(details["nonce"], 16) for key, value in details["storage"].items(): - account.storage[int(key, 16)] = int(value, 16) + key_bitvec = symbol_factory.BitVecVal(int(key, 16), 256) + account.storage[key_bitvec] = int(value, 16) world_state.put_account(account) account.set_balance(int(details["balance"], 16)) From 18f22f57755837d5404090b49d60ffd37dee87bc Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Fri, 7 Jun 2019 13:30:36 +0530 Subject: [PATCH 4/4] Fix type hints and more merge conflicts --- mythril/laser/ethereum/state/account.py | 10 +++++----- tests/laser/evm_testsuite/evm_test.py | 2 -- 2 files changed, 5 insertions(+), 7 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index e806a71e..7a037792 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -7,7 +7,7 @@ from typing import Any, Dict, KeysView, Union from z3 import ExprRef -from mythril.laser.smt import Array, symbol_factory, BitVec +from mythril.laser.smt import Array, symbol_factory, BitVec, Expression from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory @@ -20,12 +20,12 @@ class Storage: :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic """ - self._storage = {} # type: Dict[Union[int, str], Any] + self._storage = {} # type: Dict[Expression, Any] self.concrete = concrete self.dynld = dynamic_loader self.address = address - def __getitem__(self, item: Union[str, int]) -> Any: + def __getitem__(self, item: Expression) -> Any: try: return self._storage[item] except KeyError: @@ -38,7 +38,7 @@ class Storage: self._storage[item] = symbol_factory.BitVecVal( int( self.dynld.read_storage( - contract_address=self.address, index=int(item) + contract_address=self.address, index=int(item.raw) ), 16, ), @@ -56,7 +56,7 @@ class Storage: ) return self._storage[item] - def __setitem__(self, key: Union[int, str], value: Any) -> None: + def __setitem__(self, key: Expression, value: Any) -> None: self._storage[key] = value def keys(self) -> KeysView: diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py index 51b61b30..184cfeab 100644 --- a/tests/laser/evm_testsuite/evm_test.py +++ b/tests/laser/evm_testsuite/evm_test.py @@ -114,8 +114,6 @@ def test_vmtest( post_condition: dict, ) -> None: - if test_name != "JDfromStorageDynamicJump0_jumpdest0": - return # Arrange if test_name in ignored_test_names: return