From fbdfddb01ef073f316417028f102bb7ea61b5f5d Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 5 Nov 2018 16:40:47 +0530 Subject: [PATCH] Add multiple transactions to onchain analysis and fix suicide module --- mythril/analysis/modules/suicide.py | 29 ++++++++++++++++++++--------- mythril/laser/ethereum/svm.py | 14 +++++++++++++- 2 files changed, 33 insertions(+), 10 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index 2eb2cf98..b23b29b3 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -3,6 +3,7 @@ from mythril.analysis.ops import * 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 logging @@ -54,15 +55,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 = state.world_state.transaction_sequence[0].caller - 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) - ) + 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) + ) try: model = solver.get_model(node.constraints + not_creator_constraints) diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 4882671b..cba200dc 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -84,7 +84,19 @@ class LaserEVM: if main_address: logging.info("Starting message call transaction to {}".format(main_address)) - execute_message_call(self, main_address) + for i in range(self.max_transaction_count): + initial_coverage = self._get_covered_instructions() + + self.time = datetime.now() + logging.info( + "Starting message call transaction, iteration: {}".format(i) + ) + execute_message_call(self, main_address) + + end_coverage = self._get_covered_instructions() + if end_coverage == initial_coverage: + break + elif creation_code: logging.info("Starting contract creation transaction") created_account = execute_contract_creation(