Update security checks

mythril/analysis/modules/ether_send.py

@@ -1,6 +1,8 @@
 from z3 import *
 from mythril.analysis.ops import *
+from mythril.analysis import solver
 from mythril.analysis.report import Issue
+from mythril.exceptions import UnsatError
 import re
 import logging
 
@@ -41,6 +43,8 @@ def execute(statespace):
             issue.description += "a non-zero amount of Ether is sent to an address taken from function arguments.\n"
             interesting = True
 
+        issue.description += "Call value is " + str(call.value) + "\n"
+
         if interesting:
 
             node = call.node
@@ -48,33 +52,44 @@ def execute(statespace):
             can_solve = True
 
             for constraint in node.constraints:
-                m = re.search(r'storage_([0-9a-f])+', str(constraint))
 
-                if (m):
-                    index = m.group(1)
+                m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
 
-                    write_func = statespace.find_storage_write(index)
+                can_solve = True
 
-                    if write_func is None:
-                        can_solve = False
-                        break
+                if (m):
+                    index = m.group(1)
 
-            if can_solve:
+                    try:
+                        can_write = False
 
-                s = Solver()
+                        for s in statespace.sstors[index]:
 
-                for constraint in node.constraints:
-                    s.add(constraint)
+                            if s.tainted:
+                                can_write = True
 
-                if (s.check() == sat):
+                                issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'."
+                                break
 
-                    m = s.model()
+                        if not can_write:
+                            logging.info("No storage writes to index " + str(index))
+                            can_solve = False
+                            break
 
-                    logging.debug("Model for node " + str(node.uid) + ", function " +  node.function_name + ": ")
+                    except KeyError:
+                        logging.info("No storage writes to index " + str(index))
+                        can_solve = False
+                        break
 
-                    for d in m.decls():
-                        logging.debug("%s = 0x%x" % (d.name(), m[d].as_long()))
+            if can_solve:
 
+                try:
+                    model = solver.get_model(node.constraints)
                     issues.append(issue)
 
+                    for d in model.decls():
+                        logging.debug("[UNCHECKED_SEND] %s = 0x%x" % (d.name(), model[d].as_long()))
+                except UnsatError:
+                        logging.debug("[UNCHECKED_SEND] no model found")  
+
     return issues

mythril/analysis/modules/unchecked_suicide.py

@@ -1,10 +1,13 @@
 from z3 import *
+from mythril.analysis import solver
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
+from mythril.exceptions import UnsatError
 import re
 import logging
 
 
+
 '''
 MODULE DESCRIPTION:
 
@@ -52,8 +55,9 @@ def execute(statespace):
                             can_write = False
 
                             for s in statespace.sstors[index]:
+
                                 if s.tainted:
-                                    can_write = True
+                                    can_write = Trues
 
                                     issue.description += "\nThere is a check on storage index " + str(index) + ". This storage index can be written to by calling the function '" + s.node.function_name + "'."
                                     break
@@ -70,24 +74,13 @@ def execute(statespace):
 
                 if can_solve:
 
-                    s = Solver()
-
-                    for constraint in node.constraints:
-                        s.add(constraint)
-
-                    if (s.check() == sat):
-
-                        m = s.model()
-
-                        logging.debug("Model for node " + str(node.uid) + ", function " +  node.function_name + ": ")
-
-                        for d in m.decls():
-                            logging.debug("%s = 0x%x" % (d.name(), m[d].as_long()))
-
+                    try:
+                        model = solver.get_model(node.constraints)
                         issues.append(issue)
 
-                    else:
-                        logging.debug("unsat")
-
+                        for d in model.decls():
+                            logging.debug("[UNCHECKED_SUICIDE] main model: %s = 0x%x" % (d.name(), model[d].as_long()))
+                    except UnsatError:
+                            logging.debug("[UNCHECKED_SUICIDE] no model found")         
 
     return issues

mythril/analysis/solver.py

@@ -0,0 +1,16 @@
+from z3 import *
+from mythril.exceptions import UnsatError
+
+def get_model(constraints):
+    s = Solver()
+
+    for constraint in constraints:
+        s.add(constraint)
+
+    if (s.check() == sat):
+
+        return s.model()
+
+    else:
+            raise UnsatError
+

mythril/analysis/symbolic.py

@@ -1,5 +1,8 @@
+from mythril.analysis import solver
+from mythril.exceptions import UnsatError
 from laser.ethereum import svm
 from .ops import *
+import logging
 
 
 class StateSpace:
@@ -66,18 +69,26 @@ class StateSpace:
 
     def sstor_analysis(self):
 
+        logging.debug("Analyzing storage operations...")
+
         for index in self.sstors:
             for s in self.sstors[index]:
 
-                s.tainted = True
-
-                # For now we simply 'taint' every storage location that can be written to without any constraint on msg.sender
+                # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender
 
                 for constraint in s.node.constraints:
+                    logging.debug("Constraint: " + str(constraint))
                     if ("caller" in str(constraint)):
                         s.tainted = False
                         break
 
+                    try:
+                        solver.get_model(s.node.constraints)
+                        s.tainted = True
+                    except UnsatError:
+                        s.tainted = False
+
+
 
     def find_storage_write(self, index):
 

mythril/exceptions.py

@@ -1,2 +1,5 @@
 class CompilerError(Exception):
+    pass
+
+class UnsatError(Exception):
     pass