Remove integer overflow check (performance, false positives)

mythril/analysis/modules/integer_overflow.py

@@ -1,110 +0,0 @@
-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 copy
-import re
-import logging
-
-
-UINT_MAX = BitVecVal(2 ** 256 - 1, 256)
-
-
-'''
-MODULE DESCRIPTION:
-
-Check for integer overflows.
-'''
-
-def execute(statespace):
-
-    logging.debug("Executing module: INTEGER_OVERFLOW")
-
-    issues = []
-
-    for k in statespace.nodes:
-        node = statespace.nodes[k]
-
-        for instruction in node.instruction_list:
-
-            ''' This generates a lot of noise.
-
-            if(instruction['opcode'] == "ADD"):
-
-                stack = node.states[instruction['address']].stack
-
-                op0 = stack[-1]
-                op1 = stack[-2]
-
-                if type(op0) == int and type(op1) == int:
-                    continue
-
-                logging.debug("[INTEGER_OVERFLOW] Checking ADD " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address']))
-
-                constraints = copy.deepcopy(node.constraints)
-
-                constraints.append(UGT(op0, UINT_MAX - op1))
-
-                try:
-                    
-                    model = solver.get_model(constraints)
-
-                    issue = Issue(node.module_name, node.function_name, instruction['address'], "Integer Overflow", "Warning")
-
-                    issue.description = "A possible integer overflow exists in the function " + node.function_name + ".\n" \
-                        "The addition at address " + str(instruction['address']) + " may result in a value greater than UINT_MAX." 
-
-                    issue.debug = "(" + str(op0) + ") + (" + str(op1) + ") > (" + hex(UINT_MAX.as_long()) + ")"
-
-                    issues.append(issue)
-
-                    for d in model.decls():
-                        logging.debug("[INTEGER_OVERFLOW] model: %s = 0x%x" % (d.name(), model[d].as_long()))
-
-                except UnsatError:
-                    logging.debug("[INTEGER_OVERFLOW] no model found")   
-
-            '''
-
-            if(instruction['opcode'] == "MUL"):
-
-                stack = node.states[instruction['address']].stack
-
-                op0 = stack[-1]
-                op1 = stack[-2]
-
-                if (type(op0) == int and type(op1) == int) or type(op0) == BoolRef or type(op1) == BoolRef:
-                    continue
-
-                logging.debug("[INTEGER_OVERFLOW] Checking MUL " + str(op0) + ", " + str(op1) + " at address " + str(instruction['address']))
-
-                if re.search(r'146150163733', str(op0), re.DOTALL) or re.search(r'146150163733', str(op1), re.DOTALL) or "(2 << 160 - 1)" in str(op0) or "(2 << 160 - 1)" in str(op1):
-                    continue
-
-                constraints = copy.deepcopy(node.constraints)
-
-                constraints.append(UGT(op0, UDiv(UINT_MAX, op1)))
-                
-                try:
-                    
-                    model = solver.get_model(constraints)
-
-                    issue = Issue(node.module_name, node.function_name, instruction['address'], "Integer Overflow", "Warning")
-
-                    issue.description = "A possible integer overflow exists in the function " + node.function_name + ".\n" \
-                        "The multiplication at address " + str(instruction['address']) + " may result in a value greater than UINT_MAX." 
-
-                    issue.debug = "(" + str(op0) + ") * (" + str(op1) + ") > (" + hex(UINT_MAX.as_long()) + ")"
-
-                    issues.append(issue)
-
-                    logging.debug("Constraints: " + str(constraints))   
-
-                    for d in model.decls():
-                        logging.debug("[INTEGER_OVERFLOW] model: %s = 0x%x" % (d.name(), model[d].as_long()))
-
-                except UnsatError:
-                    logging.debug("[INTEGER_OVERFLOW] no model found")   
-
-    return issues

mythril/analysis/symbolic.py

@@ -5,6 +5,11 @@ from .ops import *
 import logging
 
 
+class SStorTaintStatus(Enum):
+    TAINTED = 1
+    UNTAINTED = 2 
+
+
 class StateSpace:
 
     '''
@@ -34,6 +39,9 @@ class StateSpace:
         self.suicides = []
         self.sstors = {}
 
+        self.sstor_taint_cache = []
+
+
         for key in self.svm.nodes:
 
             for instruction in self.nodes[key].instruction_list:
@@ -72,9 +80,10 @@ class StateSpace:
                     except KeyError:
                         self.sstors[str(index)] = [SStore(self.nodes[key], instruction['address'], value)]
 
-        self.sstor_analysis()
+        # self.sstor_analysis()
 
 
+    '''
     def sstor_analysis(self):
 
         logging.info("Analyzing storage operations...")
@@ -82,7 +91,7 @@ class StateSpace:
         for index in self.sstors:
             for s in self.sstors[index]:
 
-                # For now we simply 'taint' every storage location that is reachable without any constraint on msg.sender
+                # 'Taint' every 'store' instruction that is reachable without any constraint on msg.sender
 
                 taint = True
 
@@ -99,17 +108,25 @@ class StateSpace:
                         s.tainted = True
                     except UnsatError:
                         s.tainted = False
+    '''
 
 
 
     def find_storage_write(self, index):
 
-        # Find a tainted (unconstrained) SSTOR that writes to 'index'
+        # Find a an unconstrained SSTOR that writes to storage index "index"
 
         try:
             for s in self.sstors[index]:
-                if s.tainted:
+                taint = True
+
+                for constraint in s.node.constraints:
+                    if ("caller" in str(constraint)):
+                        taint = False
+                        break
+
                     return s.node.function_name
+
             return None
         except KeyError:
             return None

security_checks.md

@@ -8,7 +8,7 @@
 |Multiple sends in a single transaction| External calls can fail accidentally or deliberately. Avoid combining multiple send() calls in a single transaction. |           |   [Favor pull over push for external calls](https://consensys.github.io/smart-contract-best-practices/recommendations/#favor-pull-over-push-for-external-calls) |
 |Function call to untrusted contract|             |           [call to untrusted contract with gas](mythril/analysis/modules/call_to_dynamic_with_gas.py) | |
 |Delegatecall or callcode to untrusted contract|                   | [delegatecall_forward](mythril/analysis/modules/delegatecall_forward.py), [delegatecall_to_dynamic.py](mythril/analysis/modules/delegatecall_to_dynamic.py) |  |
-|Integer overflow/underflow|                        | [integer_underflow](mythril/analysis/modules/integer_underflow.py), [Integer overflow](/mythril/analysis/modules/integer_overflow.py)   |  |
+|Integer overflow/underflow|                        | [integer_underflow](mythril/analysis/modules/integer_underflow.py)   |  |
 |Timestamp dependence|                        |           |  |
 |Payable transaction does not revert in case of failure | | |   |
 |Call depth attack|                        |           |   |