From 09d29b690cebfab06cb0b6cc0d0a615f9eb01227 Mon Sep 17 00:00:00 2001 From: William Bruneau Date: Mon, 9 Oct 2017 14:21:26 +0200 Subject: [PATCH 1/5] Reinitialize _history when restoring snapshot Each time we restore a snapshot we want to restore _history. If not done, each time we use restore_snapshot() we continue appending the new _history to the old one. --- miasm2/analysis/dse.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index d97897d80..7f132c25c 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -493,6 +493,8 @@ def take_snapshot(self, *args, **kwargs): snap["new_solutions"] = {dst: src.copy for dst, src in self.new_solutions.iteritems()} snap["cur_constraints"] = self.cur_solver.assertions() + if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: + snap["_history"] = list(self._history) return snap def restore_snapshot(self, snapshot, keep_known_solutions=True, **kwargs): @@ -507,6 +509,8 @@ def restore_snapshot(self, snapshot, keep_known_solutions=True, **kwargs): self.cur_solver.add(snapshot["cur_constraints"]) if not keep_known_solutions: self._known_solutions.clear() + if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: + self._history = list(snapshot["_history"]) def _key_for_solution_strategy(self, destination): """Return the associated identifier for the current solution strategy""" From c446bdf327ae279b18596c750db45d93618f7269 Mon Sep 17 00:00:00 2001 From: William Bruneau Date: Mon, 9 Oct 2017 14:32:10 +0200 Subject: [PATCH 2/5] Do not use current address to compute path for the new solution When using path coverage strategy we do not want to include the current address in the path that will be reached by the new solution. Indeed, 'destination' is the address that we could have reached instead of the current address using the new solution. --- miasm2/analysis/dse.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index 7f132c25c..4762dd085 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -531,7 +531,10 @@ def _key_for_solution_strategy(self, destination): elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: # Decision based on path coverage # -> produce a solution if the current path has never been take - key = tuple(self._history + [destination]) + # Note: we are taking all steps of the current history but the last + # one ([:-1]) because destination is a step that will replace the + # one we just made. + key = tuple(self._history[:-1] + [destination]) else: raise ValueError("Unknown produce solution strategy") From 76edc6ab9708f07d6423c1eb10e626dfa09faab4 Mon Sep 17 00:00:00 2001 From: William Bruneau Date: Mon, 9 Oct 2017 15:20:55 +0200 Subject: [PATCH 3/5] Compute branches using the previous address 'destination' is the address that we could have reached instead of the current address. Therefore the new branch that can be reach with the new solution is 'previous_addr -> destination'. --- miasm2/analysis/dse.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index 4762dd085..d0f71b5df 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -484,6 +484,7 @@ def __init__(self, machine, produce_solution=PRODUCE_SOLUTION_CODE_COV, self._known_solutions = set() # set of solution identifiers self.z3_trans = Translator.to_language("z3") self._produce_solution_strategy = produce_solution + self._previous_addr = None self._history = None if produce_solution == self.PRODUCE_SOLUTION_PATH_COV: self._history = [] # List of addresses in the current path @@ -495,6 +496,8 @@ def take_snapshot(self, *args, **kwargs): snap["cur_constraints"] = self.cur_solver.assertions() if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: snap["_history"] = list(self._history) + if self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: + snap["_previous_addr"] = self._previous_addr return snap def restore_snapshot(self, snapshot, keep_known_solutions=True, **kwargs): @@ -511,6 +514,8 @@ def restore_snapshot(self, snapshot, keep_known_solutions=True, **kwargs): self._known_solutions.clear() if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: self._history = list(snapshot["_history"]) + if self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: + self._previous_addr = snapshot["_previous_addr"] def _key_for_solution_strategy(self, destination): """Return the associated identifier for the current solution strategy""" @@ -525,8 +530,7 @@ def _key_for_solution_strategy(self, destination): elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: # Decision based on branch coverage # -> produce a solution if the current branch has never been take - cur_addr = ExprInt(self.jitter.pc, self.ir_arch.IRDst.size) - key = (cur_addr, destination) + key = (self._previous_addr, destination) elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: # Decision based on path coverage @@ -632,3 +636,6 @@ def handle(self, cur_addr): # Update current solver for cons in cur_path_constraint: self.cur_solver.add(self.z3_trans.from_expr(cons)) + + if self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: + self._previous_addr = cur_addr From bdea996affba643636aad922d85b63981a72cbd0 Mon Sep 17 00:00:00 2001 From: William Bruneau Date: Mon, 6 Nov 2017 09:06:38 +0100 Subject: [PATCH 4/5] Fix according to @p-l- comment --- miasm2/analysis/dse.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index d0f71b5df..c9b270780 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -496,7 +496,7 @@ def take_snapshot(self, *args, **kwargs): snap["cur_constraints"] = self.cur_solver.assertions() if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: snap["_history"] = list(self._history) - if self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: + elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: snap["_previous_addr"] = self._previous_addr return snap @@ -514,7 +514,7 @@ def restore_snapshot(self, snapshot, keep_known_solutions=True, **kwargs): self._known_solutions.clear() if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: self._history = list(snapshot["_history"]) - if self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: + elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: self._previous_addr = snapshot["_previous_addr"] def _key_for_solution_strategy(self, destination): From b6555f16b4e8ec504ff9d9fb1eed67b386cb1db4 Mon Sep 17 00:00:00 2001 From: William Bruneau Date: Mon, 12 Mar 2018 10:51:47 +0100 Subject: [PATCH 5/5] Add handle_correct_destination() --- miasm2/analysis/dse.py | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index c9b270780..38c9aeafd 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -535,10 +535,7 @@ def _key_for_solution_strategy(self, destination): elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: # Decision based on path coverage # -> produce a solution if the current path has never been take - # Note: we are taking all steps of the current history but the last - # one ([:-1]) because destination is a step that will replace the - # one we just made. - key = tuple(self._history[:-1] + [destination]) + key = tuple(self._history + [destination]) else: raise ValueError("Unknown produce solution strategy") @@ -564,17 +561,28 @@ def handle_solution(self, model, destination): self.new_solutions[key] = model self._known_solutions.add(key) - def handle(self, cur_addr): - # Update history if needed + def handle_correct_destination(self, destination, path_constraints): + """[DEV] Called by handle() to update internal structures giving the + correct destination (the concrete execution one). + """ + + # Update structure used by produce_solution() if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: - self._history.append(cur_addr) + self._history.append(destination) + elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: + self._previous_addr = destination + + # Update current solver + for cons in path_constraints: + self.cur_solver.add(self.z3_trans.from_expr(cons)) + def handle(self, cur_addr): symb_pc = self.eval_expr(self.ir_arch.IRDst) possibilities = possible_values(symb_pc) + cur_path_constraint = set() # path_constraint for the concrete path if len(possibilities) == 1: assert next(iter(possibilities)).value == cur_addr else: - cur_path_constraint = set() # path_constraint for the concrete path for possibility in possibilities: path_constraint = set() # Set of ExprAff for the possible path @@ -633,9 +641,5 @@ def handle(self, cur_addr): self.handle_solution(model, possibility.value) self.cur_solver.pop() - # Update current solver - for cons in cur_path_constraint: - self.cur_solver.add(self.z3_trans.from_expr(cons)) + self.handle_correct_destination(cur_addr, cur_path_constraint) - if self._produce_solution_strategy == self.PRODUCE_SOLUTION_BRANCH_COV: - self._previous_addr = cur_addr