From e9c5f6a89756b521d896fd1455308f5bb5f31f44 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 16 May 2022 14:24:44 +0100 Subject: [PATCH] Use a more precise modeling of return data (#1630) * remove depth for jump * Use a more precise modeling of return data * Fix issues with lists * Fix issues --- mythril/laser/ethereum/instructions.py | 90 ++++++++++++++----- mythril/laser/ethereum/state/return_data.py | 32 +++++++ mythril/laser/ethereum/svm.py | 3 +- .../transaction/transaction_models.py | 26 ++++-- mythril/laser/smt/bitvec_helper.py | 10 ++- 5 files changed, 125 insertions(+), 36 deletions(-) create mode 100644 mythril/laser/ethereum/state/return_data.py diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b06fc99d..7886015a 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -52,6 +52,8 @@ from mythril.laser.ethereum.evm_exceptions import ( ) from mythril.laser.ethereum.instruction_data import get_opcode_gas, calculate_sha3_gas from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.return_data import ReturnData + from mythril.laser.ethereum.transaction import ( MessageCallTransaction, TransactionStartSignal, @@ -1340,7 +1342,7 @@ class Instruction: for i in range(concrete_size): global_state.mstate.memory[concrete_memory_offset + i] = ( global_state.last_return_data[concrete_return_offset + i] - if i < len(global_state.last_return_data) + if i < global_state.last_return_data.size else 0 ) @@ -1353,16 +1355,10 @@ class Instruction: :param global_state: :return: """ - if global_state.last_return_data is None: - log.debug( - "No last_return_data found, adding an unconstrained bitvec to the stack" - ) - global_state.mstate.stack.append( - global_state.new_bitvec("returndatasize", 256) - ) + if global_state.last_return_data: + global_state.mstate.stack.append(global_state.last_return_data.size) else: - global_state.mstate.stack.append(len(global_state.last_return_data)) - + global_state.mstate.stack.append(0) return [global_state] @StateTransition() @@ -1865,7 +1861,9 @@ class Instruction: state.mem_extend(offset, length) StateTransition.check_gas_usage_limit(global_state) return_data = state.memory[offset : offset + length] - global_state.current_transaction.end(global_state, return_data) + global_state.current_transaction.end( + global_state, ReturnData(return_data, length) + ) @StateTransition(is_state_mutation_instruction=True) def selfdestruct_(self, global_state: GlobalState): @@ -1898,7 +1896,25 @@ class Instruction: """ state = global_state.mstate offset, length = state.stack.pop(), state.stack.pop() - return_data = [global_state.new_bitvec("return_data", 8)] + if length.symbolic is False: + return_data = [ + global_state.new_bitvec( + f"{global_state.current_transaction.id}_return_data_{i}", 8 + ) + for i in range(length.value) + ] + else: + return_data = [ + If( + i < length, + global_state.new_bitvec( + f"{global_state.current_transaction.id}_return_data_{i}", 8 + ), + 0, + ) + for i in range(300) + ] + try: return_data = state.memory[ util.get_concrete_int(offset) : util.get_concrete_int(offset + length) @@ -1906,7 +1922,7 @@ class Instruction: except TypeError: log.debug("Return with symbolic length or offset. Not supported") global_state.current_transaction.end( - global_state, return_data=return_data, revert=True + global_state, return_data=ReturnData(return_data, length), revert=True ) @StateTransition() @@ -1947,13 +1963,27 @@ class Instruction: """ if memory_out_offset.symbolic is True or memory_out_size.symbolic is True: return + return_data = [] + return_data_size = global_state.new_bitvec("returndatasize", 256) + for i in range(memory_out_size.value): - global_state.mstate.memory[memory_out_offset + i] = global_state.new_bitvec( + data = global_state.new_bitvec( "call_output_var({})_{}".format( simplify(memory_out_offset + i), global_state.mstate.pc ), 8, ) + return_data.append(data) + for i in range(memory_out_size.value): + global_state.mstate.memory[memory_out_offset + i] = If( + i <= return_data_size, + return_data[i], + global_state.mstate.memory[memory_out_offset + i], + ) + + global_state.last_return_data = ReturnData( + return_data=return_data, return_data_size=return_data_size + ) @StateTransition() def call_(self, global_state: GlobalState) -> List[GlobalState]: @@ -1982,6 +2012,9 @@ class Instruction: sender = environment.active_account.address receiver = callee_account.address transfer_ether(global_state, sender, receiver, value) + 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) @@ -2072,6 +2105,9 @@ class Instruction: sender = global_state.environment.active_account.address receiver = callee_account.address transfer_ether(global_state, sender, receiver, value) + 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) @@ -2176,9 +2212,9 @@ class Instruction: # Copy memory global_state.mstate.mem_extend( - memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) + memory_out_offset, min(memory_out_size, global_state.last_return_data.size) ) - for i in range(min(memory_out_size, len(global_state.last_return_data))): + for i in range(min(memory_out_size, global_state.last_return_data.size)): global_state.mstate.memory[ i + memory_out_offset ] = global_state.last_return_data[i] @@ -2216,6 +2252,9 @@ class Instruction: sender = global_state.environment.active_account.address receiver = callee_account.address transfer_ether(global_state, sender, receiver, value) + 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) @@ -2317,9 +2356,9 @@ class Instruction: # Copy memory global_state.mstate.mem_extend( - memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) + memory_out_offset, min(memory_out_size, global_state.last_return_data.size) ) - for i in range(min(memory_out_size, len(global_state.last_return_data))): + for i in range(min(memory_out_size, global_state.last_return_data.size)): global_state.mstate.memory[ i + memory_out_offset ] = global_state.last_return_data[i] @@ -2356,10 +2395,13 @@ class Instruction: sender = environment.active_account.address receiver = callee_account.address transfer_ether(global_state, sender, receiver, value) - + 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] except ValueError as e: @@ -2458,17 +2500,19 @@ class Instruction: ) return [global_state] - # Copy memory global_state.mstate.mem_extend( - memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) + memory_out_offset, min(memory_out_size, global_state.last_return_data.size) ) - for i in range(min(memory_out_size, len(global_state.last_return_data))): + + for i in range(min(memory_out_size, global_state.last_return_data.size)): global_state.mstate.memory[ i + memory_out_offset ] = global_state.last_return_data[i] # Put return value on stack - return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256) + return_value = global_state.new_bitvec( + "retval_" + str(global_state.get_current_instruction()["address"]), 256 + ) global_state.mstate.stack.append(return_value) global_state.world_state.constraints.append(return_value == 1) diff --git a/mythril/laser/ethereum/state/return_data.py b/mythril/laser/ethereum/state/return_data.py new file mode 100644 index 00000000..ce4f930c --- /dev/null +++ b/mythril/laser/ethereum/state/return_data.py @@ -0,0 +1,32 @@ +"""This module declares classes to represent call data.""" +from typing import List + +from mythril.laser.smt import ( + BitVec, +) + + +class ReturnData: + """Base returndata class.""" + + def __init__(self, return_data: List[BitVec], return_data_size: BitVec) -> None: + """ + + :param tx_id: + """ + self.return_data = return_data + self.return_data_size = return_data_size + + @property + def size(self) -> BitVec: + """ + + :return: Calldata size for this calldata object + """ + return self.return_data_size + + def __getitem__(self, index): + if index < self.size: + return self.return_data[index] + else: + return 0 diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 09dc7c7e..0e02df3e 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -270,6 +270,7 @@ class LaserEVM: hook() for global_state in self.strategy: + if create and self._check_create_termination(): log.debug("Hit create timeout, returning.") return final_states + [global_state] if track_gas else None @@ -277,13 +278,11 @@ class LaserEVM: if not create and self._check_execution_termination(): log.debug("Hit execution timeout, returning.") return final_states + [global_state] if track_gas else None - try: new_states, op_code = self.execute_state(global_state) except NotImplementedError: log.debug("Encountered unimplemented instruction") continue - if args.sparse_pruning is False: new_states = [ state diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index f354402e..c519af44 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -148,12 +148,20 @@ class BaseTransaction: raise NotImplementedError def __str__(self) -> str: - return "{} {} from {} to {:#42x}".format( - self.__class__.__name__, - self.id, - self.caller, - int(str(self.callee_account.address)) if self.callee_account else -1, - ) + if self.callee_account is None or self.callee_account.address.symbolic is False: + return "{} {} from {} to {:#42x}".format( + self.__class__.__name__, + self.id, + self.caller, + int(str(self.callee_account.address)) if self.callee_account else -1, + ) + else: + return "{} {} from {} to {}".format( + self.__class__.__name__, + self.id, + self.caller, + str(self.callee_account.address), + ) class MessageCallTransaction(BaseTransaction): @@ -258,11 +266,13 @@ class ContractCreationTransaction(BaseTransaction): :param revert: """ - if return_data is None or len(return_data) == 0: + if return_data is None or return_data.size == 0: self.return_data = None raise TransactionEndSignal(global_state, revert=revert) - global_state.environment.active_account.code.assign_bytecode(tuple(return_data)) + global_state.environment.active_account.code.assign_bytecode( + tuple(return_data.return_data) + ) self.return_data = str( hex(global_state.environment.active_account.address.value) ) diff --git a/mythril/laser/smt/bitvec_helper.py b/mythril/laser/smt/bitvec_helper.py index da39000f..e8b3304f 100644 --- a/mythril/laser/smt/bitvec_helper.py +++ b/mythril/laser/smt/bitvec_helper.py @@ -59,11 +59,15 @@ def If( if isinstance(b, BaseArray) and isinstance(c, BaseArray): array = z3.If(a.raw, b.raw, c.raw) return _z3_array_converter(array) - + default_sort_size = 256 + if isinstance(b, BitVec): + default_sort_size = b.size() + if isinstance(c, BitVec): + default_sort_size = c.size() if not isinstance(b, BitVec): - b = BitVec(z3.BitVecVal(b, 256)) + b = BitVec(z3.BitVecVal(b, default_sort_size)) if not isinstance(c, BitVec): - c = BitVec(z3.BitVecVal(c, 256)) + c = BitVec(z3.BitVecVal(c, default_sort_size)) union = a.annotations.union(b.annotations).union(c.annotations) return BitVec(z3.If(a.raw, b.raw, c.raw), union)