HITCON 2015 risky

result.txt

hitcon{dYauhy0urak9nbavca1m}

solve.py

from z3 import *
from struct import pack

b0 = BitVec("b0", 32)
b1 = BitVec("b1", 32)
b2 = BitVec("b2", 32)
b3 = BitVec("b3", 32)
b4 = BitVec("b4", 32)

s = Solver()

s.add(0x181a9c5f == b2 * b3 + b0 * b1 + b4)
s.add(0x2deacccb == b2 * b0 + b4 + b1)
s.add(0x8e2f6780 == b1 + b0 + b2 + b3 + b4)
s.add(0xb3da7b5f == (b2 + b1 + b4) * (b0 + b3))
s.add(0xe3b0cdef == b2 + b1 + b4)
s.add(0x4978d844 == b0 * b4)
s.add(0x9bcd30de == b1 * b2)
s.add(0x41c7a3a0 == b1 * b2 * b2 * b3 * b4)
s.add(0x313ac784 == b2 * b3)

s.check()

sp_32 = (
    (0x2c281 << 12) + -721,
    (0x38053 << 12) + 1317,
    (0x6b5c3 << 12) + -1500,
    (0x27542 << 12) + 1832,
    (0x29755 << 12) + 1839
)

sp_56 = (b0, b1, b2, b3, b4)
sp_56 = [s.model().eval(v).as_long() for v in sp_56]

flag = 'hitcon{'
flag += pack('<I', sp_32[0] ^ sp_56[0])
flag += pack('<I', sp_32[1] ^ sp_56[1])
flag += pack('<I', sp_32[2] ^ sp_56[2])
flag += pack('<I', sp_32[3] ^ sp_56[3])
flag += pack('<I', sp_32[4] ^ sp_56[4])
flag += '}'

print flag