diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 9fbf9340..8404b21a 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -6,6 +6,10 @@ from typing import List, cast, Dict from mythril.analysis import solver from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT +from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) from mythril.analysis.report import Issue from mythril.analysis.modules.base import DetectionModule from mythril.exceptions import UnsatError @@ -17,16 +21,19 @@ log = logging.getLogger(__name__) class DelegateCallAnnotation(StateAnnotation): - def __init__(self, call_state: GlobalState) -> None: + def __init__(self, call_state: GlobalState, constraints: List) -> None: """ Initialize DelegateCall Annotation :param call_state: Call state """ self.call_state = call_state + self.constraints = constraints self.return_value = call_state.new_bitvec( "retval_{}".format(call_state.get_current_instruction()["address"]), 256 ) + return DelegateCallAnnotation(self.call_state, copy(self.constraints)) + def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue: """ Returns Issue for the annotation @@ -107,26 +114,26 @@ def _analyze_states(state: GlobalState) -> List[Issue]: gas = state.mstate.stack[-1] to = state.mstate.stack[-2] - constraints = copy(state.mstate.constraints) - # Check whether we can also set the callee address - - constraints += [ - to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, + constraints = [ + to == ATTACKER_ADDRESS, UGT(gas, symbol_factory.BitVecVal(2300, 256)), ] - try: - solver.get_model(constraints) - state.annotate(DelegateCallAnnotation(call_state=state)) - except UnsatError: - log.debug("[DELEGATECALL] Annotation skipped.") + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + + state.annotate(DelegateCallAnnotation(state, constraints)) return [] else: for annotation in annotations: try: transaction_sequence = solver.get_transaction_sequence( - state, state.mstate.constraints + [annotation.return_value == 1] + state, + state.mstate.constraints + + annotation.constraints + + [annotation.return_value == 1], ) issues.append( annotation.get_issue( diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py index d8b879d3..293b4f69 100644 --- a/mythril/analysis/modules/ether_thief.py +++ b/mythril/analysis/modules/ether_thief.py @@ -8,6 +8,9 @@ from mythril.analysis import solver from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL from mythril.exceptions import UnsatError from mythril.laser.ethereum.state.global_state import GlobalState @@ -85,11 +88,10 @@ class EtherThief(DetectionModule): constraints += [BVAddNoOverflow(eth_sent_total, tx.call_value, False)] eth_sent_total = Sum(eth_sent_total, tx.call_value) - constraints += [ - tx.caller == ATTACKER_ADDRESS, - UGT(call_value, eth_sent_total), - target == ATTACKER_ADDRESS, - ] + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + + constraints += [UGT(call_value, eth_sent_total), target == ATTACKER_ADDRESS] try: @@ -114,7 +116,7 @@ class EtherThief(DetectionModule): log.debug("[ETHER_THIEF] no model found") return [] - self._cache_addresses[address] = True + # self._cache_addresses[address] = True return [issue] diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index 59f8e7bd..c4230cb9 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -3,6 +3,10 @@ calls.""" from mythril.analysis import solver from mythril.analysis.swc_data import REENTRANCY +from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) from mythril.analysis.modules.base import DetectionModule from mythril.analysis.report import Issue from mythril.laser.smt import UGT, symbol_factory, Or, BitVec @@ -44,7 +48,12 @@ def _analyze_state(state): # Check whether we can also set the callee address try: - constraints += [to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF] + constraints += [to == ATTACKER_ADDRESS] + + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + transaction_sequence = solver.get_transaction_sequence(state, constraints) description_head = "A call to a user-supplied address is executed." diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index ee0f81ee..546219a3 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -5,6 +5,9 @@ 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 ATTACKER_ADDRESS +from mythril.laser.ethereum.transaction.transaction_models import ( + ContractCreationTransaction, +) import logging import json @@ -58,16 +61,18 @@ class SuicideModule(DetectionModule): ) description_head = "The contract can be killed by anyone." - caller = state.current_transaction.caller + + constraints = [] + + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + try: try: transaction_sequence = solver.get_transaction_sequence( state, - state.mstate.constraints - + [ - to == 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, - caller == ATTACKER_ADDRESS, - ], + state.mstate.constraints + constraints + [to == ATTACKER_ADDRESS], ) description_tail = ( "Anyone can kill this contract and withdraw its balance to an arbitrary " @@ -75,7 +80,7 @@ class SuicideModule(DetectionModule): ) except UnsatError: transaction_sequence = solver.get_transaction_sequence( - state, state.mstate.constraints + [caller == ATTACKER_ADDRESS] + state, state.mstate.constraints + constraints ) description_tail = "Arbitrary senders can kill this contract."