Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
ASIS CTF Quals 2019 Key maker
#!/usr/bin/env python
from z3 import *
def main():
cmp_to_local_148 = [0x758, 0x2c0, 0x808, 0x306, 0x251, 0x116, 0x2c9, 0x144, 0x5f7, 0x2d5, 0x3d7, 0x298, 0x88a, 0x2bf, 0xa86, 0x347]
cmp_to_local_188 = [0x14f, 0x6e8, 0x6db, 0x69b, 0x3ae, 0x403, 0x3ff, 0x6fd, 0x2f6, 0x515, 0x4fa, 0x6fa, 0x30c, 0x310, 0x26c, 0x540]
cmp_to_local_1c8 = [0x4ab, 0x3d4, 0x47c, 0x56f, 0x58a, 0x4ec, 0x32b, 0x3f1, 0x556, 0x486, 0x3cb, 0x481, 0x42c, 0x2e0, 0x3a4, 0x348]
cmp_to_local_208 = [0x798, 0x3ef, 0x5a0, 0x3d2, 0x4ad, 0x127, 0x585, 0x15e, 0x622, 0x385, 0x53a, 0x382, 0x3ae, 0x2d0, 0x24a, 0x2b1]
cmp_to_local_248 = [0x3ca, 0x5a7, 0x567, 0x8b1, 0x089, 0x48b, 0x538, 0x488, 0x15c, 0x505, 0x533, 0x4fd, 0x120, 0x2ca, 0x291, 0x2df]
cmp_to_local_288 = [0x534, 0x5c0, 0x24c, 0x4b4, 0x1f7, 0x289, 0x06e, 0x199, 0x4af, 0x2d5, 0x375, 0x2b8, 0x671, 0x7f0, 0x180, 0x535]
local_148 = [0] * 16
local_188 = [0] * 16
local_1c8 = [0] * 16
local_208 = [0] * 16
local_248 = [0] * 16
local_288 = [0] * 16
solver = Solver()
keyarray1 = [Int('s_%d' % i) for i in range(16)]
keyarray2 = [Int('t_%d' % i) for i in range(16)]
keyarray3 = [Int('u_%d' % i) for i in range(16)]
for i in range(len(keyarray1)):
solver.add(0 <= keyarray1[i], keyarray1[i] <= 35)
for i in range(len(keyarray2)):
solver.add(0 <= keyarray2[i], keyarray2[i] <= 35)
for i in range(len(keyarray3)):
solver.add(0 <= keyarray3[i], keyarray3[i] <= 35)
FUN_00401530(keyarray1, keyarray2, local_148)
FUN_00401530(keyarray2, keyarray1, local_188)
FUN_00401530(keyarray2, keyarray3, local_1c8)
FUN_00401530(keyarray3, keyarray2, local_208)
FUN_00401530(keyarray3, keyarray1, local_248)
FUN_00401530(keyarray1, keyarray3, local_288)
for i in range(4):
for j in range(4):
solver.add(local_148[j + i * 4] == cmp_to_local_148[j + i * 4])
solver.add(local_188[j + i * 4] == cmp_to_local_188[j + i * 4])
solver.add(local_1c8[j + i * 4] == cmp_to_local_1c8[j + i * 4])
solver.add(local_208[j + i * 4] == cmp_to_local_208[j + i * 4])
solver.add(local_248[j + i * 4] == cmp_to_local_248[j + i * 4])
solver.add(local_288[j + i * 4] == cmp_to_local_288[j + i * 4])
if solver.check() == sat:
m = solver.model()
print m
flag = ''
flag += make_flag(m, keyarray1)
flag += "_"
flag += make_flag(m, keyarray2)
flag += "_"
flag += make_flag(m, keyarray3)
flag = flag[:4] + "{" + flag[5:]
flag = flag[:-1] + "}"
print "\nflag: %s" % flag
else:
print "Not found."
def make_flag(m, arr):
flag = ''
for i in arr:
n = m[i].as_long()
if n >= 0 and n <= 9:
flag += str(n)
elif n >= 10 and n <= 35:
flag += chr(n + 55)
return flag
def FUN_00401530(arr1, arr2, dest):
for i in range(4):
for j in range(4):
for k in range(4):
dest[i * 4 + j] = dest[i * 4 + j] + j + (arr1[i * 4 + k] * arr2[k * 4 + j]) + i
if __name__ == "__main__":
main()
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.