From 28ed9d48160ce66d9f77250d5c6db8ff3dfc9641 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Tue, 24 Jul 2018 20:34:53 +0200 Subject: [PATCH 1/8] Implement codecopy concretization and add bytecodearray to environment --- mythril/laser/ethereum/instructions.py | 31 +++++++++++++++++++++++--- mythril/laser/ethereum/state.py | 5 +++++ 2 files changed, 33 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 2db3adf7..c3dff1f2 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -516,9 +516,34 @@ class Instruction: @instruction def codecopy_(self, global_state): - # FIXME: not implemented - state = global_state.mstate - start, s1, size = state.stack.pop(), state.stack.pop(), state.stack.pop() + memory_offset, code_offset, size = global_state.mstate.stack.pop(), global_state.mstate.stack.pop(), global_state.mstate.stack.pop() + + try: + concrete_memory_offset = helper.get_concrete_int(memory_offset) + except: + logging.debug("Unsupported symbolic memory offset in CODECOPY") + return [global_state] + + try: + concrete_size = helper.get_concrete_int(size) + except: + logging.debug("Unsupported symbolic size in CODECOPY") + 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) + return [global_state] + + try: + concrete_code_offset = helper.get_concrete_int(code_offset) + except: + logging.debug("Unsupported symbolic code offset in CODECOPY") + 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) + return [global_state] + + return [global_state] @instruction diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 7cb865b6..1d62c212 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -66,7 +66,11 @@ class Environment: self.active_function_name = "" self.address = BitVecVal(int(active_account.address, 16), 256) + + # Code contains the instruction models self.code = active_account.code + # Bytecode contains the actual bytes + self.bytecode = [] self.sender = sender self.calldata = calldata @@ -75,6 +79,7 @@ class Environment: self.origin = origin self.callvalue = callvalue + def __str__(self): return str(self.as_dict) From b9f5f6644efaa1272d0f89223cff6b0cf50038e1 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 25 Jul 2018 15:15:50 +0200 Subject: [PATCH 2/8] copy over bytecode --- mythril/laser/ethereum/instructions.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index c3dff1f2..63538c80 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -543,6 +543,10 @@ class Instruction: BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) return [global_state] + bytecode = global_state.environment.active_account.code.bytecode + + for i in range(concrete_size): + global_state.mstate.memory[concrete_memory_offset + i] = bytecode[concrete_code_offset + i] return [global_state] From d092064f67b4a8714ce3d6f9842c57b7b3cea825 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 25 Jul 2018 15:22:17 +0200 Subject: [PATCH 3/8] Parse byte and handle out of range code --- mythril/laser/ethereum/instructions.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 63538c80..eba654ca 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -546,7 +546,12 @@ class Instruction: bytecode = global_state.environment.active_account.code.bytecode for i in range(concrete_size): - global_state.mstate.memory[concrete_memory_offset + i] = bytecode[concrete_code_offset + i] + try: + global_state.mstate.memory[concrete_memory_offset + i] =\ + int(bytecode[concrete_code_offset + i: concrete_code_offset + i + 2], 16) + except IndexError: + global_state.mstate.memory[concrete_memory_offset + i] = \ + BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) return [global_state] From 133bc11ec1effd20be908edd5d49e24d29fa7c49 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 25 Jul 2018 15:26:35 +0200 Subject: [PATCH 4/8] Extend memory --- mythril/laser/ethereum/instructions.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index eba654ca..d64ea764 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -520,14 +520,16 @@ class Instruction: try: concrete_memory_offset = helper.get_concrete_int(memory_offset) - except: + except AttributeError: logging.debug("Unsupported symbolic memory offset in CODECOPY") return [global_state] try: concrete_size = helper.get_concrete_int(size) + global_state.mstate.mem_extend(concrete_memory_offset, concrete_size) + except: - logging.debug("Unsupported symbolic size in CODECOPY") + # 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) @@ -535,7 +537,7 @@ class Instruction: try: concrete_code_offset = helper.get_concrete_int(code_offset) - except: + except AttributeError: logging.debug("Unsupported symbolic code offset in CODECOPY") global_state.mstate.mem_extend(concrete_memory_offset, concrete_size) for i in range(concrete_size): From 98e50fb64ac9c9693efc5eb3a880c32b863bdbca Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 25 Jul 2018 15:31:10 +0200 Subject: [PATCH 5/8] Remove space --- 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 d64ea764..ba23241c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -527,7 +527,6 @@ class Instruction: try: concrete_size = helper.get_concrete_int(size) global_state.mstate.mem_extend(concrete_memory_offset, concrete_size) - except: # except both attribute error and Exception global_state.mstate.mem_extend(concrete_memory_offset, 1) From 534e2f7cc086719576105596772909c846e2d93a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 25 Jul 2018 16:06:40 +0200 Subject: [PATCH 6/8] Adds concrete codecopy test --- mythril/laser/ethereum/instructions.py | 2 +- tests/instructions/__init__.py | 0 tests/instructions/codecopy_test.py | 20 ++++++++++++++++++++ 3 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 tests/instructions/__init__.py create mode 100644 tests/instructions/codecopy_test.py diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index ba23241c..8c50219e 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -549,7 +549,7 @@ class Instruction: for i in range(concrete_size): try: global_state.mstate.memory[concrete_memory_offset + i] =\ - int(bytecode[concrete_code_offset + i: concrete_code_offset + i + 2], 16) + int(bytecode[2*(concrete_code_offset + i): 2*(concrete_code_offset + i + 1)], 16) except IndexError: global_state.mstate.memory[concrete_memory_offset + i] = \ BitVec("code({})".format(global_state.environment.active_account.contract_name), 256) diff --git a/tests/instructions/__init__.py b/tests/instructions/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/tests/instructions/codecopy_test.py b/tests/instructions/codecopy_test.py new file mode 100644 index 00000000..53ae049d --- /dev/null +++ b/tests/instructions/codecopy_test.py @@ -0,0 +1,20 @@ +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state import MachineState, GlobalState, Environment, Account +from mythril.laser.ethereum.instructions import Instruction + + +def test_codecopy_concrete(): + # Arrange + active_account = Account("0x0", code= Disassembly("60606040")) + environment = Environment(active_account, None, None, None, None, None) + og_state = GlobalState(None, environment, None, MachineState(gas=10000000)) + + og_state.mstate.stack = [2, 2, 2] + instruction = Instruction("codecopy", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(og_state)[0] + + # Assert + assert new_state.mstate.memory[2] == 96 + assert new_state.mstate.memory[3] == 64 From 15fef84b637b3c52bb39737bd1c78ae0f3a8ad11 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Wed, 25 Jul 2018 16:34:57 +0200 Subject: [PATCH 7/8] remove bytecode array --- mythril/laser/ethereum/state.py | 3 --- 1 file changed, 3 deletions(-) diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index 1d62c212..9b49d8eb 100644 --- a/mythril/laser/ethereum/state.py +++ b/mythril/laser/ethereum/state.py @@ -67,10 +67,7 @@ class Environment: self.address = BitVecVal(int(active_account.address, 16), 256) - # Code contains the instruction models self.code = active_account.code - # Bytecode contains the actual bytes - self.bytecode = [] self.sender = sender self.calldata = calldata From d294692327d514966198b63d0434afecfbbaca5a Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 30 Jul 2018 10:31:38 +0200 Subject: [PATCH 8/8] Sort inputfiles --- tests/report_test.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/report_test.py b/tests/report_test.py index 7f1da181..a5c41f21 100644 --- a/tests/report_test.py +++ b/tests/report_test.py @@ -38,7 +38,7 @@ def _generate_report(input_file): def reports(): """ Fixture that analyses all reports""" pool = Pool(cpu_count()) - input_files = [f for f in TESTDATA_INPUTS.iterdir()] + input_files = sorted([f for f in TESTDATA_INPUTS.iterdir()]) results = pool.map(_generate_report, input_files) return results