diff --git a/mythril/analysis/module/modules/ether_thief.py b/mythril/analysis/module/modules/ether_thief.py index be3939df..54cb34d0 100644 --- a/mythril/analysis/module/modules/ether_thief.py +++ b/mythril/analysis/module/modules/ether_thief.py @@ -11,24 +11,16 @@ from mythril.analysis.potential_issues import ( 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, UGE -from mythril.laser.smt.bool import And +from mythril.analysis import solver +from mythril.exceptions import UnsatError +from mythril.laser.smt import UGT log = logging.getLogger(__name__) DESCRIPTION = """ - Search for cases where Ether can be withdrawn to a user-specified address. - -An issue is reported if: - -- The transaction sender does not match contract creator; -- The sender address can be chosen arbitrarily; -- The receiver address is identical to the sender address; -- The sender can withdraw *more* than the total amount they sent over all transactions. - +An issue is reported if there is a valid end state where the attacker has successfully +increased their Ether balance. """ @@ -40,7 +32,7 @@ class EtherThief(DetectionModule): swc_id = UNPROTECTED_ETHER_WITHDRAWAL description = DESCRIPTION entry_point = EntryPoint.CALLBACK - pre_hooks = ["STOP"] + post_hooks = ["CALL", "STATICCALL"] def reset_module(self): """ @@ -51,7 +43,6 @@ class EtherThief(DetectionModule): def _execute(self, state: GlobalState) -> None: """ - :param state: :return: """ @@ -64,7 +55,6 @@ class EtherThief(DetectionModule): def _analyze_state(self, state): """ - :param state: :return: """ @@ -73,32 +63,36 @@ class EtherThief(DetectionModule): constraints = copy(state.world_state.constraints) - attacker_address_bitvec = ACTORS.attacker - constraints += [ UGT( - state.world_state.balances[attacker_address_bitvec], - state.world_state.starting_balances[attacker_address_bitvec], + state.world_state.balances[ACTORS.attacker], + state.world_state.starting_balances[ACTORS.attacker], ) ] - potential_issue = PotentialIssue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=instruction["address"], - swc_id=UNPROTECTED_ETHER_WITHDRAWAL, - title="Unprotected Ether Withdrawal", - severity="High", - bytecode=state.environment.code.bytecode, - description_head="Anyone can withdraw ETH from the contract account.", - description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" - + " account without previously having sent an equivalent amount of ETH to it. This is likely to be" - + " a vulnerability.", - detector=self, - constraints=constraints, - ) - - return [potential_issue] + try: + # Pre-solve so we only add potential issues if the attacker's balance is increased. + + solver.get_model(constraints) + + potential_issue = PotentialIssue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=instruction["address"], + swc_id=UNPROTECTED_ETHER_WITHDRAWAL, + title="Unprotected Ether Withdrawal", + severity="High", + bytecode=state.environment.code.bytecode, + description_head="Anyone can withdraw ETH from the contract account.", + description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract" + + " account. This is likely to be a vulnerability.", + detector=self, + constraints=constraints, + ) + + return [potential_issue] + except UnsatError: + return [] detector = EtherThief() diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 02e55c7b..73963d3a 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -5,10 +5,12 @@ from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( ) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.svm import LaserEVM +from mythril.laser.smt import UGT, symbol_factory from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) -from mythril.laser.smt import And, symbol_factory +from mythril.analysis import solver +from mythril.exceptions import UnsatError class MutationPruner(LaserPlugin): @@ -38,6 +40,10 @@ class MutationPruner(LaserPlugin): def sstore_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + """FIXME: Check for changes in world_state.balances instead of adding MutationAnnotation for all calls. + Requires world_state.starting_balances to be initalized at every tx start *after* call value has been added. + """ + @symbolic_vm.pre_hook("CALL") def call_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) @@ -48,17 +54,30 @@ class MutationPruner(LaserPlugin): @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): - if And( - *global_state.world_state.constraints[:] - + [ - global_state.environment.callvalue - > symbol_factory.BitVecVal(0, 256) - ] - ).is_false: - return + if isinstance( global_state.current_transaction, ContractCreationTransaction ): return + + if isinstance(global_state.environment.callvalue, int): + callvalue = symbol_factory.BitVecVal( + global_state.environment.callvalue, 256 + ) + else: + callvalue = global_state.environment.callvalue + + try: + + constraints = global_state.world_state.constraints + [ + UGT(callvalue, symbol_factory.BitVecVal(0, 256)) + ] + + solver.get_model(constraints) + return + except UnsatError: + # callvalue is constrained to 0, therefore there is no balance based world state mutation + pass + if len(list(global_state.get_annotations(MutationAnnotation))) == 0: raise PluginSkipWorldState diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index a5ee883d..505b6f9e 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -145,6 +145,7 @@ def execute_contract_creation( ) _setup_global_state_for_execution(laser_evm, transaction) new_account = new_account or transaction.callee_account + laser_evm.exec(True) return new_account