ASIS CTF Quals 2019 Key maker

key_maker.py

#!/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()