From 01724da877971027ea82a080a8e202c20bea69c0 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Tue, 20 Aug 2019 00:29:46 -0700 Subject: [PATCH 01/13] Added new calculation to codesize. --- mythril/laser/ethereum/instructions.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 5d2b9e93..1895eefe 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -902,7 +902,8 @@ class Instruction: state = global_state.mstate environment = global_state.environment disassembly = environment.code - state.stack.append(len(disassembly.bytecode) // 2) + no_of_bytes = min(len(disassembly.bytecode) / 2, 320) + (len(disassembly.bytecode) / 2) + state.stack.append(no_of_bytes) return [global_state] @StateTransition(enable_gas=False) From 4295b828f5810749baf3f037c76dda62e53c2c76 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 21 Aug 2019 00:21:53 -0700 Subject: [PATCH 02/13] Starting implementation of creationdata. --- mythril/laser/ethereum/state/creationdata.py | 51 ++++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 mythril/laser/ethereum/state/creationdata.py diff --git a/mythril/laser/ethereum/state/creationdata.py b/mythril/laser/ethereum/state/creationdata.py new file mode 100644 index 00000000..dbcd2991 --- /dev/null +++ b/mythril/laser/ethereum/state/creationdata.py @@ -0,0 +1,51 @@ +"""This module declares classes to represent creation code and call data.""" +from typing import cast, Union, Tuple, List + + +from enum import Enum +from typing import Any, Union + +from z3 import Model +from z3.z3types import Z3Exception + +from mythril.laser.ethereum.util import get_concrete_int +from mythril.laser.smt import ( + Array, + BitVec, + Bool, + Concat, + Expression, + If, + K, + simplify, + symbol_factory, +) + +from mythril.laser.smt.bitvec_helper import Sum + +from mythril.laser.ethereum.state.calldata import BaseCalldata + + +class CreationData: + """CreationData class This represents creation bytecode and calldata constructor argument provided when sending a + transaction to a contract.""" + + def __init__(self, code, calldata: BaseCalldata) -> None: + """ + + :param tx_id: + """ + self.code = code + self.calldata = calldata + + @property + def size(self) -> BitVec: + """ + + :return: codesize in bytes for this CreationData object + """ + calldata_size = self.calldata.calldatasize + code_size = symbol_factory.BitVecVal(len(self.code) // 2, 256) + if calldata_size.symbolic: + return Sum(code_size, calldata_size) + return code_size + calldata_size From 871907f6c314d73ea2a885e07abf8c1d823afe3e Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 21 Aug 2019 10:27:51 -0400 Subject: [PATCH 03/13] Add checks for creation transaction in codesize/codecopy/calldatasize/calldatacopy --- mythril/laser/ethereum/instructions.py | 76 +++++++++++++------ .../laser/ethereum/transaction/symbolic.py | 4 +- .../transaction/transaction_models.py | 4 +- 3 files changed, 59 insertions(+), 25 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 1895eefe..d010be0a 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -758,34 +758,33 @@ class Instruction: """ state = global_state.mstate environment = global_state.environment - state.stack.append(environment.calldata.calldatasize) - return [global_state] - @StateTransition() - def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: - """ + if isinstance(global_state.current_transaction, ContractCreationTransaction): + log.debug("Attempt to use CALLDATASIZE in creation transaction") + state.stack.append(0) + else: + state.stack.append(environment.calldata.calldatasize) - :param global_state: - :return: - """ - state = global_state.mstate + return [global_state] + + @staticmethod + def _calldata_copy_helper(global_state, state, mstart, dstart, size): environment = global_state.environment - op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() try: - mstart = util.get_concrete_int(op0) + mstart = util.get_concrete_int(mstart) except TypeError: log.debug("Unsupported symbolic memory offset in CALLDATACOPY") return [global_state] try: - dstart = util.get_concrete_int(op1) # type: Union[int, BitVec] + dstart = util.get_concrete_int(dstart) # type: Union[int, BitVec] except TypeError: log.debug("Unsupported symbolic calldata offset in CALLDATACOPY") - dstart = simplify(op1) + dstart = simplify(dstart) try: - size = util.get_concrete_int(op2) # type: Union[int, BitVec] + size = util.get_concrete_int(size) # type: Union[int, BitVec] except TypeError: log.debug("Unsupported symbolic size in CALLDATACOPY") size = 320 # The excess size will get overwritten @@ -839,6 +838,22 @@ class Instruction: ) return [global_state] + @StateTransition() + def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]: + """ + + :param global_state: + :return: + """ + state = global_state.mstate + op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop() + + if isinstance(global_state.current_transaction, ContractCreationTransaction): + log.debug("Attempt to use CALLDATACOPY in creation transaction") + return [global_state] + + return self._calldata_copy_helper(global_state, state, op0, op1, op2) + # Environment @StateTransition() def address_(self, global_state: GlobalState) -> List[GlobalState]: @@ -902,7 +917,12 @@ class Instruction: state = global_state.mstate environment = global_state.environment disassembly = environment.code - no_of_bytes = min(len(disassembly.bytecode) / 2, 320) + (len(disassembly.bytecode) / 2) + if isinstance(global_state.current_transaction, ContractCreationTransaction): + # Hacky way to ensure constructor arguments work - Max size is 5000 + # FIXME: Perhaps add some constraint here to ensure that concretization works correctly + no_of_bytes = len(disassembly.bytecode) // 2 + 5000 + else: + no_of_bytes = len(disassembly.bytecode) // 2 state.stack.append(no_of_bytes) return [global_state] @@ -1027,14 +1047,24 @@ class Instruction: global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), ) - return self._code_copy_helper( - code=global_state.environment.code.bytecode, - memory_offset=memory_offset, - code_offset=code_offset, - size=size, - op="CODECOPY", - global_state=global_state, - ) + + if ( + isinstance(global_state.current_transaction, ContractCreationTransaction) + and code_offset >= len(global_state.environment.code.bytecode) // 2 + ): + offset = code_offset - len(global_state.environment.code.bytecode) // 2 + return self._calldata_copy_helper( + global_state, global_state.mstate, memory_offset, offset, size + ) + else: + return self._code_copy_helper( + code=global_state.environment.code.bytecode, + memory_offset=memory_offset, + code_offset=code_offset, + size=size, + op="CODECOPY", + global_state=global_state, + ) @StateTransition() def extcodesize_(self, global_state: GlobalState) -> List[GlobalState]: diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 2212e805..ae18d3a3 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -85,6 +85,8 @@ def execute_contract_creation( new_account = None for open_world_state in open_states: next_transaction_id = get_next_transaction_id() + # call_data "should" be '[]', but it is easier to model the calldata symbolically + # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly" transaction = ContractCreationTransaction( world_state=open_world_state, identifier=next_transaction_id, @@ -98,7 +100,7 @@ def execute_contract_creation( code=Disassembly(contract_initialization_code), caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), contract_name=contract_name, - call_data=[], + call_data=None, # Hrmm call_value=symbol_factory.BitVecSym( "call_value{}".format(next_transaction_id), 256 ), diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index c2b18b9c..97f2f694 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -197,6 +197,8 @@ class ContractCreationTransaction(BaseTransaction): 0, concrete_storage=True, creator=caller.value ) callee_account.contract_name = contract_name + # init_call_data "should" be false, but it is easier to model the calldata symbolically + # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly" super().__init__( world_state=world_state, callee_account=callee_account, @@ -208,7 +210,7 @@ class ContractCreationTransaction(BaseTransaction): origin=origin, code=code, call_value=call_value, - init_call_data=False, + init_call_data=True, ) def initial_global_state(self) -> GlobalState: From 7096a2806b036f6a97007ad0321f80a6ee08c958 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 21 Aug 2019 08:27:26 -0700 Subject: [PATCH 04/13] Removed creationdata as is unnecessary for now. --- mythril/laser/ethereum/state/creationdata.py | 51 -------------------- 1 file changed, 51 deletions(-) delete mode 100644 mythril/laser/ethereum/state/creationdata.py diff --git a/mythril/laser/ethereum/state/creationdata.py b/mythril/laser/ethereum/state/creationdata.py deleted file mode 100644 index dbcd2991..00000000 --- a/mythril/laser/ethereum/state/creationdata.py +++ /dev/null @@ -1,51 +0,0 @@ -"""This module declares classes to represent creation code and call data.""" -from typing import cast, Union, Tuple, List - - -from enum import Enum -from typing import Any, Union - -from z3 import Model -from z3.z3types import Z3Exception - -from mythril.laser.ethereum.util import get_concrete_int -from mythril.laser.smt import ( - Array, - BitVec, - Bool, - Concat, - Expression, - If, - K, - simplify, - symbol_factory, -) - -from mythril.laser.smt.bitvec_helper import Sum - -from mythril.laser.ethereum.state.calldata import BaseCalldata - - -class CreationData: - """CreationData class This represents creation bytecode and calldata constructor argument provided when sending a - transaction to a contract.""" - - def __init__(self, code, calldata: BaseCalldata) -> None: - """ - - :param tx_id: - """ - self.code = code - self.calldata = calldata - - @property - def size(self) -> BitVec: - """ - - :return: codesize in bytes for this CreationData object - """ - calldata_size = self.calldata.calldatasize - code_size = symbol_factory.BitVecVal(len(self.code) // 2, 256) - if calldata_size.symbolic: - return Sum(code_size, calldata_size) - return code_size + calldata_size From d390b4a6a48aaed4f88703e52bd6a98e416d7ecc Mon Sep 17 00:00:00 2001 From: Nathan Date: Wed, 21 Aug 2019 11:47:14 -0400 Subject: [PATCH 05/13] Remove confusing comment --- mythril/laser/ethereum/transaction/symbolic.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index ae18d3a3..b8b6692c 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -100,7 +100,7 @@ def execute_contract_creation( code=Disassembly(contract_initialization_code), caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256), contract_name=contract_name, - call_data=None, # Hrmm + call_data=None, call_value=symbol_factory.BitVecSym( "call_value{}".format(next_transaction_id), 256 ), From 97ab3f9e9a4e140e72616e1613a1725c3c9fba51 Mon Sep 17 00:00:00 2001 From: Nathan Date: Mon, 26 Aug 2019 08:35:43 -0400 Subject: [PATCH 06/13] Add a descriptive comment to codecopy_ --- mythril/laser/ethereum/instructions.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index d010be0a..d79a7ca5 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1051,7 +1051,10 @@ class Instruction: if ( isinstance(global_state.current_transaction, ContractCreationTransaction) and code_offset >= len(global_state.environment.code.bytecode) // 2 - ): + ):ce + # Treat creation code after the expected disassembly as calldata. + # This is a slightly hacky way to ensure that symbolic constructor + # arguments work correctly. offset = code_offset - len(global_state.environment.code.bytecode) // 2 return self._calldata_copy_helper( global_state, global_state.mstate, memory_offset, offset, size From 3979cc27f2c569ced63b9f83516c1fc2ed34765c Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 27 Aug 2019 08:29:44 -0400 Subject: [PATCH 07/13] Fix typo --- mythril/laser/ethereum/instructions.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index d79a7ca5..6cf0d231 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1051,7 +1051,7 @@ class Instruction: if ( isinstance(global_state.current_transaction, ContractCreationTransaction) and code_offset >= len(global_state.environment.code.bytecode) // 2 - ):ce + ): # Treat creation code after the expected disassembly as calldata. # This is a slightly hacky way to ensure that symbolic constructor # arguments work correctly. From 35690d2dc797a44c8e880e0faf03f66601aca139 Mon Sep 17 00:00:00 2001 From: Eric N Date: Wed, 28 Aug 2019 23:22:00 -0700 Subject: [PATCH 08/13] Refactored delegatecall to ignore post conditions. --- mythril/analysis/modules/delegatecall.py | 58 ++++++++---------------- 1 file changed, 20 insertions(+), 38 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index b0e0435d..3fd2c3dc 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -84,7 +84,7 @@ class DelegateCallModule(DetectionModule): swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, description="Check for invocations of delegatecall(msg.data) in the fallback function.", entrypoint="callback", - pre_hooks=["DELEGATECALL", "RETURN", "STOP"], + pre_hooks=["DELEGATECALL"], ) def _execute(self, state: GlobalState) -> None: @@ -108,48 +108,30 @@ class DelegateCallModule(DetectionModule): """ issues = [] op_code = state.get_current_instruction()["opcode"] - annotations = cast( - List[DelegateCallAnnotation], - list(state.get_annotations(DelegateCallAnnotation)), - ) - - if len(annotations) == 0 and op_code in ("RETURN", "STOP"): - return [] - if op_code == "DELEGATECALL": - gas = state.mstate.stack[-1] - to = state.mstate.stack[-2] + gas = state.mstate.stack[-1] + to = state.mstate.stack[-2] - constraints = [ - to == ATTACKER_ADDRESS, - UGT(gas, symbol_factory.BitVecVal(2300, 256)), - ] + constraints = [ + to == ATTACKER_ADDRESS, + UGT(gas, symbol_factory.BitVecVal(2300, 256)), + ] - for tx in state.world_state.transaction_sequence: - if not isinstance(tx, ContractCreationTransaction): - constraints.append(tx.caller == ATTACKER_ADDRESS) - - state.annotate(DelegateCallAnnotation(state, constraints)) + for tx in state.world_state.transaction_sequence: + if not isinstance(tx, ContractCreationTransaction): + constraints.append(tx.caller == ATTACKER_ADDRESS) + try: + transaction_sequence = solver.get_transaction_sequence( + state, state.mstate.constraints + constraints + ) + return [ + DelegateCallAnnotation(state, constraints).get_issue( + state, transaction_sequence=transaction_sequence + ) + ] + except UnsatError: return [] - else: - for annotation in annotations: - try: - transaction_sequence = solver.get_transaction_sequence( - state, - state.mstate.constraints - + annotation.constraints - + [annotation.return_value == 1], - ) - issues.append( - annotation.get_issue( - state, transaction_sequence=transaction_sequence - ) - ) - except UnsatError: - continue - - return issues detector = DelegateCallModule() From 7c2f3dffc6d6192cec32718c26903d03deef6ad0 Mon Sep 17 00:00:00 2001 From: Eric N Date: Wed, 28 Aug 2019 23:51:33 -0700 Subject: [PATCH 09/13] Fix mypy --- mythril/analysis/modules/delegatecall.py | 1 - 1 file changed, 1 deletion(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 3fd2c3dc..7e15567a 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -106,7 +106,6 @@ class DelegateCallModule(DetectionModule): :param state: the current state :return: returns the issues for that corresponding state """ - issues = [] op_code = state.get_current_instruction()["opcode"] gas = state.mstate.stack[-1] From e64dcbd05deaff9ca90b93cffe087f2bfc931ebb Mon Sep 17 00:00:00 2001 From: Eric N Date: Thu, 29 Aug 2019 07:47:06 -0700 Subject: [PATCH 10/13] Removed DelegateCallAnnotation --- mythril/analysis/modules/delegatecall.py | 83 ++++++++---------------- 1 file changed, 27 insertions(+), 56 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 7e15567a..98453614 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -20,60 +20,6 @@ from mythril.laser.smt import symbol_factory, UGT log = logging.getLogger(__name__) -class DelegateCallAnnotation(StateAnnotation): - def __init__(self, call_state: GlobalState, constraints: List) -> None: - """ - Initialize DelegateCall Annotation - :param call_state: Call state - """ - self.call_state = call_state - self.constraints = constraints - self.return_value = call_state.new_bitvec( - "retval_{}".format(call_state.get_current_instruction()["address"]), 256 - ) - - def _copy__(self): - return DelegateCallAnnotation(self.call_state, copy(self.constraints)) - - def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue: - """ - Returns Issue for the annotation - :param global_state: Global State - :param transaction_sequence: Transaction sequence - :return: Issue - """ - - address = self.call_state.get_current_instruction()["address"] - logging.debug( - "[DELEGATECALL] Detected delegatecall to a user-supplied address : {}".format( - address - ) - ) - description_head = "The contract delegates execution to another contract with a user-supplied address." - description_tail = ( - "The smart contract delegates execution to a user-supplied address. Note that callers " - "can execute arbitrary contracts and that the callee contract " - "can access the storage of the calling contract. " - ) - - return Issue( - contract=self.call_state.environment.active_account.contract_name, - function_name=self.call_state.environment.active_function_name, - address=address, - swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, - title="Delegatecall Proxy To User-Supplied Address", - bytecode=global_state.environment.code.bytecode, - severity="Medium", - description_head=description_head, - description_tail=description_tail, - transaction_sequence=transaction_sequence, - gas_used=( - global_state.mstate.min_gas_used, - global_state.mstate.max_gas_used, - ), - ) - - class DelegateCallModule(DetectionModule): """This module detects calldata being forwarded using DELEGATECALL.""" @@ -124,11 +70,36 @@ class DelegateCallModule(DetectionModule): transaction_sequence = solver.get_transaction_sequence( state, state.mstate.constraints + constraints ) + + address = state.get_current_instruction()["address"] + logging.debug( + "[DELEGATECALL] Detected delegatecall to a user-supplied address : {}".format( + address + ) + ) + description_head = "The contract delegates execution to another contract with a user-supplied address." + description_tail = ( + "The smart contract delegates execution to a user-supplied address. Note that callers " + "can execute arbitrary contracts and that the callee contract " + "can access the storage of the calling contract. " + ) + return [ - DelegateCallAnnotation(state, constraints).get_issue( - state, transaction_sequence=transaction_sequence + Issue( + contract=state.environment.active_account.contract_name, + function_name=state.environment.active_function_name, + address=address, + swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT, + bytecode=state.environment.code.bytecode, + title="Delegatecall Proxy To User-Supplied Address", + severity="Medium", + description_head=description_head, + description_tail=description_tail, + transaction_sequence=transaction_sequence, + gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used), ) ] + except UnsatError: return [] From 02835c807de33a12baac25155c7d31db6b8fecef Mon Sep 17 00:00:00 2001 From: Nathan Date: Fri, 30 Aug 2019 10:35:17 -0400 Subject: [PATCH 11/13] Concretize and display calldata transaction data --- mythril/analysis/solver.py | 17 +++++++++-------- .../templates/report_as_markdown.jinja2 | 2 +- .../analysis/templates/report_as_text.jinja2 | 2 +- mythril/laser/ethereum/instructions.py | 11 ++++++++--- 4 files changed, 19 insertions(+), 13 deletions(-) diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index b6959a82..00de6bd4 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -152,16 +152,17 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction): "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long() ).zfill(40) + input_ = "" if isinstance(transaction, ContractCreationTransaction): address = "" - input_ = transaction.code.bytecode - else: - input_ = "".join( - [ - hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] - for b in transaction.call_data.concrete(model) - ] - ) + input_ += transaction.code.bytecode + + input_ += "".join( + [ + hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:] + for b in transaction.call_data.concrete(model) + ] + ) # Create concrete transaction dict concrete_transaction = dict() # type: Dict[str, str] diff --git a/mythril/analysis/templates/report_as_markdown.jinja2 b/mythril/analysis/templates/report_as_markdown.jinja2 index 9e690c43..78b0b7be 100644 --- a/mythril/analysis/templates/report_as_markdown.jinja2 +++ b/mythril/analysis/templates/report_as_markdown.jinja2 @@ -36,7 +36,7 @@ Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} -Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }} +Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }} {% else %} Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }} {% endif %} diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2 index aa5c4876..2201dbcf 100644 --- a/mythril/analysis/templates/report_as_text.jinja2 +++ b/mythril/analysis/templates/report_as_text.jinja2 @@ -29,7 +29,7 @@ Transaction Sequence: {% for step in issue.tx_sequence.steps %} {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %} -Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }} +Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }} {% else %} Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }} {% endif %} diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 6cf0d231..593be817 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -918,9 +918,13 @@ class Instruction: environment = global_state.environment disassembly = environment.code if isinstance(global_state.current_transaction, ContractCreationTransaction): - # Hacky way to ensure constructor arguments work - Max size is 5000 - # FIXME: Perhaps add some constraint here to ensure that concretization works correctly - no_of_bytes = len(disassembly.bytecode) // 2 + 5000 + # Hacky way to ensure constructor arguments work - Pick some reasonably large size. + no_of_bytes = ( + len(disassembly.bytecode) // 2 + 0x200 + ) # space for 16 32-byte arguments + global_state.mstate.constraints.append( + global_state.environment.calldata.size == no_of_bytes + ) else: no_of_bytes = len(disassembly.bytecode) // 2 state.stack.append(no_of_bytes) @@ -1056,6 +1060,7 @@ class Instruction: # This is a slightly hacky way to ensure that symbolic constructor # arguments work correctly. offset = code_offset - len(global_state.environment.code.bytecode) // 2 + log.warning("Doing hacky thing offset: {} size: {}".format(offset, size)) return self._calldata_copy_helper( global_state, global_state.mstate, memory_offset, offset, size ) From c55af2a5a0fe7b0bb13b067ee2aa457087086f62 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Wed, 4 Sep 2019 17:00:28 +0530 Subject: [PATCH 12/13] Implement static call (#991) * Implement static call * Refactor static call tests * Reuse call's post for staticcall * Change variable names and add docstring comments * Rename variable name * change the comment * Fix the tests based on the merge * Fix the tests * Remove extra declaration of WriteProtection * Fix static call test * Add the missing condition in callcode --- mythril/laser/ethereum/evm_exceptions.py | 6 + mythril/laser/ethereum/instructions.py | 192 +++++++++++------- mythril/laser/ethereum/state/environment.py | 4 +- mythril/laser/ethereum/svm.py | 4 +- .../transaction/transaction_models.py | 6 +- tests/instructions/static_call_test.py | 124 +++++++++++ 6 files changed, 260 insertions(+), 76 deletions(-) create mode 100644 tests/instructions/static_call_test.py diff --git a/mythril/laser/ethereum/evm_exceptions.py b/mythril/laser/ethereum/evm_exceptions.py index fd99aed5..7e2a7b8f 100644 --- a/mythril/laser/ethereum/evm_exceptions.py +++ b/mythril/laser/ethereum/evm_exceptions.py @@ -37,6 +37,12 @@ class OutOfGasException(VmException): pass +class WriteProtection(VmException): + """A VM exception denoting that a write operation is executed on a write protected environment""" + + pass + + class ProgramCounterException(VmException): """A VM exception denoting an invalid PC value (No stop instruction is reached).""" diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 5d2b9e93..cb2645ff 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -38,6 +38,7 @@ from mythril.laser.ethereum.evm_exceptions import ( InvalidJumpDestination, InvalidInstruction, OutOfGasException, + WriteProtection, ) from mythril.laser.ethereum.gas import OPCODE_GAS from mythril.laser.ethereum.state.global_state import GlobalState @@ -88,14 +89,18 @@ class StateTransition(object): if `increment_pc=True`. """ - def __init__(self, increment_pc=True, enable_gas=True): + def __init__( + self, increment_pc=True, enable_gas=True, is_state_mutation_instruction=False + ): """ :param increment_pc: :param enable_gas: + :param is_state_mutation_instruction: The function mutates state """ self.increment_pc = increment_pc self.enable_gas = enable_gas + self.is_state_mutation_instruction = is_state_mutation_instruction @staticmethod def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState): @@ -165,6 +170,13 @@ class StateTransition(object): :param global_state: :return: """ + if self.is_state_mutation_instruction and global_state.environment.static: + raise WriteProtection( + "The function {} cannot be executed in a static call".format( + func.__name__[:-1] + ) + ) + new_global_states = self.call_on_state_copy(func, func_obj, global_state) new_global_states = [ self.accumulate_gas(state) for state in new_global_states @@ -1396,7 +1408,7 @@ class Instruction: state.stack.append(global_state.environment.active_account.storage[index]) return [global_state] - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def sstore_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1563,7 +1575,7 @@ class Instruction: global_state.mstate.stack.append(global_state.new_bitvec("gas", 256)) return [global_state] - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def log_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1578,7 +1590,7 @@ class Instruction: # Not supported return [global_state] - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def create_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1586,13 +1598,14 @@ class Instruction: :return: """ # TODO: implement me + state = global_state.mstate state.stack.pop(), state.stack.pop(), state.stack.pop() # Not supported state.stack.append(0) return [global_state] - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def create2_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1628,7 +1641,7 @@ class Instruction: return_data = state.memory[offset : offset + length] global_state.current_transaction.end(global_state, return_data) - @StateTransition() + @StateTransition(is_state_mutation_instruction=True) def suicide_(self, global_state: GlobalState): """ @@ -1733,6 +1746,21 @@ class Instruction: ) return [global_state] + if environment.static: + if isinstance(value, int) and value > 0: + raise WriteProtection( + "Cannot call with non zero value in a static call" + ) + if isinstance(value, BitVec): + if value.symbolic: + global_state.mstate.constraints.append( + value == symbol_factory.BitVecVal(0, 256) + ) + elif value.value > 0: + raise WriteProtection( + "Cannot call with non zero value in a static call" + ) + native_result = native_call( global_state, callee_address, call_data, memory_out_offset, memory_out_size ) @@ -1747,8 +1775,9 @@ class Instruction: callee_account=callee_account, call_data=call_data, call_value=value, + static=environment.static, ) - raise TransactionStartSignal(transaction, self.op_code) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition() def call_post(self, global_state: GlobalState) -> List[GlobalState]: @@ -1757,65 +1786,8 @@ class Instruction: :param global_state: :return: """ - instr = global_state.get_current_instruction() - - try: - callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader, True - ) - except ValueError as e: - log.debug( - "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format( - e - ) - ) - global_state.mstate.stack.append( - global_state.new_bitvec("retval_" + str(instr["address"]), 256) - ) - return [global_state] - - if global_state.last_return_data is None: - # Put return value on stack - return_value = global_state.new_bitvec( - "retval_" + str(instr["address"]), 256 - ) - global_state.mstate.stack.append(return_value) - global_state.mstate.constraints.append(return_value == 0) - return [global_state] - - try: - memory_out_offset = ( - util.get_concrete_int(memory_out_offset) - if isinstance(memory_out_offset, Expression) - else memory_out_offset - ) - memory_out_size = ( - util.get_concrete_int(memory_out_size) - if isinstance(memory_out_size, Expression) - else memory_out_size - ) - except TypeError: - global_state.mstate.stack.append( - global_state.new_bitvec("retval_" + str(instr["address"]), 256) - ) - return [global_state] - - # Copy memory - global_state.mstate.mem_extend( - memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) - ) - for i in range(min(memory_out_size, len(global_state.last_return_data))): - 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) - global_state.mstate.stack.append(return_value) - global_state.mstate.constraints.append(return_value == 1) - - return [global_state] + return self.post_handler(global_state, function_name="call") @StateTransition() def callcode_(self, global_state: GlobalState) -> List[GlobalState]: @@ -1831,7 +1803,6 @@ class Instruction: callee_address, callee_account, call_data, value, gas, _, _ = 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 @@ -1864,8 +1835,9 @@ class Instruction: callee_account=environment.active_account, call_data=call_data, call_value=value, + static=environment.static, ) - raise TransactionStartSignal(transaction, self.op_code) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition() def callcode_post(self, global_state: GlobalState) -> List[GlobalState]: @@ -1949,7 +1921,7 @@ class Instruction: if callee_account is not None and callee_account.code.bytecode == "": log.debug("The call is related to ether transfer between accounts") - sender = environment.active_account.address + sender = global_state.environment.active_account.address receiver = callee_account.address transfer_ether(global_state, sender, receiver, value) @@ -1979,8 +1951,9 @@ class Instruction: callee_account=environment.active_account, call_data=call_data, call_value=environment.callvalue, + static=environment.static, ) - raise TransactionStartSignal(transaction, self.op_code) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition() def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]: @@ -2012,6 +1985,7 @@ class Instruction: "retval_" + str(instr["address"]), 256 ) global_state.mstate.stack.append(return_value) + global_state.mstate.constraints.append(return_value == 0) return [global_state] try: @@ -2053,8 +2027,8 @@ class Instruction: :param global_state: :return: """ - # TODO: implement me instr = global_state.get_current_instruction() + environment = global_state.environment try: callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( global_state, self.dynamic_loader @@ -2062,7 +2036,7 @@ class Instruction: 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 + sender = environment.active_account.address receiver = callee_account.address transfer_ether(global_state, sender, receiver, value) @@ -2085,10 +2059,82 @@ class Instruction: native_result = native_call( global_state, callee_address, call_data, memory_out_offset, memory_out_size ) + if native_result: return native_result - global_state.mstate.stack.append( - global_state.new_bitvec("retval_" + str(instr["address"]), 256) + transaction = MessageCallTransaction( + world_state=global_state.world_state, + gas_price=environment.gasprice, + gas_limit=gas, + origin=environment.origin, + code=callee_account.code, + caller=environment.address, + callee_account=environment.active_account, + call_data=call_data, + call_value=value, + static=True, ) + raise TransactionStartSignal(transaction, self.op_code, global_state) + + def staticcall_post(self, global_state: GlobalState) -> List[GlobalState]: + return self.post_handler(global_state, function_name="staticcall") + + def post_handler(self, global_state, function_name: str): + instr = global_state.get_current_instruction() + + try: + callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( + global_state, self.dynamic_loader, True + ) + except ValueError as e: + log.debug( + "Could not determine required parameters for {}, putting fresh symbol on the stack. \n{}".format( + function_name, e + ) + ) + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + + if global_state.last_return_data is None: + # Put return value on stack + return_value = global_state.new_bitvec( + "retval_" + str(instr["address"]), 256 + ) + global_state.mstate.stack.append(return_value) + return [global_state] + + try: + memory_out_offset = ( + util.get_concrete_int(memory_out_offset) + if isinstance(memory_out_offset, Expression) + else memory_out_offset + ) + memory_out_size = ( + util.get_concrete_int(memory_out_size) + if isinstance(memory_out_size, Expression) + else memory_out_size + ) + except TypeError: + global_state.mstate.stack.append( + global_state.new_bitvec("retval_" + str(instr["address"]), 256) + ) + return [global_state] + + # Copy memory + global_state.mstate.mem_extend( + memory_out_offset, min(memory_out_size, len(global_state.last_return_data)) + ) + for i in range(min(memory_out_size, len(global_state.last_return_data))): + 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) + global_state.mstate.stack.append(return_value) + global_state.mstate.constraints.append(return_value == 1) + return [global_state] diff --git a/mythril/laser/ethereum/state/environment.py b/mythril/laser/ethereum/state/environment.py index a3300f9a..4cfb51e0 100644 --- a/mythril/laser/ethereum/state/environment.py +++ b/mythril/laser/ethereum/state/environment.py @@ -22,6 +22,7 @@ class Environment: callvalue: ExprRef, origin: ExprRef, code=None, + static=False, ) -> None: """ @@ -32,7 +33,7 @@ class Environment: :param callvalue: :param origin: :param code: - :param calldata_type: + :param static: Makes the environment static. """ # Metadata @@ -50,6 +51,7 @@ class Environment: self.gasprice = gasprice self.origin = origin self.callvalue = callvalue + self.static = static def __str__(self) -> str: """ diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 88b362c8..8ef03531 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -324,7 +324,9 @@ class LaserEVM: global_state.transaction_stack ) + [(start_signal.transaction, global_state)] new_global_state.node = global_state.node - new_global_state.mstate.constraints = global_state.mstate.constraints + new_global_state.mstate.constraints = ( + start_signal.global_state.mstate.constraints + ) log.debug("Starting new transaction %s", start_signal.transaction) diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index c2b18b9c..fb62864d 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -45,9 +45,11 @@ class TransactionStartSignal(Exception): self, transaction: Union["MessageCallTransaction", "ContractCreationTransaction"], op_code: str, + global_state: GlobalState, ) -> None: self.transaction = transaction self.op_code = op_code + self.global_state = global_state class BaseTransaction: @@ -66,6 +68,7 @@ class BaseTransaction: code=None, call_value=None, init_call_data=True, + static=False, ) -> None: assert isinstance(world_state, WorldState) self.world_state = world_state @@ -101,7 +104,7 @@ class BaseTransaction: if call_value is not None else symbol_factory.BitVecSym("callvalue{}".format(identifier), 256) ) - + self.static = static self.return_data = None # type: str def initial_global_state_from_environment(self, environment, active_function): @@ -159,6 +162,7 @@ class MessageCallTransaction(BaseTransaction): self.call_value, self.origin, code=self.code or self.callee_account.code, + static=self.static, ) return super().initial_global_state_from_environment( environment, active_function="fallback" diff --git a/tests/instructions/static_call_test.py b/tests/instructions/static_call_test.py new file mode 100644 index 00000000..b9bcc26c --- /dev/null +++ b/tests/instructions/static_call_test.py @@ -0,0 +1,124 @@ +import pytest +from mock import patch + +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.smt import symbol_factory +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.ethereum.call import SymbolicCalldata +from mythril.laser.ethereum.transaction import TransactionStartSignal + +from mythril.laser.ethereum.evm_exceptions import WriteProtection + + +def get_global_state(): + active_account = Account("0x0", code=Disassembly("60606040")) + environment = Environment( + active_account, None, SymbolicCalldata("2"), None, None, None + ) + world_state = WorldState() + world_state.put_account(active_account) + state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) + state.transaction_stack.append( + (MessageCallTransaction(world_state=world_state, gas_limit=8000000), None) + ) + return state + + +@patch( + "mythril.laser.ethereum.instructions.get_call_parameters", + return_value=( + "0", + Account(code=Disassembly(code="0x00"), address="0x19"), + 0, + 0, + 0, + 0, + 0, + ), +) +def test_staticcall(f1): + # Arrange + state = get_global_state() + state.mstate.stack = [10, 10, 10, 10, 10, 10, 10, 10, 0] + instruction = Instruction("staticcall", dynamic_loader=None) + + # Act and Assert + with pytest.raises(TransactionStartSignal) as ts: + instruction.evaluate(state) + assert ts.value.transaction.static + assert ts.value.transaction.initial_global_state().environment.static + + +test_data = ( + "suicide", + "create", + "create2", + "log0", + "log1", + "log2", + "log3", + "log4", + "sstore", +) + + +@pytest.mark.parametrize("input", test_data) +def test_staticness(input): + # Arrange + state = get_global_state() + state.environment.static = True + state.mstate.stack = [] + instruction = Instruction(input, dynamic_loader=None) + + # Act and Assert + with pytest.raises(WriteProtection): + instruction.evaluate(state) + + +test_data_call = ((0, True), (100, False)) + + +@pytest.mark.parametrize("input, success", test_data_call) +@patch("mythril.laser.ethereum.instructions.get_call_parameters") +def test_staticness_call_concrete(f1, input, success): + # Arrange + state = get_global_state() + state.environment.static = True + state.mstate.stack = [] + code = Disassembly(code="616263") + f1.return_value = ("0", Account(code=code, address="0x19"), 0, input, 0, 0, 0) + instruction = Instruction("call", dynamic_loader=None) + + # Act and Assert + if success: + with pytest.raises(TransactionStartSignal) as ts: + instruction.evaluate(state) + assert ts.value.transaction.static + else: + with pytest.raises(WriteProtection): + instruction.evaluate(state) + + +@patch("mythril.laser.ethereum.instructions.get_call_parameters") +def test_staticness_call_symbolic(f1): + # Arrange + state = get_global_state() + state.environment.static = True + state.mstate.stack = [] + 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) + instruction = Instruction("call", dynamic_loader=None) + + # Act and Assert + with pytest.raises(TransactionStartSignal) as ts: + instruction.evaluate(state) + + assert ts.value.transaction.static + assert ts.value.global_state.mstate.constraints[-1] == (call_value == 0) From 4ea9827d663eb1fde412ede78b2a26710b0a1aec Mon Sep 17 00:00:00 2001 From: palkeo Date: Wed, 4 Sep 2019 14:43:58 +0200 Subject: [PATCH 13/13] Propagate annotations to the parent call, when a call succeeds. (#1197) * Propagate annotations to the parent call, when a call succeeds. This makes the MutationPruner behave correctly. * Add a copy_annotations_from method. * Run black. * WIP * Use persist_to_world_state and the world state instead. --- .../plugins/implementations/mutation_pruner.py | 16 ++++++++++++++-- mythril/laser/ethereum/state/annotation.py | 2 ++ 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 86755610..fa6aef58 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -15,7 +15,10 @@ class MutationAnnotation(StateAnnotation): This is the annotation used by the MutationPruner plugin to record mutations """ - pass + @property + def persist_to_world_state(self): + # This should persist among calls, and be but as a world state annotation. + return True class MutationPruner(LaserPlugin): @@ -44,10 +47,16 @@ class MutationPruner(LaserPlugin): @symbolic_vm.pre_hook("SSTORE") def sstore_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + assert len( + list(global_state.world_state.get_annotations(MutationAnnotation)) + ) @symbolic_vm.pre_hook("CALL") def call_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + assert len( + list(global_state.world_state.get_annotations(MutationAnnotation)) + ) @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): @@ -63,5 +72,8 @@ class MutationPruner(LaserPlugin): global_state.current_transaction, ContractCreationTransaction ): return - if len(list(global_state.get_annotations(MutationAnnotation))) == 0: + if ( + len(list(global_state.world_state.get_annotations(MutationAnnotation))) + == 0 + ): raise PluginSkipWorldState diff --git a/mythril/laser/ethereum/state/annotation.py b/mythril/laser/ethereum/state/annotation.py index 6a321776..0f25a311 100644 --- a/mythril/laser/ethereum/state/annotation.py +++ b/mythril/laser/ethereum/state/annotation.py @@ -12,6 +12,8 @@ class StateAnnotation: traverse the state space themselves. """ + # TODO: Remove this? It seems to be used only in the MutationPruner, and + # we could simply use world state annotations if we want them to be persisted. @property def persist_to_world_state(self) -> bool: """If this function returns true then laser will also annotate the