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
| from z3 import *
datan=[0x00000008, 0x00000001, 0x00000007, 0x00000001, 0x00000001, 0x00000000, 0x00000004, 0x00000008,
0x00000001, 0x00000002, 0x00000003, 0x00000009, 0x00000003, 0x00000008, 0x00000006, 0x00000006,
0x00000004, 0x00000008, 0x00000003, 0x00000005, 0x00000007, 0x00000008, 0x00000008, 0x00000007,
0x00000000, 0x00000009, 0x00000000, 0x00000002, 0x00000003, 0x00000004, 0x00000002, 0x00000003,
0x00000002, 0x00000005, 0x00000004, 0x00000000]
data=[0x0000007A, 0x000000CF, 0x0000008C, 0x00000095, 0x0000008E, 0x000000A8, 0x0000005F, 0x000000C9,
0x0000007A, 0x00000091, 0x00000088, 0x000000A7, 0x00000070, 0x000000C0, 0x0000007F, 0x00000089,
0x00000086, 0x00000093, 0x0000005F, 0x000000CF, 0x0000006E, 0x00000086, 0x00000085, 0x000000AD,
0x00000088, 0x000000D4, 0x000000A0, 0x000000A2, 0x00000098, 0x000000B3, 0x00000079, 0x000000C1,
0x0000007E, 0x0000007E, 0x00000077, 0x00000093]
data1=[0x00000010, 0x00000008, 0x00000008, 0x0000000E, 0x00000006, 0x0000000B, 0x00000005, 0x00000017,
0x00000005, 0x0000000A, 0x0000000C, 0x00000017, 0x0000000E, 0x00000017, 0x00000013, 0x00000007,
0x00000008, 0x0000000A, 0x00000004, 0x0000000D, 0x00000016, 0x00000011, 0x0000000B, 0x00000016,
0x00000006, 0x0000000E, 0x00000002, 0x0000000B, 0x00000012, 0x00000009, 0x00000005, 0x00000008,
0x00000008, 0x0000000A, 0x00000010, 0x0000000D]
s= Solver()
flag = [BitVec("%d" % i, 8) for i in range(36)]
for i in range(len(flag)):
s.add(flag[i] < 127)
s.add(flag[i] > 32)
ptr = [(i >> 4) for i in flag]
v7 = [(i & 15) for i in flag]
v8 = [0]*36
v9 = [0]*36
for i in range(6):
for j in range(6):
for k in range(6):
v8[6 * i + j] += ptr[6 * i + k] * datan[6 * k + j]
for i in range(6):
for j in range(6):
v9[6 * i + j] = v7[6 * i + j] + datan[6 * i + j]
for i in range(36):
s.add(v8[i] == data[i])
s.add(v9[i] == data1[i])
if s.check() == sat:
model = s.model()
s = []
for i in range(36):
s += chr(model[flag[i]].as_long().real)
print ("".join(s))
else:
print( "别看了没有")
|
