1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
import operator
import idaapi
import idc
from miasm2.expression.expression_helper import Variables_Identifier
from utils import expr2colorstr
class symbolicexec_t(idaapi.simplecustviewer_t):
def add(self, key, value):
self.AddLine("%s = %s" % (expr2colorstr(self.machine.mn.regs.all_regs_ids, key),
expr2colorstr(self.machine.mn.regs.all_regs_ids, value)))
def expand(self, linenum):
element = self.line2eq[linenum]
expanded = Variables_Identifier(element[1])
self.line2eq = self.line2eq[0:linenum] + \
expanded.vars.items() + \
[(element[0], expanded.equation)] + \
self.line2eq[linenum + 1:]
def print_lines(self):
self.ClearLines()
for element in self.line2eq:
self.add(*element)
self.Refresh()
def Create(self, equations, machine, *args, **kwargs):
if not super(symbolicexec_t, self).Create(*args, **kwargs):
return False
self.machine = machine
self.line2eq = sorted(equations.items(), key=operator.itemgetter(0))
self.lines_expanded = set()
self.print_lines()
self.menu_expand = self.AddPopupMenu("Expand [E]")
return True
def OnPopupMenu(self, menu_id):
if menu_id == self.menu_expand:
self.expand(self.GetLineNo())
self.print_lines()
return True
def OnKeydown(self, vkey, shift):
# ESCAPE
if vkey == 27:
self.Close()
return True
# E (expand)
if vkey == 69:
self.OnPopupMenu(self.menu_expand)
return False
def symbolic_exec():
from miasm2.analysis.machine import Machine
from miasm2.ir.symbexec import symbexec
from miasm2.core.bin_stream_ida import bin_stream_ida
from utils import guess_machine
bs = bin_stream_ida()
machine = guess_machine()
mdis = machine.dis_engine(bs)
start, end = SelStart(), SelEnd()
mdis.dont_dis = [end]
blocs = mdis.dis_multibloc(start)
ira = machine.ira()
for bloc in blocs:
ira.add_bloc(bloc)
print "Run symbolic execution..."
sb = symbexec(ira, machine.mn.regs.regs_init)
sb.emul_ir_blocs(ira, start)
modified = {}
for ident in sb.symbols.symbols_id:
if ident in sb.ir_arch.arch.regs.regs_init and \
ident in sb.symbols.symbols_id and \
sb.symbols.symbols_id[ident] == sb.ir_arch.arch.regs.regs_init[ident]:
continue
modified[ident] = sb.symbols.symbols_id[ident]
for ident in sb.symbols.symbols_mem:
modified[sb.symbols.symbols_mem[ident][0]] = sb.symbols.symbols_mem[ident][1]
view = symbolicexec_t()
if not view.Create(modified, machine,
"Symbolic Execution - 0x%x to 0x%x" % (start, end)):
return
view.Show()
idaapi.CompileLine('static key_F3() { RunPythonStatement("symbolic_exec()"); }')
idc.AddHotkey("F3", "key_F3")
print "=" * 50
print """Available commands:
symbolic_exec() - F3: Symbolic execution of current selection
"""
|