Merge pull request #1079 from ConsenSys/delegatecall_fix

Add caller constraints on all transactions in tx sequence

mythril/analysis/modules/delegatecall.py

@@ -6,6 +6,10 @@ from typing import List, cast, Dict
 
 from mythril.analysis import solver
 from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT
+from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
+from mythril.laser.ethereum.transaction.transaction_models import (
+    ContractCreationTransaction,
+)
 from mythril.analysis.report import Issue
 from mythril.analysis.modules.base import DetectionModule
 from mythril.exceptions import UnsatError
@@ -17,16 +21,19 @@ log = logging.getLogger(__name__)
 
 
 class DelegateCallAnnotation(StateAnnotation):
-    def __init__(self, call_state: GlobalState) -> None:
+    def __init__(self, call_state: GlobalState, constraints: List) -> None:
         """
         Initialize DelegateCall Annotation
         :param call_state: Call state
         """
         self.call_state = call_state
+        self.constraints = constraints
         self.return_value = call_state.new_bitvec(
             "retval_{}".format(call_state.get_current_instruction()["address"]), 256
         )
 
+        return DelegateCallAnnotation(self.call_state, copy(self.constraints))
+
     def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue:
         """
         Returns Issue for the annotation
@@ -107,26 +114,26 @@ def _analyze_states(state: GlobalState) -> List[Issue]:
         gas = state.mstate.stack[-1]
         to = state.mstate.stack[-2]
 
-        constraints = copy(state.mstate.constraints)
-        # Check whether we can also set the callee address
-
-        constraints += [
-            to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF,
+        constraints = [
+            to == ATTACKER_ADDRESS,
             UGT(gas, symbol_factory.BitVecVal(2300, 256)),
         ]
-        try:
-            solver.get_model(constraints)
-            state.annotate(DelegateCallAnnotation(call_state=state))
 
-        except UnsatError:
-            log.debug("[DELEGATECALL] Annotation skipped.")
+        for tx in state.world_state.transaction_sequence:
+            if not isinstance(tx, ContractCreationTransaction):
+                constraints.append(tx.caller == ATTACKER_ADDRESS)
+
+        state.annotate(DelegateCallAnnotation(state, constraints))
 
         return []
     else:
         for annotation in annotations:
             try:
                 transaction_sequence = solver.get_transaction_sequence(
-                    state, state.mstate.constraints + [annotation.return_value == 1]
+                    state,
+                    state.mstate.constraints
+                    + annotation.constraints
+                    + [annotation.return_value == 1],
                 )
                 issues.append(
                     annotation.get_issue(

mythril/analysis/modules/ether_thief.py

@@ -8,6 +8,9 @@ from mythril.analysis import solver
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
 from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
+from mythril.laser.ethereum.transaction.transaction_models import (
+    ContractCreationTransaction,
+)
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -85,11 +88,10 @@ class EtherThief(DetectionModule):
             constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)]
             eth_sent_total = Sum(eth_sent_total, tx.call_value)
 
-        constraints += [
-            tx.caller == ATTACKER_ADDRESS,
-            UGT(call_value, eth_sent_total),
-            target == ATTACKER_ADDRESS,
-        ]
+            if not isinstance(tx, ContractCreationTransaction):
+                constraints.append(tx.caller == ATTACKER_ADDRESS)
+
+        constraints += [UGT(call_value, eth_sent_total), target == ATTACKER_ADDRESS]
 
         try:
 
@@ -114,7 +116,7 @@ class EtherThief(DetectionModule):
             log.debug("[ETHER_THIEF] no model found")
             return []
 
-        self._cache_addresses[address] = True
+        # self._cache_addresses[address] = True
 
         return [issue]
 

mythril/analysis/modules/external_calls.py

@@ -3,6 +3,10 @@ calls."""
 
 from mythril.analysis import solver
 from mythril.analysis.swc_data import REENTRANCY
+from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
+from mythril.laser.ethereum.transaction.transaction_models import (
+    ContractCreationTransaction,
+)
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
 from mythril.laser.smt import UGT, symbol_factory, Or, BitVec
@@ -44,7 +48,12 @@ def _analyze_state(state):
         # Check whether we can also set the callee address
 
         try:
-            constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF]
+            constraints += [to == ATTACKER_ADDRESS]
+
+            for tx in state.world_state.transaction_sequence:
+                if not isinstance(tx, ContractCreationTransaction):
+                    constraints.append(tx.caller == ATTACKER_ADDRESS)
+
             transaction_sequence = solver.get_transaction_sequence(state, constraints)
 
             description_head = "A call to a user-supplied address is executed."

mythril/analysis/modules/suicide.py

@@ -5,6 +5,9 @@ from mythril.exceptions import UnsatError
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
+from mythril.laser.ethereum.transaction.transaction_models import (
+    ContractCreationTransaction,
+)
 import logging
 import json
 
@@ -58,16 +61,18 @@ class SuicideModule(DetectionModule):
         )
 
         description_head = "The contract can be killed by anyone."
-        caller = state.current_transaction.caller
+
+        constraints = []
+
+        for tx in state.world_state.transaction_sequence:
+            if not isinstance(tx, ContractCreationTransaction):
+                constraints.append(tx.caller == ATTACKER_ADDRESS)
+
         try:
             try:
                 transaction_sequence = solver.get_transaction_sequence(
                     state,
-                    state.mstate.constraints
-                    + [
-                        to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF,
-                        caller == ATTACKER_ADDRESS,
-                    ],
+                    state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS],
                 )
                 description_tail = (
                     "Anyone can kill this contract and withdraw its balance to an arbitrary "
@@ -75,7 +80,7 @@ class SuicideModule(DetectionModule):
                 )
             except UnsatError:
                 transaction_sequence = solver.get_transaction_sequence(
-                    state, state.mstate.constraints + [caller == ATTACKER_ADDRESS]
+                    state, state.mstate.constraints + constraints
                 )
                 description_tail = "Arbitrary senders can kill this contract."