From 3e167282e78cfa719b129441a87d1838a7e67940 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 14 Jan 2020 14:54:42 +0000 Subject: [PATCH] Bugfix calls (#1288) * Fix bugs * Change tests * black * Fix the string * Change the name and add a docstring * Change max-depth to 128 * refactor with black * Rename function name and remove constraints append code --- mythril/analysis/modules/external_calls.py | 10 ++-- mythril/interfaces/cli.py | 2 +- mythril/laser/ethereum/instructions.py | 62 +++++++++++++++++++--- tests/instructions/static_call_test.py | 4 +- 4 files changed, 62 insertions(+), 16 deletions(-) diff --git a/mythril/analysis/modules/external_calls.py b/mythril/analysis/modules/external_calls.py index a09cf517..67c1261d 100644 --- a/mythril/analysis/modules/external_calls.py +++ b/mythril/analysis/modules/external_calls.py @@ -94,14 +94,10 @@ class ExternalCalls(DetectionModule): # Check whether we can also set the callee address try: - constraints += [to == ACTORS.attacker] - - for tx in state.world_state.transaction_sequence: - if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ACTORS.attacker) + new_constraints = constraints + [to == ACTORS.attacker] solver.get_transaction_sequence( - state, constraints + state.world_state.constraints + state, new_constraints + state.world_state.constraints ) description_head = "A call to a user-supplied address is executed." @@ -122,7 +118,7 @@ class ExternalCalls(DetectionModule): severity="Medium", description_head=description_head, description_tail=description_tail, - constraints=constraints, + constraints=new_constraints, detector=self, ) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 96731a10..e326ae85 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -384,7 +384,7 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): options.add_argument( "--max-depth", type=int, - default=50, + default=128, help="Maximum recursion depth for symbolic execution", ) options.add_argument( diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 8a4b4b8d..cebd961d 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -732,7 +732,6 @@ class Instruction: :return: """ state = global_state.mstate - val = state.stack.pop() exp = Not(val) if isinstance(val, Bool) else val == 0 @@ -1395,7 +1394,6 @@ class Instruction: state.mem_extend(offset, 32) data = state.memory.get_word_at(offset) - state.stack.append(data) return [global_state] @@ -1518,7 +1516,6 @@ class Instruction: states = [] op0, condition = state.stack.pop(), state.stack.pop() - try: jump_addr = util.get_concrete_int(op0) except TypeError: @@ -1712,7 +1709,6 @@ class Instruction: :return: """ call_value, mem_offset, mem_size = global_state.mstate.pop(3) - return self._create_transaction_helper( global_state, call_value, mem_offset, mem_size ) @@ -1837,6 +1833,27 @@ class Instruction: """ global_state.current_transaction.end(global_state) + @staticmethod + def _write_symbolic_returndata( + global_state: GlobalState, memory_out_offset: BitVec, memory_out_size: BitVec + ): + """ + Writes symbolic return-data into memory, The memory offset and size should be concrete + :param global_state: + :param memory_out_offset: + :param memory_out_size: + :return: + """ + if memory_out_offset.symbolic is True or memory_out_size.symbolic is True: + return + for i in range(memory_out_size.value): + global_state.mstate.memory[memory_out_offset + i] = global_state.new_bitvec( + "call_output_var({})_{}".format( + simplify(memory_out_offset + i), global_state.mstate.pc, + ), + 8, + ) + @StateTransition() def call_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1847,6 +1864,7 @@ class Instruction: instr = global_state.get_current_instruction() environment = global_state.environment + memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5] try: ( callee_address, @@ -1875,6 +1893,9 @@ class Instruction: e ) ) + self._write_symbolic_returndata( + global_state, memory_out_offset, memory_out_size + ) # TODO: decide what to do in this case global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) @@ -1933,7 +1954,7 @@ class Instruction: """ instr = global_state.get_current_instruction() environment = global_state.environment - + memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5] try: ( callee_address, @@ -1944,6 +1965,7 @@ class Instruction: _, _, ) = get_call_parameters(global_state, self.dynamic_loader, True) + if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") sender = global_state.environment.active_account.address @@ -1961,6 +1983,9 @@ class Instruction: e ) ) + 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) ) @@ -1988,7 +2013,7 @@ class Instruction: :return: """ instr = global_state.get_current_instruction() - + memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5] try: ( callee_address, @@ -2005,6 +2030,9 @@ class Instruction: e ) ) + 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) ) @@ -2016,6 +2044,9 @@ class Instruction: "retval_" + str(instr["address"]), 256 ) global_state.mstate.stack.append(return_value) + self._write_symbolic_returndata( + global_state, memory_out_offset, memory_out_size + ) global_state.world_state.constraints.append(return_value == 0) return [global_state] @@ -2060,6 +2091,7 @@ class Instruction: """ instr = global_state.get_current_instruction() environment = global_state.environment + memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4] try: ( @@ -2089,6 +2121,9 @@ class Instruction: e ) ) + 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) ) @@ -2116,6 +2151,7 @@ class Instruction: :return: """ instr = global_state.get_current_instruction() + memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4] try: ( @@ -2136,6 +2172,9 @@ class Instruction: global_state.mstate.stack.append( global_state.new_bitvec("retval_" + str(instr["address"]), 256) ) + self._write_symbolic_returndata( + global_state, memory_out_offset, memory_out_size + ) return [global_state] if global_state.last_return_data is None: @@ -2188,6 +2227,7 @@ class Instruction: """ instr = global_state.get_current_instruction() environment = global_state.environment + memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4] try: ( callee_address, @@ -2216,6 +2256,9 @@ class Instruction: e ) ) + 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) ) @@ -2248,6 +2291,10 @@ class Instruction: def post_handler(self, global_state, function_name: str): instr = global_state.get_current_instruction() + if function_name in ("staticcall", "delegatecall"): + memory_out_size, memory_out_offset = global_state.mstate.stack[-6:-4] + else: + memory_out_size, memory_out_offset = global_state.mstate.stack[-7:-5] try: with_value = function_name is not "staticcall" @@ -2266,6 +2313,9 @@ class Instruction: function_name, e ) ) + 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) ) diff --git a/tests/instructions/static_call_test.py b/tests/instructions/static_call_test.py index 70cbccdc..0d27eb21 100644 --- a/tests/instructions/static_call_test.py +++ b/tests/instructions/static_call_test.py @@ -90,7 +90,7 @@ def test_staticness_call_concrete(f1, input, success): # Arrange state = get_global_state() state.environment.static = True - state.mstate.stack = [] + state.mstate.stack = [10] * 100 code = Disassembly(code="616263") f1.return_value = ("0", Account(code=code, address="0x19"), 0, input, 0, 0, 0) instruction = Instruction("call", dynamic_loader=None) @@ -110,7 +110,7 @@ def test_staticness_call_symbolic(f1): # Arrange state = get_global_state() state.environment.static = True - state.mstate.stack = [] + state.mstate.stack = [10] * 100 call_value = symbol_factory.BitVecSym("x", 256) code = Disassembly(code="616263") f1.return_value = ("0", Account(code=code, address="0x19"), 0, call_value, 0, 0, 0)