Refactor analysis modules

mythril/analysis/modules/delegatecall.py

@@ -25,7 +25,6 @@ def execute(statespace):
             if (call.node.function_name == "fallback"):
 
                 stack = state.mstate.stack
-
                 meminstart = get_variable(stack[-3])
 
                 if meminstart.type == VarType.CONCRETE:

mythril/analysis/modules/ether_send.py

@@ -39,7 +39,7 @@ def execute(statespace):
 
         interesting = False
 
-        description = "In the function '" + call.node.function_name +"' "
+        description = "In the function '" + call.node.function_name + "' "
 
         if re.search(r'caller', str(call.to)):
             description += "a non-zero amount of Ether is sent to msg.sender.\n"
@@ -55,10 +55,12 @@ def execute(statespace):
             if (m):
                 idx = m.group(1)
 
+                description += "a non-zero amount of Ether is sent to an address taken from storage slot " + str(idx)
+
                 func = statespace.find_storage_write(idx)
 
                 if (func):
-                    description += "\nThere is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function '" + func + "'.\n"
+                    description += "There is a check on storage index " + str(idx) + ". This storage slot can be written to by calling the function '" + func + "'.\n"
                     interesting = True
                 else:
                     logging.debug("[ETHER_SEND] No storage writes to index " + str(idx))
@@ -108,12 +110,13 @@ def execute(statespace):
 
                 try:
                     model = solver.get_model(node.constraints)
-                    logging.debug("[ETHER_SEND] MODEL: " + str(model))
 
                     for d in model.decls():
                         logging.debug("[ETHER_SEND] main model: %s = 0x%x" % (d.name(), model[d].as_long()))
 
-                    issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning", description)
+                    debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
+
+                    issue = Issue(call.node.contract_name, call.node.function_name, address, "Ether send", "Warning", description, debug)
                     issues.append(issue)
 
                 except UnsatError:

mythril/analysis/modules/exceptions.py

@@ -1,14 +1,14 @@
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
 from mythril.analysis import solver
-from z3 import simplify
 import logging
 
 
 '''
 MODULE DESCRIPTION:
 
-Check for constraints on tx.origin (i.e., access to some functionality is restricted to a specific origin).
+Checks whether any exception states are reachable.
+
 '''
 
 
@@ -27,30 +27,18 @@ def execute(statespace):
 
             if(instruction['opcode'] == "ASSERT_FAIL"):
 
-                logging.debug("Opcode 0xfe detected.")
-
                 try:
                     model = solver.get_model(node.constraints)
-                    logging.debug("[EXCEPTIONS] MODEL: " + str(model))
-
                     address = state.get_current_instruction()['address']
 
                     description = "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. "
                     description += "This is acceptable in most situations. Note however that assert() should only be used to check invariants. Use require() for regular input checking. "
-                    description += "The exception is triggered under the following conditions:\n\n"
-
-                    for d in model.decls():
-
-                        try:
-                            condition = hex(model[d].as_long())
-                        except:
-                            condition = str(simplify(model[d]))
 
-                        description += ("%s: %s\n" % (d.name(), condition))
+                    debug = "The exception is triggered under the following conditions:\n\n"
 
-                    description += "\n"
+                    debug += solver.pretty_print_model(model)
 
-                    issues.append(Issue(node.contract_name, node.function_name, address, "Exception state", "Informational", description))
+                    issues.append(Issue(node.contract_name, node.function_name, address, "Exception state", "Informational", description, debug))
 
                 except UnsatError:
                     logging.debug("[EXCEPTIONS] no model found")

mythril/analysis/modules/external_calls.py

@@ -1,6 +1,7 @@
 from z3 import *
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
+from mythril.analysis import solver
 import re
 import logging
 

mythril/analysis/modules/integer.py

@@ -4,6 +4,7 @@ from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.exceptions import UnsatError
 import re
+import copy
 import logging
 
 
