Update security tests

mythril/analysis/modules/ether_send.py

@@ -25,8 +25,6 @@ def execute(statespace):
             logging.debug("[ETHER_SEND] Skipping refund function")
             continue
 
-        issue = Issue("Ether send", "Warning")
-
         # We're only interested in calls that send Ether
 
         if call.value.type == VarType.CONCRETE:
@@ -35,10 +33,9 @@ def execute(statespace):
 
         interesting = False
 
+        issue = Issue("Ether send", "Warning")
         issue.description = "In the function '" + call.node.function_name +"' "
 
-        # Check the CALL target
-
         if re.search(r'caller', str(call.to)):
             issue.description += "a non-zero amount of Ether is sent to msg.sender.\n"
             interesting = True

mythril/analysis/modules/integer_underflow.py

@@ -46,6 +46,9 @@ def execute(statespace):
 
                     issue = Issue("Integer Underflow", "Warning")
 
+                    op0 = str(op0).replace("\n","")
+                    op1 = str(op1).replace("\n","")
+
                     issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \
                         "There SUB instruction at address " + str(instruction['address']) + " performs the operation " + str(op0) + " - " + str(op1) + ". " \
                         "However, it is not verified that " + str(op0) + " >= " + str(op1) + "."

mythril/analysis/modules/send_with_gas.py

@@ -0,0 +1,114 @@
+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
+
+
+'''
+MODULE DESCRIPTION:
+
+Check for CALLs that send >0 Ether to either the transaction sender, or to an address provided as a function argument.
+If msg.sender is checked against a value in storage, check whether that storage index is tainted (i.e. there's an unconstrained write
+to that index).
+'''
+
+def execute(statespace):
+
+    issues = []
+
+    for call in statespace.calls:
+
+        if ("callvalue" in str(call.value)):
+            logging.debug("[ETHER_SEND] Skipping refund function")
+            continue
+
+        # We're only interested in calls that send Ether
+
+        if call.value.type == VarType.CONCRETE:
+            if call.value.val == 0:
+                continue
+
+        logging.debug("[SEND_WITH_GAS]: ")
+
+        # Check the CALL target
+
+        if re.search(r'caller', str(call.to)):
+            issue.description += "a non-zero amount of Ether is sent to msg.sender.\n"
+            interesting = True
+
+        if re.search(r'calldata', str(call.to)):
+            issue.description += "a non-zero amount of Ether is sent to an address taken from function arguments.\n"
+            interesting = True
+
+        if interesting:
+
+            issue = Issue("Ether send", "Warning")
+            issue.description = "In the function '" + call.node.function_name +"' "
+            issue.description += "Call value is " + str(call.value) + "\n"
+
+            node = call.node
+
+            constrained = False
+            can_solve = True
+
+            index = 0
+
+            while(can_solve and index < len(node.constraints)):
+
+                constraint = node.constraints[index]
+                index += 1
+                logging.debug("[ETHER_SEND] Constraint: " + str(constraint))
+
+                m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint))
+
+                overwrite = False
+
+                if (m):
+                    constrained = True
+                    index = m.group(1)
+
+                    try:
+
+                        for s in statespace.sstors[index]:
+
+                            if s.tainted:
+                                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
+
+                        if not overwrite:
+                            logging.debug("[ETHER_SEND] No storage writes to index " + str(index))
+                            can_solve = False
+                            break
+
+                    except KeyError:
+                        logging.debug("[ETHER_SEND] No storage writes to index " + str(index))
+                        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
+
+
+            if not constrained:
+                issue.description += "\nIt seems that this function can be called without restrictions."
+
+            if can_solve:
+
+                try:
+                    model = solver.get_model(node.constraints)
+                    logging.debug("[ETHER_SEND] MODEL: " + str(model))
+                    issues.append(issue)
+
+                    for d in model.decls():
+                        logging.debug("[ETHER_SEND] main model: %s = 0x%x" % (d.name(), model[d].as_long()))
+                except UnsatError:
+                        logging.debug("[ETHER_SEND] no model found")  
+
+    return issues

mythril/analysis/security.py

@@ -1,5 +1,5 @@
 from mythril.analysis.report import Report
-from .modules import delegatecall_forward, unchecked_suicide, ether_send, unchecked_retval, integer_underflow, delegatecall_to_dynamic
+from .modules import delegatecall_forward, unchecked_suicide, ether_send, unchecked_retval, delegatecall_to_dynamic, integer_underflow
 
 
 def fire_lasers(statespace):
@@ -9,8 +9,8 @@ def fire_lasers(statespace):
 	issues += delegatecall_forward.execute(statespace)
 	issues += delegatecall_to_dynamic.execute(statespace)
 	issues += unchecked_suicide.execute(statespace)
-	issues += ether_send.execute(statespace)
 	issues += unchecked_retval.execute(statespace)
+	issues += ether_send.execute(statespace)
 	issues += integer_underflow.execute(statespace)
 
 	if (len(issues)):