Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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)
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}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.