@@ -14,6 +15,7 @@ Check for integer underflows.
 For every SUB instruction, check if there's a possible state where op1 > op0.
 '''
 
+
 def execute(statespace):
 
     logging.debug("Executing module: INTEGER")
@@ -43,13 +45,11 @@ def execute(statespace):
                     or (re.search(r'256\*.*If\(1', str(op0), re.DOTALL) or re.search(r'256\*.*If\(1', str(op1), re.DOTALL)) \
                     or (re.search(r'32 \+.*calldata', str(op0), re.DOTALL) or re.search(r'32 \+.*calldata', str(op1), re.DOTALL)):
 
-                    # Filter for patterns that contain possible (but apparently non-exploitable) Integer underflows.
+                    # Filter for patterns that contain bening nteger underflows.
 
                     # Pattern 1: (96 + calldatasize_MAIN) - (96), where (96 + calldatasize_MAIN) would underflow if calldatasize is very large.
                     # Pattern 2: (256*If(1 & storage_0 == 0, 1, 0)) - 1, this would underlow if storage_0 = 0
 
-                    # Both seem to be standard compiler outputs that exist in many contracts.
-
                     continue
 
                 logging.debug("[INTEGER_UNDERFLOW] Checking SUB " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address']))
@@ -60,22 +60,18 @@ def execute(statespace):
                     constraints.append(UGT(op1,op0))
 
                     try:
-                        
+
                         model = solver.get_model(constraints)
 
                         issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Underflow", "Warning")
 
                         issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \
-                            "The SUB instruction at address " + str(instruction['address']) + " may result in a value < 0." 
-
-                        issue.debug = "(" + str(op0) + ") - (" + str(op1) + ").]"
+                            "The substraction may result in a value < 0."
 
+                        issue.debug = solver.pretty_print_model(model)
                         issues.append(issue)
 
-                        for d in model.decls():
-                            logging.debug("[INTEGER_UNDERFLOW] model: %s = 0x%x" % (d.name(), model[d].as_long()))
-
                     except UnsatError:
-                        logging.debug("[INTEGER_UNDERFLOW] no model found")         
+                        logging.debug("[INTEGER_UNDERFLOW] no model found") 
 
     return issues

mythril/analysis/modules/suicide.py

@@ -38,13 +38,13 @@ def execute(statespace):
                 to = stack.pop()
 
                 if ("caller" in str(to)):
-                    description += "The remaining Ether is sent to the caller's address."
+                    description += "The remaining Ether is sent to the caller's address.\n"
                 elif ("storage" in str(to)):
-                    description += "The remaining Ether is sent to a stored address."
+                    description += "The remaining Ether is sent to a stored address.\n"
                 elif ("calldata" in str(to)):
-                    description += "The remaining Ether is sent to an address provided as a function argument."
+                    description += "The remaining Ether is sent to an address provided as a function argument.\n"
                 elif (type(to) == BitVecNumRef):
-                    description += "The remaining Ether is sent to: " + hex(to.as_long())
+                    description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n"
                 else:
                     description += "The remaining Ether is sent to: " + str(to) + "\n"
 
@@ -62,8 +62,6 @@ def execute(statespace):
 
                     m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
 
-                    overwrite = False
-
                     if (m):
                         constrained = True
                         idx = m.group(1)
@@ -80,11 +78,9 @@ def execute(statespace):
                             can_solve = False
                             break
 
-                    # CALLER may also be constrained to hardcoded address. I.e. 'caller' and some integer
-
                     elif (re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint))):
-                       can_solve = False
-                       break
+                        can_solve = False
+                        break
 
                 if not constrained:
                     description += "\nIt seems that this function can be called without restrictions."
@@ -93,18 +89,14 @@ def execute(statespace):
 
                     try:
 
-
                         model = solver.get_model(node.constraints)
-                        logging.debug("[UNCHECKED_SUICIDE] MODEL: " + str(model))
-
 
-                        for d in model.decls():
-                            logging.debug("[UNCHECKED_SUICIDE] main model: %s = 0x%x" % (d.name(), model[d].as_long()))
+                        debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
 
-                        issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description)
+                        issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug)
                         issues.append(issue)
 
                     except UnsatError:
-                            logging.debug("[UNCHECKED_SUICIDE] no model found")    
+                            logging.debug("[UNCHECKED_SUICIDE] no model found")
 
     return issues

mythril/analysis/report.py

@@ -68,7 +68,7 @@ class Report:
                 text += "\n\n" + issue.code + "\n\n--------------------\n"
 
             if self.verbose and issue.debug:
-                text += "\nDEBUGGING INFORMATION:\n\n" + issue.debug + "\n\n--------------------\n"
+                text += "\nDEBUGGING INFORMATION:\n\n" + issue.debug + "\n--------------------\n"
 
             text += "\n"
 

mythril/analysis/solver.py

@@ -1,6 +1,7 @@
-from z3 import *
+from z3 import Solver, simplify, sat
 from mythril.exceptions import UnsatError
-import logging
+import re
+
 
 def get_model(constraints):
     s = Solver()
@@ -14,4 +15,23 @@ def get_model(constraints):
         return s.model()
 
     else:
-        raise UnsatError
+        raise UnsatError
+
+
+def pretty_print_model(model):
+
+    ret = ""
+
+    for d in model.decls():
+
+        try:
+            if (re.match(r'^calldata_.*_(\d)+', d.name())):
+                condition = "%064x" % model[d].as_long()
+            else:
+                condition = str(model[d].as_long())
+        except:
+            condition = str(simplify(model[d]))
+
+        ret += ("%s: %s\n" % (d.name(), condition))
+
+    return ret

solidity_examples/suicide.sol

@@ -0,0 +1,7 @@
+contract Suicide {
+
+  function kill(address addr) {
+    selfdestruct(addr);
+  }
+
+}