diff options
Diffstat (limited to 'miasm2')
| -rw-r--r-- | miasm2/analysis/dse.py | 83 | ||||
| -rw-r--r-- | miasm2/arch/x86/arch.py | 7 | ||||
| -rw-r--r-- | miasm2/arch/x86/sem.py | 44 | ||||
| -rw-r--r-- | miasm2/expression/expression.py | 182 |
4 files changed, 300 insertions, 16 deletions
diff --git a/miasm2/analysis/dse.py b/miasm2/analysis/dse.py index 74cc87e9..d97897d8 100644 --- a/miasm2/analysis/dse.py +++ b/miasm2/analysis/dse.py @@ -26,8 +26,9 @@ On branch, if the decision is symbolic, one can also collect "path constraints" and inverse them to produce new inputs potentially reaching new paths. Basically, this is done through DSEPathConstraint. In order to produce a new -solution, one can extend this class, and override 'handle_solution' to -produce a solution which fit its needs. +solution, one can extend this class, and override 'handle_solution' to produce a +solution which fit its needs. It could avoid computing new solution by +overriding 'produce_solution'. If one is only interested in constraints associated to its path, the option "produce_solution" should be set to False, to speed up emulation. @@ -448,7 +449,8 @@ class DSEPathConstraint(DSEEngine): to a new path. In order to produce a new solution, one can extend this class, and override - 'handle_solution' to produce a solution which fit its needs. + 'handle_solution' to produce a solution which fit its needs. It could avoid + computing new solution by overriding 'produce_solution'. If one is only interested in constraints associated to its path, the option "produce_solution" should be set to False, to speed up emulation. @@ -459,7 +461,15 @@ class DSEPathConstraint(DSEEngine): # Maximum memory size to inject in constraints solving MAX_MEMORY_INJECT = 0x10000 - def __init__(self, machine, produce_solution=True, **kwargs): + # Produce solution strategies + PRODUCE_NO_SOLUTION = 0 + PRODUCE_SOLUTION_CODE_COV = 1 + PRODUCE_SOLUTION_BRANCH_COV = 2 + PRODUCE_SOLUTION_PATH_COV = 3 + + def __init__(self, machine, produce_solution=PRODUCE_SOLUTION_CODE_COV, + known_solutions=None, + **kwargs): """Init a DSEPathConstraint @machine: Machine of the targeted architecture instance @produce_solution: (optional) if set, new solutions will be computed""" @@ -469,10 +479,14 @@ class DSEPathConstraint(DSEEngine): assert z3 is not None # Init PathConstraint specifics structures - self.produce_solution = produce_solution self.cur_solver = z3.Solver() - self.new_solutions = {} # destination -> set of model + self.new_solutions = {} # solution identifier -> solution's model + self._known_solutions = set() # set of solution identifiers self.z3_trans = Translator.to_language("z3") + self._produce_solution_strategy = produce_solution + self._history = None + if produce_solution == self.PRODUCE_SOLUTION_PATH_COV: + self._history = [] # List of addresses in the current path def take_snapshot(self, *args, **kwargs): snap = super(DSEPathConstraint, self).take_snapshot(*args, **kwargs) @@ -481,22 +495,69 @@ class DSEPathConstraint(DSEEngine): snap["cur_constraints"] = self.cur_solver.assertions() return snap - def restore_snapshot(self, snapshot, *args, **kwargs): - super(DSEPathConstraint, self).restore_snapshot(snapshot, *args, - **kwargs) + def restore_snapshot(self, snapshot, keep_known_solutions=True, **kwargs): + """Restore a DSEPathConstraint snapshot + @keep_known_solutions: if set, do not forget solutions already found. + -> They will not appear in 'new_solutions' + """ + super(DSEPathConstraint, self).restore_snapshot(snapshot, **kwargs) self.new_solutions.clear() self.new_solutions.update(snapshot["new_solutions"]) self.cur_solver = z3.Solver() self.cur_solver.add(snapshot["cur_constraints"]) + if not keep_known_solutions: + self._known_solutions.clear() + + def _key_for_solution_strategy(self, destination): + """Return the associated identifier for the current solution strategy""" + if self._produce_solution_strategy == self.PRODUCE_NO_SOLUTION: + # Never produce a solution + return None + elif self._produce_solution_strategy == self.PRODUCE_SOLUTION_CODE_COV: + # Decision based on code coverage + # -> produce a solution if the destination has never been seen + key = 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) + + 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]) + else: + raise ValueError("Unknown produce solution strategy") + + return key + + def produce_solution(self, destination): + """Called to determine if a solution for @destination should be test for + satisfiability and computed + @destination: Expr instance of the target @destination + """ + key = self._key_for_solution_strategy(destination) + if key is None: + return False + return key not in self._known_solutions def handle_solution(self, model, destination): """Called when a new solution for destination @destination is founded @model: z3 model instance @destination: Expr instance for an addr which is not on the DSE path """ - self.new_solutions.setdefault(destination, set()).add(model) + key = self._key_for_solution_strategy(destination) + assert key is not None + self.new_solutions[key] = model + self._known_solutions.add(key) def handle(self, cur_addr): + # Update history if needed + if self._produce_solution_strategy == self.PRODUCE_SOLUTION_PATH_COV: + self._history.append(cur_addr) + symb_pc = self.eval_expr(self.ir_arch.IRDst) possibilities = possible_values(symb_pc) if len(possibilities) == 1: @@ -547,7 +608,7 @@ class DSEPathConstraint(DSEEngine): # Add path constraint cur_path_constraint = path_constraint - elif self.produce_solution: + elif self.produce_solution(possibility.value): # Looking for a new solution self.cur_solver.push() for cons in path_constraint: diff --git a/miasm2/arch/x86/arch.py b/miasm2/arch/x86/arch.py index 73c9fc0d..6725f5bc 100644 --- a/miasm2/arch/x86/arch.py +++ b/miasm2/arch/x86/arch.py @@ -4254,6 +4254,8 @@ addop("pcmpgtd", [bs8(0x0f), bs8(0x66), no_xmm_pref] + addop("pcmpgtd", [bs8(0x0f), bs8(0x66), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) +addop("pcmpeqq", [bs8(0x0f), bs8(0x38), bs8(0x29), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) +addop("pcmpgtq", [bs8(0x0f), bs8(0x38), bs8(0x37), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) addop("punpckhbw", [bs8(0x0f), bs8(0x68), no_xmm_pref] + rmmod(mm_reg, rm_arg_mm)) @@ -4355,6 +4357,11 @@ addop("shufps", [bs8(0x0f), bs8(0xc6), no_xmm_pref] + addop("shufpd", [bs8(0x0f), bs8(0xc6), pref_66] + rmmod(xmm_reg, rm_arg_xmm) + [u08]) +addop("aesenc", [bs8(0x0f), bs8(0x38), bs8(0xdc), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) +addop("aesdec", [bs8(0x0f), bs8(0x38), bs8(0xde), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) + +addop("aesenclast", [bs8(0x0f), bs8(0x38), bs8(0xdd), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) +addop("aesdeclast", [bs8(0x0f), bs8(0x38), bs8(0xdf), pref_66] + rmmod(xmm_reg, rm_arg_xmm)) mn_x86.bintree = factor_one_bit(mn_x86.bintree) # mn_x86.bintree = factor_fields_all(mn_x86.bintree) diff --git a/miasm2/arch/x86/sem.py b/miasm2/arch/x86/sem.py index 1fceab30..5d564fb1 100644 --- a/miasm2/arch/x86/sem.py +++ b/miasm2/arch/x86/sem.py @@ -3819,25 +3819,53 @@ def pminud(ir, instr, dst, src): def pcmpeq(_, instr, dst, src, size): e = [] for i in xrange(0, dst.size, size): - test = dst[i:i + size] - src[i:i + size] + test = m2_expr.expr_is_equal(dst[i:i + size], src[i:i + size]) e.append(m2_expr.ExprAff(dst[i:i + size], m2_expr.ExprCond(test, - m2_expr.ExprInt(0, size), - m2_expr.ExprInt(-1, size)))) + m2_expr.ExprInt(-1, size), + m2_expr.ExprInt(0, size)))) + return e, [] + + +def pcmpgt(_, instr, dst, src, size): + e = [] + for i in xrange(0, dst.size, size): + test = m2_expr.expr_is_signed_greater(dst[i:i + size], src[i:i + size]) + e.append(m2_expr.ExprAff(dst[i:i + size], + m2_expr.ExprCond(test, + m2_expr.ExprInt(-1, size), + m2_expr.ExprInt(0, size)))) return e, [] def pcmpeqb(ir, instr, dst, src): return pcmpeq(ir, instr, dst, src, 8) - def pcmpeqw(ir, instr, dst, src): return pcmpeq(ir, instr, dst, src, 16) - def pcmpeqd(ir, instr, dst, src): return pcmpeq(ir, instr, dst, src, 32) +def pcmpeqq(ir, instr, dst, src): + return pcmpeq(ir, instr, dst, src, 64) + + + + +def pcmpgtb(ir, instr, dst, src): + return pcmpgt(ir, instr, dst, src, 8) + +def pcmpgtw(ir, instr, dst, src): + return pcmpgt(ir, instr, dst, src, 16) + +def pcmpgtd(ir, instr, dst, src): + return pcmpgt(ir, instr, dst, src, 32) + +def pcmpgtq(ir, instr, dst, src): + return pcmpgt(ir, instr, dst, src, 64) + + def punpck(_, instr, dst, src, size, off): e = [] @@ -4504,6 +4532,12 @@ mnemo_func = {'mov': mov, "pcmpeqb": pcmpeqb, "pcmpeqw": pcmpeqw, "pcmpeqd": pcmpeqd, + "pcmpeqq": pcmpeqq, + + "pcmpgtb": pcmpgtb, + "pcmpgtw": pcmpgtw, + "pcmpgtd": pcmpgtd, + "pcmpgtq": pcmpgtq, "punpckhbw": punpckhbw, "punpckhwd": punpckhwd, diff --git a/miasm2/expression/expression.py b/miasm2/expression/expression.py index b7b90470..591dc024 100644 --- a/miasm2/expression/expression.py +++ b/miasm2/expression/expression.py @@ -1538,3 +1538,185 @@ def get_expr_mem(expr): ops = set() expr.visit(lambda x: visit_getmem(x, ops)) return ops + + +def _expr_compute_cf(op1, op2): + """ + Get carry flag of @op1 - @op2 + Ref: x86 cf flag + @op1: Expression + @op2: Expression + """ + res = op1 - op2 + cf = (((op1 ^ op2) ^ res) ^ ((op1 ^ res) & (op1 ^ op2))).msb() + return cf + +def _expr_compute_of(op1, op2): + """ + Get overflow flag of @op1 - @op2 + Ref: x86 of flag + @op1: Expression + @op2: Expression + """ + res = op1 - op2 + of = (((op1 ^ res) & (op1 ^ op2))).msb() + return of + +def _expr_compute_zf(op1, op2): + """ + Get zero flag of @op1 - @op2 + @op1: Expression + @op2: Expression + """ + res = op1 - op2 + zf = ExprCond(res, + ExprInt(0, 1), + ExprInt(1, 1)) + return zf + + +def _expr_compute_nf(op1, op2): + """ + Get negative (or sign) flag of @op1 - @op2 + @op1: Expression + @op2: Expression + """ + res = op1 - op2 + nf = res.msb() + return nf + + +def expr_is_equal(op1, op2): + """ + if op1 == op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + zf = _expr_compute_zf(op1, op2) + return zf + + +def expr_is_not_equal(op1, op2): + """ + if op1 != op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + zf = _expr_compute_zf(op1, op2) + return ~zf + + +def expr_is_unsigned_greater(op1, op2): + """ + UNSIGNED cmp + if op1 > op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + cf = _expr_compute_cf(op1, op2) + zf = _expr_compute_zf(op1, op2) + return ~(cf | zf) + + +def expr_is_unsigned_greater_or_equal(op1, op2): + """ + Unsigned cmp + if op1 >= op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + cf = _expr_compute_cf(op1, op2) + return ~cf + + +def expr_is_unsigned_lower(op1, op2): + """ + Unsigned cmp + if op1 < op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + cf = _expr_compute_cf(op1, op2) + return cf + + +def expr_is_unsigned_lower_or_equal(op1, op2): + """ + Unsigned cmp + if op1 <= op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + cf = _expr_compute_cf(op1, op2) + zf = _expr_compute_zf(op1, op2) + return cf | zf + + +def expr_is_signed_greater(op1, op2): + """ + Signed cmp + if op1 > op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + nf = _expr_compute_nf(op1, op2) + of = _expr_compute_of(op1, op2) + zf = _expr_compute_zf(op1, op2) + return ~(zf | (nf ^ of)) + + +def expr_is_signed_greater_or_equal(op1, op2): + """ + Signed cmp + if op1 > op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + nf = _expr_compute_nf(op1, op2) + of = _expr_compute_of(op1, op2) + return ~(nf ^ of) + + +def expr_is_signed_lower(op1, op2): + """ + Signed cmp + if op1 < op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + nf = _expr_compute_nf(op1, op2) + of = _expr_compute_of(op1, op2) + return nf ^ of + + +def expr_is_signed_lower_or_equal(op1, op2): + """ + Signed cmp + if op1 <= op2: + Return ExprInt(1, 1) + else: + Return ExprInt(0, 1) + """ + + nf = _expr_compute_nf(op1, op2) + of = _expr_compute_of(op1, op2) + zf = _expr_compute_zf(op1, op2) + return zf | (nf ^ of) |