Merge branch 'develop' into refactor/disassembly

mythril/analysis/symbolic.py

@@ -4,7 +4,8 @@ from mythril.ether.soliditycontract import SolidityContract
 import copy
 import logging
 from .ops import get_variable, SStore, Call, VarType
-from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy, BreadthFirstSearchStrategy
+from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy, BreadthFirstSearchStrategy, \
+    ReturnRandomNaivelyStrategy, ReturnWeightedRandomStrategy
 
 
 class SymExecWrapper:
@@ -20,6 +21,10 @@ class SymExecWrapper:
             s_strategy = DepthFirstSearchStrategy
         elif strategy == 'bfs':
             s_strategy = BreadthFirstSearchStrategy
+        elif strategy == 'naive-random':
+            s_strategy = ReturnRandomNaivelyStrategy
+        elif strategy == 'weighted-random':
+            s_strategy = ReturnWeightedRandomStrategy
         else:
             raise ValueError("Invalid strategy argument supplied")
 

mythril/interfaces/cli.py

@@ -70,8 +70,11 @@ def main():
     options = parser.add_argument_group('options')
     options.add_argument('-m', '--modules', help='Comma-separated list of security analysis modules', metavar='MODULES')
     options.add_argument('--max-depth', type=int, default=22, help='Maximum recursion depth for symbolic execution')
+
+    options.add_argument('--strategy', choices=['dfs', 'bfs', 'naive-random', 'weighted-random'],
+                         default='dfs', help='Symbolic execution strategy')
     options.add_argument('--max-transaction-count', type=int, default=3, help='Maximum number of transactions issued by laser')
-    options.add_argument('--strategy', choices=['dfs', 'bfs'], default='dfs', help='Symbolic execution strategy')
+
     options.add_argument('--execution-timeout', type=int, default=600, help="The amount of seconds to spend on symbolic execution")
     options.add_argument('--create-timeout', type=int, default=10, help="The amount of seconds to spend on "
                                                                         "the initial contract creation")

mythril/laser/ethereum/strategy/__init__.py

@@ -0,0 +1,25 @@
+from abc import ABC, abstractmethod
+
+
+class BasicSearchStrategy(ABC):
+    __slots__ = 'work_list', 'max_depth'
+
+    def __init__(self, work_list, max_depth):
+        self.work_list = work_list
+        self.max_depth = max_depth
+
+    def __iter__(self):
+        return self
+
+    @abstractmethod
+    def get_strategic_global_state(self):
+        raise NotImplementedError("Must be implemented by a subclass")
+
+    def __next__(self):
+        try:
+            global_state = self.get_strategic_global_state()
+            if global_state.mstate.depth >= self.max_depth:
+                return self.__next__()
+            return global_state
+        except IndexError:
+            raise StopIteration

mythril/laser/ethereum/strategy/basic.py

@@ -1,54 +1,67 @@
 """
 This module implements basic symbolic execution search strategies
 """
+from random import randrange
+from . import BasicSearchStrategy
 
+try:
+    from random import choices
+except ImportError:
 
-class DepthFirstSearchStrategy:
+    # This is for supporting python versions < 3.6
+    from itertools import accumulate
+    from random import random
+    from bisect import bisect
+
+    def choices(population, weights=None):
+        """
+        Returns a random element out of the population based on weight.
+        If the relative weights or cumulative weights are not specified,
+        the selections are made with equal probability.
+        """
+        if weights is None:
+            return [population[int(random() * len(population))]]
+        cum_weights = accumulate(weights)
+        return [population[bisect(cum_weights, random()*cum_weights[-1], 0, len(population)-1)]]
+
+
+class DepthFirstSearchStrategy(BasicSearchStrategy):
     """
     Implements a depth first search strategy
     I.E. Follow one path to a leaf, and then continue to the next one
     """
-    def __init__(self, work_list, max_depth):
-        self.work_list = work_list
-        self.max_depth = max_depth
-
-    def __iter__(self):
-        return self
 
-    def __next__(self):
-        """ Picks the next state to execute """
-        try:
-            # This strategies assumes that new states are appended at the end of the work_list
-            # By taking the last element we effectively pick the "newest" states, which amounts to dfs
-            global_state = self.work_list.pop()
-            if global_state.mstate.depth >= self.max_depth:
-                return self.__next__()
-            return global_state
-        except IndexError:
-            raise StopIteration()
+    def get_strategic_global_state(self):
+        return self.work_list.pop()
 
 
-class BreadthFirstSearchStrategy:
+class BreadthFirstSearchStrategy(BasicSearchStrategy):
     """
     Implements a breadth first search strategy
     I.E. Execute all states of a "level" before continuing
     """
-    def __init__(self, work_list, max_depth):
-        self.work_list = work_list
-        self.max_depth = max_depth
-
-    def __iter__(self):
-        return self
-
-    def __next__(self):
-        """ Picks the next state to execute """
-        try:
-            # This strategies assumes that new states are appended at the end of the work_list
-            # By taking the first element we effectively pick the "oldest" states, which amounts to bfs
-            global_state = self.work_list.pop(0)
-            if global_state.mstate.depth >= self.max_depth:
-                return self.__next__()
-            return global_state
-        except IndexError:
-            raise StopIteration()
+
+    def get_strategic_global_state(self):
+        return self.work_list.pop(0)
+
+
+class ReturnRandomNaivelyStrategy(BasicSearchStrategy):
+    """
+    chooses a random state from the worklist with equal likelihood
+    """
+    def get_strategic_global_state(self):
+        if len(self.work_list) > 0:
+            return self.work_list.pop(randrange(len(self.work_list)))
+        else:
+            raise IndexError
+
+
+class ReturnWeightedRandomStrategy(BasicSearchStrategy):
+    """
+    chooses a random state from the worklist with likelihood based on inverse proportion to depth
+    """
+
+    def get_strategic_global_state(self):
+        probability_distribution = [1/(global_state.mstate.depth+1) for global_state in self.work_list]
+        return self.work_list.pop(choices(range(len(self.work_list)), probability_distribution)[0])