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
| from z3 import *
flag=[BitVec('flag[%d]'%i,32)for i in range(11)]
s=Solver()
b=[0x38, 0x05, 0xC0, 0x2E, 0xB1, 0x80, 0x2D, 0x8D, 0x1E, 0xC9, 0x50]
c=[0xA1, 0x55, 0x58, 0xCE, 0x94, 0x37, 0x8B, 0x9A, 0xB1, 0xEF, 0xAD]
d=[0x19, 0x25, 0x19, 0x99, 0xDC, 0x21, 0x8E, 0x9B, 0xC3, 0x40, 0xB8]
e=[0xE7, 0x1F, 0x37, 0x40, 0xFB, 0x5F, 0x1C, 0x81, 0x07, 0x5D, 0xBC]
f=[0xB5, 0xD4, 0x7B, 0xA1, 0x7C, 0xA0, 0x9C, 0x4C, 0xE8, 0xEF, 0x9C]
g=[0x8A, 0x80, 0xC9, 0xA5, 0xD2, 0x5C, 0x25, 0xBD, 0x44, 0xBD, 0x11]
h=[0x12, 0x97, 0x1F, 0xAB, 0xCD, 0xE9, 0x8C, 0x50, 0x46, 0xD6, 0x10]
i=[0xFA, 0xA2, 0x59, 0x7F, 0xE6, 0x7B, 0x4C, 0x50, 0xF4, 0x99, 0x5E]
j=[0xC5, 0x24, 0xC0, 0x5F, 0x63, 0x4B, 0xE3, 0x70, 0x01, 0x5D, 0x76]
k=[0x45, 0xC6, 0x1D, 0xDD, 0x94, 0x0F, 0xA6, 0x62, 0x2C, 0xB5, 0x38]
s.add(And((flag[0]*0x82+flag[1]*0x23+flag[2]*0x63+flag[3]*0xb8+flag[4]*0x01+flag[5]*0x3C+flag[6]*0x32+flag[7]*0x18+flag[8]*0x1b+flag[9]*0xd1+flag[10]*0xa1==0xC7B5FE04),
(flag[0]*b[0]+flag[1]*b[1]+flag[2]*b[2]+flag[3]*b[3]+flag[4]*b[4]+flag[5]*b[5]+flag[6]*b[6]+flag[7]*b[7]+flag[8]*b[8]+flag[9]*b[9]+flag[10]*b[10]==0xBDFFD372),
(flag[0]*c[0]+flag[1]*c[1]+flag[2]*c[2]+flag[3]*c[3]+flag[4]*c[4]+flag[5]*c[5]+flag[6]*c[6]+flag[7]*c[7]+flag[8]*c[8]+flag[9]*c[9]+flag[10]*c[10]==0x74FCAC49),
(flag[0]*d[0]+flag[1]*d[1]+flag[2]*d[2]+flag[3]*d[3]+flag[4]*d[4]+flag[5]*d[5]+flag[6]*d[6]+flag[7]*d[7]+flag[8]*d[8]+flag[9]*d[9]+flag[10]*d[10]==0x65097B47),
(flag[0]*e[0]+flag[1]*e[1]+flag[2]*e[2]+flag[3]*e[3]+flag[4]*e[4]+flag[5]*e[5]+flag[6]*e[6]+flag[7]*e[7]+flag[8]*e[8]+flag[9]*e[9]+flag[10]*e[10]==0x8106D3B9),
(flag[0]*f[0]+flag[1]*f[1]+flag[2]*f[2]+flag[3]*f[3]+flag[4]*f[4]+flag[5]*f[5]+flag[6]*f[6]+flag[7]*f[7]+flag[8]*f[8]+flag[9]*f[9]+flag[10]*f[10]==0x10CCFFD5),
(flag[0]*g[0]+flag[1]*g[1]+flag[2]*g[2]+flag[3]*g[3]+flag[4]*g[4]+flag[5]*g[5]+flag[6]*g[6]+flag[7]*g[7]+flag[8]*g[8]+flag[9]*g[9]+flag[10]*g[10]==0xFC6964C6),
(flag[0]*h[0]+flag[1]*h[1]+flag[2]*h[2]+flag[3]*h[3]+flag[4]*h[4]+flag[5]*h[5]+flag[6]*h[6]+flag[7]*h[7]+flag[8]*h[8]+flag[9]*h[9]+flag[10]*h[10]==0x65FB0C40),
(flag[0]*i[0]+flag[1]*i[1]+flag[2]*i[2]+flag[3]*i[3]+flag[4]*i[4]+flag[5]*i[5]+flag[6]*i[6]+flag[7]*i[7]+flag[8]*i[8]+flag[9]*i[9]+flag[10]*i[10]==0xC38A2B32),
(flag[0]*j[0]+flag[1]*j[1]+flag[2]*j[2]+flag[3]*j[3]+flag[4]*j[4]+flag[5]*j[5]+flag[6]*j[6]+flag[7]*j[7]+flag[8]*j[8]+flag[9]*j[9]+flag[10]*j[10]==0x3613D94F),
(flag[0]*k[0]+flag[1]*k[1]+flag[2]*k[2]+flag[3]*k[3]+flag[4]*k[4]+flag[5]*k[5]+flag[6]*k[6]+flag[7]*k[7]+flag[8]*k[8]+flag[9]*k[9]+flag[10]*k[10]==0xD7CE6DD2)))
s.add(flag[0]==0x54505542)
if s.check() == sat:
m = s.model()
for i in range(0,11):
if(len(hex(m[flag[i]].as_long())[2:])%2==0):
print hex(m[flag[i]].as_long())[2:].decode('hex')
else:
print hex(m[flag[i]].as_long())[2:-1].decode('hex')
|
