From 8071a3c617870ab653a275a43da7b0ae57f9d9d0 Mon Sep 17 00:00:00 2001 From: e-ngo <52668908+e-ngo@users.noreply.github.com> Date: Thu, 25 Jul 2019 00:16:39 -0700 Subject: [PATCH 1/9] Updated jinja templates to report initial state of the transaction sequences. (#1173) --- mythril/analysis/templates/report_as_markdown.jinja2 | 6 ++++++ mythril/analysis/templates/report_as_text.jinja2 | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/mythril/analysis/templates/report_as_markdown.jinja2 b/mythril/analysis/templates/report_as_markdown.jinja2 index 4583eb26..9e690c43 100644 --- a/mythril/analysis/templates/report_as_markdown.jinja2 +++ b/mythril/analysis/templates/report_as_markdown.jinja2 @@ -26,6 +26,12 @@ In file: {{ issue.filename }}:{{ issue.lineno }} {% endif %} {% if issue.tx_sequence %} +### Initial State: + +{% for key, value in issue.tx_sequence.initialState.accounts.items() %} +Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif key == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, balance: {{value.balance}}, nonce:{{value.nonce}}, storage:{{value.storage}} +{% endfor %} + ### Transaction Sequence {% for step in issue.tx_sequence.steps %} diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2 index d7b84355..aa5c4876 100644 --- a/mythril/analysis/templates/report_as_text.jinja2 +++ b/mythril/analysis/templates/report_as_text.jinja2 @@ -19,6 +19,12 @@ In file: {{ issue.filename }}:{{ issue.lineno }} -------------------- {% endif %} {% if issue.tx_sequence %} +Initial State: + +{% for key, value in issue.tx_sequence.initialState.accounts.items() %} +Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif key == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, balance: {{value.balance}}, nonce:{{value.nonce}}, storage:{{value.storage}} +{% endfor %} + Transaction Sequence: {% for step in issue.tx_sequence.steps %} From 9cb791958d669c32d0416f9289e7ce7751d62ec8 Mon Sep 17 00:00:00 2001 From: Aleksandr Sobolev Date: Thu, 25 Jul 2019 17:18:22 +0600 Subject: [PATCH 2/9] Inject missing env variables (#1174) --- .circleci/config.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.circleci/config.yml b/.circleci/config.yml index f18896f1..ae1a05d1 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -103,6 +103,8 @@ jobs: name: Run Edelweiss command: | docker run \ + -e CIRCLE_BRANCH=$CIRCLE_BRANCH \ + -e CIRCLE_SHA1=$CIRCLE_SHA1 \ -e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \ -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \ -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \ From dbe1f5210aab74340016c441477448754943800d Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 18:24:22 +0200 Subject: [PATCH 3/9] Various small fixes. --- mythril/analysis/modules/ether_thief.py | 16 ++++++++++------ mythril/laser/ethereum/call.py | 16 ++++++++-------- mythril/laser/ethereum/instructions.py | 2 +- mythril/laser/ethereum/state/account.py | 3 ++- mythril/laser/ethereum/svm.py | 17 ++++++++++------- 5 files changed, 31 insertions(+), 23 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index a6836f7b..d7098179 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -21,7 +21,7 @@ log = logging.getLogger(__name__) DESCRIPTION = """ -Search for cases where Ether can be withdrawn to a user-specified address. +Search for cases where Ether can be withdrawn to a user-specified address. An issue is reported if: @@ -79,8 +79,6 @@ class EtherThief(DetectionModule): if instruction["opcode"] != "CALL": return [] - address = instruction["address"] - value = state.mstate.stack[-3] target = state.mstate.stack[-2] @@ -92,10 +90,10 @@ class EtherThief(DetectionModule): """ Constraint: The call value must be greater than the sum of Ether sent by the attacker over all transactions. This prevents false positives caused by legitimate refund functions. - Also constrain the addition from overflowing (otherwise the solver produces solutions with + Also constrain the addition from overflowing (otherwise the solver produces solutions with ridiculously high call values). """ - constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, False)] + constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False)] eth_sent_by_attacker = Sum( eth_sent_by_attacker, tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0), @@ -120,6 +118,8 @@ class EtherThief(DetectionModule): state.current_transaction.caller == ATTACKER_ADDRESS, ] + log.debug("Constraints: %s", constraints) + try: transaction_sequence = solver.get_transaction_sequence(state, constraints) @@ -140,9 +140,13 @@ class EtherThief(DetectionModule): gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) except UnsatError: - log.debug("[ETHER_THIEF] no model found") + log.debug("No model found") return [] + log.debug("Found ether thief issue: %s", issue.as_dict) + + log.debug("Model: %s", solver.pretty_print_model(solver.get_model(constraints))) + return [issue] diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py index 918c1d3f..b003e2fb 100644 --- a/mythril/laser/ethereum/call.py +++ b/mythril/laser/ethereum/call.py @@ -4,7 +4,7 @@ parameters for the new global state.""" import logging import re -from typing import Union, List, cast, Callable +from typing import Union, List, cast, Callable, Optional import mythril.laser.ethereum.util as util from mythril.laser.ethereum import natives @@ -84,6 +84,7 @@ def get_callee_address( except TypeError: log.debug("Symbolic call encountered") + # TODO: This is broken. Now it should be Storage[(\d+)]. match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address))) log.debug("CALL to: " + str(simplify(symbolic_to_address))) @@ -99,7 +100,7 @@ def get_callee_address( "0x{:040X}".format(environment.active_account.address.value), index ) # TODO: verify whether this happens or not - except: + except Exception: log.debug("Error accessing contract storage.") raise ValueError @@ -120,28 +121,27 @@ def get_callee_account( :param dynamic_loader: dynamic loader to use :return: Account belonging to callee """ - environment = global_state.environment accounts = global_state.accounts try: return global_state.accounts[int(callee_address, 16)] except KeyError: # We have a valid call address, but contract is not in the modules list - log.debug("Module with address " + callee_address + " not loaded.") + log.debug("Module with address %s not loaded.", callee_address) if dynamic_loader is None: - raise ValueError() + raise ValueError("dynamic_loader is None") log.debug("Attempting to load dependency") try: code = dynamic_loader.dynld(callee_address) except ValueError as error: - log.debug("Unable to execute dynamic loader because: {}".format(str(error))) + log.debug("Unable to execute dynamic loader because: %s", error) raise error if code is None: log.debug("No code returned, not a contract account?") - raise ValueError() + raise ValueError("No code returned") log.debug("Dependency loaded: " + callee_address) callee_account = Account( @@ -213,7 +213,7 @@ def native_call( call_data: BaseCalldata, memory_out_offset: Union[int, Expression], memory_out_size: Union[int, Expression], -) -> Union[List[GlobalState], None]: +) -> Optional[List[GlobalState]]: if not 0 < int(callee_address, 16) < 5: return None diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b3e3eaa6..16cb4d38 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -172,7 +172,7 @@ class Instruction: :return: """ # Generalize some ops - log.debug("Evaluating {}".format(self.op_code)) + log.debug("Evaluating %s at %i", self.op_code, global_state.mstate.pc) op = self.op_code.lower() if self.op_code.startswith("PUSH"): op = "push" diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 1a32ad37..6f50e8ec 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -93,7 +93,8 @@ class Storage: ) self.printable_storage[item] = storage[item] return storage[item] - except ValueError: + except ValueError as e: + log.debug("Couldn't read storage at %s: %s", item, e) pass return simplify(storage[item]) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index c5d5c68e..c9fc393c 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -3,7 +3,7 @@ import logging from collections import defaultdict from copy import copy from datetime import datetime, timedelta -from typing import Callable, Dict, DefaultDict, List, Tuple, Union +from typing import Callable, Dict, DefaultDict, List, Tuple, Optional from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType from mythril.laser.ethereum.evm_exceptions import StackUnderflowException @@ -75,6 +75,7 @@ class LaserEVM: self.total_states = 0 self.dynamic_loader = dynamic_loader + # TODO: What about using a deque here? self.work_list = [] # type: List[GlobalState] self.strategy = strategy(self.work_list, max_depth) self.max_depth = max_depth @@ -209,7 +210,7 @@ class LaserEVM: for hook in self._stop_sym_trans_hooks: hook() - def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]: + def exec(self, create=False, track_gas=False) -> Optional[List[GlobalState]]: """ :param create: @@ -223,6 +224,7 @@ class LaserEVM: and create and self.time + timedelta(seconds=self.create_timeout) <= datetime.now() ): + log.debug("Hit create timeout, returning.") return final_states + [global_state] if track_gas else None if ( @@ -231,6 +233,7 @@ class LaserEVM: <= datetime.now() and not create ): + log.debug("Hit execution timeout, returning.") return final_states + [global_state] if track_gas else None try: @@ -243,8 +246,7 @@ class LaserEVM: state for state in new_states if state.mstate.constraints.is_possible ] - self.manage_cfg(op_code, new_states) - + self.manage_cfg(op_code, new_states) # TODO: What about op_code is None? if new_states: self.work_list += new_states elif track_gas: @@ -265,11 +267,11 @@ class LaserEVM: def execute_state( self, global_state: GlobalState - ) -> Tuple[List[GlobalState], Union[str, None]]: - """ + ) -> Tuple[List[GlobalState], Optional[str]]: + """Execute a single instruction in global_state. :param global_state: - :return: + :return: A list of successor states. """ # Execute hooks for hook in self._execute_state_hooks: @@ -405,6 +407,7 @@ class LaserEVM: for state in new_states: self._new_node_state(state) elif opcode == "JUMPI": + assert len(new_states) <= 2 for state in new_states: self._new_node_state( state, JumpType.CONDITIONAL, state.mstate.constraints[-1] From 83f0cc966de4a5e61f3aad82820cf066acb047cc Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 18:35:37 +0200 Subject: [PATCH 4/9] Reformat with black. --- mythril/analysis/modules/ether_thief.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index d7098179..67df35cd 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -93,7 +93,9 @@ class EtherThief(DetectionModule): Also constrain the addition from overflowing (otherwise the solver produces solutions with ridiculously high call values). """ - constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False)] + constraints += [ + BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False) + ] eth_sent_by_attacker = Sum( eth_sent_by_attacker, tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0), From a2a85081f60c883c756f6b7b4e283e41900fb3de Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 19:39:01 +0200 Subject: [PATCH 5/9] Add a logger in account.py --- mythril/laser/ethereum/state/account.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 6f50e8ec..26f04a01 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -2,6 +2,7 @@ This includes classes representing accounts and their storage. """ +import logging from copy import copy, deepcopy from typing import Any, Dict, Union, Tuple, cast @@ -19,6 +20,8 @@ from mythril.laser.smt import ( from mythril.disassembler.disassembly import Disassembly from mythril.laser.smt import symbol_factory +log = logging.getLogger(__name__) + class StorageRegion: def __getitem__(self, item): From 49fbb5f82ff151484785158bd238c871cc44232e Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 20:43:25 +0200 Subject: [PATCH 6/9] Fix #1176: retrieve map items. --- mythril/laser/ethereum/state/account.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 26f04a01..b5dcb3ae 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -76,8 +76,9 @@ class Storage: if is_keccak_storage: item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] + if ( - value.value == 0 + (value.value == 0 or value.value is None) # 0 for Array, None for K and self.address and item.symbolic is False and self.address.value != 0 From 739ac0337b60740c06a148b4233333a6b0cff4f1 Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 20:49:05 +0200 Subject: [PATCH 7/9] Fix #1176: load map items --- mythril/laser/ethereum/state/account.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 1a32ad37..07e82fad 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -74,7 +74,7 @@ class Storage: item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] if ( - value.value == 0 + (value.value == 0 or value.value is None) # 0 for Array, None for K and self.address and item.symbolic is False and self.address.value != 0 From d22b791ba733474814805ff9447862ec548a9171 Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 21:40:55 +0200 Subject: [PATCH 8/9] Remove logging messages, and a "pass" --- mythril/analysis/modules/ether_thief.py | 6 ------ mythril/laser/ethereum/state/account.py | 1 - 2 files changed, 7 deletions(-) diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index 67df35cd..c1c5c442 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -120,8 +120,6 @@ class EtherThief(DetectionModule): state.current_transaction.caller == ATTACKER_ADDRESS, ] - log.debug("Constraints: %s", constraints) - try: transaction_sequence = solver.get_transaction_sequence(state, constraints) @@ -145,10 +143,6 @@ class EtherThief(DetectionModule): log.debug("No model found") return [] - log.debug("Found ether thief issue: %s", issue.as_dict) - - log.debug("Model: %s", solver.pretty_print_model(solver.get_model(constraints))) - return [issue] diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index b5dcb3ae..929efea7 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -99,7 +99,6 @@ class Storage: return storage[item] except ValueError as e: log.debug("Couldn't read storage at %s: %s", item, e) - pass return simplify(storage[item]) From 0844497e412c59df4cb0ed1aecdfdf7c3210dce9 Mon Sep 17 00:00:00 2001 From: palkeo Date: Mon, 29 Jul 2019 22:06:39 +0200 Subject: [PATCH 9/9] =?UTF-8?q?Revert=20commit=20that=20should=20not=20hav?= =?UTF-8?q?e=20been=20here=20(other=C2=A0PR)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mythril/laser/ethereum/state/account.py | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py index 929efea7..07fb4323 100644 --- a/mythril/laser/ethereum/state/account.py +++ b/mythril/laser/ethereum/state/account.py @@ -76,9 +76,8 @@ class Storage: if is_keccak_storage: item = self._sanitize(cast(BitVecFunc, item).input_) value = storage[item] - if ( - (value.value == 0 or value.value is None) # 0 for Array, None for K + value.value == 0 and self.address and item.symbolic is False and self.address.value != 0