From 9dc1007a152eac16b3216298b4bd3f9a6ec68974 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 13:26:24 -0700 Subject: [PATCH 01/28] Implemented extcodehash --- mythril/laser/ethereum/instructions.py | 26 ++++++++++++---- tests/instructions/extcodehash_test.py | 43 ++++++++++++++++++++++++++ 2 files changed, 63 insertions(+), 6 deletions(-) create mode 100644 tests/instructions/extcodehash_test.py diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 16cb4d38..531aaf03 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -46,6 +46,8 @@ from mythril.laser.ethereum.transaction import ( ContractCreationTransaction, ) +from mythril.support.support_utils import get_code_hash + from mythril.support.loader import DynLoader log = logging.getLogger(__name__) @@ -1155,18 +1157,30 @@ class Instruction: global_state=global_state, ) - @StateTransition + @StateTransition() def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]: """ :param global_state: :return: List of global states possible, list of size 1 in this case """ - # TODO: To be implemented - address = global_state.mstate.stack.pop() - global_state.mstate.stack.append( - global_state.new_bitvec("extcodehash_{}".format(str(address)), 256) - ) + world_state = global_state.world_state + stack = global_state.mstate.stack + address = stack.pop() + if address.symbolic: + log.debug("unsupported symbolic address for EXTCODEHASH") + stack.append(global_state.new_bitvec("extcodehash_" + str(address), 256)) + return [global_state] + address = address.value + + mask = int((symbol_factory.BitVecVal(TT256M1, 256) >> 96).value) + address = address & mask + if address not in world_state.accounts: + code_hash = symbol_factory.BitVecVal(0, 256) + else: + code = world_state.accounts_exist_or_load(hex(address), self.dynamic_loader) + code_hash = get_code_hash(code) + stack.append(code_hash) return [global_state] @StateTransition() diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py new file mode 100644 index 00000000..e4586285 --- /dev/null +++ b/tests/instructions/extcodehash_test.py @@ -0,0 +1,43 @@ +from mythril.disassembler.disassembly import Disassembly +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.support.support_utils import get_code_hash + +from mythril.laser.smt import symbol_factory + +def test_extcodehash_concrete(): + # Arrange + world_state = WorldState() + account = world_state.create_account(balance=10, address=101) + account.code = Disassembly("60606040") + world_state.create_account(balance = 10, address = 1000) + environment = Environment(account, None, None, None, None, None) + og_state = GlobalState( + world_state, environment, None, MachineState(gas_limit=8000000) + ) + og_state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + + instruction = Instruction("extcodehash", dynamic_loader=None) + + # If account does not exist, return 0 + og_state.mstate.stack = [symbol_factory.BitVecVal(1, 256)] + new_state = instruction.evaluate(og_state)[0] + assert new_state.mstate.stack[-1] == 0 + + # If account code does not exist, return hash of empty set. + og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)] + new_state = instruction.evaluate(og_state)[0] + assert new_state.mstate.stack[-1] == '0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470' + + # If account code exists, return hash of the code. + og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)] + new_state = instruction.evaluate(og_state)[0] + assert new_state.mstate.stack[-1] == get_code_hash("60606040") \ No newline at end of file From 1a0ea91267af3323c71b44f1d1c44b20a9339e65 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 15:20:00 -0700 Subject: [PATCH 02/28] Refactored instructions for extcodehash and its test --- mythril/laser/ethereum/instructions.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 531aaf03..17173363 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1166,15 +1166,14 @@ class Instruction: """ world_state = global_state.world_state stack = global_state.mstate.stack - address = stack.pop() + address = Extract(159, 0, stack.pop()) + if address.symbolic: log.debug("unsupported symbolic address for EXTCODEHASH") stack.append(global_state.new_bitvec("extcodehash_" + str(address), 256)) return [global_state] address = address.value - - mask = int((symbol_factory.BitVecVal(TT256M1, 256) >> 96).value) - address = address & mask + if address not in world_state.accounts: code_hash = symbol_factory.BitVecVal(0, 256) else: From 268d5d3bbbd136aaa01f782d69f021f813fd09df Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 15:27:36 -0700 Subject: [PATCH 03/28] Ran black --- tests/instructions/extcodehash_test.py | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py index e4586285..c677d5ef 100644 --- a/tests/instructions/extcodehash_test.py +++ b/tests/instructions/extcodehash_test.py @@ -11,12 +11,13 @@ from mythril.support.support_utils import get_code_hash from mythril.laser.smt import symbol_factory + def test_extcodehash_concrete(): # Arrange world_state = WorldState() account = world_state.create_account(balance=10, address=101) account.code = Disassembly("60606040") - world_state.create_account(balance = 10, address = 1000) + world_state.create_account(balance=10, address=1000) environment = Environment(account, None, None, None, None, None) og_state = GlobalState( world_state, environment, None, MachineState(gas_limit=8000000) @@ -24,9 +25,9 @@ def test_extcodehash_concrete(): og_state.transaction_stack.append( (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) ) - + instruction = Instruction("extcodehash", dynamic_loader=None) - + # If account does not exist, return 0 og_state.mstate.stack = [symbol_factory.BitVecVal(1, 256)] new_state = instruction.evaluate(og_state)[0] @@ -35,9 +36,12 @@ def test_extcodehash_concrete(): # If account code does not exist, return hash of empty set. og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)] new_state = instruction.evaluate(og_state)[0] - assert new_state.mstate.stack[-1] == '0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470' + assert ( + new_state.mstate.stack[-1] + == "0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470" + ) # If account code exists, return hash of the code. og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)] new_state = instruction.evaluate(og_state)[0] - assert new_state.mstate.stack[-1] == get_code_hash("60606040") \ No newline at end of file + assert new_state.mstate.stack[-1] == get_code_hash("60606040") From 7cf89a0dfee15169602eb96a346a7bf3e07f05fa Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 15:49:10 -0700 Subject: [PATCH 04/28] Fixed linting errors --- mythril/laser/ethereum/instructions.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 17173363..d53b033d 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1172,13 +1172,12 @@ class Instruction: log.debug("unsupported symbolic address for EXTCODEHASH") stack.append(global_state.new_bitvec("extcodehash_" + str(address), 256)) return [global_state] - address = address.value - if address not in world_state.accounts: + if address.value not in world_state.accounts: code_hash = symbol_factory.BitVecVal(0, 256) else: - code = world_state.accounts_exist_or_load(hex(address), self.dynamic_loader) - code_hash = get_code_hash(code) + code = world_state.accounts_exist_or_load(hex(address.value), self.dynamic_loader) + code_hash = symbol_factory.BitVecVal(int(get_code_hash(code), 16), 256) stack.append(code_hash) return [global_state] From 59dffe97f7a8be06be25c41ac56780a817044d81 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 15:57:37 -0700 Subject: [PATCH 05/28] Ran black --- mythril/laser/ethereum/instructions.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index d53b033d..37e90acd 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1176,7 +1176,9 @@ class Instruction: if address.value not in world_state.accounts: code_hash = symbol_factory.BitVecVal(0, 256) else: - code = world_state.accounts_exist_or_load(hex(address.value), self.dynamic_loader) + code = world_state.accounts_exist_or_load( + hex(address.value), self.dynamic_loader + ) code_hash = symbol_factory.BitVecVal(int(get_code_hash(code), 16), 256) stack.append(code_hash) return [global_state] From 83937a9a5545e312e771afdc94bad8de3fc91ba5 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 16:26:47 -0700 Subject: [PATCH 06/28] Fixed errors in asserts in extcodehash tests --- tests/instructions/extcodehash_test.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py index c677d5ef..ff1fff52 100644 --- a/tests/instructions/extcodehash_test.py +++ b/tests/instructions/extcodehash_test.py @@ -37,11 +37,11 @@ def test_extcodehash_concrete(): og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)] new_state = instruction.evaluate(og_state)[0] assert ( - new_state.mstate.stack[-1] - == "0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470" + hex(new_state.mstate.stack[-1].value) + == get_code_hash("") ) # If account code exists, return hash of the code. og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)] new_state = instruction.evaluate(og_state)[0] - assert new_state.mstate.stack[-1] == get_code_hash("60606040") + assert hex(new_state.mstate.stack[-1].value) == get_code_hash("60606040") From 1e225eb7701ae11ade6cc6a9c017a00355e42f67 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Wed, 7 Aug 2019 16:33:30 -0700 Subject: [PATCH 07/28] Ran black... --- tests/instructions/extcodehash_test.py | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py index ff1fff52..e1ea30c1 100644 --- a/tests/instructions/extcodehash_test.py +++ b/tests/instructions/extcodehash_test.py @@ -36,10 +36,7 @@ def test_extcodehash_concrete(): # If account code does not exist, return hash of empty set. og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)] new_state = instruction.evaluate(og_state)[0] - assert ( - hex(new_state.mstate.stack[-1].value) - == get_code_hash("") - ) + assert hex(new_state.mstate.stack[-1].value) == get_code_hash("") # If account code exists, return hash of the code. og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)] From 52ba355b657f34c11dd405057a76e46ac8fb9bab Mon Sep 17 00:00:00 2001 From: e-ngo Date: Thu, 8 Aug 2019 23:30:52 -0700 Subject: [PATCH 08/28] Add logic for CREATE opcode, still need to add unit test for CREATE. Refactored extcodehash unit tests into separate test units. --- mythril/laser/ethereum/gas.py | 5 +-- mythril/laser/ethereum/instructions.py | 42 ++++++++++++++++++++++---- tests/instructions/extcodehash_test.py | 34 ++++++++++++--------- 3 files changed, 56 insertions(+), 25 deletions(-) diff --git a/mythril/laser/ethereum/gas.py b/mythril/laser/ethereum/gas.py index 7e283d15..4d8de488 100644 --- a/mythril/laser/ethereum/gas.py +++ b/mythril/laser/ethereum/gas.py @@ -180,10 +180,7 @@ OPCODE_GAS = { "LOG3": (4 * 375, 4 * 375 + 8 * 32), "LOG4": (5 * 375, 5 * 375 + 8 * 32), "CREATE": (32000, 32000), - "CREATE2": ( - 32000, - 32000, - ), # TODO: The gas value is dynamic, to be done while implementing create2 + "CREATE2": (32000, 32000), # TODO: Make the gas value is dynamic "CALL": (700, 700 + 9000 + 25000), "NATIVE_COST": calculate_native_gas, "CALLCODE": (700, 700 + 9000 + 25000), diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 1c663ded..35e98e0c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1605,12 +1605,42 @@ class Instruction: :param global_state: :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] + mstate = global_state.mstate + environment = global_state.environment + world_state = global_state.world_state + + call_value, mem_offset, mem_size = ( + mstate.stack.pop(), + mstate.stack.pop(), + mstate.stack.pop(), + ) + + try: + call_data = mstate.memory[ + util.get_concrete_int(mem_offset) : util.get_concrete_int( + mem_offset + mem_size + ) + ] + except TypeError: + log.debug("Create with symbolic length or offset. Not supported") + + caller = environment.sender + gas_price = environment.gasprice + origin = environment.origin + transaction = ContractCreationTransaction( + world_state=world_state, + caller=caller, + call_data=call_data, + gas_price=gas_price, + origin=origin, + call_value=call_value, + ) + + contract_address = transaction.callee_account.address + + mstate.stack.append(contract_address) + + raise TransactionStartSignal(transaction, self.op_code) @StateTransition() def create2_(self, global_state: GlobalState) -> List[GlobalState]: diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py index e1ea30c1..14f2ad65 100644 --- a/tests/instructions/extcodehash_test.py +++ b/tests/instructions/extcodehash_test.py @@ -11,33 +11,37 @@ from mythril.support.support_utils import get_code_hash from mythril.laser.smt import symbol_factory +# Arrange +world_state = WorldState() +account = world_state.create_account(balance=10, address=101) +account.code = Disassembly("60606040") +world_state.create_account(balance=10, address=1000) +environment = Environment(account, None, None, None, None, None) +og_state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) +og_state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) +) -def test_extcodehash_concrete(): - # Arrange - world_state = WorldState() - account = world_state.create_account(balance=10, address=101) - account.code = Disassembly("60606040") - world_state.create_account(balance=10, address=1000) - environment = Environment(account, None, None, None, None, None) - og_state = GlobalState( - world_state, environment, None, MachineState(gas_limit=8000000) - ) - og_state.transaction_stack.append( - (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) - ) - - instruction = Instruction("extcodehash", dynamic_loader=None) +instruction = Instruction("extcodehash", dynamic_loader=None) + + +def test_extcodehash_no_account(): # If account does not exist, return 0 og_state.mstate.stack = [symbol_factory.BitVecVal(1, 256)] new_state = instruction.evaluate(og_state)[0] assert new_state.mstate.stack[-1] == 0 + +def test_extcodehash_no_code(): + # If account code does not exist, return hash of empty set. og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)] new_state = instruction.evaluate(og_state)[0] assert hex(new_state.mstate.stack[-1].value) == get_code_hash("") + +def test_extcodehash_return_hash(): # If account code exists, return hash of the code. og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)] new_state = instruction.evaluate(og_state)[0] From 06fce92c10f2c712f66cdeb41349ce6d92048f90 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Sun, 11 Aug 2019 23:19:56 -0700 Subject: [PATCH 09/28] Refactored create_ opcode --- mythril/laser/ethereum/instructions.py | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 35e98e0c..40c46747 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -31,7 +31,7 @@ from mythril.laser.smt import symbol_factory import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util -from mythril.laser.ethereum.call import get_call_parameters, native_call +from mythril.laser.ethereum.call import get_call_parameters, native_call, get_call_data from mythril.laser.ethereum.evm_exceptions import ( VmException, StackUnderflowException, @@ -1616,17 +1616,20 @@ class Instruction: ) try: - call_data = mstate.memory[ - util.get_concrete_int(mem_offset) : util.get_concrete_int( - mem_offset + mem_size - ) - ] + call_data = get_call_data( + global_state, + util.get_concrete_int(mem_offset), + util.get_concrete_int(mem_offset + mem_size), + ) except TypeError: log.debug("Create with symbolic length or offset. Not supported") + mstate.stack.append(0, 256) + return [global_state] caller = environment.sender gas_price = environment.gasprice origin = environment.origin + transaction = ContractCreationTransaction( world_state=world_state, caller=caller, @@ -1636,10 +1639,6 @@ class Instruction: call_value=call_value, ) - contract_address = transaction.callee_account.address - - mstate.stack.append(contract_address) - raise TransactionStartSignal(transaction, self.op_code) @StateTransition() From 5e1fb6067037781479a8b832aeef7fcb197f6b64 Mon Sep 17 00:00:00 2001 From: e-ngo Date: Thu, 22 Aug 2019 18:27:03 -0700 Subject: [PATCH 10/28] Added CREATE --- mythril/laser/ethereum/instructions.py | 39 ++++++++++++++++++------- tests/instructions/createopcode_test.py | 16 ++++++++++ 2 files changed, 44 insertions(+), 11 deletions(-) create mode 100644 tests/instructions/createopcode_test.py diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index ca3b9631..1b287e58 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -29,6 +29,8 @@ from mythril.laser.smt import ( ) from mythril.laser.smt import symbol_factory +from mythril.disassembler.disassembly import Disassembly + import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util from mythril.laser.ethereum.call import get_call_parameters, native_call, get_call_data @@ -904,7 +906,8 @@ class Instruction: state = global_state.mstate environment = global_state.environment disassembly = environment.code - state.stack.append(len(disassembly.bytecode) // 2) + no_of_bytes = len(disassembly.bytecode) // 2 + 5000 + state.stack.append(no_of_bytes) return [global_state] @StateTransition(enable_gas=False) @@ -1194,16 +1197,12 @@ class Instruction: address = Extract(159, 0, stack.pop()) if address.symbolic: - log.debug("unsupported symbolic address for EXTCODEHASH") - stack.append(global_state.new_bitvec("extcodehash_" + str(address), 256)) - return [global_state] - - if address.value not in world_state.accounts: + code_hash = symbol_factory.BitVecVal(int(get_code_hash(""), 16), 256) + elif address.value not in world_state.accounts: code_hash = symbol_factory.BitVecVal(0, 256) else: - code = world_state.accounts_exist_or_load( - hex(address.value), self.dynamic_loader - ) + addr = "0" * (40 - len(hex(address.value))) + hex(address.value) + code = world_state.accounts_exist_or_load(addr, self.dynamic_loader) code_hash = symbol_factory.BitVecVal(int(get_code_hash(code), 16), 256) stack.append(code_hash) return [global_state] @@ -1615,26 +1614,44 @@ class Instruction: util.get_concrete_int(mem_offset), util.get_concrete_int(mem_offset + mem_size), ) + except TypeError: log.debug("Create with symbolic length or offset. Not supported") mstate.stack.append(0, 256) return [global_state] - caller = environment.sender + call_data = call_data.concrete(None) + code_str = bytes.hex(bytes(call_data)) + # for i in call_data.size: + # if isinstance(call_data[0], int): + # code_str += "00" if not call_data[0] else bytes.hex([call_data[i]]) + # + + code = Disassembly(code_str) + + caller = environment.active_account.address gas_price = environment.gasprice origin = environment.origin transaction = ContractCreationTransaction( world_state=world_state, caller=caller, - call_data=call_data, + code=code, gas_price=gas_price, + gas_limit=mstate.gas_limit, origin=origin, call_value=call_value, ) raise TransactionStartSignal(transaction, self.op_code) + @StateTransition() + def create_post(self, global_state: GlobalState) -> List[GlobalState]: + + global_state.mstate.stack.append(global_state.world_state.accounts[-1].address) + + return [global_state] + @StateTransition() def create2_(self, global_state: GlobalState) -> List[GlobalState]: """ diff --git a/tests/instructions/createopcode_test.py b/tests/instructions/createopcode_test.py new file mode 100644 index 00000000..64dc7cdf --- /dev/null +++ b/tests/instructions/createopcode_test.py @@ -0,0 +1,16 @@ +from mythril.disassembler.disassembly import Disassembly +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.support.support_utils import get_code_hash + +from mythril.laser.smt import symbol_factory + +def test_create(): + # TODO: ... + pass \ No newline at end of file From f58aaa1830c4bedde24e08803ff7287c46908724 Mon Sep 17 00:00:00 2001 From: ricengo Date: Fri, 23 Aug 2019 00:17:20 -0700 Subject: [PATCH 11/28] Updated create implementation. TODO: finish log, create2, and staticcall --- mythril/laser/ethereum/instructions.py | 30 ++++++++----------- mythril/laser/ethereum/svm.py | 6 ++++ .../transaction/transaction_models.py | 2 +- 3 files changed, 20 insertions(+), 18 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index e1e1f292..79948bc8 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1632,18 +1632,10 @@ class Instruction: environment = global_state.environment world_state = global_state.world_state - call_value, mem_offset, mem_size = ( - mstate.stack.pop(), - mstate.stack.pop(), - mstate.stack.pop(), - ) + call_value, mem_offset, mem_size = mstate.pop(3) try: - call_data = get_call_data( - global_state, - util.get_concrete_int(mem_offset), - util.get_concrete_int(mem_offset + mem_size), - ) + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) except TypeError: log.debug("Create with symbolic length or offset. Not supported") @@ -1651,11 +1643,16 @@ class Instruction: return [global_state] call_data = call_data.concrete(None) - code_str = bytes.hex(bytes(call_data)) - # for i in call_data.size: - # if isinstance(call_data[0], int): - # code_str += "00" if not call_data[0] else bytes.hex([call_data[i]]) - # + + code_end = 0 + for i in range(len(call_data)): + if not isinstance(call_data[i], int): + code_end = i + break + + code_str = bytes.hex(bytes(call_data[0:code_end])) + + constructor_arguments = call_data[code_end:] code = Disassembly(code_str) @@ -1667,6 +1664,7 @@ class Instruction: world_state=world_state, caller=caller, code=code, + call_data=constructor_arguments, gas_price=gas_price, gas_limit=mstate.gas_limit, origin=origin, @@ -1678,8 +1676,6 @@ class Instruction: @StateTransition() def create_post(self, global_state: GlobalState) -> List[GlobalState]: - global_state.mstate.stack.append(global_state.world_state.accounts[-1].address) - return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 88b362c8..f6b69a2a 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -375,6 +375,12 @@ class LaserEVM: :param return_data: :return: """ + if isinstance(global_state.current_transaction, ContractCreationTransaction): + return_global_state.mstate.stack.append( + global_state.environment.active_account.address + ) + return_global_state.mstate.min_gas_used += global_state.mstate.min_gas_used + return_global_state.mstate.max_gas_used += global_state.mstate.max_gas_used return_global_state.mstate.constraints += global_state.mstate.constraints # Resume execution of the transaction initializing instruction diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 97f2f694..a85160e2 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -93,7 +93,7 @@ class BaseTransaction: self.call_data = ( call_data if isinstance(call_data, BaseCalldata) - else ConcreteCalldata(self.id, []) + else ConcreteCalldata(self.id, call_data) ) self.call_value = ( From e8b50b57efc3c1429bdf8e8cdbbd0b387af7a4a7 Mon Sep 17 00:00:00 2001 From: Eric N Date: Sat, 24 Aug 2019 00:20:07 -0700 Subject: [PATCH 12/28] Fix bug and comment code. Adding tests. --- mythril/laser/ethereum/instructions.py | 9 +++++-- mythril/laser/ethereum/svm.py | 1 + tests/instructions/create_test.py | 35 +++++++++++++++++++++++++ tests/instructions/createopcode_test.py | 16 ----------- 4 files changed, 43 insertions(+), 18 deletions(-) create mode 100644 tests/instructions/create_test.py delete mode 100644 tests/instructions/createopcode_test.py diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 79948bc8..6288d8f8 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1635,16 +1635,21 @@ class Instruction: call_value, mem_offset, mem_size = mstate.pop(3) try: - call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + call_data = get_call_data( + global_state, + util.get_concrete_int(mem_offset), + util.get_concrete_int(mem_offset + mem_size), + ) except TypeError: + # can be reached? log.debug("Create with symbolic length or offset. Not supported") mstate.stack.append(0, 256) return [global_state] call_data = call_data.concrete(None) - code_end = 0 + code_end = len(call_data) for i in range(len(call_data)): if not isinstance(call_data[i], int): code_end = i diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index f6b69a2a..572830bb 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -376,6 +376,7 @@ class LaserEVM: :return: """ if isinstance(global_state.current_transaction, ContractCreationTransaction): + # is this the proper place to put CREATE handle? return_global_state.mstate.stack.append( global_state.environment.active_account.address ) diff --git a/tests/instructions/create_test.py b/tests/instructions/create_test.py new file mode 100644 index 00000000..5941949d --- /dev/null +++ b/tests/instructions/create_test.py @@ -0,0 +1,35 @@ +from mythril.disassembler.disassembly import Disassembly +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.svm import LaserEVM + +from mythril.laser.smt import symbol_factory + + +def test_create(): + creating_contract_runtime_code = "608060405260043610601c5760003560e01c8063efc81a8c146021575b600080fd5b60276029565b005b60006040516035906056565b604051809103906000f0801580156050573d6000803e3d6000fd5b50905050565b605b806100638339019056fe6080604052348015600f57600080fd5b50603e80601d6000396000f3fe6080604052600080fdfea265627a7a72315820f4040cbd444dcd2f49f1daf46a116eb32396f1cc84a9e79e3836d4bfe84d6bca64736f6c634300050b0032a265627a7a72315820e2350a73a28ed02b4dac678f2b77a330dc512c3cce8ca53fa1c30869f443553d64736f6c634300050b0032" + created_contract_init_code = "6080604052348015600f57600080fd5b50603e80601d6000396000f3fe6080604052600080fdfea265627a7a72315820f4040cbd444dcd2f49f1daf46a116eb32396f1cc84a9e79e3836d4bfe84d6bca64736f6c634300050b0032" + created_contract_runtime_code = "6080604052600080fdfea265627a7a72315820f4040cbd444dcd2f49f1daf46a116eb32396f1cc84a9e79e3836d4bfe84d6bca64736f6c634300050b0032" + world_state = WorldState() + account = world_state.create_account(balance=1000, address=101) + account.code = Disassembly(creating_contract_runtime_code) + environment = Environment(account, None, None, None, None, None) + og_state = GlobalState( + world_state, environment, None, MachineState(gas_limit=8000000) + ) + og_state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + + laser_evm = LaserEVM() + + new_states, op_code = laser_evm.execute_state(og_state) + # checks + + # TODO: come up with sequence, then grab an address from stack and check that its code is created. diff --git a/tests/instructions/createopcode_test.py b/tests/instructions/createopcode_test.py deleted file mode 100644 index 64dc7cdf..00000000 --- a/tests/instructions/createopcode_test.py +++ /dev/null @@ -1,16 +0,0 @@ -from mythril.disassembler.disassembly import Disassembly -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.support.support_utils import get_code_hash - -from mythril.laser.smt import symbol_factory - -def test_create(): - # TODO: ... - pass \ No newline at end of file From 2f2c56ac6d04abdc166f7fdfc20aa09676b92274 Mon Sep 17 00:00:00 2001 From: Eric N Date: Sat, 24 Aug 2019 12:56:24 -0700 Subject: [PATCH 13/28] Add create_post logic --- 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 6288d8f8..792c39fa 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1680,7 +1680,8 @@ class Instruction: @StateTransition() def create_post(self, global_state: GlobalState) -> List[GlobalState]: - + addr, call_value, mem_offset, mem_size = global_state.mstate.pop(4) + global_state.mstate.stack.append(addr) return [global_state] @StateTransition() From 43b15324a1ba18bab395621d92b7024049a79d21 Mon Sep 17 00:00:00 2001 From: Eric N Date: Sun, 25 Aug 2019 18:20:25 -0700 Subject: [PATCH 14/28] Add logic for create and create2. --- mythril/laser/ethereum/instructions.py | 63 +++++++++++++------ .../transaction/transaction_models.py | 3 +- 2 files changed, 46 insertions(+), 20 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 792c39fa..984d0592 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1231,7 +1231,7 @@ class Instruction: elif address.value not in world_state.accounts: code_hash = symbol_factory.BitVecVal(0, 256) else: - addr = "0" * (40 - len(hex(address.value))) + hex(address.value) + addr = "0" * (40 - len(hex(address.value)[2:])) + hex(address.value)[2:] code = world_state.accounts_exist_or_load(addr, self.dynamic_loader) code_hash = symbol_factory.BitVecVal(int(get_code_hash(code), 16), 256) stack.append(code_hash) @@ -1621,19 +1621,15 @@ class Instruction: # Not supported return [global_state] - @StateTransition() - def create_(self, global_state: GlobalState) -> List[GlobalState]: - """ + @staticmethod + def _create_transaction_helper( + global_state, call_value, mem_offset, mem_size, op_code + ): - :param global_state: - :return: - """ mstate = global_state.mstate environment = global_state.environment world_state = global_state.world_state - call_value, mem_offset, mem_size = mstate.pop(3) - try: call_data = get_call_data( global_state, @@ -1665,6 +1661,21 @@ class Instruction: gas_price = environment.gasprice origin = environment.origin + contract_address = None + if op_code is "CREATE2": + salt = hex(mstate.stack.pop().value)[2:] + salt = "0" * (64 - len(salt)) + salt + + addr = hex(caller.value)[2:] + addr = "0" * (40 - len(addr)) + addr + + contract_address = int( + get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:], + 16, + ) + + # TODO: calculate gas cost + transaction = ContractCreationTransaction( world_state=world_state, caller=caller, @@ -1674,9 +1685,23 @@ class Instruction: gas_limit=mstate.gas_limit, origin=origin, call_value=call_value, + contract_address=contract_address, ) + raise TransactionStartSignal(transaction, op_code) - raise TransactionStartSignal(transaction, self.op_code) + @StateTransition() + def create_(self, global_state: GlobalState) -> List[GlobalState]: + """ + + :param global_state: + :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, self.op_code + ) @StateTransition() def create_post(self, global_state: GlobalState) -> List[GlobalState]: @@ -1691,16 +1716,16 @@ class Instruction: :param global_state: :return: """ - # TODO: implement me - state = global_state.mstate - endowment, memory_start, memory_length, salt = ( - state.stack.pop(), - state.stack.pop(), - state.stack.pop(), - state.stack.pop(), + call_value, mem_offset, mem_size = global_state.mstate.pop(3) + + return self._create_transaction_helper( + global_state, call_value, mem_offset, mem_size, self.op_code ) - # Not supported - state.stack.append(0) + + @StateTransition() + def create2_post(self, global_state: GlobalState) -> List[GlobalState]: + addr, call_value, mem_offset, mem_size = global_state.mstate.pop(4) + global_state.mstate.stack.append(addr) return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index a85160e2..a92421c8 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -191,10 +191,11 @@ class ContractCreationTransaction(BaseTransaction): code=None, call_value=None, contract_name=None, + contract_address=None, ) -> None: self.prev_world_state = deepcopy(world_state) callee_account = world_state.create_account( - 0, concrete_storage=True, creator=caller.value + 0, concrete_storage=True, creator=caller.value, address=contract_address ) callee_account.contract_name = contract_name # init_call_data "should" be false, but it is easier to model the calldata symbolically From 3c3153e24240e7c0c42afb4555c9b3b2c8fd2d3b Mon Sep 17 00:00:00 2001 From: Eric N Date: Thu, 5 Sep 2019 22:19:48 -0700 Subject: [PATCH 15/28] Cleaned up stupid logic. Add gas calculation to create2. --- mythril/laser/ethereum/instructions.py | 27 +++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 984d0592..80b51cd2 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -930,6 +930,14 @@ class Instruction: state.stack.append(no_of_bytes) return [global_state] + @staticmethod + def _sha3_gas_helper(global_state, length): + min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length) + global_state.mstate.min_gas_used += min_gas + global_state.mstate.max_gas_used += max_gas + StateTransition.check_gas_usage_limit(global_state) + return global_state + @StateTransition(enable_gas=False) def sha3_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -955,10 +963,7 @@ class Instruction: state.max_gas_used += gas_tuple[1] return [global_state] - min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length) - state.min_gas_used += min_gas - state.max_gas_used += max_gas - StateTransition.check_gas_usage_limit(global_state) + _sha3_gas_helper(global_state, length) state.mem_extend(index, length) data_list = [ @@ -1623,7 +1628,7 @@ class Instruction: @staticmethod def _create_transaction_helper( - global_state, call_value, mem_offset, mem_size, op_code + global_state, call_value, mem_offset, mem_size, op_code, create2_salt=None ): mstate = global_state.mstate @@ -1662,20 +1667,20 @@ class Instruction: origin = environment.origin contract_address = None - if op_code is "CREATE2": - salt = hex(mstate.stack.pop().value)[2:] + if create2_salt: + salt = hex(create2_salt)[2:] salt = "0" * (64 - len(salt)) + salt addr = hex(caller.value)[2:] addr = "0" * (40 - len(addr)) + addr + _sha3_gas_helper(global_state, len(code_str[:2] // 2)) + contract_address = int( get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:], 16, ) - # TODO: calculate gas cost - transaction = ContractCreationTransaction( world_state=world_state, caller=caller, @@ -1716,10 +1721,10 @@ class Instruction: :param global_state: :return: """ - call_value, mem_offset, mem_size = global_state.mstate.pop(3) + call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) return self._create_transaction_helper( - global_state, call_value, mem_offset, mem_size, self.op_code + global_state, call_value, mem_offset, mem_size, self.op_code, salt ) @StateTransition() From 3dced432169b8f9ddab41714cca5edbc4856266e Mon Sep 17 00:00:00 2001 From: Eric N Date: Thu, 5 Sep 2019 22:39:00 -0700 Subject: [PATCH 16/28] Syntax errors --- mythril/laser/ethereum/instructions.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 80b51cd2..fe8d4c8e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -963,7 +963,7 @@ class Instruction: state.max_gas_used += gas_tuple[1] return [global_state] - _sha3_gas_helper(global_state, length) + Instruction._sha3_gas_helper(global_state, length) state.mem_extend(index, length) data_list = [ @@ -1674,7 +1674,7 @@ class Instruction: addr = hex(caller.value)[2:] addr = "0" * (40 - len(addr)) + addr - _sha3_gas_helper(global_state, len(code_str[:2] // 2)) + Instruction._sha3_gas_helper(global_state, len(code_str[:2] // 2)) contract_address = int( get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:], From 7483bc80fd837b65b4e604f317032380cc1effb2 Mon Sep 17 00:00:00 2001 From: Eric N Date: Sun, 8 Sep 2019 21:33:25 -0700 Subject: [PATCH 17/28] Refactored code. --- mythril/laser/ethereum/instructions.py | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 7d21854c..ce2d2a96 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1655,24 +1655,20 @@ class Instruction: environment = global_state.environment world_state = global_state.world_state - call_data = get_call_data( - global_state, - mem_offset, - mem_offset + mem_size, - ) - - call_data = call_data.concrete(None) + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) - code_end = len(call_data) - for i in range(len(call_data)): - if not isinstance(call_data[i], int): + code_raw = [] + code_end = call_data.size + for i in range(call_data.size): + # Proper way to delimit init_bytecode? Seems to work. + if call_data[i].symbolic: code_end = i break + code_raw.append(call_data[i].value) - code_str = bytes.hex(bytes(call_data[0:code_end])) + code_str = bytes.hex(bytes(code_raw)) constructor_arguments = call_data[code_end:] - code = Disassembly(code_str) caller = environment.active_account.address @@ -1705,7 +1701,7 @@ class Instruction: call_value=call_value, contract_address=contract_address, ) - raise TransactionStartSignal(transaction, op_code) + raise TransactionStartSignal(transaction, op_code, global_state) @StateTransition(is_state_mutation_instruction=True) def create_(self, global_state: GlobalState) -> List[GlobalState]: From 3eaf917b228cf90c36427959d958de3e0f500a3d Mon Sep 17 00:00:00 2001 From: Eric N Date: Tue, 10 Sep 2019 23:51:20 -0700 Subject: [PATCH 18/28] Fixing CCT logic. Fixes CREATE with symbolic constructor arguments, but not Concrete. --- mythril/laser/ethereum/instructions.py | 162 ++++++++++++++---- .../transaction/transaction_models.py | 2 +- 2 files changed, 132 insertions(+), 32 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index ce2d2a96..e5c62f2a 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -31,6 +31,8 @@ from mythril.laser.smt import symbol_factory from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.calldata import ConcreteCalldata, SymbolicCalldata + import mythril.laser.ethereum.util as helper from mythril.laser.ethereum import util from mythril.laser.ethereum.call import get_call_parameters, native_call, get_call_data @@ -933,14 +935,18 @@ class Instruction: state = global_state.mstate environment = global_state.environment disassembly = environment.code + calldata = global_state.environment.calldata if isinstance(global_state.current_transaction, ContractCreationTransaction): # 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 - ) + no_of_bytes = len(disassembly.bytecode) // 2 + if isinstance(calldata, ConcreteCalldata): + no_of_bytes += calldata.size + else: + no_of_bytes += 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) @@ -1072,28 +1078,115 @@ class Instruction: global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), ) + code = global_state.environment.code.bytecode + if code[0:2] == "0x": + code = code[2:] + code_size = len(code) // 2 - if ( - isinstance(global_state.current_transaction, ContractCreationTransaction) - and code_offset >= len(global_state.environment.code.bytecode) // 2 - ): + if isinstance(global_state.current_transaction, ContractCreationTransaction): # 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 + offset = code_offset - code_size log.warning("Doing hacky thing offset: {} size: {}".format(offset, size)) - 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, - ) + + if isinstance(global_state.environment.calldata, SymbolicCalldata): + if code_offset >= code_size: + return self._calldata_copy_helper( + global_state, global_state.mstate, memory_offset, offset, size + ) + else: + # creation code and arguments may be in same object. + # Copy from both code and calldata appropriately. + state = global_state.mstate + environment = global_state.environment + concrete_memory_offset = helper.get_concrete_int(memory_offset) + concrete_code_offset = helper.get_concrete_int(code_offset) + concrete_size = helper.get_concrete_int(size) + + calldata = global_state.environment.calldata + calldata_size = helper.get_concrete_int(calldata.size) + + total_size = code_size + calldata_size + + if concrete_size > 0: + # borrow some logic from codecopyhelper and calldatacopyhelper + try: + state.mem_extend(concrete_memory_offset, concrete_size) + except TypeError as e: + log.debug("Memory allocation error: {}".format(e)) + state.mem_extend(concrete_memory_offset, 1) + state.memory[mstart] = global_state.new_bitvec( + "calldata_" + + str(environment.active_account.contract_name) + + "[" + + str(offset) + + ": + " + + str(concrete_size) + + "]", + 8, + ) + return [global_state] + + try: + i_data = code_size + new_memory = [] + for i in range(concrete_size): + if concrete_code_offset + i < code_size: + # copy from code + state.memory[concrete_memory_offset + i] = int( + code[ + 2 + * (concrete_code_offset + i) : 2 + * (concrete_code_offset + i + 1) + ], + 16, + ) + elif concrete_code_offset + i < total_size: + # copy from calldata + value = environment.calldata[i_data] + new_memory.append(value) + + i_data = ( + i_data + 1 + if isinstance(i_data, int) + else simplify(cast(BitVec, i_data) + 1) + ) + else: + raise IndexError + if new_memory: + for i in range(len(new_memory)): + state.memory[i + mstart] = new_memory[i] + except IndexError: + log.debug("Exception copying code to memory") + + state.memory[mstart] = global_state.new_bitvec( + "code_" + + str(environment.active_account.contract_name) + + "[" + + str(code_offset) + + ": + " + + str(concrete_size) + + "]", + 8, + ) + elif concrete_size == 0 and isinstance( + global_state.current_transaction, ContractCreationTransaction + ): + if concrete_code_offset >= total_size: + Instruction._handle_symbolic_args( + global_state, concrete_memory_offset + ) + + return [global_state] + 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]: @@ -1657,16 +1750,24 @@ class Instruction: call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) - code_raw = [] - code_end = call_data.size - for i in range(call_data.size): - # Proper way to delimit init_bytecode? Seems to work. - if call_data[i].symbolic: + # code_raw = [] + # code_end = call_data.size + # for i in range(call_data.size): + # # Proper way to delimit init_bytecode? Seems to work. + # if call_data[i].symbolic: + # code_end = i + # break + # code_raw.append(call_data[i].value) + call_data = call_data.concrete(None) + + code_end = len(call_data) + for i in range(len(call_data)): + if not isinstance(call_data[i], int): code_end = i break - code_raw.append(call_data[i].value) - code_str = bytes.hex(bytes(code_raw)) + # code_str = bytes.hex(bytes(code_raw)) + code_str = bytes.hex(bytes(call_data[0:code_end])) constructor_arguments = call_data[code_end:] code = Disassembly(code_str) @@ -1689,7 +1790,6 @@ class Instruction: get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:], 16, ) - transaction = ContractCreationTransaction( world_state=world_state, caller=caller, diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 563e9e2f..3195365d 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -96,7 +96,7 @@ class BaseTransaction: self.call_data = ( call_data if isinstance(call_data, BaseCalldata) - else ConcreteCalldata(self.id, call_data) + else ConcreteCalldata(self.id, []) ) self.call_value = ( From a9755b8c67ee6a6fc5f782f3d31c0d703235585b Mon Sep 17 00:00:00 2001 From: Eric N Date: Sun, 15 Sep 2019 23:50:14 -0700 Subject: [PATCH 19/28] Modified codecopy. Debugging issue with contract function calls. --- mythril/laser/ethereum/gas.py | 2 +- mythril/laser/ethereum/instructions.py | 171 +++++++++++-------------- 2 files changed, 77 insertions(+), 96 deletions(-) diff --git a/mythril/laser/ethereum/gas.py b/mythril/laser/ethereum/gas.py index 4d8de488..0a0c0a38 100644 --- a/mythril/laser/ethereum/gas.py +++ b/mythril/laser/ethereum/gas.py @@ -180,7 +180,7 @@ OPCODE_GAS = { "LOG3": (4 * 375, 4 * 375 + 8 * 32), "LOG4": (5 * 375, 5 * 375 + 8 * 32), "CREATE": (32000, 32000), - "CREATE2": (32000, 32000), # TODO: Make the gas value is dynamic + "CREATE2": (32000, 32000), # TODO: Make the gas values dynamic "CALL": (700, 700 + 9000 + 25000), "NATIVE_COST": calculate_native_gas, "CALLCODE": (700, 700 + 9000 + 25000), diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index e5c62f2a..903fe1ec 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -50,6 +50,7 @@ from mythril.laser.ethereum.transaction import ( MessageCallTransaction, TransactionStartSignal, ContractCreationTransaction, + get_next_transaction_id, ) from mythril.support.support_utils import get_code_hash @@ -939,13 +940,13 @@ class Instruction: if isinstance(global_state.current_transaction, ContractCreationTransaction): # Hacky way to ensure constructor arguments work - Pick some reasonably large size. no_of_bytes = len(disassembly.bytecode) // 2 - if isinstance(calldata, ConcreteCalldata): - no_of_bytes += calldata.size - else: - no_of_bytes += 0x200 # space for 16 32-byte arguments - global_state.mstate.constraints.append( - global_state.environment.calldata.size == no_of_bytes - ) + # if isinstance(calldata, ConcreteCalldata): + # no_of_bytes += calldata.size + 5000 + # else: + no_of_bytes += 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 @@ -1096,7 +1097,6 @@ class Instruction: global_state, global_state.mstate, memory_offset, offset, size ) else: - # creation code and arguments may be in same object. # Copy from both code and calldata appropriately. state = global_state.mstate environment = global_state.environment @@ -1105,80 +1105,67 @@ class Instruction: concrete_size = helper.get_concrete_int(size) calldata = global_state.environment.calldata - calldata_size = helper.get_concrete_int(calldata.size) - - total_size = code_size + calldata_size - - if concrete_size > 0: - # borrow some logic from codecopyhelper and calldatacopyhelper - try: - state.mem_extend(concrete_memory_offset, concrete_size) - except TypeError as e: - log.debug("Memory allocation error: {}".format(e)) - state.mem_extend(concrete_memory_offset, 1) - state.memory[mstart] = global_state.new_bitvec( - "calldata_" - + str(environment.active_account.contract_name) - + "[" - + str(offset) - + ": + " - + str(concrete_size) - + "]", - 8, + + code_copy_offset = concrete_code_offset + code_copy_size = ( + concrete_size + if concrete_code_offset + concrete_size <= code_size + else code_size - concrete_code_offset + ) + code_copy_size = code_copy_size if code_copy_size >= 0 else 0 + + calldata_copy_offset = ( + concrete_code_offset - code_size + if concrete_code_offset - code_size > 0 + else 0 + ) + calldata_copy_size = concrete_code_offset + concrete_size - code_size + calldata_copy_size = ( + calldata_copy_size if calldata_copy_size >= 0 else 0 + ) + + try: + global_state.mstate.mem_extend( + concrete_memory_offset, concrete_size + calldata_copy_size + ) + except TypeError: + global_state.mstate.mem_extend(concrete_memory_offset, 1) + global_state.mstate.memory[ + concrete_memory_offset + ] = global_state.new_bitvec( + "code({})".format( + global_state.environment.active_account.contract_name + ), + 8, + ) + return [global_state] + + for i in range(code_copy_size + calldata_copy_size): + if i < code_copy_size: + global_state.mstate.memory[concrete_memory_offset + i] = int( + code[ + 2 + * (code_copy_offset + i) : 2 + * (code_copy_offset + i + 1) + ], + 16, ) - return [global_state] - - try: - i_data = code_size - new_memory = [] - for i in range(concrete_size): - if concrete_code_offset + i < code_size: - # copy from code - state.memory[concrete_memory_offset + i] = int( - code[ - 2 - * (concrete_code_offset + i) : 2 - * (concrete_code_offset + i + 1) - ], - 16, - ) - elif concrete_code_offset + i < total_size: - # copy from calldata - value = environment.calldata[i_data] - new_memory.append(value) - - i_data = ( - i_data + 1 - if isinstance(i_data, int) - else simplify(cast(BitVec, i_data) + 1) - ) - else: - raise IndexError - if new_memory: - for i in range(len(new_memory)): - state.memory[i + mstart] = new_memory[i] - except IndexError: - log.debug("Exception copying code to memory") - - state.memory[mstart] = global_state.new_bitvec( - "code_" - + str(environment.active_account.contract_name) - + "[" - + str(code_offset) - + ": + " - + str(concrete_size) - + "]", + elif i < code_copy_size + calldata_copy_size: + # copy from calldata + global_state.mstate.memory[ + concrete_memory_offset + i + ] = calldata[calldata_copy_offset + i] + else: + global_state.mstate.memory[ + concrete_memory_offset + i + ] = global_state.new_bitvec( + "code({})".format( + global_state.environment.active_account.contract_name + ), 8, ) - elif concrete_size == 0 and isinstance( - global_state.current_transaction, ContractCreationTransaction - ): - if concrete_code_offset >= total_size: - Instruction._handle_symbolic_args( - global_state, concrete_memory_offset - ) - return [global_state] + return self._code_copy_helper( code=global_state.environment.code.bytecode, memory_offset=memory_offset, @@ -1750,26 +1737,20 @@ class Instruction: call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) - # code_raw = [] - # code_end = call_data.size - # for i in range(call_data.size): - # # Proper way to delimit init_bytecode? Seems to work. - # if call_data[i].symbolic: - # code_end = i - # break - # code_raw.append(call_data[i].value) - call_data = call_data.concrete(None) - - code_end = len(call_data) - for i in range(len(call_data)): - if not isinstance(call_data[i], int): + code_raw = [] + code_end = call_data.size + for i in range(call_data.size): + if call_data[i].symbolic: code_end = i break + code_raw.append(call_data[i].value) - # code_str = bytes.hex(bytes(code_raw)) - code_str = bytes.hex(bytes(call_data[0:code_end])) + code_str = bytes.hex(bytes(code_raw)) - constructor_arguments = call_data[code_end:] + next_transaction_id = get_next_transaction_id() + constructor_arguments = ConcreteCalldata( + next_transaction_id, call_data[code_end:] + ) code = Disassembly(code_str) caller = environment.active_account.address @@ -1838,7 +1819,7 @@ class Instruction: @StateTransition() def create2_post(self, global_state: GlobalState) -> List[GlobalState]: - addr, call_value, mem_offset, mem_size = global_state.mstate.pop(4) + addr, call_value, mem_offset, mem_size, salt = global_state.mstate.pop(5) global_state.mstate.stack.append(addr) return [global_state] From bc0f677e87c65c091ab257baae306eaf39d29cd0 Mon Sep 17 00:00:00 2001 From: Eric N Date: Tue, 17 Sep 2019 00:02:41 -0700 Subject: [PATCH 20/28] Cleaned up code. Add create test. --- mythril/laser/ethereum/instructions.py | 51 ++++++++++------- mythril/laser/ethereum/svm.py | 16 +++--- tests/instructions/create_test.py | 77 +++++++++++++++++++------- 3 files changed, 97 insertions(+), 47 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 903fe1ec..5d37350b 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -940,13 +940,13 @@ class Instruction: if isinstance(global_state.current_transaction, ContractCreationTransaction): # Hacky way to ensure constructor arguments work - Pick some reasonably large size. no_of_bytes = len(disassembly.bytecode) // 2 - # if isinstance(calldata, ConcreteCalldata): - # no_of_bytes += calldata.size + 5000 - # else: - no_of_bytes += 0x200 # space for 16 32-byte arguments - # global_state.mstate.constraints.append( - # global_state.environment.calldata.size == no_of_bytes - # ) + if isinstance(calldata, ConcreteCalldata): + no_of_bytes += calldata.size + else: + no_of_bytes += 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 @@ -1139,9 +1139,9 @@ class Instruction: 8, ) return [global_state] - - for i in range(code_copy_size + calldata_copy_size): + for i in range(concrete_size): if i < code_copy_size: + # copy from code global_state.mstate.memory[concrete_memory_offset + i] = int( code[ 2 @@ -1154,7 +1154,7 @@ class Instruction: # copy from calldata global_state.mstate.memory[ concrete_memory_offset + i - ] = calldata[calldata_copy_offset + i] + ] = calldata[calldata_copy_offset + i - code_copy_size] else: global_state.mstate.memory[ concrete_memory_offset + i @@ -1726,11 +1726,9 @@ class Instruction: # Not supported return [global_state] - @staticmethod def _create_transaction_helper( - global_state, call_value, mem_offset, mem_size, op_code, create2_salt=None + self, global_state, call_value, mem_offset, mem_size, create2_salt=None ): - mstate = global_state.mstate environment = global_state.environment world_state = global_state.world_state @@ -1782,7 +1780,7 @@ class Instruction: call_value=call_value, contract_address=contract_address, ) - raise TransactionStartSignal(transaction, op_code, global_state) + raise TransactionStartSignal(transaction, self.op_code, global_state) @StateTransition(is_state_mutation_instruction=True) def create_(self, global_state: GlobalState) -> List[GlobalState]: @@ -1795,13 +1793,20 @@ class Instruction: call_value, mem_offset, mem_size = global_state.mstate.pop(3) return self._create_transaction_helper( - global_state, call_value, mem_offset, mem_size, self.op_code + global_state, call_value, mem_offset, mem_size ) @StateTransition() def create_post(self, global_state: GlobalState) -> List[GlobalState]: - addr, call_value, mem_offset, mem_size = global_state.mstate.pop(4) - global_state.mstate.stack.append(addr) + call_value, mem_offset, mem_size = global_state.mstate.pop(3) + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + if global_state.last_return_data: + global_state.mstate.stack.append( + symbol_factory.BitVecVal(int(global_state.last_return_data, 16), 256) + ) + else: + global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256)) + return [global_state] @StateTransition(is_state_mutation_instruction=True) @@ -1814,13 +1819,19 @@ class Instruction: call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) return self._create_transaction_helper( - global_state, call_value, mem_offset, mem_size, self.op_code, salt + global_state, call_value, mem_offset, mem_size, salt ) @StateTransition() def create2_post(self, global_state: GlobalState) -> List[GlobalState]: - addr, call_value, mem_offset, mem_size, salt = global_state.mstate.pop(5) - global_state.mstate.stack.append(addr) + call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) + call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) + if global_state.last_return_data: + global_state.mstate.stack.append( + symbol_factory.BitVecVal(int(global_state.last_return_data), 256) + ) + else: + global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256)) return [global_state] @StateTransition() diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index fa78c840..e2b53199 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -380,13 +380,6 @@ class LaserEVM: :param return_data: :return: """ - if isinstance(global_state.current_transaction, ContractCreationTransaction): - # is this the proper place to put CREATE handle? - return_global_state.mstate.stack.append( - global_state.environment.active_account.address - ) - return_global_state.mstate.min_gas_used += global_state.mstate.min_gas_used - return_global_state.mstate.max_gas_used += global_state.mstate.max_gas_used return_global_state.mstate.constraints += global_state.mstate.constraints # Resume execution of the transaction initializing instruction @@ -401,6 +394,15 @@ class LaserEVM: return_global_state.environment.active_account = global_state.accounts[ return_global_state.environment.active_account.address.value ] + if isinstance( + global_state.current_transaction, ContractCreationTransaction + ): + return_global_state.mstate.min_gas_used += ( + global_state.mstate.min_gas_used + ) + return_global_state.mstate.max_gas_used += ( + global_state.mstate.max_gas_used + ) # Execute the post instruction handler new_global_states = Instruction( diff --git a/tests/instructions/create_test.py b/tests/instructions/create_test.py index 5941949d..0a97565e 100644 --- a/tests/instructions/create_test.py +++ b/tests/instructions/create_test.py @@ -6,30 +6,67 @@ 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.state.calldata import ConcreteCalldata from mythril.laser.ethereum.svm import LaserEVM - from mythril.laser.smt import symbol_factory +# contract A { +# uint256 public val = 10; +# } +contract_init_code = "6080604052600a600055348015601457600080fd5b506084806100236000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032" +contract_runtime_code = "6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032" -def test_create(): - creating_contract_runtime_code = "608060405260043610601c5760003560e01c8063efc81a8c146021575b600080fd5b60276029565b005b60006040516035906056565b604051809103906000f0801580156050573d6000803e3d6000fd5b50905050565b605b806100638339019056fe6080604052348015600f57600080fd5b50603e80601d6000396000f3fe6080604052600080fdfea265627a7a72315820f4040cbd444dcd2f49f1daf46a116eb32396f1cc84a9e79e3836d4bfe84d6bca64736f6c634300050b0032a265627a7a72315820e2350a73a28ed02b4dac678f2b77a330dc512c3cce8ca53fa1c30869f443553d64736f6c634300050b0032" - created_contract_init_code = "6080604052348015600f57600080fd5b50603e80601d6000396000f3fe6080604052600080fdfea265627a7a72315820f4040cbd444dcd2f49f1daf46a116eb32396f1cc84a9e79e3836d4bfe84d6bca64736f6c634300050b0032" - created_contract_runtime_code = "6080604052600080fdfea265627a7a72315820f4040cbd444dcd2f49f1daf46a116eb32396f1cc84a9e79e3836d4bfe84d6bca64736f6c634300050b0032" - world_state = WorldState() - account = world_state.create_account(balance=1000, address=101) - account.code = Disassembly(creating_contract_runtime_code) - environment = Environment(account, None, None, None, None, None) - og_state = GlobalState( - world_state, environment, None, MachineState(gas_limit=8000000) - ) - og_state.transaction_stack.append( - (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) - ) +last_state = None +created_contract_account = None + + +def execute_create(): + global last_state + global created_contract_account + if not last_state and not created_contract_account: + code_raw = [] + for i in range(len(contract_init_code) // 2): + code_raw.append(int(contract_init_code[2 * i : 2 * (i + 1)], 16)) + calldata = ConcreteCalldata(0, code_raw) - laser_evm = LaserEVM() + world_state = WorldState() + account = world_state.create_account(balance=1000000, address=101) + account.code = Disassembly("60a760006000f000") + environment = Environment(account, None, calldata, None, None, None) + og_state = GlobalState( + world_state, environment, None, MachineState(gas_limit=8000000) + ) + og_state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) - new_states, op_code = laser_evm.execute_state(og_state) - # checks + laser = LaserEVM() + states = [og_state] + last_state = og_state + for state in states: + new_states, op_code = laser.execute_state(state) + last_state = state + if op_code == "STOP": + break + states.extend(new_states) - # TODO: come up with sequence, then grab an address from stack and check that its code is created. + created_contract_address = last_state.mstate.stack[-1].value + created_contract_account = last_state.world_state.accounts[ + created_contract_address + ] + + return last_state, created_contract_account + + +def test_create_has_code(): + last_state, created_contract_account = execute_create() + assert created_contract_account.code.bytecode == contract_runtime_code + + +def test_create_has_storage(): + last_state, created_contract_account = execute_create() + storage = created_contract_account.storage + # From contract, val = 10. + assert storage[symbol_factory.BitVecVal(0, 256)] == symbol_factory.BitVecVal( + 10, 256 + ) From 126fc26da6de0b00809dc1ae4767b501a02975fa Mon Sep 17 00:00:00 2001 From: Eric N Date: Tue, 17 Sep 2019 22:58:29 -0700 Subject: [PATCH 21/28] Cleaned up some logic. Fixed issue with VMException and freezing on staticcall. --- mythril/analysis/call_helpers.py | 2 +- mythril/laser/ethereum/instructions.py | 20 +++++++++---------- .../transaction/transaction_models.py | 2 +- 3 files changed, 11 insertions(+), 13 deletions(-) diff --git a/mythril/analysis/call_helpers.py b/mythril/analysis/call_helpers.py index 270ff5af..cb6f55d7 100644 --- a/mythril/analysis/call_helpers.py +++ b/mythril/analysis/call_helpers.py @@ -18,7 +18,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]: op = instruction["opcode"] stack = state.mstate.stack - if op in ("CALL", "CALLCODE", "STATICCALL"): + if op in ("CALL", "CALLCODE"): gas, to, value, meminstart, meminsz, memoutstart, memoutsz = ( get_variable(stack[-1]), get_variable(stack[-2]), diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 5d37350b..09ea0a2b 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1789,7 +1789,6 @@ class Instruction: :param global_state: :return: """ - call_value, mem_offset, mem_size = global_state.mstate.pop(3) return self._create_transaction_helper( @@ -1801,12 +1800,10 @@ class Instruction: call_value, mem_offset, mem_size = global_state.mstate.pop(3) call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) if global_state.last_return_data: - global_state.mstate.stack.append( - symbol_factory.BitVecVal(int(global_state.last_return_data, 16), 256) - ) + return_val = symbol_factory.BitVecVal(int(global_state.last_return_data, 16), 256) else: - global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256)) - + return_val = symbol_factory.BitVecVal(0, 256) + global_state.mstate.stack.append(return_val) return [global_state] @StateTransition(is_state_mutation_instruction=True) @@ -1827,11 +1824,10 @@ class Instruction: call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) if global_state.last_return_data: - global_state.mstate.stack.append( - symbol_factory.BitVecVal(int(global_state.last_return_data), 256) - ) + return_val = symbol_factory.BitVecVal(int(global_state.last_return_data), 256) else: - global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256)) + return_val = symbol_factory.BitVecVal(0, 256) + global_state.mstate.stack.append(return_val) return [global_state] @StateTransition() @@ -2287,6 +2283,7 @@ class Instruction: ) raise TransactionStartSignal(transaction, self.op_code, global_state) + @StateTransition() def staticcall_post(self, global_state: GlobalState) -> List[GlobalState]: return self.post_handler(global_state, function_name="staticcall") @@ -2294,8 +2291,9 @@ class Instruction: instr = global_state.get_current_instruction() try: + with_value = function_name is not "staticcall" callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters( - global_state, self.dynamic_loader, True + global_state, self.dynamic_loader, with_value ) except ValueError as e: log.debug( diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 3195365d..06019646 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -201,7 +201,7 @@ class ContractCreationTransaction(BaseTransaction): callee_account = world_state.create_account( 0, concrete_storage=True, creator=caller.value, address=contract_address ) - callee_account.contract_name = contract_name + callee_account.contract_name = contract_name or callee_account.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__( From 079b8a70da18c944ecbbb9973518a6fd46367bfc Mon Sep 17 00:00:00 2001 From: Eric N Date: Tue, 17 Sep 2019 23:00:02 -0700 Subject: [PATCH 22/28] Ran black. TODO: Fix issue with storage. --- mythril/laser/ethereum/instructions.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 09ea0a2b..e91862b7 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1800,7 +1800,9 @@ class Instruction: call_value, mem_offset, mem_size = global_state.mstate.pop(3) call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) if global_state.last_return_data: - return_val = symbol_factory.BitVecVal(int(global_state.last_return_data, 16), 256) + return_val = symbol_factory.BitVecVal( + int(global_state.last_return_data, 16), 256 + ) else: return_val = symbol_factory.BitVecVal(0, 256) global_state.mstate.stack.append(return_val) @@ -1824,7 +1826,9 @@ class Instruction: call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4) call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size) if global_state.last_return_data: - return_val = symbol_factory.BitVecVal(int(global_state.last_return_data), 256) + return_val = symbol_factory.BitVecVal( + int(global_state.last_return_data), 256 + ) else: return_val = symbol_factory.BitVecVal(0, 256) global_state.mstate.stack.append(return_val) From 72db1237fbf64e42b042040bc8b5978b5e3fee2b Mon Sep 17 00:00:00 2001 From: Eric N Date: Tue, 17 Sep 2019 23:48:32 -0700 Subject: [PATCH 23/28] Fixed issue with staticcall. --- 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 e91862b7..b7709343 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -2280,7 +2280,7 @@ class Instruction: origin=environment.origin, code=callee_account.code, caller=environment.address, - callee_account=environment.active_account, + callee_account=callee_account, call_data=call_data, call_value=value, static=True, From 581c8d7b018448a7a6fd419357ae00e48572a1a4 Mon Sep 17 00:00:00 2001 From: Eric N Date: Wed, 18 Sep 2019 13:31:23 -0700 Subject: [PATCH 24/28] Refactor code --- mythril/laser/ethereum/instructions.py | 109 ++++-------------- .../transaction/transaction_models.py | 3 + 2 files changed, 27 insertions(+), 85 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index b7709343..70467da3 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -787,7 +787,7 @@ class Instruction: return [global_state] @staticmethod - def _calldata_copy_helper(global_state, state, mstart, dstart, size): + def _calldata_copy_helper(global_state, mstate, mstart, dstart, size): environment = global_state.environment try: @@ -811,11 +811,11 @@ class Instruction: size = cast(int, size) if size > 0: try: - state.mem_extend(mstart, size) + mstate.mem_extend(mstart, size) except TypeError as e: log.debug("Memory allocation error: {}".format(e)) - state.mem_extend(mstart, 1) - state.memory[mstart] = global_state.new_bitvec( + mstate.mem_extend(mstart, 1) + mstate.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" @@ -840,12 +840,12 @@ class Instruction: else simplify(cast(BitVec, i_data) + 1) ) for i in range(len(new_memory)): - state.memory[i + mstart] = new_memory[i] + mstate.memory[i + mstart] = new_memory[i] except IndexError: log.debug("Exception copying calldata to memory") - state.memory[mstart] = global_state.new_bitvec( + mstate.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" @@ -1039,34 +1039,6 @@ class Instruction: global_state.mstate.stack.append(global_state.environment.gasprice) return [global_state] - @staticmethod - def _handle_symbolic_args( - global_state: GlobalState, concrete_memory_offset: int - ) -> None: - """ - In contract creation transaction with dynamic arguments(like arrays, maps) solidity will try to - execute CODECOPY with code size as len(with_args) - len(without_args) which in our case - would be 0, hence we are writing 10 symbol words onto the memory on the assumption that - no one would use 10 array/map arguments for constructor. - :param global_state: The global state - :param concrete_memory_offset: The memory offset on which symbols should be written - """ - no_of_words = ceil( - min(len(global_state.environment.code.bytecode) / 2, 320) / 32 - ) - global_state.mstate.mem_extend(concrete_memory_offset, 32 * no_of_words) - for i in range(no_of_words): - global_state.mstate.memory.write_word_at( - concrete_memory_offset + i * 32, - global_state.new_bitvec( - "code_{}({})".format( - concrete_memory_offset + i * 32, - global_state.environment.active_account.contract_name, - ), - 256, - ), - ) - @StateTransition() def codecopy_(self, global_state: GlobalState) -> List[GlobalState]: """ @@ -1088,17 +1060,17 @@ class Instruction: # Treat creation code after the expected disassembly as calldata. # This is a slightly hacky way to ensure that symbolic constructor # arguments work correctly. + mstate = global_state.mstate offset = code_offset - code_size - log.warning("Doing hacky thing offset: {} size: {}".format(offset, size)) + log.debug("Copying from code offset: {} with size: {}".format(offset, size)) if isinstance(global_state.environment.calldata, SymbolicCalldata): if code_offset >= code_size: return self._calldata_copy_helper( - global_state, global_state.mstate, memory_offset, offset, size + global_state, mstate, memory_offset, offset, size ) else: # Copy from both code and calldata appropriately. - state = global_state.mstate environment = global_state.environment concrete_memory_offset = helper.get_concrete_int(memory_offset) concrete_code_offset = helper.get_concrete_int(code_offset) @@ -1124,47 +1096,21 @@ class Instruction: calldata_copy_size if calldata_copy_size >= 0 else 0 ) - try: - global_state.mstate.mem_extend( - concrete_memory_offset, concrete_size + calldata_copy_size - ) - except TypeError: - global_state.mstate.mem_extend(concrete_memory_offset, 1) - global_state.mstate.memory[ - concrete_memory_offset - ] = global_state.new_bitvec( - "code({})".format( - global_state.environment.active_account.contract_name - ), - 8, - ) - return [global_state] - for i in range(concrete_size): - if i < code_copy_size: - # copy from code - global_state.mstate.memory[concrete_memory_offset + i] = int( - code[ - 2 - * (code_copy_offset + i) : 2 - * (code_copy_offset + i + 1) - ], - 16, - ) - elif i < code_copy_size + calldata_copy_size: - # copy from calldata - global_state.mstate.memory[ - concrete_memory_offset + i - ] = calldata[calldata_copy_offset + i - code_copy_size] - else: - global_state.mstate.memory[ - concrete_memory_offset + i - ] = global_state.new_bitvec( - "code({})".format( - global_state.environment.active_account.contract_name - ), - 8, - ) - return [global_state] + [global_state] = self._code_copy_helper( + code=global_state.environment.code.bytecode, + memory_offset=memory_offset, + code_offset=code_copy_offset, + size=code_copy_size, + op="CODECOPY", + global_state=global_state, + ) + return self._calldata_copy_helper( + global_state=global_state, + mstate=mstate, + mstart=memory_offset + code_copy_size, + dstart=calldata_copy_offset, + size=calldata_copy_size, + ) return self._code_copy_helper( code=global_state.environment.code.bytecode, @@ -1254,13 +1200,6 @@ class Instruction: if code[0:2] == "0x": code = code[2:] - if concrete_size == 0 and isinstance( - global_state.current_transaction, ContractCreationTransaction - ): - if concrete_code_offset >= len(code) // 2: - Instruction._handle_symbolic_args(global_state, concrete_memory_offset) - return [global_state] - for i in range(concrete_size): if 2 * (concrete_code_offset + i + 1) <= len(code): global_state.mstate.memory[concrete_memory_offset + i] = int( diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 06019646..b36cc61d 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -198,6 +198,9 @@ class ContractCreationTransaction(BaseTransaction): contract_address=None, ) -> None: self.prev_world_state = deepcopy(world_state) + contract_address = ( + contract_address if isinstance(contract_address, int) else None + ) callee_account = world_state.create_account( 0, concrete_storage=True, creator=caller.value, address=contract_address ) From e47c35ee154a755ca5a59dcfc00f65df6b3e1c03 Mon Sep 17 00:00:00 2001 From: Eric N Date: Wed, 18 Sep 2019 14:16:36 -0700 Subject: [PATCH 25/28] Fixed mypy. --- mythril/laser/ethereum/instructions.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 70467da3..39ea5c4c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1152,9 +1152,9 @@ class Instruction: @staticmethod def _code_copy_helper( code: str, - memory_offset: BitVec, - code_offset: BitVec, - size: BitVec, + memory_offset: Union[int, BitVec], + code_offset: Union[int, BitVec], + size: Union[int, BitVec], op: str, global_state: GlobalState, ) -> List[GlobalState]: From 44856621262c67161cea7a2963ed9c40416b7e84 Mon Sep 17 00:00:00 2001 From: Nathan Date: Thu, 19 Sep 2019 20:19:28 -0400 Subject: [PATCH 26/28] Remove unused variables --- mythril/laser/ethereum/instructions.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 39ea5c4c..46111773 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1071,13 +1071,9 @@ class Instruction: ) else: # Copy from both code and calldata appropriately. - environment = global_state.environment - concrete_memory_offset = helper.get_concrete_int(memory_offset) concrete_code_offset = helper.get_concrete_int(code_offset) concrete_size = helper.get_concrete_int(size) - calldata = global_state.environment.calldata - code_copy_offset = concrete_code_offset code_copy_size = ( concrete_size From b2bbe2568a0a60977a03c9370e876c80a9595834 Mon Sep 17 00:00:00 2001 From: Nathan Date: Thu, 19 Sep 2019 20:30:08 -0400 Subject: [PATCH 27/28] Remove unused import --- mythril/laser/ethereum/instructions.py | 1 - 1 file changed, 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 46111773..2f1c7f03 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -6,7 +6,6 @@ import logging from copy import copy, deepcopy from typing import cast, Callable, List, Set, Union, Tuple, Any from datetime import datetime -from math import ceil from ethereum import utils from mythril.laser.smt import ( From cb307f0d94082b88d71ea88d81ea92cceb212bf3 Mon Sep 17 00:00:00 2001 From: Nathan Date: Tue, 24 Sep 2019 05:30:45 -0400 Subject: [PATCH 28/28] Check delegatecall after execution finishes (#1215) --- mythril/analysis/modules/delegatecall.py | 38 ++++++++++-------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/mythril/analysis/modules/delegatecall.py b/mythril/analysis/modules/delegatecall.py index 4b97228b..aa0cae6a 100644 --- a/mythril/analysis/modules/delegatecall.py +++ b/mythril/analysis/modules/delegatecall.py @@ -1,19 +1,18 @@ """This module contains the detection code for insecure delegate call usage.""" -import json import logging -from copy import copy -from typing import List, cast, Dict +from typing import List -from mythril.analysis import solver +from mythril.analysis.potential_issues import ( + get_potential_issues_annotation, + PotentialIssue, +) from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) -from mythril.analysis.report import Issue from mythril.analysis.modules.base import DetectionModule from mythril.exceptions import UnsatError -from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.smt import symbol_factory, UGT @@ -41,19 +40,16 @@ class DelegateCallModule(DetectionModule): """ if state.get_current_instruction()["address"] in self.cache: return - issues = self._analyze_state(state) - for issue in issues: - self.cache.add(issue.address) - self.issues.extend(issues) + potential_issues = self._analyze_state(state) + + annotation = get_potential_issues_annotation(state) + annotation.potential_issues.extend(potential_issues) - @staticmethod - def _analyze_state(state: GlobalState) -> List[Issue]: + def _analyze_state(self, state: GlobalState) -> List[PotentialIssue]: """ :param state: the current state :return: returns the issues for that corresponding state """ - op_code = state.get_current_instruction()["opcode"] - gas = state.mstate.stack[-1] to = state.mstate.stack[-2] @@ -67,16 +63,14 @@ class DelegateCallModule(DetectionModule): constraints.append(tx.caller == ATTACKER_ADDRESS) try: - 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( + "[DELEGATECALL] Detected potential 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 " @@ -85,7 +79,7 @@ class DelegateCallModule(DetectionModule): ) return [ - Issue( + PotentialIssue( contract=state.environment.active_account.contract_name, function_name=state.environment.active_function_name, address=address, @@ -95,8 +89,8 @@ class DelegateCallModule(DetectionModule): 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), + constraints=constraints, + detector=self, ) ]