From ec4acd85ec79aeffaffb5bb26b77dd78997b6147 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 3 Jul 2019 17:00:20 +0200 Subject: [PATCH 1/3] Fix issues in dependency pruning plugin --- .../implementations/dependency_pruner.py | 36 ++++++++++++------- 1 file changed, 23 insertions(+), 13 deletions(-) diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index 8c827d91..7afe6699 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -150,6 +150,12 @@ class DependencyPruner(LaserPlugin): :param target_location """ + log.debug( + "Updating dependency map for path: {} with location: {}".format( + path, target_location + ) + ) + try: for address in path: if address in self.dependency_map: @@ -170,13 +176,15 @@ class DependencyPruner(LaserPlugin): for address in path: self.protected_addresses.add(address) - def wanna_execute(self, address: int, storage_write_cache) -> bool: + def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool: """Decide whether the basic block starting at 'address' should be executed. :param address :param storage_write_cache """ + storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1) + if address in self.protected_addresses or address not in self.dependency_map: return True @@ -187,6 +195,14 @@ class DependencyPruner(LaserPlugin): for location in storage_write_cache: for dependency in dependencies: + try: + solver.get_model([location == dependency]) + return True + + except UnsatError: + continue + + for dependency in annotation.storage_loaded: try: solver.get_model([location == dependency]) return True @@ -216,27 +232,25 @@ class DependencyPruner(LaserPlugin): @symbolic_vm.post_hook("JUMP") def jump_hook(state: GlobalState): address = state.get_current_instruction()["address"] - annotation = get_dependency_annotation(state) - - _check_basic_block(address, annotation) - @symbolic_vm.pre_hook("JUMPDEST") - def jumpdest_hook(state: GlobalState): - address = state.get_current_instruction()["address"] annotation = get_dependency_annotation(state) + annotation.path.append(address) _check_basic_block(address, annotation) @symbolic_vm.post_hook("JUMPI") def jumpi_hook(state: GlobalState): address = state.get_current_instruction()["address"] + annotation = get_dependency_annotation(state) + annotation.path.append(address) _check_basic_block(address, annotation) @symbolic_vm.pre_hook("SSTORE") def sstore_hook(state: GlobalState): annotation = get_dependency_annotation(state) + annotation.extend_storage_write_cache( self.iteration, state.mstate.stack[-1] ) @@ -288,15 +302,11 @@ class DependencyPruner(LaserPlugin): if self.iteration < 2: return - annotation.path.append(address) - - if self.wanna_execute( - address, annotation.get_storage_write_cache(self.iteration - 1) - ): + if self.wanna_execute(address, annotation): return else: log.debug( - "Skipping state: Storage slots {} not read in block at address {}".format( + "Skipping state: Storage slots {} not read in block at address {}, function".format( annotation.get_storage_write_cache(self.iteration - 1), address ) ) From 004a9f618980cf8d5f8d77a5e70b3d36fbb5488b Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 4 Jul 2019 10:30:11 +0200 Subject: [PATCH 2/3] Add explanative comments --- .../ethereum/plugins/implementations/dependency_pruner.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index 7afe6699..962417ec 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -185,6 +185,8 @@ 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. + if address in self.protected_addresses or address not in self.dependency_map: return True @@ -195,6 +197,8 @@ class DependencyPruner(LaserPlugin): for location in storage_write_cache: for dependency in dependencies: + # Is there a known read operation along this path that matches a write in the previous transaction? + try: solver.get_model([location == dependency]) return True @@ -202,6 +206,8 @@ class DependencyPruner(LaserPlugin): except UnsatError: continue + # Has the *currently executed* path been influenced by a write operation in the previous transaction? + for dependency in annotation.storage_loaded: try: solver.get_model([location == dependency]) From f6820175bd5e966eb90ee7bac89a0d1959cb1885 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Thu, 4 Jul 2019 11:03:27 +0200 Subject: [PATCH 3/3] Change second list to tuple --- .../laser/ethereum/plugins/implementations/dependency_pruner.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index a1c6097d..7c1c0f83 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -200,7 +200,7 @@ class DependencyPruner(LaserPlugin): # Is there a known read operation along this path that matches a write in the previous transaction? try: - solver.get_model([location == dependency]) + solver.get_model((location == dependency,)) return True except UnsatError: