From 8a526ad48e377c506ebfd86987e49f2613477227 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Mon, 26 Nov 2018 14:25:00 +0700 Subject: [PATCH] Refactor to concrete senders --- mythril/analysis/analysis_utils.py | 48 ------------------- mythril/analysis/modules/ether_thief.py | 14 +----- mythril/analysis/modules/suicide.py | 15 +----- .../laser/ethereum/transaction/symbolic.py | 10 ++-- 4 files changed, 9 insertions(+), 78 deletions(-) delete mode 100644 mythril/analysis/analysis_utils.py diff --git a/mythril/analysis/analysis_utils.py b/mythril/analysis/analysis_utils.py deleted file mode 100644 index f4fc8e29..00000000 --- a/mythril/analysis/analysis_utils.py +++ /dev/null @@ -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 diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index c304fb11..f70973a1 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/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), - state.environment.sender == ARBITRARY_SENDER_ADDRESS, - target == state.environment.sender, - ], + + [UGT(call_value, eth_sent_total), target == state.environment.sender], ) debug = "Transaction Sequence: " + str(transaction_sequence) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index d49d1e0c..7a21b990 100644 --- a/mythril/analysis/modules/suicide.py +++ b/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: diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 88e16780..6d58d195 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/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,