Reverse Engineering for Beginners

CHAPTER 77. HAND DECOMPILING + Z3 SMT SOLVER CHAPTER 77. HAND DECOMPILING + Z3 SMT SOLVER

22 m=s.model()
23 print m
24 print (" inp=0x%X" % m[inp].as_long())
25 print ("outp=0x%X" % m[outp].as_long())

Indeed, it finds another correct result:

...>python.exe 2.py

sat

[i1 = 3959740824832824396,

i3 = 8957124831728646493,

i5 = 10816636949158156260,

inp = 10587495961463360371,

outp = 10816636949158156260,

i4 = 14065440378185297801,

i2 = 4954926323707358301]

inp=0x92EE577B63E80B73

outp=0x961C69FF0AEFD7E4

This can be automated. Each found result can be added as a constraint and then the next result will be searched for. Here

is a slightly more sophisticated example:

1 from z3 import
2
3 C1=0x5D7E0D1F2E0F1F84
4 C2=0x388D76AEE8CB1500
5 C3=0xD2E9EE7E83C4285B
6
7 inp, i1, i2, i3, i4, i5, i6, outp = BitVecs('inp i1 i2 i3 i4 i5 i6 outp', 64)
8
9 s = Solver()
10 s.add(i1==inpC1)
11 s.add(i2==RotateRight (i1, i1 & 0xF))
12 s.add(i3==i2 ^ C2)
13 s.add(i4==RotateLeft(i3, i3 & 0xF))
14 s.add(i5==i4 + C3)
15 s.add(outp==RotateLeft (i5, URem(i5, 60)))
16
17 s.add(outp==10816636949158156260)
18
19 # copypasted from http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-⤦
Çequation
20 result=[]
21 while True:
22 if s.check() == sat:
23 m = s.model()
24 print m[inp]
25 result.append(m)
26 # Create a new constraint the blocks the current model
27 block = []
28 for d in m:
29 # d is a declaration
30 if d.arity() > 0:
31 raise Z3Exception("uninterpreted functions are not supported")
32 # create a constant from declaration
33 c=d()
34 if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
35 raise Z3Exception("arrays and uninterpreted sorts are not supported")
36 block.append(c != m[d])
37 s.add(Or(block))
38 else:
39 print "results total=",len(result)
40 break

We got:

1364123924608584563

1234567890

9223372038089343698

4611686019661955794