Instantly share code, notes, and snippets.

Embed
What would you like to do?
#!/usr/bin/env python
from z3 import *
import string
solver = z3.Solver()
for x in range(0,5):
for y in range(0,5):
varname = "mat_%i_%i" % (x,y)
globals()[varname] = BitVec(varname,32)
solver.add(globals()[varname] >= 0x20)
solver.add(globals()[varname] <= 0xF0)
def check(x):
for i in range(0,25):
m = (i * 2) % 25
f = (i * 7) % 25
vname = "mat_%i_%i" % (m / 5, m % 5)
if f == x:
return vname
print check(4)
print check(5)
# import sys
# sys.exit(0)
# mat_0_0
# mat_2_1
# mat_4_2
# mat_1_3
solver.add(mat_0_0 == BitVecVal(ord('T'),32))
solver.add(mat_2_1 == BitVecVal(ord('U'),32))
solver.add(mat_4_2 == BitVecVal(ord('C'),32))
solver.add(mat_1_3 == BitVecVal(ord('T'),32))
solver.add(mat_3_4 == BitVecVal(ord('F'),32))
solver.add(mat_1_0 == BitVecVal(ord('{'),32))
solver.add(mat_0_0 + mat_4_4 == BitVecVal(0x8b,32))
solver.add(mat_2_1 + mat_0_2 == BitVecVal(0xce,32))
solver.add(mat_4_2 + mat_4_1 == BitVecVal(0xb0,32))
solver.add(mat_1_3 + mat_3_1 == BitVecVal(0x89,32))
solver.add(mat_3_4 + mat_1_2 == BitVecVal(0x7b,32))
solver.add(mat_1_0 + mat_2_3 == BitVecVal(0xb0,32))
solver.add(mat_2_4 + mat_2_0 == BitVecVal(0xb0,32))
solver.add(mat_3_3 + mat_3_2 + mat_0_3 == BitVecVal(0xee,32))
solver.add(mat_0_4 + mat_4_0 + mat_0_1 == BitVecVal(0xbf,32))
solver.add(mat_3_3 + mat_2_0 == BitVecVal(0x92,32))
solver.add(mat_4_0 + mat_1_2 == BitVecVal(0x65,32))
solver.add(mat_0_4 + mat_4_1 == BitVecVal(0x9d,32))
solver.add(mat_0_3 + mat_0_2 == BitVecVal(0x9a,32))
solver.add(mat_3_0 + mat_2_0 == BitVecVal(0x99,32))
solver.add(mat_1_4 + mat_1_2 == BitVecVal(0x99,32))
solver.add(mat_4_3 + mat_2_3 == BitVecVal(0x94,32))
solver.add(mat_2_2 + mat_0_2 == BitVecVal(0xad,32))
solver.add(mat_1_1 + mat_4_1 == BitVecVal(0xe4,32))
print solver.check()
n = solver.model()
print n
soln_array = {}
for d in n.decls():
print "%s = %s" % (d.name(),n[d])
soln_array[d.name()] = n[d]
out = ""
for i in range(0,25):
vn = check(i)
out += chr(int(str(soln_array[vn])))
print out
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment