Merge pull request #127 from JoranHonig/features/integeroverflow_benign

Check for benign cases in integer overflows

mythril/analysis/modules/integer.py

@@ -12,7 +12,7 @@ MODULE DESCRIPTION:
 
 Check for integer underflows.
 For every SUB instruction, check if there's a possible state where op1 > op0.
-For every ADD instruction, check if there's a possible state where op1 + op0 > 2^32 - 1
+For every ADD, MUL instruction, check if there's a possible state where op1 + op0 > 2^32 - 1
 '''
 
 MAX_UINT = 2 ** 32 - 1
@@ -52,49 +52,83 @@ def _check_integer_overflow(statespace, state, node):
 
     # Check the instruction
     instruction = state.get_current_instruction()
-    if instruction['opcode'] in("ADD", "MUL"):
-
-        constraints = copy.deepcopy(node.constraints)
+    if instruction['opcode'] not in ("ADD", "MUL"):
+        return issues
 
     # Formulate overflow constraints
     stack = state.mstate.stack
     op0, op1 = stack[-1], stack[-2]
 
     # An integer overflow is possible if op0 + op1 or op0 * op1 > MAX_UINT
-
+    # Do a type check
     allowed_types = [int, BitVecRef, BitVecNumRef]
+    if not (type(op0) in allowed_types and type(op1) in allowed_types):
+        return issues
 
-        if type(op0) in allowed_types and type(op1) in allowed_types:
-
+    # Formulate expression
     if instruction['opcode'] == "ADD":
         expr = op0 + op1
     else:
         expr = op0 * op1
 
-            constraints.append(UGT(expr, MAX_UINT))
+    # Check satisfiable
+    constraint = UGT(expr, MAX_UINT)
+    model = _try_constraints(node.constraints, [constraint])
 
-            try:
-                model = solver.get_model(constraints)
+    if model is None:
+        logging.debug("[INTEGER_OVERFLOW] no model found")
+        return issues
+
+    if not _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1):
+        return issues
+
+    # Build issue
+    issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning")
+
+    issue.description = "A possible integer overflow exists in the function `{}`.\n" \
+                        "The addition or multiplication may result in a value higher than the maximum representable integer.".format(
+        node.function_name)
+    issue.debug = solver.pretty_print_model(model)
+    issues.append(issue)
+
+    return issues
 
+
+def _verify_integer_overflow(statespace, node, expr, state, model, constraint, op0, op1):
+    """ Verifies existence of integer overflow """
     # If we get to this point then there has been an integer overflow
     # Find out if the overflowed value is actually used
     interesting_usages = _search_children(statespace, node, expr, index=node.states.index(state))
 
     # Stop if it isn't
     if len(interesting_usages) == 0:
-                    return issues
+        return False
 
-                issue = Issue(node.contract_name, node.function_name, instruction['address'], "Integer Overflow ", "Warning")
+    op0_value = int(str(model.eval(op0, model_completion=True)))
+    model0 = _try_constraints(node.constraints, [constraint, op0 != op0_value])
 
-                issue.description = "A possible integer overflow exists in the function `{}`.\n" \
-                                    "The addition or multiplication may result in a value higher than the maximum representable integer.".format(node.function_name)
-                issue.debug = solver.pretty_print_model(model)
-                issues.append(issue)
+    op1_value = int(str(model.eval(op1, model_completion=True)))
+    model1 = _try_constraints(node.constraints, [constraint, op1 != op1_value])
 
-            except UnsatError:
-                logging.debug("[INTEGER_OVERFLOW] no model found")
+    if model0 is None and model1 is None:
+        return False
 
-    return issues
+    return True
+
+
+def _try_constraints(constraints, new_constraints):
+    """
+    Tries new constraints
+    :return Model if satisfiable otherwise None
+    """
+    _constraints = copy.deepcopy(constraints)
+    for constraint in new_constraints:
+        _constraints.append(copy.deepcopy(constraint))
+    try:
+        model = solver.get_model(_constraints)
+        return model
+    except UnsatError:
+        return None
 
 
 def _check_integer_underflow(statespace, state, node):