Use a class of actors

mythril/analysis/modules/delegatecall.py

@@ -7,7 +7,7 @@ from mythril.analysis.potential_issues import (
     PotentialIssue,
 )
 from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT
-from mythril.laser.ethereum.transaction.symbolic import ACTOR_ADDRESSES
+from mythril.laser.ethereum.transaction.symbolic import ACTORS
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
@@ -54,7 +54,7 @@ class DelegateCallModule(DetectionModule):
         to = state.mstate.stack[-2]
 
         constraints = [
-            to == ACTOR_ADDRESSES["ATTACKER"],
+            to == ACTORS.attacker,
             UGT(gas, symbol_factory.BitVecVal(2300, 256)),
             state.new_bitvec(
                 "retval_{}".format(state.get_current_instruction()["address"]), 256
@@ -64,7 +64,7 @@ class DelegateCallModule(DetectionModule):
 
         for tx in state.world_state.transaction_sequence:
             if not isinstance(tx, ContractCreationTransaction):
-                constraints.append(tx.caller == ACTOR_ADDRESSES["ATTACKER"])
+                constraints.append(tx.caller == ACTORS.attacker)
 
         try:
             address = state.get_current_instruction()["address"]

mythril/analysis/modules/ether_thief.py

@@ -8,12 +8,12 @@ from mythril.analysis.potential_issues import (
     get_potential_issues_annotation,
     PotentialIssue,
 )
-from mythril.laser.ethereum.transaction.symbolic import ACTOR_ADDRESSES
+from mythril.laser.ethereum.transaction.symbolic import ACTORS
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
 
-from mythril.laser.smt import UGT, symbol_factory, UGE
+from mythril.laser.smt import UGT, UGE
 
 log = logging.getLogger(__name__)
 
@@ -90,9 +90,9 @@ class EtherThief(DetectionModule):
             This prevents false positives where the owner willingly transfers ownership to another address.
             """
             if not isinstance(tx, ContractCreationTransaction):
-                constraints += [tx.caller != ACTOR_ADDRESSES["CREATOR"]]
+                constraints += [tx.caller != ACTORS.creator]
 
-        attacker_address_bitvec = ACTOR_ADDRESSES["ATTACKER"]
+        attacker_address_bitvec = ACTORS.attacker
 
         constraints += [
             UGE(
@@ -108,8 +108,8 @@ class EtherThief(DetectionModule):
                 state.world_state.balances[attacker_address_bitvec],
                 state.world_state.starting_balances[attacker_address_bitvec],
             ),
-            target == ACTOR_ADDRESSES["ATTACKER"],
+            target == ACTORS.attacker,
-            state.current_transaction.caller == ACTOR_ADDRESSES["ATTACKER"],
+            state.current_transaction.caller == ACTORS.attacker,
         ]
 
         potential_issue = PotentialIssue(

mythril/analysis/modules/external_calls.py

@@ -8,7 +8,7 @@ from mythril.analysis.potential_issues import (
 )
 from mythril.analysis.swc_data import REENTRANCY
 from mythril.laser.ethereum.state.constraints import Constraints
-from mythril.laser.ethereum.transaction.symbolic import ACTOR_ADDRESSES
+from mythril.laser.ethereum.transaction.symbolic import ACTORS
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
@@ -94,11 +94,11 @@ class ExternalCalls(DetectionModule):
             # Check whether we can also set the callee address
 
             try:
-                constraints += [to == ACTOR_ADDRESSES["ATTACKER"]]
+                constraints += [to == ACTORS.attacker]
 
                 for tx in state.world_state.transaction_sequence:
                     if not isinstance(tx, ContractCreationTransaction):
-                        constraints.append(tx.caller == ACTOR_ADDRESSES["ATTACKER"])
+                        constraints.append(tx.caller == ACTORS.attacker)
 
                 solver.get_transaction_sequence(
                     state, constraints + state.mstate.constraints

mythril/analysis/modules/suicide.py

@@ -4,7 +4,7 @@ from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT
 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 ACTOR_ADDRESSES
+from mythril.laser.ethereum.transaction.symbolic import ACTORS
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
@@ -68,15 +68,13 @@ class SuicideModule(DetectionModule):
 
         for tx in state.world_state.transaction_sequence:
             if not isinstance(tx, ContractCreationTransaction):
-                constraints.append(tx.caller == ACTOR_ADDRESSES["ATTACKER"])
+                constraints.append(tx.caller == ACTORS.attacker)
 
         try:
             try:
                 transaction_sequence = solver.get_transaction_sequence(
                     state,
-                    state.mstate.constraints
+                    state.mstate.constraints + constraints + [to == ACTORS.attacker],
-                    + constraints
-                    + [to == ACTOR_ADDRESSES["ATTACKER"]],
                 )
                 description_tail = (
                     "Anyone can kill this contract and withdraw its balance to an arbitrary "

mythril/analysis/symbolic.py

@@ -16,7 +16,7 @@ from mythril.laser.ethereum.strategy.basic import (
 )
 
 from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
-from mythril.laser.ethereum.transaction.symbolic import ACTOR_ADDRESSES
+from mythril.laser.ethereum.transaction.symbolic import ACTORS
 
 
 from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
@@ -92,16 +92,10 @@ class SymExecWrapper:
             raise ValueError("Invalid strategy argument supplied")
 
         creator_account = Account(
-            hex(ACTOR_ADDRESSES["CREATOR"].value),
+            hex(ACTORS.creator.value), "", dynamic_loader=dynloader, contract_name=None
-            "",
-            dynamic_loader=dynloader,
-            contract_name=None,
         )
         attacker_account = Account(
-            hex(ACTOR_ADDRESSES["ATTACKER"].value),
+            hex(ACTORS.attacker.value), "", dynamic_loader=dynloader, contract_name=None
-            "",
-            dynamic_loader=dynloader,
-            contract_name=None,
         )
 
         requires_statespace = (
@@ -109,11 +103,11 @@ class SymExecWrapper:
             or len(get_detection_modules("post", modules, custom_modules_directory)) > 0
         )
         if not contract.creation_code:
-            self.accounts = {hex(ACTOR_ADDRESSES["ATTACKER"].value): attacker_account}
+            self.accounts = {hex(ACTORS.attacker.value): attacker_account}
         else:
             self.accounts = {
-                hex(ACTOR_ADDRESSES["CREATOR"].value): creator_account,
+                hex(ACTORS.creator.value): creator_account,
-                hex(ACTOR_ADDRESSES["ATTACKER"].value): attacker_account,
+                hex(ACTORS.attacker.value): attacker_account,
             }
 
         instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin()

mythril/interfaces/cli.py

@@ -18,7 +18,7 @@ import mythril.support.signatures as sigs
 from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
 from mythril import mythx
 from mythril.exceptions import AddressNotFoundError, CriticalError
-from mythril.laser.ethereum.transaction.symbolic import ACTOR_ADDRESSES, set_actor
+from mythril.laser.ethereum.transaction.symbolic import ACTORS
 from mythril.mythril import (
     MythrilAnalyzer,
     MythrilDisassembler,
@@ -675,13 +675,13 @@ def execute_command(
 
         if args.attacker_address:
             try:
-                set_actor("ATTACKER", args.attacker_address)
+                ACTORS["ATTACKER"] = args.attacker_address
             except ValueError:
                 exit_with_error(args.outform, "Attacker address is invalid")
 
         if args.creator_address:
             try:
-                set_actor("CREATOR", args.creator_address)
+                ACTORS["CREATOR"] = args.creator_address
             except ValueError:
                 exit_with_error(args.outform, "Creator address is invalid")
 

mythril/laser/ethereum/transaction/symbolic.py

@@ -18,33 +18,53 @@ from mythril.laser.smt import symbol_factory, Or, BitVec
 
 log = logging.getLogger(__name__)
 
-ACTOR_ADDRESSES = {
-    "CREATOR": symbol_factory.BitVecVal(
-        0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256
-    ),
-    "ATTACKER": symbol_factory.BitVecVal(
-        0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256
-    ),
-    "SOMEGUY": symbol_factory.BitVecVal(
-        0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256
-    ),
-}
-
-
-def set_actor(actor: str, address: Optional[str]):
-    """
-    Sets an actor to a desired address
 
-    :param actor: Name of the actor to set
+class Actors:
-    :param address: Address to set the actor to. None to delete the actor
+    def __init__(
-    """
+        self,
-    if address is None:
+        creator=0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE,
-        del ACTOR_ADDRESSES[actor]
+        attacker=0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF,
-    else:
+        someguy=0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA,
-        if address[0:2] != "0x":
+    ):
-            raise ValueError("Actor address not in valid format")
+        self.addresses = {
+            "CREATOR": symbol_factory.BitVecVal(creator, 256),
+            "ATTACKER": symbol_factory.BitVecVal(attacker, 256),
+            "SOMEGUY": symbol_factory.BitVecVal(someguy, 256),
+        }
+
+    def __setitem__(self, actor: str, address: Optional[str]):
+        """
+        Sets an actor to a desired address
+
+        :param actor: Name of the actor to set
+        :param address: Address to set the actor to. None to delete the actor
+        """
+        if address is None:
+            if actor in ("CREATOR", "ATTACKER"):
+                raise ValueError("Can't delete creator or attacker address")
+            del self.addresses[actor]
+        else:
+            if address[0:2] != "0x":
+                raise ValueError("Actor address not in valid format")
+
+            self.addresses[actor] = symbol_factory.BitVecVal(int(address[2:], 16), 256)
+
+    def __getitem__(self, actor: str):
+        return self.addresses[actor]
+
+    @property
+    def creator(self):
+        return self.addresses["CREATOR"]
+
+    @property
+    def attacker(self):
+        return self.addresses["ATTACKER"]
+
+    def __len__(self):
+        return len(self.addresses)
+
 
-        ACTOR_ADDRESSES[actor] = symbol_factory.BitVecVal(int(address[2:], 16), 256)
+ACTORS = Actors()
 
 
 def execute_message_call(laser_evm, callee_address: BitVec) -> None:
@@ -118,7 +138,7 @@ def execute_contract_creation(
                 "origin{}".format(next_transaction_id), 256
             ),
             code=Disassembly(contract_initialization_code),
-            caller=ACTOR_ADDRESSES["CREATOR"],
+            caller=ACTORS["CREATOR"],
             contract_name=contract_name,
             call_data=None,
             call_value=symbol_factory.BitVecSym(
@@ -143,7 +163,7 @@ def _setup_global_state_for_execution(laser_evm, transaction: BaseTransaction) -
     global_state.transaction_stack.append((transaction, None))
 
     global_state.mstate.constraints.append(
-        Or(*[transaction.caller == actor for actor in ACTOR_ADDRESSES.values()])
+        Or(*[transaction.caller == actor for actor in ACTORS.addresses.values()])
     )
 
     new_node = Node(