Skip to content

Instantly share code, notes, and snippets.

@lieanu

lieanu/solve.py

Created May 14, 2016 11:16
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save lieanu/9c9a9395db7e9509cc28352538b03378 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save lieanu/9c9a9395db7e9509cc28352538b03378 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+1, j+1), 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 i in range(6):
for j in range(6):
s.add(And(a[i][j] <= 0x7f, a[i][j] >= 0))
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)
print s.check()
A = s.model()
print A
# print A["a_1_1"]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment