uitm jasin ctf 2019

bin300_solver.py

from z3 import *
from struct import pack

# define vars
LENGTH = 8
DEBUG = 0
Buf = [BitVec("%i" % i, 16) for i in range(LENGTH)]
solver = Solver()

solver.add(
    Buf[0] == 0xc0c0,
    URem(Buf[1], 0x5050) == 0x140D,
    (Buf[1] ^ Buf[2]) == 0x5A7D,
    (Buf[2] ^ Buf[3]) == 0x2E2F,
    Buf[4] == 0xCEBA,
    (2 * Buf[1]) == 0x695A,
    LShR(Buf[5], 3) == 0x1A1F,
    LShR(Buf[6], LShR(Buf[5] << 8, 14)) == 0x181A,
    DEBUG + Buf[7] == 0xBEDE,
    (Buf[6] ^ Buf[4] ^ Buf[2] ^ Buf[0]) == 0x2079,
    (Buf[7] ^ Buf[5] ^ Buf[3] ^ Buf[1]) == 0x1A76
)

if solver.check() == sat:
    model = solver.model()
    serial = list("a" * LENGTH)
    for name in model:
        serial[int(name.__str__())] = pack('<H', model[name].as_long())
    with open('serial.bin', 'wb') as fp:
        fp.write(b''.join(serial))
else:
    print("unsat")