diff --git a/mythril/analysis/module/modules/user_assertions.py b/mythril/analysis/module/modules/user_assertions.py index feac8059..172d9dba 100644 --- a/mythril/analysis/module/modules/user_assertions.py +++ b/mythril/analysis/module/modules/user_assertions.py @@ -1,13 +1,12 @@ """This module contains the detection code for potentially insecure low-level calls.""" -from mythril.analysis.potential_issues import ( - PotentialIssue, - get_potential_issues_annotation, -) +from mythril.analysis import solver +from mythril.analysis.potential_issues import Issue from mythril.analysis.swc_data import ASSERT_VIOLATION from mythril.analysis.module.base import DetectionModule, EntryPoint from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.exceptions import UnsatError import logging import eth_abi @@ -40,10 +39,12 @@ class UserAssertions(DetectionModule): :param state: :return: """ - potential_issues = self._analyze_state(state) - annotation = get_potential_issues_annotation(state) - annotation.potential_issues.extend(potential_issues) + issues = self._analyze_state(state) + for issue in issues: + self.cache.add(issue.address) + self.issues.extend(issues) + def _analyze_state(self, state: GlobalState): """ @@ -51,46 +52,60 @@ class UserAssertions(DetectionModule): :param state: :return: """ - topic, size, mem_start = state.mstate.stack[-3:] - - if topic.symbolic or topic.value != assertion_failed_hash: - return [] - - message = None - if not mem_start.symbolic and not size.symbolic: - message = eth_abi.decode_single( - "string", - bytes( - state.mstate.memory[ - mem_start.value + 32 : mem_start.value + size.value - ] - ), - ).decode("utf8") - - description_head = "A user-provided assertion failed." - if message: - description_tail = "A user-provided assertion failed with the message '{}'".format( - message + + try: + + transaction_sequence = solver.get_transaction_sequence( + state, state.world_state.constraints ) - else: - description_tail = "A user-provided assertion failed." - - address = state.get_current_instruction()["address"] - issue = PotentialIssue( - contract=state.environment.active_account.contract_name, - function_name=state.environment.active_function_name, - address=address, - swc_id=ASSERT_VIOLATION, - title="Assertion Failed", - bytecode=state.environment.code.bytecode, - severity="Medium", - description_head=description_head, - description_tail=description_tail, - constraints=[], - detector=self, - ) - - return [issue] + + topic, size, mem_start = state.mstate.stack[-3:] + + if topic.symbolic or topic.value != assertion_failed_hash: + return [] + + message = None + if not mem_start.symbolic and not size.symbolic: + message = eth_abi.decode_single( + "string", + bytes( + state.mstate.memory[ + mem_start.value + 32 : mem_start.value + size.value + ] + ), + ).decode("utf8") + + if message: + description_tail = "A user-provided assertion failed with the message '{}'".format( + message + ) + log.info("MythX assertion emitted: {}".format(message)) + + else: + description_tail = "A user-provided assertion failed." + + + address = state.get_current_instruction()["address"] + + issue = Issue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=address, + swc_id=ASSERT_VIOLATION, + title="Exception State", + severity="Medium", + description_head="A user-provided assertion failed.", + description_tail=description_tail, + bytecode=state.environment.code.bytecode, + transaction_sequence=transaction_sequence, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), + ) + return [issue] + + except UnsatError: + log.debug("no model found") + + return [] detector = UserAssertions() diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 175ef9db..9ace7cac 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -62,6 +62,7 @@ log = logging.getLogger(__name__) TT256 = 2 ** 256 TT256M1 = 2 ** 256 - 1 +MAX_CALL_DEPTH = 5 def transfer_ether( global_state: GlobalState, @@ -1909,6 +1910,21 @@ class Instruction: environment = global_state.environment memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5] + + if(len(global_state.transaction_stack) >= MAX_CALL_DEPTH): + log.info( + "Max call depth reached" + ) + + self._write_symbolic_returndata( + global_state, memory_out_offset, memory_out_size + ) + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + + return [global_state] + try: ( callee_address, @@ -2137,6 +2153,20 @@ class Instruction: environment = global_state.environment memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4] + if(len(global_state.transaction_stack) >= MAX_CALL_DEPTH): + log.info( + "Max call depth reached" + ) + + self._write_symbolic_returndata( + global_state, memory_out_offset, memory_out_size + ) + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + + return [global_state] + try: ( callee_address, @@ -2272,6 +2302,21 @@ class Instruction: instr = global_state.get_current_instruction() environment = global_state.environment memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4] + + if(len(global_state.transaction_stack) >= MAX_CALL_DEPTH): + log.info( + "Max call depth reached" + ) + + self._write_symbolic_returndata( + global_state, memory_out_offset, memory_out_size + ) + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + + return [global_state] + try: ( callee_address, diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 904a07da..4568638a 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -144,7 +144,7 @@ class LaserEVM: if pre_configuration_mode: self.open_states = [world_state] - log.info("Starting message call transaction to {}".format(target_address)) + log.info("Starting message call transaction to {:#42x}".format(target_address)) self._execute_transactions(symbol_factory.BitVecVal(target_address, 256)) elif scratch_mode: @@ -356,7 +356,7 @@ class LaserEVM: start_signal.transaction.call_value, ) - log.debug("Starting new transaction %s", start_signal.transaction) + log.debug("Starting new transaction %s, call stack size %d", start_signal.transaction, len(new_global_state.transaction_stack)) return [new_global_state], op_code diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 71630a07..529894eb 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -138,10 +138,16 @@ class BaseTransaction: raise NotImplementedError def __str__(self) -> str: + + try: + _caller = "{:#42x}".format(int(str(self.caller))) + except: + _caller = str(self.caller) + return "{} {} from {} to {:#42x}".format( self.__class__.__name__, self.id, - self.caller, + _caller, int(str(self.callee_account.address)) if self.callee_account else -1, )