Skip to content

Instantly share code, notes, and snippets.

@lieanu

lieanu/solve.py

Created May 14, 2016 12:00
Show Gist options
  • Save lieanu/0bc8fcf5f15e9ebd2f73646e8945fef5 to your computer and use it in GitHub Desktop.
Save lieanu/0bc8fcf5f15e9ebd2f73646e8945fef5 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
solve.py
#!/usr/bin/env python2
from pwn import *
from z3 import *
fd = open("./Crackme_6.exe", "rb")
data = fd.read()[0x1400:0x1490]
d = []
for x in range(0, 0x90, 4):
d.append(u32(data[x:x+4]))
print d
s = Solver()
a = [ [ BitVec("a_%s_%s" % (i, j), 8) for j in range(6) ]
for i in range(6) ]
b = [ [ 0 for j in range(6) ]
for i in range(6) ]
for i in range(6):
for j in range(6):
b[j][i] = a[i][j]
c = [ [ 0 for j in range(6) ]
for i in range(6) ]
for i in range(6):
for j in range(6):
for k in range(6):
c[i][j] += a[i][k]*b[k][j]
for k in range(27):
j = k%6
i = k/6
s.add(And(a[i][j] < 0x7f, a[i][j] >= 47))
for i in range(6):
for j in range(6):
s.add(c[i][j] == d[i*6+j])
for k in range(27, 36):
j = k%6
i = k/6
s.add(a[i][j]==1)
s.add(a[0][0] == ord("w"))
s.add(a[0][1] == ord("h"))
s.add(a[0][2] == ord("c"))
s.add(a[0][3] == ord("t"))
s.add(a[0][4] == ord("f"))
s.add(a[0][5] == ord("{"))
print s.check()
A = s.model()
print A
# print A["a_1_1"]
A ={
"a_4_1" : 104,
"a_2_4" : 48,
"a_3_5" : 52,
"a_1_2" : 117,
"a_2_0" : 51,
"a_2_3" : 48,
"a_1_1" : 48,
"a_2_5" : 100,
"a_2_1" : 95,
"a_1_3" : 95,
"a_3_2" : 55,
"a_3_3" : 95,
"a_3_4" : 109,
"a_1_0" : 89,
"a_4_0" : 116,
"a_2_2" : 103,
"a_3_1" : 97,
"a_1_5" : 114,
"a_1_4" : 97,
"a_3_0" : 95,
"a_4_2" : 125,
"a_0_5" : 123,
"a_0_4" : 102,
"a_0_3" : 116,
"a_0_2" : 99,
"a_0_1" : 104,
"a_0_0" : 119,
"a_5_5" : 1,
"a_5_4" : 1,
"a_5_3" : 1,
"a_5_2" : 1,
"a_5_1" : 1,
"a_5_0" : 1,
"a_4_5" : 1,
"a_4_4" : 1,
"a_4_3" : 1}
res = []
for i in range(6):
for j in range(6):
res.append(A["a_%s_%s"%(i, j)])
print "".join(chr(x) for x in res)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment