From 02aa2952e4336d7c4ebaaca412d84baed8426e79 Mon Sep 17 00:00:00 2001 From: Konrad Weiss Date: Thu, 14 Jun 2018 14:51:20 +0200 Subject: [PATCH] Adding first working transacation application purely working on the stack and not considering the combination of constraints --- mythril/analysis/modules/build_traces.py | 8 +++++ mythril/analysis/modules/dummy.py | 6 ++-- mythril/{ => solidnotary}/solidnotary.py | 4 +-- mythril/solidnotary/transactiontrace.py | 42 +++++++++++++++++++----- 4 files changed, 47 insertions(+), 13 deletions(-) rename mythril/{ => solidnotary}/solidnotary.py (92%) diff --git a/mythril/analysis/modules/build_traces.py b/mythril/analysis/modules/build_traces.py index d20dae21..73a39a07 100644 --- a/mythril/analysis/modules/build_traces.py +++ b/mythril/analysis/modules/build_traces.py @@ -1,4 +1,6 @@ from mythril.analysis.report import Issue +from mythril.solidnotary.transactiontrace import TransactionTrace +from mythril.solidnotary.solidnotary import SolidNotary import logging @@ -19,4 +21,10 @@ def execute(statespace): traces = [] + traces = SolidNotary().get_transaction_traces(statespace) + + print("==== Second level traces ====") + for trace in traces: + print(trace.apply_traces_parallel(traces)) + return [] diff --git a/mythril/analysis/modules/dummy.py b/mythril/analysis/modules/dummy.py index 0d877f85..f795504c 100644 --- a/mythril/analysis/modules/dummy.py +++ b/mythril/analysis/modules/dummy.py @@ -9,7 +9,8 @@ import logging def print_obj(obj): print() print(obj) - # print(dir(obj)) + print(type(obj)) + print(dir(obj)) print() @@ -27,7 +28,8 @@ def execute(statespace): instruction = state.get_current_instruction() if(instruction['opcode'] == "STOP"): - print_obj(state.environment.active_account.storage) + for k,v in state.environment.active_account.storage.items(): + print_obj(v) # print("opc: {}, add: {} {}".format(instruction['opcode'], instruction['address'], instruction['argument'] if 'argument' in instruction else "")) return issues diff --git a/mythril/solidnotary.py b/mythril/solidnotary/solidnotary.py similarity index 92% rename from mythril/solidnotary.py rename to mythril/solidnotary/solidnotary.py index 2207b26f..dd5f0806 100644 --- a/mythril/solidnotary.py +++ b/mythril/solidnotary/solidnotary.py @@ -13,7 +13,7 @@ class SolidNotary: # Todo Find how they are storing results pass - def get_transaction_traces(statespace): + def get_transaction_traces(self, statespace): logging.debug("Executing module: Transaction End") traces = [] @@ -24,4 +24,4 @@ class SolidNotary: instruction = state.get_current_instruction() if instruction['opcode'] == "STOP": traces.append(TransactionTrace(state.environment.active_account.storage)) - return traces + return traces diff --git a/mythril/solidnotary/transactiontrace.py b/mythril/solidnotary/transactiontrace.py index cee4b6de..d2937d66 100644 --- a/mythril/solidnotary/transactiontrace.py +++ b/mythril/solidnotary/transactiontrace.py @@ -1,16 +1,45 @@ +from z3 import * + class TransactionTrace: def __init__(self, storage): self.storage = storage + # Todo the constraints of a trace are probably also important here and have to be somehow aggregated # Todo Identifiy addional trace information such as blocknumber and more + """ + Either do only deep checing here and use the proper trace or storage_slot reduction in the apply function. Or do + both here. + """ + + def deep_equals(trace_lvl1, trace_lvl2): + return set(trace_lvl1) == set(trace_lvl2) # Todo Impelement an ACTUAL deep comparison + + def simplify_storage(self): + for k,v in self.storage.items(): + # Todo explore the arguments of this storage simplification in z3 to find ways to further simplify and to + # sort this expressions for equality comparison + self.storage[k] = simplify(v) + """ Applies the new trace tt on a possibly even changed trace self. """ def apply_trace(self, tt): if tt is None: return self - # Todo implement application of a trace on a existing trace. + subs_map = list(map(lambda x: (BitVec("storage_" + str(x[0]), 256), x[1]), tt.storage.items())) + print("_________") + print(subs_map) + print(self.storage) + print("+++++++++") + for k,v in self.storage.items(): + self.storage[k] = substitute(v, subs_map) + # Todo Add combination of constraints, this might by tricky if we cannot identify which entrancy constraints of + # self can be omitted (e.g. when related storage locations were overwritten) + print(self.storage) + print("=========") + self.simplify_storage() + print(self.storage) return None def apply_traces_parallel(self, traces): @@ -27,7 +56,7 @@ class TransactionTrace: trace_lvl_np1 = [] for trace in trace_lvl_n: trace_lvl_np1.append(trace.apply_traces_parallel(traces)) - if deep_equals(trace_lvl_np1, trace_lvl_n): # Fixpoint detected, function needs to ignore lists, dicts and objects. + if TransactionTrace.deep_equals(trace_lvl_np1, trace_lvl_n): # Fixpoint detected, function needs to ignore lists, dicts and objects. return trace_lvl_n trace_lvl_n = trace_lvl_np1 return trace_lvl_n @@ -40,15 +69,10 @@ class TransactionTrace: trace_lvl_np1.append(trace.apply_traces_parallel(traces)) for trace_lvl_i in traces_up_to: # the following might be faster to check when using a content representing hash - if deep_equals(trace_lvl_np1, trace_lvl_i): # cycle in the traces of trace chains detected: levels + if TransactionTrace.deep_equals(trace_lvl_np1, trace_lvl_i): # cycle in the traces of trace chains detected: levels # while repeat themselves, function needs to ignore lists, dicts and objects. return traces_up_to traces_up_to.append(trace_lvl_np1) return traces_up_to - """ - Either do only deep checing here and use the proper trace or storage_slot reduction in the apply function. Or do - both here. - """ - def deep_equals(trace_lvl1, trace_lvl2): - pass +