diff --git a/mythril/__version__.py b/mythril/__version__.py index e9c67101..069a8c91 100644 --- a/mythril/__version__.py +++ b/mythril/__version__.py @@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well as for importing into Python. """ -__version__ = "v0.21.8" +__version__ = "v0.21.9" diff --git a/mythril/analysis/modules/dos.py b/mythril/analysis/modules/dos.py index d691f1ab..20426727 100644 --- a/mythril/analysis/modules/dos.py +++ b/mythril/analysis/modules/dos.py @@ -80,9 +80,11 @@ class DosModule(DetectionModule): if annotation.loop_start is not None: return [] - - target = util.get_concrete_int(state.mstate.stack[-1]) - + try: + target = util.get_concrete_int(state.mstate.stack[-1]) + except TypeError: + log.debug("Symbolic target encountered in dos module") + return [] if target in annotation.jump_targets: annotation.jump_targets[target] += 1 else: diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index ae1faf2c..104dbb4c 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -135,7 +135,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]): data["storage"] = str(account.storage) data["balance"] = min_price_dict.get(address, 0) accounts[hex(address)] = data - return accounts + return {"accounts": accounts} def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index 7c1c0f83..bb78fdd8 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -7,7 +7,6 @@ from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) from mythril.exceptions import UnsatError -from z3.z3types import Z3Exception from mythril.analysis import solver from typing import cast, List, Dict, Set from copy import copy @@ -26,15 +25,15 @@ class DependencyAnnotation(StateAnnotation): def __init__(self): self.storage_loaded = [] # type: List self.storage_written = {} # type: Dict[int, List] - self.has_call = False self.path = [0] # type: List + self.blocks_seen = set() # type: Set[int] def __copy__(self): result = DependencyAnnotation() result.storage_loaded = copy(self.storage_loaded) result.storage_written = copy(self.storage_written) result.path = copy(self.path) - result.has_call = self.has_call + result.blocks_seen = copy(self.blocks_seen) return result def get_storage_write_cache(self, iteration: int): @@ -44,15 +43,10 @@ class DependencyAnnotation(StateAnnotation): return self.storage_written[iteration] def extend_storage_write_cache(self, iteration: int, value: object): - try: - if iteration not in self.storage_written: - self.storage_written[iteration] = [value] - else: - if value not in self.storage_written[iteration]: - self.storage_written[iteration].append(value) - except Z3Exception as e: - # FIXME: This should not happen unless there's a bug in laser such as a BitVec512 being generated - log.debug("Error updating storage write cache: {}".format(e)) + if iteration not in self.storage_written: + self.storage_written[iteration] = [value] + elif value not in self.storage_written[iteration]: + self.storage_written[iteration].append(value) class WSDependencyAnnotation(StateAnnotation): @@ -140,41 +134,37 @@ class DependencyPruner(LaserPlugin): def _reset(self): self.iteration = 0 - self.dependency_map = {} # type: Dict[int, List[object]] - self.protected_addresses = set() # type: Set[int] + self.sloads_on_path = {} # type: Dict[int, List[object]] + self.sstores_on_path = {} # type: Dict[int, List[object]] + self.storage_accessed_global = set() # type: Set - def update_dependency_map(self, path: List[int], target_location: object) -> None: + def update_sloads(self, path: List[int], target_location: object) -> None: """Update the dependency map for the block offsets on the given path. :param path :param target_location """ - log.debug( - "Updating dependency map for path: {} with location: {}".format( - path, target_location - ) - ) + for address in path: + if address in self.sloads_on_path: + if target_location not in self.sloads_on_path[address]: + self.sloads_on_path[address].append(target_location) + else: + self.sloads_on_path[address] = [target_location] - try: - for address in path: - if address in self.dependency_map: - if target_location not in self.dependency_map[address]: - self.dependency_map[address].append(target_location) - else: - self.dependency_map[address] = [target_location] - except Z3Exception as e: - # FIXME: This should not happen unless there's a bug in laser such as a BitVec512 being generated - log.debug("Error updating dependency map: {}".format(e)) - - def protect_path(self, path: List[int]) -> None: - """Prevent an execution path of being pruned. + def update_sstores(self, path: List[int], target_location: object) -> None: + """Update the dependency map for the block offsets on the given path. :param path + :param target_location """ for address in path: - self.protected_addresses.add(address) + if address in self.sstores_on_path: + if target_location not in self.sstores_on_path[address]: + self.sstores_on_path[address].append(target_location) + else: + self.sstores_on_path[address] = [target_location] def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool: """Decide whether the basic block starting at 'address' should be executed. @@ -185,14 +175,25 @@ class DependencyPruner(LaserPlugin): storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1) - # Execute the block if it's marked as "protected" or doesn't yet have an entry in the dependency map. + # Skip "pure" paths that don't have any dependencies. - if address in self.protected_addresses or address not in self.dependency_map: - return True + if address not in self.sloads_on_path: + return False - dependencies = self.dependency_map[address] + # Execute the path if there are state modifications along it that *could* be relevant - # Return if *any* dependency is found + if address in self.storage_accessed_global: + for location in self.sstores_on_path: + try: + solver.get_model((location == address,)) + return True + + except UnsatError: + continue + + dependencies = self.sloads_on_path[address] + + # Execute the path if there's any dependency on state modified in the previous transaction for location in storage_write_cache: for dependency in dependencies: @@ -228,13 +229,6 @@ class DependencyPruner(LaserPlugin): def start_sym_trans_hook(): self.iteration += 1 - @symbolic_vm.post_hook("CALL") - def call_hook(state: GlobalState): - annotation = get_dependency_annotation(state) - - annotation.has_call = True - self.protect_path(annotation.path) - @symbolic_vm.post_hook("JUMP") def jump_hook(state: GlobalState): address = state.get_current_instruction()["address"] @@ -257,9 +251,10 @@ class DependencyPruner(LaserPlugin): def sstore_hook(state: GlobalState): annotation = get_dependency_annotation(state) - annotation.extend_storage_write_cache( - self.iteration, state.mstate.stack[-1] - ) + location = state.mstate.stack[-1] + + self.update_sstores(annotation.path, location) + annotation.extend_storage_write_cache(self.iteration, location) @symbolic_vm.pre_hook("SLOAD") def sload_hook(state: GlobalState): @@ -272,7 +267,8 @@ class DependencyPruner(LaserPlugin): # We backwards-annotate the path here as sometimes execution never reaches a stop or return # (and this may change in a future transaction). - self.update_dependency_map(annotation.path, location) + self.update_sloads(annotation.path, location) + self.storage_accessed_global.add(location) @symbolic_vm.pre_hook("STOP") def stop_hook(state: GlobalState): @@ -291,11 +287,11 @@ class DependencyPruner(LaserPlugin): annotation = get_dependency_annotation(state) - if annotation.has_call: - self.protect_path(annotation.path) - for index in annotation.storage_loaded: - self.update_dependency_map(annotation.path, index) + self.update_sloads(annotation.path, index) + + for index in annotation.storage_written: + self.update_sstores(annotation.path, index) def _check_basic_block(address: int, annotation: DependencyAnnotation): """This method is where the actual pruning happens. @@ -308,6 +304,11 @@ class DependencyPruner(LaserPlugin): if self.iteration < 2: return + # Don't skip newly discovered blocks + if address not in annotation.blocks_seen: + annotation.blocks_seen.add(address) + return + if self.wanna_execute(address, annotation): return else: @@ -335,7 +336,6 @@ class DependencyPruner(LaserPlugin): annotation.path = [0] annotation.storage_loaded = [] - annotation.has_call = False world_state_annotation.annotations_stack.append(annotation) @@ -344,7 +344,7 @@ class DependencyPruner(LaserPlugin): self.iteration, state.get_current_instruction()["address"], state.node.function_name, - self.dependency_map, + self.sloads_on_path, annotation.storage_written[self.iteration], ) )