Skip to content

Instantly share code, notes, and snippets.

@lieanu

lieanu/solve.py

Created May 14, 2016 10:48
Show Gist options

  • Select an option

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

Select an option

Learn more about clone URLs
Save lieanu/befa86d9978958fdd2927f1846801b8e to your computer and use it in GitHub Desktop.
Download ZIP
Raw
solve.py
#!/usr/bin/env python2
from pwn import *
from z3 import *
flag = ""
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(a[i][j] != 0)
s.add(b[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)
for i in range(6):
for j in range(6):
s.add(0x20 < a[i][j] <= 0x7f)
print s.check()
print s.model()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment