diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 55ebf39d..e4099469 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -96,6 +96,7 @@ class SymExecWrapper: plugin_loader = LaserPluginLoader(self.laser) plugin_loader.load(PluginFactory.build_mutation_pruner_plugin()) + plugin_loader.load(PluginFactory.build_dependency_pruner_plugin()) plugin_loader.load(PluginFactory.build_instruction_coverage_plugin()) if run_analysis_modules: diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index e8d531c7..673a7f0b 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -1,68 +1,145 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.plugin import LaserPlugin -from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState +from mythril.laser.ethereum.plugins.signals import PluginSkipState from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.global_state import GlobalState -from mythril.laser.ethereum.util import get_concrete_int +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) +from typing import cast, List from copy import copy +import logging +log = logging.getLogger(__name__) -class PathAnnotation(StateAnnotation): + +class DependencyAnnotation(StateAnnotation): """Dependency Annotation - This is the annotation used to annotate paths + This annotation tracks read and write access to the state. """ def __init__(self): - self.path = [] + self.storage_loaded = [] # type: List + self.storage_written = [] # type: List + self.path = [] # type: List[int] def __copy__(self): - result = PathAnnotation() + result = DependencyAnnotation() + result.storage_loaded = copy(self.storage_loaded) + result.storage_written = copy(self.storage_written) result.path = copy(self.path) return result +def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation: + + annotations = cast( + List[DependencyAnnotation], + list(state.world_state.get_annotations(DependencyAnnotation)), + ) + if len(annotations) == 0: + annotations = cast( + List[DependencyAnnotation], + list(state.get_annotations(DependencyAnnotation)), + ) + + if len(annotations) == 0: + annotation = DependencyAnnotation() + state.annotate(annotation) + else: + annotation = annotations[0] + else: + annotation = annotations[0] + + return annotation + + class DependencyPruner(LaserPlugin): """Dependency Pruner Plugin """ def __init__(self): """Creates DependencyPruner""" - pass + self.iteration = 0 + self.dependency_map = {} # type: Dict[int, List] def _reset(self): - """Reset this plugin""" + """TODO: Reset this plugin""" pass def initialize(self, symbolic_vm: LaserEVM): """Initializes the DependencyPruner - Introduces hooks in symbolic_vm to track the desired values :param symbolic_vm """ self._reset() @symbolic_vm.laser_hook("start_sym_trans") - def start_sym_exec_hook(): - pass - - @symbolic_vm.laser_hook("stop_sym_trans") - def stop_sym_exec_hook(): - pass + def start_sym_trans_hook(): + self.iteration += 1 + logging.info("Starting iteration {}".format(self.iteration)) @symbolic_vm.pre_hook("JUMPDEST") - def mutator_hook(global_state: GlobalState): - pass + def mutator_hook(state: GlobalState): + annotation = get_dependency_annotation(state) + address = state.get_current_instruction()["address"] + + annotation.path.append(state.get_current_instruction()["address"]) + + if self.iteration < 2 or address not in self.dependency_map: + return + + if not set(annotation.storage_written).intersection( + set(self.dependency_map[address]) + ): + logging.info("Skipping state") + raise PluginSkipState @symbolic_vm.pre_hook("SSTORE") - def mutator_hook(global_state: GlobalState): - pass + def mutator_hook(state: GlobalState): + annotation = get_dependency_annotation(state) + annotation.storage_written.append(state.mstate.stack[-1]) + annotation.storage_written = list( + set(annotation.storage_written + [state.mstate.stack[-1]]) + ) + + @symbolic_vm.pre_hook("SLOAD") + def mutator_hook(state: GlobalState): + + annotation = get_dependency_annotation(state) + annotation.storage_loaded.append(state.mstate.stack[-1]) @symbolic_vm.pre_hook("STOP") - def mutator_hook(global_state: GlobalState): - pass + def mutator_hook(state: GlobalState): + annotation = get_dependency_annotation(state) + + for index in annotation.storage_loaded: + + for address in annotation.path: + + if address in self.dependency_map: + self.dependency_map[address] = list( + set(self.dependency_map[address] + [index]) + ) + else: + self.dependency_map[address] = [index] @symbolic_vm.laser_hook("add_world_state") - def world_state_filter_hook(global_state: GlobalState): - # raise PluginSkipWorldState - pass + def world_state_filter_hook(state: GlobalState): + + if isinstance(state.current_transaction, ContractCreationTransaction): + return + + annotation = get_dependency_annotation(state) + state.world_state.annotate(annotation) + + """ + log.info( + "Add World State {}\nDependency map: {}\nStorage indices written: {}".format( + state.get_current_instruction()["address"], + self.dependency_map, + annotation.storage_written, + ) + ) + """ diff --git a/mythril/laser/ethereum/plugins/plugin_factory.py b/mythril/laser/ethereum/plugins/plugin_factory.py index 1ce61b34..a81f80c4 100644 --- a/mythril/laser/ethereum/plugins/plugin_factory.py +++ b/mythril/laser/ethereum/plugins/plugin_factory.py @@ -30,3 +30,12 @@ class PluginFactory: ) return InstructionCoveragePlugin() + + @staticmethod + def build_dependency_pruner_plugin() -> LaserPlugin: + """ Creates an instance of the mutation pruner plugin""" + from mythril.laser.ethereum.plugins.implementations.dependency_pruner import ( + DependencyPruner, + ) + + return DependencyPruner() diff --git a/mythril/laser/ethereum/plugins/signals.py b/mythril/laser/ethereum/plugins/signals.py index 325f2d6a..b59614ca 100644 --- a/mythril/laser/ethereum/plugins/signals.py +++ b/mythril/laser/ethereum/plugins/signals.py @@ -15,3 +15,13 @@ class PluginSkipWorldState(PluginSignal): """ pass + + +class PluginSkipState(PluginSignal): + """ Plugin to skip world state + + Plugins that raise this signal while the add_world_state hook is being executed + will force laser to abandon that world state. + """ + + pass diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index a13cf5b7..e257e5f4 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -10,7 +10,7 @@ from mythril.laser.ethereum.evm_exceptions import StackUnderflowException from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler -from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState +from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy @@ -271,7 +271,12 @@ class LaserEVM: self._add_world_state(global_state) return [], None - self._execute_pre_hook(op_code, global_state) + try: + self._execute_pre_hook(op_code, global_state) + except PluginSkipState: + self._add_world_state(global_state) + return [], None + try: new_global_states = Instruction( op_code, self.dynamic_loader, self.iprof