Add integer underflow check

mythril/analysis/modules/integer_underflow.py

@@ -0,0 +1,67 @@
+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:
+
+Check for integer underflows.
+For every SUB instruction, check if there's a possible state where op1 > op0.
+'''
+
+def execute(statespace):
+
+    issues = []
+
+    for k in statespace.nodes:
+        node = statespace.nodes[k]
+
+        for instruction in node.instruction_list:
+
+            if(instruction['opcode'] == "SUB"):
+
+                stack = node.states[instruction['address']].stack
+
+                op0 = stack[-1]
+                op1 = stack[-2]
+
+                constraints = node.constraints
+
+                if (type(op0) == int and type(op1) == int):
+                    continue
+
+                logging.debug("[INTEGER_UNDERFLOW] Checking SUB " + str(op0) + ", " + str(op1))
+
+                constraints.append(UGT(op1,op0))
+
+                try:
+                    
+                    model = solver.get_model(node.constraints)
+
+                    issue = Issue("Integer Underflow", "Warning")
+
+                    m = re.search(r'(storage_\d+)', str(op0))
+
+                    if (m):
+                        storage_index = m.group(1)
+                    else:
+                        storage_index = "unknown"
+
+                    issue.description = "A possible integer underflow exists in the function " + node.function_name + ".\n" \
+                        "There SUB instruction at address " + str(instruction['address']) + " may underflow the state variable stored at position " + storage_index + "."
+
+                    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")         
+
+    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
+from .modules import delegatecall_forward, unchecked_suicide, ether_send, unchecked_retval, integer_underflow
 
 
 def fire_lasers(statespace):
@@ -10,6 +10,7 @@ def fire_lasers(statespace):
 	issues += unchecked_suicide.execute(statespace)
 	issues += ether_send.execute(statespace)
 	issues += unchecked_retval.execute(statespace)
+	issues += integer_underflow.execute(statespace)
 
 	if (len(issues)):
 		report = Report(issues)