Merge pull request #869 from ConsenSys/enhance/optimize

Cache integer overflows/underflows, selfdestruct module

mythril/analysis/modules/base.py

@@ -34,7 +34,6 @@ class DetectionModule:
             )
         self.entrypoint = entrypoint
         self._issues = []
-        self._cache_addresses = {}
 
     @property
     def issues(self):
@@ -45,10 +44,9 @@ class DetectionModule:
 
     def reset_module(self):
         """
-        Resets issues and cache addresses
+        Resets issues
         """
         self._issues = []
-        self._cache_addresses = {}
 
     def execute(self, statespace):
         """The entry point for execution, which is being called by Mythril.

mythril/analysis/modules/ether_thief.py

@@ -41,6 +41,15 @@ class EtherThief(DetectionModule):
             entrypoint="callback",
             pre_hooks=["CALL"],
         )
+        self._cache_addresses = {}
+
+    def reset_module(self):
+        """
+        Resets the module by clearing everything
+        :return:
+        """
+        super().reset_module()
+        self._cache_addresses = {}
 
     def execute(self, state: GlobalState):
         """

mythril/analysis/modules/integer.py

@@ -49,6 +49,17 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             entrypoint="callback",
             pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI"],
         )
+        self._overflow_cache = {}
+        self._underflow_cache = {}
+
+    def reset_module(self):
+        """
+        Resets the module
+        :return:
+        """
+        super().reset_module()
+        self._overflow_cache = {}
+        self._underflow_cache = {}
 
     def execute(self, state: GlobalState):
         """Executes analysis module for integer underflow and integer overflow.
@@ -56,6 +67,11 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         :param state: Statespace to analyse
         :return: Found issues
         """
+        address = _get_address_from_state(state)
+        has_overflow = self._overflow_cache.get(address, False)
+        has_underflow = self._underflow_cache.get(address, False)
+        if has_overflow or has_underflow:
+            return
         if state.get_current_instruction()["opcode"] == "ADD":
             self._handle_add(state)
         elif state.get_current_instruction()["opcode"] == "MUL":
@@ -153,7 +169,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
         if not isinstance(value, Expression):
             return
-
         for annotation in value.annotations:
             if not isinstance(annotation, OverUnderflowAnnotation):
                 continue
@@ -175,6 +190,17 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
 
