diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index a6836f7b..c1c5c442 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,12 @@ 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), @@ -140,7 +140,7 @@ 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 [] 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..4c47516a 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): @@ -74,7 +77,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 @@ -93,8 +96,8 @@ class Storage: ) self.printable_storage[item] = storage[item] return storage[item] - except ValueError: - pass + except ValueError as e: + log.debug("Couldn't read storage at %s: %s", item, e) 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]