beginners CTF 2018 crackme

beginners_ctf_2018_crackme_solve_half_z3.py

#!/usr/bin/env python
from z3 import *


def main():
    solver = Solver()

    s = [BitVec('s_%d' % i, 8) for i in range(16)]

    for i in range(len(s)):
        solver.add(s[i] != 0)
        solver.add(0x20 <= s[i], s[i] <= 0x7e)

    val_x = 0xff
    flag_list = [0x9c, 0x9e, 0x8c, 0x3e, 0x68, 0x64, 0x7b, 0x3f, 0x50, 0x63, 0x0a, 0x7f, 0x55, 0x73, 0x1e, 0x64]

    for i in range(4):
        flag1 = s[0 + i * 4] ^ val_x
        solver.add(flag1 == flag_list[0 + i * 4])

        val_x = val_x ^ 0x15
        flag2 = s[1 + i * 4] ^ val_x
        solver.add(flag2 == flag_list[1 + i * 4])

        val_x = val_x | 0x20
        flag3 = s[2 + i * 4] ^ val_x
        solver.add(flag3 == flag_list[2 + i * 4])

        val_x = val_x & 0xf
        flag4 = s[3 + i * 4] ^ val_x
        solver.add(flag4 == flag_list[3 + i * 4])

    if solver.check() == sat:
        m = solver.model()
        print m

        flag = ''
        for i in s:
            flag += chr(m[i].as_long())

        print "\nflag: %s" % flag
    else:
        print "Not found."


if __name__ == '__main__':
    main()