+            address = _get_address_from_state(ostate)
+
+            if annotation.operator == "subtraction" and self._underflow_cache.get(
+                address, False
+            ):
+                continue
+            if annotation.operator != "subtraction" and self._overflow_cache.get(
+                address, False
+            ):
+                continue
+
             try:
 
                 transaction_sequence = solver.get_transaction_sequence(
@@ -184,7 +210,12 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 issue.debug = json.dumps(transaction_sequence, indent=4)
 
             except UnsatError:
-                return
+                continue
+            if annotation.operator == "subtraction":
+                self._underflow_cache[address] = True
+            else:
+                self._overflow_cache[address] = True
+
             self._issues.append(issue)
 
     def _handle_jumpi(self, state):
@@ -211,6 +242,18 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
 
+            address = _get_address_from_state(ostate)
+
+            if annotation.operator == "subtraction" and self._underflow_cache.get(
+                address, False
+            ):
+                continue
+
+            if annotation.operator != "subtraction" and self._overflow_cache.get(
+                address, False
+            ):
+                continue
+
             try:
 
                 transaction_sequence = solver.get_transaction_sequence(
@@ -220,7 +263,12 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 issue.debug = json.dumps(transaction_sequence, indent=4)
 
             except UnsatError:
-                return
+                continue
+
+            if annotation.operator == "subtraction":
+                self._underflow_cache[address] = True
+            else:
+                self._overflow_cache[address] = True
             self._issues.append(issue)
 
     @staticmethod
@@ -236,3 +284,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
 
 detector = IntegerOverflowUnderflowModule()
+
+
+def _get_address_from_state(state):
+    return state.get_current_instruction()["address"]

mythril/analysis/modules/suicide.py

@@ -15,54 +15,6 @@ For kill-able contracts, also check whether it is possible to direct the contrac
 """
 
 
-def _analyze_state(state):
-    log.info("Suicide module: Analyzing suicide instruction")
-    node = state.node
-    instruction = state.get_current_instruction()
-    to = state.mstate.stack[-1]
-
-    log.debug("[SUICIDE] SUICIDE in function " + node.function_name)
-
-    description_head = "The contract can be killed by anyone."
-
-    try:
-        try:
-            transaction_sequence = solver.get_transaction_sequence(
-                state,
-                node.constraints + [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF],
-            )
-            description_tail = "Arbitrary senders can kill this contract and withdraw its balance to their own account."
-        except UnsatError:
-            transaction_sequence = solver.get_transaction_sequence(
-                state, node.constraints
-            )
-            description_tail = (
-                "Arbitrary senders can kill this contract but it is not possible to set the target address to which"
-                "the contract balance is sent."
-            )
-
-        debug = json.dumps(transaction_sequence, indent=4)
-
-        issue = Issue(
-            contract=node.contract_name,
-            function_name=node.function_name,
-            address=instruction["address"],
-            swc_id=UNPROTECTED_SELFDESTRUCT,
-            bytecode=state.environment.code.bytecode,
-            title="Unprotected Selfdestruct",
-            severity="High",
-            description_head=description_head,
-            description_tail=description_tail,
-            debug=debug,
-            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
-        )
-        return [issue]
-    except UnsatError:
-        log.info("[UNCHECKED_SUICIDE] no model found")
-
-    return []
-
-
 class SuicideModule(DetectionModule):
     """This module checks if the contact can be 'accidentally' killed by
     anyone."""
@@ -75,6 +27,15 @@ class SuicideModule(DetectionModule):
             entrypoint="callback",
             pre_hooks=["SUICIDE"],
         )
+        self._cache_address = {}
+
+    def reset_module(self):
+        """
+        Resets the module
+        :return:
+        """
+        super().reset_module()
+        self._cache_address = {}
 
     def execute(self, state: GlobalState):
         """
@@ -82,8 +43,59 @@ class SuicideModule(DetectionModule):
         :param state:
         :return:
         """
-        self._issues.extend(_analyze_state(state))
+        self._issues.extend(self._analyze_state(state))
         return self.issues
 
+    def _analyze_state(self, state):
+        log.info("Suicide module: Analyzing suicide instruction")
+        node = state.node
+        instruction = state.get_current_instruction()
+        if self._cache_address.get(instruction["address"], False):
+            return []
+        to = state.mstate.stack[-1]
+
+        log.debug("[SUICIDE] SUICIDE in function " + node.function_name)
+
+        description_head = "The contract can be killed by anyone."
+
+        try:
+            try:
+                transaction_sequence = solver.get_transaction_sequence(
+                    state,
+                    node.constraints
+                    + [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF],
+                )
+                description_tail = "Arbitrary senders can kill this contract and withdraw its balance to their own account."
+            except UnsatError:
+                transaction_sequence = solver.get_transaction_sequence(
+                    state, node.constraints
+                )
+                description_tail = (
+                    "Arbitrary senders can kill this contract but it is not possible to set the target address to which"
+                    "the contract balance is sent."
+                )
+
+            debug = json.dumps(transaction_sequence, indent=4)
+            self._cache_address[instruction["address"]] = True
+
+            issue = Issue(
+                contract=node.contract_name,
+                function_name=node.function_name,
+                address=instruction["address"],
+                swc_id=UNPROTECTED_SELFDESTRUCT,
+                bytecode=state.environment.code.bytecode,
+                title="Unprotected Selfdestruct",
+                severity="High",
+                description_head=description_head,
+                description_tail=description_tail,
+                debug=debug,
+                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+            )
+            return [issue]
+        except UnsatError:
+            log.info("[UNCHECKED_SUICIDE] no model found")
+
+        return []
+
 
 detector = SuicideModule()

mythril/analysis/security.py

@@ -28,6 +28,7 @@ def get_detection_module_hooks(modules, hook_type="pre"):
             if hook_type == "pre"
             else module.detector.post_hooks
         )
+
         for op_code in map(lambda x: x.upper(), hooks):
             if op_code in OPCODE_LIST:
                 hook_dict[op_code].append(module.detector.execute)

tests/testdata/outputs_expected/overflow.sol.o.json

@@ -1,32 +1,29 @@
 {
-    "error": null,
-    "issues": [
-        {
-            "address": 567,
-            "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
-            "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
-            "function": "sendeth(address,uint256)",
-            "max_gas_used": 1774,
-            "min_gas_used": 1299,
-            "severity": "High",
-            "sourceMap": null,
-            "swc-id": "101",
-            "title": "Integer Underflow"
-        },
-        {
-            "address": 649,
-            "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
-            "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
-            "function": "sendeth(address,uint256)",
-            "max_gas_used": 1774,
-            "min_gas_used": 1299,
-            "severity": "High",
-            "sourceMap": null,
-            "swc-id": "101",
-            "title": "Integer Underflow"
-        }
-    ],
-    "success": true
-}
+	"error": null,
+	"issues": [{
+		"address": 567,
+		"contract": "Unknown",
+		"debug": "<DEBUG-DATA>",
+		"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
+		"function": "sendeth(address,uint256)",
+		"max_gas_used": 1053,
+		"min_gas_used": 768,
+		"severity": "High",
+		"sourceMap": null,
+		"swc-id": "101",
+		"title": "Integer Underflow"
+	}, {
+		"address": 649,
+		"contract": "Unknown",
+		"debug": "<DEBUG-DATA>",
+		"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
+		"function": "sendeth(address,uint256)",
+		"max_gas_used": 1774,
+		"min_gas_used": 1299,
+		"severity": "High",
+		"sourceMap": null,
+		"swc-id": "101",
+		"title": "Integer Underflow"
+	}],
+	"success": true
+}

tests/testdata/outputs_expected/overflow.sol.o.markdown

@@ -6,7 +6,7 @@
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 567
-- Estimated Gas Usage: 1299 - 1774
+- Estimated Gas Usage: 768 - 1053
 
 ### Description
 

tests/testdata/outputs_expected/overflow.sol.o.text

@@ -4,7 +4,7 @@ Severity: High
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
-Estimated Gas Usage: 1299 - 1774
+Estimated Gas Usage: 768 - 1053
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------

tests/testdata/outputs_expected/underflow.sol.o.json

@@ -1,32 +1,29 @@
 {
-    "error": null,
-    "issues": [
-        {
-            "address": 567,
-            "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
-            "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
-            "function": "sendeth(address,uint256)",
-            "max_gas_used": 1774,
-            "min_gas_used": 1299,
-            "severity": "High",
-            "sourceMap": null,
-            "swc-id": "101",
-            "title": "Integer Underflow"
-        },
-        {
-            "address": 649,
-            "contract": "Unknown",
-            "debug": "<DEBUG-DATA>",
-            "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
-            "function": "sendeth(address,uint256)",
-            "max_gas_used": 1774,
-            "min_gas_used": 1299,
-            "severity": "High",
-            "sourceMap": null,
-            "swc-id": "101",
-            "title": "Integer Underflow"
-        }
-    ],
-    "success": true
-}
+	"error": null,
+	"issues": [{
+		"address": 567,
+		"contract": "Unknown",
+		"debug": "<DEBUG-DATA>",
+		"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
+		"function": "sendeth(address,uint256)",
+		"max_gas_used": 1053,
+		"min_gas_used": 768,
+		"severity": "High",
+		"sourceMap": null,
+		"swc-id": "101",
+		"title": "Integer Underflow"
+	}, {
+		"address": 649,
+		"contract": "Unknown",
+		"debug": "<DEBUG-DATA>",
+		"description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
+		"function": "sendeth(address,uint256)",
+		"max_gas_used": 1774,
+		"min_gas_used": 1299,
+		"severity": "High",
+		"sourceMap": null,
+		"swc-id": "101",
+		"title": "Integer Underflow"
+	}],
+	"success": true
+}

tests/testdata/outputs_expected/underflow.sol.o.markdown

@@ -6,7 +6,7 @@
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 567
-- Estimated Gas Usage: 1299 - 1774
+- Estimated Gas Usage: 768 - 1053
 
 ### Description
 

tests/testdata/outputs_expected/underflow.sol.o.text

@@ -4,7 +4,7 @@ Severity: High
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
-Estimated Gas Usage: 1299 - 1774
+Estimated Gas Usage: 768 - 1053
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------