Solver for hxphash (rev 250) from TUM CTF 2016

hxphash_solver.py

#!/usr/bin/env python
#-*- coding:utf-8 -*-

import random, zlib, re
from struct import *
from base64 import *
from commands import getoutput
from sock import *
from z3.z3 import *

def rol(x, n, bits=64):
    n %= bits
    return (x << n) | LShR(x, bits - n)

def ror(x, n, bits=64):
    return rol(x, -n, bits)

sess = random.randint(0, 2**32)
f = Sock("104.197.187.242 2048")
f.send_line("L")
for itr in xrange(100):
    try:
        f.read_until("-------------------------------------------")
    except:
        print f.buf
        quit()
    f.read_line()
    base = f.read_until("---").strip("-").strip()
    binary = zlib.decompress(base.decode("base64"))
    fname = "bins/%08x_%d" % (sess, itr)
    open(fname, "w").write(binary)

    f.read_until("You have")
    f.read_line()

    s = Solver()

    key = [0xDEADBEEF, 0x1337F000, 0x42424242, 0x0C0FFEE]

    reg1 = BitVec("reg1", 64)
    reg2 = BitVec("reg2", 64)
    reg3 = BitVec("reg3", 64)
    reg4 = BitVec("reg4", 64)

    xs = [BitVec("x%d" % i, 64) for i in xrange(4)]
    for x in xs:
        s.add(x >= 0)
        s.add(x <= 2**32-1)
    for r in (reg1, reg2, reg3, reg4):
        s.add(r == 0)

    for x, k in zip(xs, key):
        v10 = x
        v11 = k
        v12 = rol(reg1, 13)
        reg1 = v11 + (v10 ^ v12)
        v13 = ror(reg2, 13)
        reg2 = (v10 ^ v13) - v11
        v11 <<= 32
        v14 = ror(reg3, 19)
        reg3 = v11 + (v10 ^ v14)
        v15 = rol(reg4, 19)
        reg4 = (v15 ^ v10) - v11

    dis = getoutput("objdump -d '%s'" % fname)
    consts = re.findall(r"movabs\s+\$0x(\w+),\%rax", dis)
    consts = [int(c, 16) for c in consts]
    print "#%d" % itr
    print "Targets:",
    for c in consts:
        print hex(c)
    print

    s.add(reg1 == consts[0])
    s.add(reg2 == consts[1])
    s.add(reg3 == consts[2])
    s.add(reg4 == consts[3])

    print "Solving"
    print s.check()
    m = s.model()
    res = ""
    for x in xs:
        x = int(m[x].as_long())
        res += pack("<I", x)

    print res.encode("hex")
    print b64encode(res)
    f.send_line(b64encode(res))

    print "resp:", `f.read_line()`

# hxp{th3y_s4y_pr0gr4m_4n4ly515_15_m4ch1n3_d0m41n_n0w4d4y5}