From 5272d54953c7484625c1be456af9ed0983e7d1d4 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sun, 26 Aug 2018 18:12:20 +0530 Subject: [PATCH 01/32] Add constructor mapping for SolidityContract --- mythril/analysis/report.py | 2 +- mythril/ether/ethcontract.py | 3 +- mythril/ether/soliditycontract.py | 51 +++++++++++++++++++------------ 3 files changed, 34 insertions(+), 22 deletions(-) diff --git a/mythril/analysis/report.py b/mythril/analysis/report.py index 2e2e04d5..35bbae07 100644 --- a/mythril/analysis/report.py +++ b/mythril/analysis/report.py @@ -35,7 +35,7 @@ class Issue: def add_code_info(self, contract): if self.address: - codeinfo = contract.get_source_info(self.address) + codeinfo = contract.get_source_info(self.address, constructor=(self.function == 'constructor')) self.filename = codeinfo.filename self.code = codeinfo.code self.lineno = codeinfo.lineno diff --git a/mythril/ether/ethcontract.py b/mythril/ether/ethcontract.py index 5f42f2a5..24a859e8 100644 --- a/mythril/ether/ethcontract.py +++ b/mythril/ether/ethcontract.py @@ -17,7 +17,8 @@ class ETHContract(persistent.Persistent): code = re.sub(r'(_+.*_+)', 'aa' * 20, code) self.code = code - self.disassembly = Disassembly(self.code, enable_online_lookup=enable_online_lookup) + self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup) + self.creation_disassemble = Disassembly(creation_code, enable_online_lookup=enable_online_lookup) def as_dict(self): diff --git a/mythril/ether/soliditycontract.py b/mythril/ether/soliditycontract.py index 2fa6c78b..22f742d8 100644 --- a/mythril/ether/soliditycontract.py +++ b/mythril/ether/soliditycontract.py @@ -52,7 +52,8 @@ class SolidityContract(ETHContract): has_contract = False # If a contract name has been specified, find the bytecode of that specific contract - + srcmap_constructor = [] + srcmap = [] if name: for key, contract in sorted(data['contracts'].items()): filename, _name = key.split(":") @@ -61,6 +62,7 @@ class SolidityContract(ETHContract): code = contract['bin-runtime'] creation_code = contract['bin'] srcmap = contract['srcmap-runtime'].split(";") + srcmap_constructor = contract['srcmap'].split(";") has_contract = True break @@ -74,6 +76,7 @@ class SolidityContract(ETHContract): code = contract['bin-runtime'] creation_code = contract['bin'] srcmap = contract['srcmap-runtime'].split(";") + srcmap_constructor = contract['srcmap'].split(";") has_contract = True if not has_contract: @@ -81,6 +84,32 @@ class SolidityContract(ETHContract): self.mappings = [] + self.constructor_mappings = [] + + self._get_solc_mappings(srcmap) + self._get_solc_mappings(srcmap_constructor, constructor=True) + + super().__init__(code, creation_code, name=name) + + def get_source_info(self, address, constructor=False): + disassembly = self.creation_disassemble if constructor else self.disassembly + mappings = self.constructor_mappings if constructor else self.mappings + index = helper.get_instruction_index(disassembly.instruction_list, address) + + solidity_file = self.solidity_files[mappings[index].solidity_file_idx] + + filename = solidity_file.filename + + offset = mappings[index].offset + length = mappings[index].length + + code = solidity_file.data.encode('utf-8')[offset:offset + length].decode('utf-8', errors="ignore") + lineno = mappings[index].lineno + + return SourceCodeInfo(filename, lineno, code) + + def _get_solc_mappings(self, srcmap, constructor=False): + mappings = self.constructor_mappings if constructor else self.mappings for item in srcmap: mapping = item.split(":") @@ -94,22 +123,4 @@ class SolidityContract(ETHContract): idx = int(mapping[2]) lineno = self.solidity_files[idx].data.encode('utf-8')[0:offset].count('\n'.encode('utf-8')) + 1 - self.mappings.append(SourceMapping(idx, offset, length, lineno)) - - super().__init__(code, creation_code, name=name) - - def get_source_info(self, address): - - index = helper.get_instruction_index(self.disassembly.instruction_list, address) - - solidity_file = self.solidity_files[self.mappings[index].solidity_file_idx] - - filename = solidity_file.filename - - offset = self.mappings[index].offset - length = self.mappings[index].length - - code = solidity_file.data.encode('utf-8')[offset:offset + length].decode('utf-8') - lineno = self.mappings[index].lineno - - return SourceCodeInfo(filename, lineno, code) + mappings.append(SourceMapping(idx, offset, length, lineno)) From 7387f14ba1c9ac01de7cdaaeb941c2733e43a003 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Sun, 26 Aug 2018 18:20:00 +0530 Subject: [PATCH 02/32] Get solc constructor code --- mythril/ether/util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/ether/util.py b/mythril/ether/util.py index e01cae28..ac09b4fb 100644 --- a/mythril/ether/util.py +++ b/mythril/ether/util.py @@ -18,7 +18,7 @@ def safe_decode(hex_encoded_string): def get_solc_json(file, solc_binary="solc", solc_args=None): - cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap-runtime", '--allow-paths', "."] + cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap,srcmap-runtime", '--allow-paths', "."] if solc_args: cmd.extend(solc_args.split(" ")) From b78529cea04ef0b20da3f969eb8492bd017601e5 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 27 Aug 2018 16:31:40 +0200 Subject: [PATCH 03/32] Retain transaction sequence --- mythril/laser/ethereum/state.py | 5 +++-- mythril/laser/ethereum/transaction/symbolic.py | 8 +++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 93cb2887..e48cd9d5 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -219,12 +219,13 @@ class WorldState: """ The WorldState class represents the world state as described in the yellow paper """ - def __init__(self): + def __init__(self, transaction_sequence=None): """ Constructor for the world state. Initializes the accounts record """ self.accounts = {} self.node = None + self.transaction_sequence = transaction_sequence or [] def __getitem__(self, item): """ @@ -235,7 +236,7 @@ class WorldState: return self.accounts[item] def __copy__(self): - new_world_state = WorldState() + new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:]) new_world_state.accounts = copy(self.accounts) new_world_state.node = self.node return new_world_state diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 01b22c55..fb3eeb54 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -1,8 +1,9 @@ -from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction from z3 import BitVec -from mythril.laser.ethereum.state import CalldataType + from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType +from mythril.laser.ethereum.state import CalldataType +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction def execute_message_call(laser_evm, callee_address): @@ -38,7 +39,7 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_ for open_world_state in open_states: transaction = ContractCreationTransaction( open_world_state, - BitVec("caller", 256), + BitVec("creator", 256), new_account, Disassembly(contract_initialization_code), [], @@ -69,6 +70,7 @@ def _setup_global_state_for_execution(laser_evm, transaction): global_state.mstate.constraints = transaction.world_state.node.constraints new_node.constraints = global_state.mstate.constraints + global_state.world_state.transaction_sequence.append(transaction) global_state.node = new_node new_node.states.append(global_state) laser_evm.work_list.append(global_state) From dea9c3c11e64cf4791520ee7fafce21147fe5268 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 27 Aug 2018 16:34:09 +0200 Subject: [PATCH 04/32] Refactor of suicide analysis --- mythril/analysis/modules/suicide.py | 119 +++++++++++----------------- 1 file changed, 46 insertions(+), 73 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index cad914bc..d613a775 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -1,9 +1,7 @@ -from z3 import * from mythril.analysis import solver from mythril.analysis.ops import * from mythril.analysis.report import Issue from mythril.exceptions import UnsatError -import re import logging @@ -15,86 +13,61 @@ Check for SUICIDE instructions that either can be reached by anyone, or where ms ''' -def execute(statespace): +def execute(state_space): logging.debug("Executing module: UNCHECKED_SUICIDE") issues = [] - for k in statespace.nodes: - node = statespace.nodes[k] + for k in state_space.nodes: + node = state_space.nodes[k] for state in node.states: + issues += _analyze_state(state, node) - instruction = state.get_current_instruction() - - if(instruction['opcode'] == "SUICIDE"): - - logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name) - - description = "The function `" + node.function_name + "` executes the SUICIDE instruction. " - - stack = copy.deepcopy(state.mstate.stack) - to = stack.pop() - - if ("caller" in str(to)): - description += "The remaining Ether is sent to the caller's address.\n" - elif ("storage" in str(to)): - description += "The remaining Ether is sent to a stored address.\n" - elif ("calldata" in str(to)): - description += "The remaining Ether is sent to an address provided as a function argument.\n" - elif (type(to) == BitVecNumRef): - description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n" - else: - description += "The remaining Ether is sent to: " + str(to) + "\n" - - constrained = False - can_solve = True - - index = 0 - - while(can_solve and index < len(node.constraints)): - - constraint = node.constraints[index] - index += 1 - - m = re.search(r'storage_([a-z0-9_&^]+)', str(constraint)) - - if (m): - constrained = True - idx = m.group(1) - - logging.debug("STORAGE CONSTRAINT FOUND: " + idx) - - func = statespace.find_storage_write(state.environment.active_account.address, idx) - - if func: - description += "\nThere is a check on storage index " + str(idx) + ". This storage index can be written to by calling the function `" + func + "`." - break - else: - logging.debug("[UNCHECKED_SUICIDE] No storage writes to index " + str(idx)) - can_solve = False - break - - elif (re.search(r"caller", str(constraint)) and re.search(r'[0-9]{20}', str(constraint))): - can_solve = False - break - - if not constrained: - description += "\nIt seems that this function can be called without restrictions." - - if can_solve: - - try: - - model = solver.get_model(node.constraints) - - debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model) + return issues - issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug) - issues.append(issue) - except UnsatError: - logging.debug("[UNCHECKED_SUICIDE] no model found") +def _analyze_state(state, node): + issues = [] + instruction = state.get_current_instruction() + + if instruction['opcode'] != "SUICIDE": + return [] + + to = state.mstate.stack[-1] + + logging.debug("[UNCHECKED_SUICIDE] suicide in function " + node.function_name) + description = "The function `" + node.function_name + "` executes the SUICIDE instruction. " + + if "caller" in str(to): + description += "The remaining Ether is sent to the caller's address.\n" + elif "storage" in str(to): + description += "The remaining Ether is sent to a stored address.\n" + elif "calldata" in str(to): + description += "The remaining Ether is sent to an address provided as a function argument.\n" + elif type(to) == BitVecNumRef: + description += "The remaining Ether is sent to: " + hex(to.as_long()) + "\n" + else: + description += "The remaining Ether is sent to: " + str(to) + "\n" + + not_creator_constraints = [] + if len(state.world_state.transaction_sequence) > 1: + try: + creator = state.world_state.transaction_sequence[0].caller + for transaction in state.world_state.transaction_sequence[1:]: + not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))) + except IndexError: + return [] + + try: + model = solver.get_model(node.constraints + not_creator_constraints) + + debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model) + + issue = Issue(node.contract_name, node.function_name, instruction['address'], "Unchecked SUICIDE", "Warning", description, debug) + issues.append(issue) + except UnsatError: + logging.debug("[UNCHECKED_SUICIDE] no model found") return issues From e218c20e918c16de44ca89c141a32ff8a04ce3a2 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 27 Aug 2018 20:48:36 +0530 Subject: [PATCH 05/32] Add new tests for SolidityContract --- mythril/ether/ethcontract.py | 2 +- mythril/ether/soliditycontract.py | 3 +-- tests/solidity_contract_test.py | 11 +++++++++++ 3 files changed, 13 insertions(+), 3 deletions(-) diff --git a/mythril/ether/ethcontract.py b/mythril/ether/ethcontract.py index 24a859e8..b43b1919 100644 --- a/mythril/ether/ethcontract.py +++ b/mythril/ether/ethcontract.py @@ -18,7 +18,7 @@ class ETHContract(persistent.Persistent): self.code = code self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup) - self.creation_disassemble = Disassembly(creation_code, enable_online_lookup=enable_online_lookup) + self.creation_disassembly = Disassembly(creation_code, enable_online_lookup=enable_online_lookup) def as_dict(self): diff --git a/mythril/ether/soliditycontract.py b/mythril/ether/soliditycontract.py index 22f742d8..0642ea21 100644 --- a/mythril/ether/soliditycontract.py +++ b/mythril/ether/soliditycontract.py @@ -92,10 +92,9 @@ class SolidityContract(ETHContract): super().__init__(code, creation_code, name=name) def get_source_info(self, address, constructor=False): - disassembly = self.creation_disassemble if constructor else self.disassembly + disassembly = self.creation_disassembly if constructor else self.disassembly mappings = self.constructor_mappings if constructor else self.mappings index = helper.get_instruction_index(disassembly.instruction_list, address) - solidity_file = self.solidity_files[mappings[index].solidity_file_idx] filename = solidity_file.filename diff --git a/tests/solidity_contract_test.py b/tests/solidity_contract_test.py index b1c02bf7..fb1a596a 100644 --- a/tests/solidity_contract_test.py +++ b/tests/solidity_contract_test.py @@ -26,3 +26,14 @@ class SolidityContractTest(BaseTestCase): self.assertEqual(code_info.filename, str(input_file)) self.assertEqual(code_info.lineno, 6) self.assertEqual(code_info.code, "msg.sender.transfer(1 ether)") + + def test_get_source_info_with_contract_name_specified_constructor(self): + input_file = TEST_FILES / "constructor_assert.sol" + contract = SolidityContract(str(input_file), name="AssertFail") + + code_info = contract.get_source_info(62, constructor=True) + + self.assertEqual(code_info.filename, str(input_file)) + self.assertEqual(code_info.lineno, 6) + self.assertEqual(code_info.code, "assert(var1>0)") + From 752e9c64a73f46ba3cadfe97afc2641579096f13 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 27 Aug 2018 20:49:43 +0530 Subject: [PATCH 06/32] add solidity test file for SolidityContract --- tests/testdata/input_contracts/constructor_assert.sol | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 tests/testdata/input_contracts/constructor_assert.sol diff --git a/tests/testdata/input_contracts/constructor_assert.sol b/tests/testdata/input_contracts/constructor_assert.sol new file mode 100644 index 00000000..aff01b47 --- /dev/null +++ b/tests/testdata/input_contracts/constructor_assert.sol @@ -0,0 +1,8 @@ +pragma solidity ^0.4.24; + +contract AssertFail { + + constructor(uint8 var1){ + assert(var1>0); + } +} From dd08a8dd37c5cd1fcaa8f2fd2530a0b00c928417 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Mon, 27 Aug 2018 22:36:38 +0530 Subject: [PATCH 07/32] Add the constructor test file --- .../constructor_assert.sol.json | 472 ++++++++++++++++++ 1 file changed, 472 insertions(+) create mode 100644 tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json diff --git a/tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json b/tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json new file mode 100644 index 00000000..94cfd175 --- /dev/null +++ b/tests/testdata/outputs_expected_laser_result/constructor_assert.sol.json @@ -0,0 +1,472 @@ +{ + "accounts": { + "0x0000000000000000000000000000000000000000": { + "storage": "", + "nonce": 0, + "balance": "balance", + "code": [ + { + "address": 0, + "argument": "0x80", + "opcode": "PUSH1" + }, + { + "address": 2, + "argument": "0x40", + "opcode": "PUSH1" + }, + { + "address": 4, + "opcode": "MSTORE" + }, + { + "address": 5, + "argument": "0x00", + "opcode": "PUSH1" + }, + { + "address": 7, + "opcode": "DUP1" + }, + { + "address": 8, + "opcode": "REVERT" + }, + { + "address": 9, + "opcode": "STOP" + } + ] + } + }, + "total_states": 5, + "nodes": { + "933": { + "contract_name": "unknown", + "flags": "NodeFlags()", + "constraints": [], + "function_name": "unknown", + "start_addr": 0, + "uid": 933, + "states": [ + { + "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])", + "mstate": { + "gas": 10000000, + "memory": [], + "pc": 0, + "memsize": 0, + "stack": [] + }, + "environment": { + "sender": "caller", + "callvalue": "call_value", + "origin": "origin", + "active_account": "0x0000000000000000000000000000000000000000", + "gasprice": "gas_price", + "calldata": [], + "calldata_type": "CalldataType.SYMBOLIC" + } + }, + { + "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])", + "mstate": { + "gas": 10000000, + "memory": [], + "pc": 1, + "memsize": 0, + "stack": [ + "128" + ] + }, + "environment": { + "sender": "caller", + "callvalue": "call_value", + "origin": "origin", + "active_account": "0x0000000000000000000000000000000000000000", + "gasprice": "gas_price", + "calldata": [], + "calldata_type": "CalldataType.SYMBOLIC" + } + }, + { + "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])", + "mstate": { + "gas": 10000000, + "memory": [], + "pc": 2, + "memsize": 0, + "stack": [ + "128", + "64" + ] + }, + "environment": { + "sender": "caller", + "callvalue": "call_value", + "origin": "origin", + "active_account": "0x0000000000000000000000000000000000000000", + "gasprice": "gas_price", + "calldata": [], + "calldata_type": "CalldataType.SYMBOLIC" + } + }, + { + "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])", + "mstate": { + "gas": 10000000, + "memory": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 128 + ], + "pc": 3, + "memsize": 96, + "stack": [] + }, + "environment": { + "sender": "caller", + "callvalue": "call_value", + "origin": "origin", + "active_account": "0x0000000000000000000000000000000000000000", + "gasprice": "gas_price", + "calldata": [], + "calldata_type": "CalldataType.SYMBOLIC" + } + }, + { + "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])", + "mstate": { + "gas": 10000000, + "memory": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 128 + ], + "pc": 4, + "memsize": 96, + "stack": [ + "0" + ] + }, + "environment": { + "sender": "caller", + "callvalue": "call_value", + "origin": "origin", + "active_account": "0x0000000000000000000000000000000000000000", + "gasprice": "gas_price", + "calldata": [], + "calldata_type": "CalldataType.SYMBOLIC" + } + }, + { + "accounts": "dict_keys(['0x0000000000000000000000000000000000000000'])", + "mstate": { + "gas": 10000000, + "memory": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 128 + ], + "pc": 5, + "memsize": 96, + "stack": [ + "0", + "0" + ] + }, + "environment": { + "sender": "caller", + "callvalue": "call_value", + "origin": "origin", + "active_account": "0x0000000000000000000000000000000000000000", + "gasprice": "gas_price", + "calldata": [], + "calldata_type": "CalldataType.SYMBOLIC" + } + } + ] + } + }, + "max_depth": 22, + "edges": [] +} From ff90044febe18c09f764f70770ef7a9e026ea142 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:14:24 +0200 Subject: [PATCH 08/32] Add transaction ids --- .../laser/ethereum/transaction/symbolic.py | 27 ++++++++----- .../transaction/transaction_models.py | 39 +++++++++++-------- 2 files changed, 39 insertions(+), 27 deletions(-) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index fb3eeb54..0b5ba51b 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -1,25 +1,30 @@ -from z3 import BitVec +from z3 import BitVec, Extract, Not from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType from mythril.laser.ethereum.state import CalldataType from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction +next_transaction_id = 0 + def execute_message_call(laser_evm, callee_address): """ Executes a message call transaction from all open states """ + global next_transaction_id open_states = laser_evm.open_states[:] del laser_evm.open_states[:] for open_world_state in open_states: + next_transaction_id += 1 transaction = MessageCallTransaction( + next_transaction_id, open_world_state, open_world_state[callee_address], - BitVec("caller", 256), + BitVec("caller{}".format(next_transaction_id), 256), [], - BitVec("gas_price", 256), - BitVec("call_value", 256), - BitVec("origin", 256), + BitVec("gas_price{}".format(next_transaction_id), 256), + BitVec("call_value{}".format(next_transaction_id), 256), + BitVec("origin{}".format(next_transaction_id), 256), CalldataType.SYMBOLIC, ) _setup_global_state_for_execution(laser_evm, transaction) @@ -29,6 +34,7 @@ def execute_message_call(laser_evm, callee_address): def execute_contract_creation(laser_evm, contract_initialization_code, contract_name=None): """ Executes a contract creation transaction from all open states""" + global next_transaction_id open_states = laser_evm.open_states[:] del laser_evm.open_states[:] @@ -37,18 +43,19 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_ new_account.contract_name = contract_name for open_world_state in open_states: + next_transaction_id += 1 transaction = ContractCreationTransaction( + next_transaction_id, open_world_state, - BitVec("creator", 256), + BitVec("creator{}".format(next_transaction_id), 256), new_account, Disassembly(contract_initialization_code), [], - BitVec("gas_price", 256), - BitVec("call_value", 256), - BitVec("origin", 256), + BitVec("gas_price{}".format(next_transaction_id), 256), + BitVec("call_value{}".format(next_transaction_id), 256), + BitVec("origin{}".format(next_transaction_id), 256), CalldataType.SYMBOLIC ) - _setup_global_state_for_execution(laser_evm, transaction) laser_evm.exec(True) diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 6a332d3d..4f1dd329 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -21,25 +21,27 @@ class TransactionStartSignal(Exception): class MessageCallTransaction: """ Transaction object models an transaction""" def __init__(self, + identifier, world_state, callee_account, caller, call_data=(), - gas_price=BitVec("gasprice", 256), - call_value=BitVec("callvalue", 256), - origin=BitVec("origin", 256), - call_data_type=BitVec("call_data_type", 256), + gas_price=None, + call_value=None, + origin=None, + call_data_type=None, code=None ): assert isinstance(world_state, WorldState) + self.id = identifier self.world_state = world_state self.callee_account = callee_account self.caller = caller self.call_data = call_data - self.gas_price = gas_price - self.call_value = call_value - self.origin = origin - self.call_data_type = call_data_type + self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price + self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value + self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin + self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type self.code = code self.return_data = None @@ -69,29 +71,32 @@ class MessageCallTransaction: class ContractCreationTransaction: """ Transaction object models an transaction""" def __init__(self, + identifier, world_state, caller, callee_account=None, code=None, call_data=(), - gas_price=BitVec("gasprice", 256), - call_value=BitVec("callvalue", 256), - origin=BitVec("origin", 256), - call_data_type=BitVec("call_data_type", 256), + gas_price=None, + call_value=None, + origin=None, + call_data_type=None, ): assert isinstance(world_state, WorldState) - + self.id = identifier self.world_state = world_state # TODO: set correct balance for new account self.callee_account = callee_account if callee_account else world_state.create_account(0, concrete_storage=True) self.caller = caller - self.call_data = call_data - self.gas_price = gas_price - self.call_value = call_value + self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price + self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value + self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin + self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type + + self.call_data = call_data self.origin = origin - self.call_data_type = call_data_type self.code = code self.return_data = None From f7ee3e5fe3158d925d141a7e33de6199036904fb Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:14:47 +0200 Subject: [PATCH 09/32] Add unique bitvecval creation to state --- mythril/laser/ethereum/state.py | 5 + solidity_examples/rubixi.sol | 8 +- test.sol | 236 ++++++++++++++++++++++ tests/testdata/input_contracts/rubixi.sol | 4 + 4 files changed, 251 insertions(+), 2 deletions(-) create mode 100644 test.sol diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index e48cd9d5..fe912db0 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -214,6 +214,11 @@ class GlobalState: def instruction(self): return self.get_current_instruction() + def new_bitvec(self, name): + transaction_id = self.current_transaction.id + node_id = self.current_transaction.uid + + return BitVec("{}_{}_{}".format(transaction_id, node_id, name)) class WorldState: """ diff --git a/solidity_examples/rubixi.sol b/solidity_examples/rubixi.sol index 7f593e5e..0a517551 100644 --- a/solidity_examples/rubixi.sol +++ b/solidity_examples/rubixi.sol @@ -30,6 +30,10 @@ contract Rubixi { init(); } + function kill(address addr) onlyowner { + selfdestruct(addr); + } + //init function run on fallback function init() private { //Ensures only tx with value of 1 ether or greater are processed and added to pyramid @@ -45,7 +49,7 @@ contract Rubixi { addPayout(_fee); } - //Function called for valid tx to the contract + //Function called for valid tx to the contract function addPayout(uint _fee) private { //Adds new address to participant array participants.push(Participant(msg.sender, (msg.value * pyramidMultiplier) / 100)); @@ -149,4 +153,4 @@ contract Rubixi { Payout = participants[orderInPyramid].payout / 1 ether; } } -} \ No newline at end of file +} diff --git a/test.sol b/test.sol new file mode 100644 index 00000000..1a99cd7d --- /dev/null +++ b/test.sol @@ -0,0 +1,236 @@ +pragma solidity ^0.4.13; + +library SafeMath { + function mul(uint256 a, uint256 b) internal constant returns (uint256) { + uint256 c = a * b; + assert(a == 0 || c / a == b); + return c; + } + + function div(uint256 a, uint256 b) internal constant returns (uint256) { + // assert(b > 0); // Solidity automatically throws when dividing by 0 + uint256 c = a / b; + // assert(a == b * c + a % b); // There is no case in which this doesn't hold + return c; + } + + function sub(uint256 a, uint256 b) internal constant returns (uint256) { + assert(b <= a); + return a - b; + } + + function add(uint256 a, uint256 b) internal constant returns (uint256) { + uint256 c = a + b; + assert(c >= a); + return c; + } +} + +contract Ownable { + address public owner; + + + /** + * @dev The Ownable constructor sets the original `owner` of the contract to the sender + * account. + */ + function Ownable() { + owner = msg.sender; + } + + + /** + * @dev Throws if called by any account other than the owner. + */ + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + + /** + * @dev Allows the current owner to transfer control of the contract to a newOwner. + * @param newOwner The address to transfer ownership to. + */ + function transferOwnership(address newOwner) onlyOwner { + if (newOwner != address(0)) { + owner = newOwner; + } + } + +} + +contract Destructible is Ownable { + + function Destructible() payable { } + + /** + * @dev Transfers the current balance to the owner and terminates the contract. + */ + function destroy() onlyOwner { + selfdestruct(owner); + } + + function destroyAndSend(address _recipient) onlyOwner { + selfdestruct(_recipient); + } +} + +contract HasNoEther is Ownable { + + /** + * @dev Constructor that rejects incoming Ether + * @dev The `payable` flag is added so we can access `msg.value` without compiler warning. If we + * leave out payable, then Solidity will allow inheriting contracts to implement a payable + * constructor. By doing it this way we prevent a payable constructor from working. Alternatively + * we could use assembly to access msg.value. + */ + function HasNoEther() payable { + require(msg.value == 0); + } + + /** + * @dev Disallows direct send by settings a default function without the `payable` flag. + */ + function() external { + } + + /** + * @dev Transfer all Ether held by the contract to the owner. + */ + function reclaimEther() external onlyOwner { + assert(owner.send(this.balance)); + } +} + +contract HasNoTokens is Ownable { + + /** + * @dev Reject all ERC23 compatible tokens + * @param from_ address The address that is transferring the tokens + * @param value_ uint256 the amount of the specified token + * @param data_ Bytes The data passed from the caller. + */ + function tokenFallback(address from_, uint256 value_, bytes data_) external { + revert(); + } + + /** + * @dev Reclaim all ERC20Basic compatible tokens + * @param tokenAddr address The address of the token contract + */ + function reclaimToken(address tokenAddr) external onlyOwner { + ERC20Basic tokenInst = ERC20Basic(tokenAddr); + uint256 balance = tokenInst.balanceOf(this); + tokenInst.transfer(owner, balance); + } +} + +contract ERC20Basic { + uint256 public totalSupply; + function balanceOf(address who) constant returns (uint256); + function transfer(address to, uint256 value) returns (bool); + event Transfer(address indexed from, address indexed to, uint256 value); +} + +contract BasicToken is ERC20Basic { + using SafeMath for uint256; + + mapping(address => uint256) balances; + + /** + * @dev transfer token for a specified address + * @param _to The address to transfer to. + * @param _value The amount to be transferred. + */ + function transfer(address _to, uint256 _value) returns (bool) { + balances[msg.sender] = balances[msg.sender].sub(_value); + balances[_to] = balances[_to].add(_value); + Transfer(msg.sender, _to, _value); + return true; + } + + /** + * @dev Gets the balance of the specified address. + * @param _owner The address to query the the balance of. + * @return An uint256 representing the amount owned by the passed address. + */ + function balanceOf(address _owner) constant returns (uint256 balance) { + return balances[_owner]; + } + +} + +contract ERC20 is ERC20Basic { + function allowance(address owner, address spender) constant returns (uint256); + function transferFrom(address from, address to, uint256 value) returns (bool); + function approve(address spender, uint256 value) returns (bool); + event Approval(address indexed owner, address indexed spender, uint256 value); +} + +contract StandardToken is ERC20, BasicToken { + + mapping (address => mapping (address => uint256)) allowed; + + + /** + * @dev Transfer tokens from one address to another + * @param _from address The address which you want to send tokens from + * @param _to address The address which you want to transfer to + * @param _value uint256 the amout of tokens to be transfered + */ + function transferFrom(address _from, address _to, uint256 _value) returns (bool) { + var _allowance = allowed[_from][msg.sender]; + + // Check is not needed because sub(_allowance, _value) will already throw if this condition is not met + // require (_value <= _allowance); + + balances[_to] = balances[_to].add(_value); + balances[_from] = balances[_from].sub(_value); + allowed[_from][msg.sender] = _allowance.sub(_value); + Transfer(_from, _to, _value); + return true; + } + + /** + * @dev Aprove the passed address to spend the specified amount of tokens on behalf of msg.sender. + * @param _spender The address which will spend the funds. + * @param _value The amount of tokens to be spent. + */ + function approve(address _spender, uint256 _value) returns (bool) { + + // To change the approve amount you first have to reduce the addresses` + // allowance to zero by calling `approve(_spender, 0)` if it is not + // already 0 to mitigate the race condition described here: + // https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 + require((_value == 0) || (allowed[msg.sender][_spender] == 0)); + + allowed[msg.sender][_spender] = _value; + Approval(msg.sender, _spender, _value); + return true; + } + + /** + * @dev Function to check the amount of tokens that an owner allowed to a spender. + * @param _owner address The address which owns the funds. + * @param _spender address The address which will spend the funds. + * @return A uint256 specifing the amount of tokens still avaible for the spender. + */ + function allowance(address _owner, address _spender) constant returns (uint256 remaining) { + return allowed[_owner][_spender]; + } + +} + +contract WIZE is StandardToken, Ownable, Destructible, HasNoEther, HasNoTokens { + + string public name = "WIZE"; + string public symbol = "WIZE"; + uint256 public decimals = 8; + + function WIZE() { + totalSupply = 100e6 * 10**decimals; + balances[0x14010814F3d6fBDe4970E4f7B36CdfFB23B5FA4A] = totalSupply; + } + +} diff --git a/tests/testdata/input_contracts/rubixi.sol b/tests/testdata/input_contracts/rubixi.sol index 91fda1b6..0a517551 100644 --- a/tests/testdata/input_contracts/rubixi.sol +++ b/tests/testdata/input_contracts/rubixi.sol @@ -30,6 +30,10 @@ contract Rubixi { init(); } + function kill(address addr) onlyowner { + selfdestruct(addr); + } + //init function run on fallback function init() private { //Ensures only tx with value of 1 ether or greater are processed and added to pyramid From 8b61134e8d2ab684da07dabf7aa81534dbe310b1 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:16:54 +0200 Subject: [PATCH 10/32] Don't do unnecessary try catch --- mythril/analysis/modules/suicide.py | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/mythril/analysis/modules/suicide.py b/mythril/analysis/modules/suicide.py index d613a775..53637ffd 100644 --- a/mythril/analysis/modules/suicide.py +++ b/mythril/analysis/modules/suicide.py @@ -53,12 +53,10 @@ def _analyze_state(state, node): not_creator_constraints = [] if len(state.world_state.transaction_sequence) > 1: - try: - creator = state.world_state.transaction_sequence[0].caller - for transaction in state.world_state.transaction_sequence[1:]: - not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))) - except IndexError: - return [] + creator = state.world_state.transaction_sequence[0].caller + for transaction in state.world_state.transaction_sequence[1:]: + not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))) + not_creator_constraints.append(Not(Extract(159, 0, transaction.caller) == 0)) try: model = solver.get_model(node.constraints + not_creator_constraints) From c62067ba300048c9633584b88b10b15d1a465e98 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:23:30 +0200 Subject: [PATCH 11/32] Use node uid vs transaction --- mythril/laser/ethereum/state.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index fe912db0..c9750858 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -214,11 +214,11 @@ class GlobalState: def instruction(self): return self.get_current_instruction() - def new_bitvec(self, name): + def new_bitvec(self, name, size=256): transaction_id = self.current_transaction.id - node_id = self.current_transaction.uid + node_id = self.node.uid - return BitVec("{}_{}_{}".format(transaction_id, node_id, name)) + return BitVec("{}_{}_{}".format(transaction_id, node_id, name), size) class WorldState: """ From bcc90a27f27025538c323ce44862c40d0f9c7502 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:24:00 +0200 Subject: [PATCH 12/32] Use global_state.new_bitvec vs directly initializing the bitvector --- mythril/laser/ethereum/instructions.py | 111 +++++++++++++------------ 1 file changed, 56 insertions(+), 55 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 31fc8aa6..948b72e3 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -4,7 +4,7 @@ from copy import copy, deepcopy import ethereum.opcodes as opcodes from ethereum import utils -from z3 import BitVec, Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \ +from z3 import Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \ is_false, is_expr, ExprRef, URem, SRem from z3 import BitVecVal, If, BoolRef @@ -159,7 +159,7 @@ class Instruction: result = Concat(BitVecVal(0, 248), Extract(offset + 7, offset, op1)) except AttributeError: logging.debug("BYTE: Unsupported symbolic byte offset") - result = BitVec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256) + result = global_state.new_bitvec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256) mstate.stack.append(simplify(result)) return [global_state] @@ -233,7 +233,7 @@ class Instruction: base, exponent = util.pop_bitvec(state), util.pop_bitvec(state) if (type(base) != BitVecNumRef) or (type(exponent) != BitVecNumRef): - state.stack.append(BitVec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256)) + state.stack.append(global_state.new_bitvec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256)) else: state.stack.append(pow(base.as_long(), exponent.as_long(), 2**256)) @@ -340,13 +340,13 @@ class Instruction: b = environment.calldata[offset] except AttributeError: logging.debug("CALLDATALOAD: Unsupported symbolic index") - state.stack.append(BitVec( - "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256)) + state.stack.append(global_state.new_bitvec( + "calldata_" + str(environment.active_account.contract_name) + str(len(global_state.current_transaction.caller)) +"[" + str(simplify(op0)) + "]", 256)) return [global_state] except IndexError: logging.debug("Calldata not set, using symbolic variable instead") - state.stack.append(BitVec( - "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256)) + state.stack.append(global_state.new_bitvec( + "calldata_" + str(environment.active_account.contract_name) +str(global_state.current_transaction.caller)+ "[" + str(simplify(op0)) + "]", 256)) return [global_state] if type(b) == int: @@ -360,11 +360,11 @@ class Instruction: state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256)) # FIXME: broad exception catch except: - state.stack.append(BitVec( + state.stack.append(global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256)) else: # symbolic variable - state.stack.append(BitVec( + state.stack.append(global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256)) return [global_state] @@ -374,7 +374,7 @@ class Instruction: state = global_state.mstate environment = global_state.environment if environment.calldata_type == CalldataType.SYMBOLIC: - state.stack.append(BitVec("calldatasize_" + environment.active_account.contract_name, 256)) + state.stack.append(global_state.new_bitvec("calldatasize_" + environment.active_account.contract_name, 256)) else: state.stack.append(BitVecVal(len(environment.calldata), 256)) return [global_state] @@ -412,7 +412,7 @@ class Instruction: if dstart_sym or size_sym: state.mem_extend(mstart, 1) - state.memory[mstart] = BitVec( + state.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str( size) + "]", 256) return [global_state] @@ -424,7 +424,7 @@ class Instruction: except: logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size)) state.mem_extend(mstart, 1) - state.memory[mstart] = BitVec( + state.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str( size) + "]", 256) return [global_state] @@ -438,7 +438,7 @@ class Instruction: except: logging.debug("Exception copying calldata to memory") - state.memory[mstart] = BitVec( + state.memory[mstart] = global_state.new_bitvec( "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str( size) + "]", 256) return [global_state] @@ -455,7 +455,7 @@ class Instruction: def balance_(self, global_state): state = global_state.mstate address = state.stack.pop() - state.stack.append(BitVec("balance_at_" + str(address), 256)) + state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256)) return [global_state] @instruction @@ -493,7 +493,7 @@ class Instruction: # Can't access symbolic memory offsets if is_expr(op0): op0 = simplify(op0) - state.stack.append(BitVec("KECCAC_mem[" + str(op0) + "]", 256)) + state.stack.append(global_state.new_bitvec("KECCAC_mem[" + str(op0) + "]", 256)) return [global_state] try: @@ -509,7 +509,7 @@ class Instruction: svar = svar.replace(" ", "_") - state.stack.append(BitVec("keccac_" + svar, 256)) + state.stack.append(global_state.new_bitvec("keccac_" + svar, 256)) return [global_state] keccac = utils.sha3(utils.bytearray_to_bytestr(data)) @@ -520,7 +520,7 @@ class Instruction: @instruction def gasprice_(self, global_state): - global_state.mstate.stack.append(BitVec("gasprice", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256)) return [global_state] @instruction @@ -540,7 +540,7 @@ class Instruction: # except both attribute error and Exception global_state.mstate.mem_extend(concrete_memory_offset, 1) global_state.mstate.memory[concrete_memory_offset] = \ - BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) + global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256) return [global_state] try: @@ -550,7 +550,7 @@ class Instruction: global_state.mstate.mem_extend(concrete_memory_offset, concrete_size) for i in range(concrete_size): global_state.mstate.memory[concrete_memory_offset + i] = \ - BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) + global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256) return [global_state] bytecode = global_state.environment.code.bytecode @@ -559,7 +559,7 @@ class Instruction: if concrete_code_offset >= len(global_state.environment.code.bytecode) // 2: global_state.mstate.mem_extend(concrete_memory_offset, 1) global_state.mstate.memory[concrete_memory_offset] = \ - BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) + global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256) return [global_state] for i in range(concrete_size): @@ -568,7 +568,7 @@ class Instruction: int(bytecode[2*(concrete_code_offset + i): 2*(concrete_code_offset + i + 1)], 16) else: global_state.mstate.memory[concrete_memory_offset + i] = \ - BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) + global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256) return [global_state] @@ -581,14 +581,14 @@ class Instruction: addr = hex(helper.get_concrete_int(addr)) except AttributeError: logging.info("unsupported symbolic address for EXTCODESIZE") - state.stack.append(BitVec("extcodesize_" + str(addr), 256)) + state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256)) return [global_state] try: code = self.dynamic_loader.dynld(environment.active_account.address, addr) except Exception as e: logging.info("error accessing contract storage due to: " + str(e)) - state.stack.append(BitVec("extcodesize_" + str(addr), 256)) + state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256)) return [global_state] if code is None: @@ -608,39 +608,39 @@ class Instruction: @instruction def returndatasize_(self, global_state): - global_state.mstate.stack.append(BitVec("returndatasize", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256)) return [global_state] @instruction def blockhash_(self, global_state): state = global_state.mstate blocknumber = state.stack.pop() - state.stack.append(BitVec("blockhash_block_" + str(blocknumber), 256)) + state.stack.append(global_state.new_bitvec("blockhash_block_" + str(blocknumber), 256)) return [global_state] @instruction def coinbase_(self, global_state): - global_state.mstate.stack.append(BitVec("coinbase", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256)) return [global_state] @instruction def timestamp_(self, global_state): - global_state.mstate.stack.append(BitVec("timestamp", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256)) return [global_state] @instruction def number_(self, global_state): - global_state.mstate.stack.append(BitVec("block_number", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256)) return [global_state] @instruction def difficulty_(self, global_state): - global_state.mstate.stack.append(BitVec("block_difficulty", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("block_difficulty", 256)) return [global_state] @instruction def gaslimit_(self, global_state): - global_state.mstate.stack.append(BitVec("block_gaslimit", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256)) return [global_state] # Memory operations @@ -655,14 +655,14 @@ class Instruction: offset = util.get_concrete_int(op0) except AttributeError: logging.debug("Can't MLOAD from symbolic index") - data = BitVec("mem[" + str(simplify(op0)) + "]", 256) + data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256) state.stack.append(data) return [global_state] try: data = util.concrete_int_from_bytes(state.memory, offset) except IndexError: # Memory slot not allocated - data = BitVec("mem[" + str(offset) + "]", 256) + data = global_state.new_bitvec("mem[" + str(offset) + "]", 256) except TypeError: # Symbolic memory data = state.memory[offset] @@ -739,7 +739,7 @@ class Instruction: try: data = global_state.environment.active_account.storage[index] except KeyError: - data = BitVec("storage_" + str(index), 256) + data = global_state.new_bitvec("storage_" + str(index), 256) global_state.environment.active_account.storage[index] = data state.stack.append(data) @@ -762,7 +762,7 @@ class Instruction: global_state.accounts[ global_state.environment.active_account.address] = global_state.environment.active_account - global_state.environment.active_account.storage[index] = value + global_state.environment.active_account.storage[index] = simplify(value) except KeyError: logging.debug("Error writing to storage: Invalid index") return [global_state] @@ -853,12 +853,12 @@ class Instruction: @instruction def msize_(self, global_state): - global_state.mstate.stack.append(BitVec("msize", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("msize", 256)) return [global_state] @instruction def gas_(self, global_state): - global_state.mstate.stack.append(BitVec("gas", 256)) + global_state.mstate.stack.append(global_state.new_bitvec("gas", 256)) return [global_state] @instruction @@ -884,7 +884,7 @@ class Instruction: def return_(self, global_state): state = global_state.mstate offset, length = state.stack.pop(), state.stack.pop() - return_data = [BitVec("return_data", 256)] + return_data = [global_state.new_bitvec("return_data", 256)] try: return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] except AttributeError: @@ -924,9 +924,9 @@ class Instruction: "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) # TODO: decide what to do in this case - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) if 0 < int(callee_address, 16) < 5: logging.info("Native contract called: " + callee_address) @@ -948,7 +948,7 @@ class Instruction: except natives.NativeContractException: contract_list = ['ecerecover', 'sha256', 'ripemd160', 'identity'] for i in range(mem_out_sz): - global_state.mstate.memory[mem_out_start + i] = BitVec(contract_list[call_address_int - 1] + + global_state.mstate.memory[mem_out_start + i] = global_state.new_bitvec(contract_list[call_address_int - 1] + "(" + str(call_data) + ")", 256) return [global_state] @@ -980,12 +980,12 @@ class Instruction: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + 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 = BitVec("retval_" + str(instr['address']), 256) + 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) @@ -995,7 +995,7 @@ class Instruction: memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size except AttributeError: - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] # Copy memory @@ -1004,7 +1004,7 @@ class Instruction: global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i] # Put return value on stack - return_value = BitVec("retval_" + str(instr['address']), 256) + 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) @@ -1022,7 +1022,7 @@ class Instruction: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] transaction = MessageCallTransaction(global_state.world_state, @@ -1048,12 +1048,12 @@ class Instruction: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + 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 = BitVec("retval_" + str(instr['address']), 256) + 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) @@ -1063,7 +1063,7 @@ class Instruction: memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size except AttributeError: - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] # Copy memory @@ -1072,7 +1072,7 @@ class Instruction: global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i] # Put return value on stack - return_value = BitVec("retval_" + str(instr['address']), 256) + 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) @@ -1091,7 +1091,7 @@ class Instruction: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] transaction = MessageCallTransaction(global_state.world_state, @@ -1118,12 +1118,12 @@ class Instruction: logging.info( "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e) ) - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + 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 = BitVec("retval_" + str(instr['address']), 256) + 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) @@ -1135,7 +1135,7 @@ class Instruction: memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size except AttributeError: - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] # Copy memory @@ -1145,7 +1145,7 @@ class Instruction: global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i] # Put return value on stack - return_value = BitVec("retval_" + str(instr['address']), 256) + 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) @@ -1155,5 +1155,6 @@ class Instruction: def staticcall_(self, global_state): # TODO: implement me instr = global_state.get_current_instruction() - global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) return [global_state] + From d37ba5effce3757d6ab669666b485713f98c7f3a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:39:09 +0200 Subject: [PATCH 13/32] Revert changes --- solidity_examples/rubixi.sol | 4 - test.sol | 236 ---------------------- tests/testdata/input_contracts/rubixi.sol | 4 - 3 files changed, 244 deletions(-) delete mode 100644 test.sol diff --git a/solidity_examples/rubixi.sol b/solidity_examples/rubixi.sol index 0a517551..91fda1b6 100644 --- a/solidity_examples/rubixi.sol +++ b/solidity_examples/rubixi.sol @@ -30,10 +30,6 @@ contract Rubixi { init(); } - function kill(address addr) onlyowner { - selfdestruct(addr); - } - //init function run on fallback function init() private { //Ensures only tx with value of 1 ether or greater are processed and added to pyramid diff --git a/test.sol b/test.sol deleted file mode 100644 index 1a99cd7d..00000000 --- a/test.sol +++ /dev/null @@ -1,236 +0,0 @@ -pragma solidity ^0.4.13; - -library SafeMath { - function mul(uint256 a, uint256 b) internal constant returns (uint256) { - uint256 c = a * b; - assert(a == 0 || c / a == b); - return c; - } - - function div(uint256 a, uint256 b) internal constant returns (uint256) { - // assert(b > 0); // Solidity automatically throws when dividing by 0 - uint256 c = a / b; - // assert(a == b * c + a % b); // There is no case in which this doesn't hold - return c; - } - - function sub(uint256 a, uint256 b) internal constant returns (uint256) { - assert(b <= a); - return a - b; - } - - function add(uint256 a, uint256 b) internal constant returns (uint256) { - uint256 c = a + b; - assert(c >= a); - return c; - } -} - -contract Ownable { - address public owner; - - - /** - * @dev The Ownable constructor sets the original `owner` of the contract to the sender - * account. - */ - function Ownable() { - owner = msg.sender; - } - - - /** - * @dev Throws if called by any account other than the owner. - */ - modifier onlyOwner() { - require(msg.sender == owner); - _; - } - - - /** - * @dev Allows the current owner to transfer control of the contract to a newOwner. - * @param newOwner The address to transfer ownership to. - */ - function transferOwnership(address newOwner) onlyOwner { - if (newOwner != address(0)) { - owner = newOwner; - } - } - -} - -contract Destructible is Ownable { - - function Destructible() payable { } - - /** - * @dev Transfers the current balance to the owner and terminates the contract. - */ - function destroy() onlyOwner { - selfdestruct(owner); - } - - function destroyAndSend(address _recipient) onlyOwner { - selfdestruct(_recipient); - } -} - -contract HasNoEther is Ownable { - - /** - * @dev Constructor that rejects incoming Ether - * @dev The `payable` flag is added so we can access `msg.value` without compiler warning. If we - * leave out payable, then Solidity will allow inheriting contracts to implement a payable - * constructor. By doing it this way we prevent a payable constructor from working. Alternatively - * we could use assembly to access msg.value. - */ - function HasNoEther() payable { - require(msg.value == 0); - } - - /** - * @dev Disallows direct send by settings a default function without the `payable` flag. - */ - function() external { - } - - /** - * @dev Transfer all Ether held by the contract to the owner. - */ - function reclaimEther() external onlyOwner { - assert(owner.send(this.balance)); - } -} - -contract HasNoTokens is Ownable { - - /** - * @dev Reject all ERC23 compatible tokens - * @param from_ address The address that is transferring the tokens - * @param value_ uint256 the amount of the specified token - * @param data_ Bytes The data passed from the caller. - */ - function tokenFallback(address from_, uint256 value_, bytes data_) external { - revert(); - } - - /** - * @dev Reclaim all ERC20Basic compatible tokens - * @param tokenAddr address The address of the token contract - */ - function reclaimToken(address tokenAddr) external onlyOwner { - ERC20Basic tokenInst = ERC20Basic(tokenAddr); - uint256 balance = tokenInst.balanceOf(this); - tokenInst.transfer(owner, balance); - } -} - -contract ERC20Basic { - uint256 public totalSupply; - function balanceOf(address who) constant returns (uint256); - function transfer(address to, uint256 value) returns (bool); - event Transfer(address indexed from, address indexed to, uint256 value); -} - -contract BasicToken is ERC20Basic { - using SafeMath for uint256; - - mapping(address => uint256) balances; - - /** - * @dev transfer token for a specified address - * @param _to The address to transfer to. - * @param _value The amount to be transferred. - */ - function transfer(address _to, uint256 _value) returns (bool) { - balances[msg.sender] = balances[msg.sender].sub(_value); - balances[_to] = balances[_to].add(_value); - Transfer(msg.sender, _to, _value); - return true; - } - - /** - * @dev Gets the balance of the specified address. - * @param _owner The address to query the the balance of. - * @return An uint256 representing the amount owned by the passed address. - */ - function balanceOf(address _owner) constant returns (uint256 balance) { - return balances[_owner]; - } - -} - -contract ERC20 is ERC20Basic { - function allowance(address owner, address spender) constant returns (uint256); - function transferFrom(address from, address to, uint256 value) returns (bool); - function approve(address spender, uint256 value) returns (bool); - event Approval(address indexed owner, address indexed spender, uint256 value); -} - -contract StandardToken is ERC20, BasicToken { - - mapping (address => mapping (address => uint256)) allowed; - - - /** - * @dev Transfer tokens from one address to another - * @param _from address The address which you want to send tokens from - * @param _to address The address which you want to transfer to - * @param _value uint256 the amout of tokens to be transfered - */ - function transferFrom(address _from, address _to, uint256 _value) returns (bool) { - var _allowance = allowed[_from][msg.sender]; - - // Check is not needed because sub(_allowance, _value) will already throw if this condition is not met - // require (_value <= _allowance); - - balances[_to] = balances[_to].add(_value); - balances[_from] = balances[_from].sub(_value); - allowed[_from][msg.sender] = _allowance.sub(_value); - Transfer(_from, _to, _value); - return true; - } - - /** - * @dev Aprove the passed address to spend the specified amount of tokens on behalf of msg.sender. - * @param _spender The address which will spend the funds. - * @param _value The amount of tokens to be spent. - */ - function approve(address _spender, uint256 _value) returns (bool) { - - // To change the approve amount you first have to reduce the addresses` - // allowance to zero by calling `approve(_spender, 0)` if it is not - // already 0 to mitigate the race condition described here: - // https://github.com/ethereum/EIPs/issues/20#issuecomment-263524729 - require((_value == 0) || (allowed[msg.sender][_spender] == 0)); - - allowed[msg.sender][_spender] = _value; - Approval(msg.sender, _spender, _value); - return true; - } - - /** - * @dev Function to check the amount of tokens that an owner allowed to a spender. - * @param _owner address The address which owns the funds. - * @param _spender address The address which will spend the funds. - * @return A uint256 specifing the amount of tokens still avaible for the spender. - */ - function allowance(address _owner, address _spender) constant returns (uint256 remaining) { - return allowed[_owner][_spender]; - } - -} - -contract WIZE is StandardToken, Ownable, Destructible, HasNoEther, HasNoTokens { - - string public name = "WIZE"; - string public symbol = "WIZE"; - uint256 public decimals = 8; - - function WIZE() { - totalSupply = 100e6 * 10**decimals; - balances[0x14010814F3d6fBDe4970E4f7B36CdfFB23B5FA4A] = totalSupply; - } - -} diff --git a/tests/testdata/input_contracts/rubixi.sol b/tests/testdata/input_contracts/rubixi.sol index 0a517551..91fda1b6 100644 --- a/tests/testdata/input_contracts/rubixi.sol +++ b/tests/testdata/input_contracts/rubixi.sol @@ -30,10 +30,6 @@ contract Rubixi { init(); } - function kill(address addr) onlyowner { - selfdestruct(addr); - } - //init function run on fallback function init() private { //Ensures only tx with value of 1 ether or greater are processed and added to pyramid From 09f287ea88b9ea67695a94face69ab869daf18e8 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 12:43:03 +0200 Subject: [PATCH 14/32] Small bugfix --- mythril/laser/ethereum/instructions.py | 2 +- mythril/laser/ethereum/transaction/concolic.py | 5 +++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 948b72e3..4edb5de9 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -762,7 +762,7 @@ class Instruction: global_state.accounts[ global_state.environment.active_account.address] = global_state.environment.active_account - global_state.environment.active_account.storage[index] = simplify(value) + global_state.environment.active_account.storage[index] = value except KeyError: logging.debug("Error writing to storage: Invalid index") return [global_state] diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 9fb50c3b..3935a68e 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -4,14 +4,19 @@ from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType +next_transaction_id = 0 + def execute_message_call(laser_evm, callee_address, caller_address, origin_address, code, data, gas, gas_price, value): """ Executes a message call transaction from all open states """ open_states = laser_evm.open_states[:] del laser_evm.open_states[:] + global next_transaction_id for open_world_state in open_states: + next_transaction_id += 1 transaction = MessageCallTransaction( + next_transaction_id, world_state=open_world_state, callee_account=open_world_state[callee_address], caller=caller_address, From 7470297c9ffaa7773006a7f40e75f5ccab684168 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 14:49:41 +0200 Subject: [PATCH 15/32] Use central transaction id and name parameters --- mythril/laser/ethereum/instructions.py | 32 +++++++++---------- .../laser/ethereum/transaction/symbolic.py | 29 ++++++++--------- .../transaction/transaction_models.py | 15 ++++++--- 3 files changed, 40 insertions(+), 36 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 4edb5de9..6216d86c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -962,11 +962,11 @@ class Instruction: transaction = MessageCallTransaction(global_state.world_state, callee_account, BitVecVal(int(environment.active_account.address, 16), 256), - call_data, - environment.gasprice, - value, - environment.origin, - call_data_type) + call_data=call_data, + gas_price=environment.gasprice, + call_value=value, + origin=environment.origin, + call_data_type=call_data_type) raise TransactionStartSignal(transaction, self.op_code) @instruction @@ -1028,12 +1028,12 @@ class Instruction: transaction = MessageCallTransaction(global_state.world_state, environment.active_account, environment.address, - call_data, - environment.gasprice, - value, - environment.origin, - call_data_type, - callee_account.code + call_data=call_data, + gas_price=environment.gasprice, + call_value=value, + origin=environment.origin, + call_data_type=call_data_type, + code=callee_account.code ) raise TransactionStartSignal(transaction, self.op_code) @@ -1098,11 +1098,11 @@ class Instruction: environment.active_account, environment.sender, call_data, - environment.gasprice, - environment.callvalue, - environment.origin, - call_data_type, - callee_account.code + gas_price=environment.gasprice, + call_value=environment.callvalue, + origin=environment.origin, + call_data_type=call_data_type, + code=callee_account.code ) raise TransactionStartSignal(transaction, self.op_code) diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 0b5ba51b..588d7981 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/mythril/laser/ethereum/transaction/symbolic.py @@ -3,29 +3,27 @@ from z3 import BitVec, Extract, Not from mythril.disassembler.disassembly import Disassembly from mythril.laser.ethereum.cfg import Node, Edge, JumpType from mythril.laser.ethereum.state import CalldataType -from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction, get_next_transaction_id -next_transaction_id = 0 def execute_message_call(laser_evm, callee_address): """ Executes a message call transaction from all open states """ - global next_transaction_id open_states = laser_evm.open_states[:] del laser_evm.open_states[:] for open_world_state in open_states: - next_transaction_id += 1 + next_transaction_id = get_next_transaction_id() transaction = MessageCallTransaction( - next_transaction_id, - open_world_state, - open_world_state[callee_address], - BitVec("caller{}".format(next_transaction_id), 256), - [], - BitVec("gas_price{}".format(next_transaction_id), 256), - BitVec("call_value{}".format(next_transaction_id), 256), - BitVec("origin{}".format(next_transaction_id), 256), - CalldataType.SYMBOLIC, + world_state=open_world_state, + callee_account=open_world_state[callee_address], + caller=BitVec("caller{}".format(next_transaction_id), 256), + identifier=next_transaction_id, + call_data=[], + gas_price=BitVec("gas_price{}".format(next_transaction_id), 256), + call_value=BitVec("call_value{}".format(next_transaction_id), 256), + origin=BitVec("origin{}".format(next_transaction_id), 256), + call_data_type=CalldataType.SYMBOLIC, ) _setup_global_state_for_execution(laser_evm, transaction) @@ -34,7 +32,6 @@ def execute_message_call(laser_evm, callee_address): def execute_contract_creation(laser_evm, contract_initialization_code, contract_name=None): """ Executes a contract creation transaction from all open states""" - global next_transaction_id open_states = laser_evm.open_states[:] del laser_evm.open_states[:] @@ -43,11 +40,11 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_ new_account.contract_name = contract_name for open_world_state in open_states: - next_transaction_id += 1 + next_transaction_id = get_next_transaction_id() transaction = ContractCreationTransaction( - next_transaction_id, open_world_state, BitVec("creator{}".format(next_transaction_id), 256), + next_transaction_id, new_account, Disassembly(contract_initialization_code), [], diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 4f1dd329..fa60599d 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/mythril/laser/ethereum/transaction/transaction_models.py @@ -4,6 +4,13 @@ from mythril.laser.ethereum.state import GlobalState, Environment, WorldState from z3 import BitVec import array +_next_transaction_id = 0 + + +def get_next_transaction_id(): + global _next_transaction_id + _next_transaction_id += 1 + return _next_transaction_id class TransactionEndSignal(Exception): """ Exception raised when a transaction is finalized""" @@ -21,11 +28,11 @@ class TransactionStartSignal(Exception): class MessageCallTransaction: """ Transaction object models an transaction""" def __init__(self, - identifier, world_state, callee_account, caller, call_data=(), + identifier=None, gas_price=None, call_value=None, origin=None, @@ -33,7 +40,7 @@ class MessageCallTransaction: code=None ): assert isinstance(world_state, WorldState) - self.id = identifier + self.id = identifier or get_next_transaction_id() self.world_state = world_state self.callee_account = callee_account self.caller = caller @@ -71,9 +78,9 @@ class MessageCallTransaction: class ContractCreationTransaction: """ Transaction object models an transaction""" def __init__(self, - identifier, world_state, caller, + identifier=None, callee_account=None, code=None, call_data=(), @@ -83,7 +90,7 @@ class ContractCreationTransaction: call_data_type=None, ): assert isinstance(world_state, WorldState) - self.id = identifier + self.id = identifier or get_next_transaction_id() self.world_state = world_state # TODO: set correct balance for new account self.callee_account = callee_account if callee_account else world_state.create_account(0, concrete_storage=True) From ae9d7146b12d01cf364bcbdd8970a091689a4a2e Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 28 Aug 2018 14:56:07 +0200 Subject: [PATCH 16/32] Use named parameter --- mythril/laser/ethereum/transaction/concolic.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 3935a68e..4823f252 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/mythril/laser/ethereum/transaction/concolic.py @@ -16,7 +16,7 @@ def execute_message_call(laser_evm, callee_address, caller_address, origin_addre for open_world_state in open_states: next_transaction_id += 1 transaction = MessageCallTransaction( - next_transaction_id, + identifier=next_transaction_id, world_state=open_world_state, callee_account=open_world_state[callee_address], caller=caller_address, From 5eb15a52201e4964c22b0d729f06690c4ec72298 Mon Sep 17 00:00:00 2001 From: Nikhil Parasaram Date: Tue, 28 Aug 2018 21:02:48 +0530 Subject: [PATCH 17/32] Use xml coverage report --- coverage_report.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/coverage_report.sh b/coverage_report.sh index 153f3d58..9f78f84a 100755 --- a/coverage_report.sh +++ b/coverage_report.sh @@ -12,4 +12,5 @@ rm -rf coverage_html_report py.test \ --cov=mythril \ --cov-config=tox.ini \ - --cov-report=html:coverage_html_report \ + --cov-report=html:coverage_reports/coverage_html_report \ + --cov-report=xml:coverage_reports/coverage_xml_report.xml From 62bca80cc914b6131ac8d510bf8cac4e316be7b8 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 31 Aug 2018 00:00:45 +0700 Subject: [PATCH 18/32] Update README.md --- README.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 749175eb..98fc7850 100644 --- a/README.md +++ b/README.md @@ -7,9 +7,11 @@ mythril -Mythril OSS is the classic open-source version of [Mythril](https://mythril.ai), a security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. +Mythril OSS is a classic security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. -**Special Announcement**: The Mythril community is moving to [Discord](https://discord.gg/dFHQGrE). Our Gitter channels and Telegram groups will be closed shortly. Whether you want to contribute, need support, or want to learn what we have cooking for the future, out [Discord server](https://discord.gg/dFHQGrE) will serve your needs! +Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/dFHQGrE) will serve your needs! + +Oh and by the way, we're now building a whole security tools ecosystem with [Mythril Platform API](https://mythril.ai). You should definitely check that out as well. ## Installation and setup From 030d1e100e582605ae948a85222d40a03e6a8be6 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 31 Aug 2018 00:01:12 +0700 Subject: [PATCH 19/32] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 98fc7850..acd896e8 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ mythril -Mythril OSS is a classic security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. +Mythril OSS is the classic security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/dFHQGrE) will serve your needs! From f69a8439dbf71362044c734b558ef990050be7bf Mon Sep 17 00:00:00 2001 From: rocky Date: Fri, 31 Aug 2018 08:19:40 -0400 Subject: [PATCH 20/32] Put issue instructions in comments... so users don't have to delete them. In bug-report.md, put possibly the more likley thing to do at the top. --- .github/ISSUE_TEMPLATE/analysis-module.md | 18 +++++----- .github/ISSUE_TEMPLATE/bug-report.md | 41 ++++++++++++++--------- .github/ISSUE_TEMPLATE/feature-request.md | 11 +++--- 3 files changed, 42 insertions(+), 28 deletions(-) diff --git a/.github/ISSUE_TEMPLATE/analysis-module.md b/.github/ISSUE_TEMPLATE/analysis-module.md index 63f4d240..3eb0eda9 100644 --- a/.github/ISSUE_TEMPLATE/analysis-module.md +++ b/.github/ISSUE_TEMPLATE/analysis-module.md @@ -4,34 +4,34 @@ about: Create an analysis module feature request --- -Please remove any of the optional sections if they are not applicable. + ## Description -Replace this text with a description of an vulnerability that should be -detected by a Mythril analysis module. + ## Tests -_This section is optional._ + ## Implementation details -_This section is optional._ + ## Links -_This section is optional._ + diff --git a/.github/ISSUE_TEMPLATE/bug-report.md b/.github/ISSUE_TEMPLATE/bug-report.md index 67f14f27..cac5714a 100644 --- a/.github/ISSUE_TEMPLATE/bug-report.md +++ b/.github/ISSUE_TEMPLATE/bug-report.md @@ -4,25 +4,20 @@ about: Tell us about Mythril bugs to help us improve --- -_Note: did you notice that there is now a template for requesting new features?_ + ## Description -Replace this text with a clear and concise description of the bug. + ## How to Reproduce -Please show both the input you gave and the -output you got in describing how to reproduce the bug: + + ## Expected behavior -A clear and concise description of what you expected to happen. + ## Screenshots -_This section is optional._ + + ## Environment -_This section sometimes is optional but helpful to us._ + + ## Additional Environment or Context -_This section is optional._ + diff --git a/.github/ISSUE_TEMPLATE/feature-request.md b/.github/ISSUE_TEMPLATE/feature-request.md index b06ae9a4..942b850c 100644 --- a/.github/ISSUE_TEMPLATE/feature-request.md +++ b/.github/ISSUE_TEMPLATE/feature-request.md @@ -6,15 +6,16 @@ about: Tell us about a new feature that would make Mythril better ## Description -Replace this text with a short description of the feature. + ## Background -Replace this text with any additional background for the -feature, for example: user scenarios, or the value of the feature. + ## Tests -_This section is optional._ + + From 50cab170a8f12800e251ed81f79f87632d2af7c2 Mon Sep 17 00:00:00 2001 From: Dominik Muhs Date: Sun, 2 Sep 2018 14:28:37 +0200 Subject: [PATCH 21/32] Remove redundant paragraph tag --- mythril/analysis/templates/callgraph.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/analysis/templates/callgraph.html b/mythril/analysis/templates/callgraph.html index e9b8f933..3536fd48 100644 --- a/mythril/analysis/templates/callgraph.html +++ b/mythril/analysis/templates/callgraph.html @@ -38,7 +38,7 @@

{{ title }}

-


+