From 7a19e55e94cc13fb48793e7928a4249c003b7852 Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 23 Oct 2019 14:02:52 -0400 Subject: [PATCH] Use a class of actors --- mythril/analysis/modules/delegatecall.py | 6 +- mythril/analysis/modules/ether_thief.py | 12 +-- mythril/analysis/modules/external_calls.py | 6 +- mythril/analysis/modules/suicide.py | 8 +- mythril/analysis/symbolic.py | 18 ++--- mythril/interfaces/cli.py | 6 +- .../laser/ethereum/transaction/symbolic.py | 74 ++++++++++++------- 7 files changed, 71 insertions(+), 59 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 3e71e924..fa001b90 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/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"] diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index ff6bb69d..6a1e30cc 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/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"], - state.current_transaction.caller == ACTOR_ADDRESSES["ATTACKER"], + target == ACTORS.attacker, + state.current_transaction.caller == ACTORS.attacker, ] potential_issue = PotentialIssue( diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index 7ab5b103..f227f7b2 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/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 diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index a5be88e3..cc2d27dc 100644 --- a/mythril/analysis/modules/suicide.py +++ b/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 - + constraints - + [to == ACTOR_ADDRESSES["ATTACKER"]], + state.mstate.constraints + constraints + [to == ACTORS.attacker], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 08346878..f9364881 100644 --- a/mythril/analysis/symbolic.py +++ b/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), - "", - dynamic_loader=dynloader, - contract_name=None, + hex(ACTORS.creator.value), "", dynamic_loader=dynloader, contract_name=None ) attacker_account = Account( - hex(ACTOR_ADDRESSES["ATTACKER"].value), - "", - dynamic_loader=dynloader, - contract_name=None, + hex(ACTORS.attacker.value), "", 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(ACTOR_ADDRESSES["ATTACKER"].value): attacker_account, + hex(ACTORS.creator.value): creator_account, + hex(ACTORS.attacker.value): attacker_account, } instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin() diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index e8f64d43..96731a10 100644 --- a/mythril/interfaces/cli.py +++ b/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") diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 81adaaf0..9e8fd558 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/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 - :param address: Address to set the actor to. None to delete the actor - """ - if address is None: - del ACTOR_ADDRESSES[actor] - else: - if address[0:2] != "0x": - raise ValueError("Actor address not in valid format") +class Actors: + def __init__( + self, + creator=0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, + attacker=0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, + someguy=0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, + ): + 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(