Refactor to concrete senders

mythril/analysis/analysis_utils.py

@@ -1,48 +0,0 @@
-import re
-from typing import List
-from z3 import *
-from mythril.laser.ethereum.transaction import ContractCreationTransaction
-from mythril.laser.ethereum.state.global_state import GlobalState
-
-
-def get_non_creator_constraints(state: GlobalState) -> (List, bool):
-    """
-    Get constraints which say that the caller isn't the creator of the contract
-    :param state: The state
-    :return: tuple of (constraints, bool) where the bool says whether the caller is constrained or not
-    """
-    not_creator_constraints = []
-    creator = None
-    if isinstance(
-        state.world_state.transaction_sequence[0], ContractCreationTransaction
-    ):
-        creator = state.world_state.transaction_sequence[0].caller
-
-    if creator is not None:
-        for transaction in state.world_state.transaction_sequence[1:]:
-            not_creator_constraints.append(
-                Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))
-            )
-            not_creator_constraints.append(
-                Not(Extract(159, 0, transaction.caller) == 0)
-            )
-    else:
-        for transaction in state.world_state.transaction_sequence:
-            not_creator_constraints.append(
-                Not(Extract(159, 0, transaction.caller) == 0)
-            )
-        if not has_caller_check_constraint(state.mstate.constraints):
-            return [], True
-    return not_creator_constraints, False
-
-
-def has_caller_check_constraint(constraints: List) -> bool:
-    """
-    Checks whether the caller is constrained to a value or not
-    """
-    for constraint in constraints:
-        if re.search(
-            r"caller.*==[0-9]{20}", str(constraint).replace("\n", "").replace(" ", "")
-        ):
-            return False
-    return True

mythril/analysis/modules/ether_thief.py

@@ -1,6 +1,5 @@
 from mythril.analysis.ops import *
 from mythril.analysis import solver
-from mythril.analysis.analysis_utils import get_non_creator_constraints
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.analysis.modules.base import DetectionModule
@@ -22,8 +21,6 @@ An issue is reported if:
 
 """
 
-ARBITRARY_SENDER_ADDRESS = 0xAAAAAAAABBBBBBBBBCCCCCCCDDDDDDDDEEEEEEEE
-
 
 class EtherThief(DetectionModule):
     def __init__(self):
@@ -56,10 +53,6 @@ class EtherThief(DetectionModule):
         call_value = state.mstate.stack[-3]
         target = state.mstate.stack[-2]
 
-        not_creator_constraints, constrained = get_non_creator_constraints(state)
-        if constrained:
-            return []
-
         eth_sent_total = BitVecVal(0, 256)
 
         for tx in state.world_state.transaction_sequence[1:]:
@@ -70,12 +63,7 @@ class EtherThief(DetectionModule):
             transaction_sequence = solver.get_transaction_sequence(
                 state,
                 node.constraints
-                + not_creator_constraints
+                + [UGT(call_value, eth_sent_total), target == state.environment.sender],
-                + [
-                    UGT(call_value, eth_sent_total),
-                    state.environment.sender == ARBITRARY_SENDER_ADDRESS,
-                    target == state.environment.sender,
-                ],
             )
 
             debug = "Transaction Sequence: " + str(transaction_sequence)

mythril/analysis/modules/suicide.py

@@ -1,5 +1,4 @@
 from mythril.analysis import solver
-from mythril.analysis.analysis_utils import get_non_creator_constraints
 from mythril.analysis.ops import *
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
@@ -13,8 +12,6 @@ Check if the contact can be 'accidentally' killed by anyone.
 For kill-able contracts, also check whether it is possible to direct the contract balance to the attacker.
 """
 
-ARBITRARY_SENDER_ADDRESS = 0xAAAAAAAABBBBBBBBBCCCCCCCDDDDDDDDEEEEEEEE
-
 
 def _analyze_state(state):
     logging.info("Suicide module: Analyzing suicide instruction")
@@ -24,20 +21,10 @@ def _analyze_state(state):
 
     logging.debug("[SUICIDE] SUICIDE in function " + node.function_name)
 
-    not_creator_constraints, constrained = get_non_creator_constraints(state)
-    constraints = (
-        node.constraints
-        + not_creator_constraints
-        + [state.environment.sender == ARBITRARY_SENDER_ADDRESS]
-    )
-
-    if constrained:
-        return []
-
     try:
         try:
             transaction_sequence = solver.get_transaction_sequence(
-                state, constraints + [to == ARBITRARY_SENDER_ADDRESS]
+                state, node.constraints
             )
             description = "Anyone can kill this contract and withdraw its balance to their own account."
         except UnsatError:

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,4 +1,4 @@
-from z3 import BitVec, Extract, Not
+from z3 import BitVec, BitVecVal
 from logging import debug
 
 from mythril.disassembler.disassembly import Disassembly
@@ -12,6 +12,10 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 )
 
 
+CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
+ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
+
+
 def execute_message_call(laser_evm, callee_address: str) -> None:
     """ Executes a message call transaction from all open states """
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
@@ -30,7 +34,7 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
             gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
             gas_limit=8000000,  # block gas limit
             origin=BitVec("origin{}".format(next_transaction_id), 256),
-            caller=BitVec("caller{}".format(next_transaction_id), 256),
+            caller=BitVecVal(ATTACKER_ADDRESS, 256),
             callee_account=open_world_state[callee_address],
             call_data=Calldata(next_transaction_id),
             call_data_type=CalldataType.SYMBOLIC,
@@ -64,7 +68,7 @@ def execute_contract_creation(
             gas_limit=8000000,  # block gas limit
             origin=BitVec("origin{}".format(next_transaction_id), 256),
             code=Disassembly(contract_initialization_code),
-            caller=BitVec("creator{}".format(next_transaction_id), 256),
+            caller=CREATOR_ADDRESS,
             callee_account=new_account,
             call_data=[],
             call_data_type=CalldataType.SYMBOLIC,