diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index b23b29b3..b4dd9feb 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -4,6 +4,7 @@ from mythril.analysis.report import Issue from mythril.analysis.swc_data import UNPROTECTED_SELFDESTRUCT from mythril.exceptions import UnsatError from mythril.laser.ethereum.transaction import ContractCreationTransaction +import re import logging @@ -55,25 +56,25 @@ def _analyze_state(state, node): description += "The remaining Ether is sent to: " + str(to) + "\n" not_creator_constraints = [] - if len(state.world_state.transaction_sequence) >= 1: - 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) - ) + 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) + ) + not_creator_constraints.append(check_changeable_constraints(node.constraints)) try: model = solver.get_model(node.constraints + not_creator_constraints) @@ -100,3 +101,12 @@ def _analyze_state(state, node): logging.debug("[UNCHECKED_SUICIDE] no model found") return issues + + +def check_changeable_constraints(constraints): + for constraint in constraints: + if re.search(r"caller", str(constraint)) and re.search( + r"[0-9]{20}", str(constraint) + ): + return False + return True diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 11d97c0d..695ac6d7 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -120,6 +120,11 @@ class LaserEVM: logging.info("Achieved {} coverage for code: {}".format(cov, code)) def _execute_transactions(self, address): + """ + This function executes multiple transactions on the address based on the coverage + :param address: Address of the contract + :return: + """ self.coverage = {} for i in range(self.max_transaction_count): initial_coverage = self._get_covered_instructions()