Solver for hxphash (rev 250) from TUM CTF 2016
#!/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) | |
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} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment