CSAW Quals 2013 - rev300

#CSAW Quals 2013 - rev300

# The Check algorithm was basically
# check(unsigned char* buf) {
# int v4 = 1337
# while(*buf) {
#   v4 += v4*32+(*buf);
#   ++buf;
# }
# and was used if (check(buf) == 0xEF2E3558) {send(key);}
# so the goal of this challenge was to craft a string with a check() result of 0xFE2E3778.


#!/usr/bin/env python
#Solving rev300 with z3

def int_overflow(val): #simulate signed 32bit integer overflow in python
  max = 2**31-1
  if not -max-1 <= val <= max:
    val = (val + (max + 1)) % (2 * (max + 1)) - max - 1
  return val

def check(s):
    s = 1337
    for c in s:
        s += 32*s+ord(c)
        s = int_overflow(s)
    return s == -0x10d1caa8 #0xEF2E3558 signed

from z3 import *

solver = Solver()
c = BitVec('c', 32)
#unrolled the loop 7 times, should be enough to modify all 32 bits
x_0 = BitVec('x_0', 32)
c_1 = c+c*32+x_0
x_1 = BitVec('x_1', 32)
c_2 = c_1+c_1*32+x_1
x_2 = BitVec('x_2', 32)
c_3 = c_2+c_2*32+x_2
x_3 = BitVec('x_3', 32)
c_4 = c_3+c_3*32+x_3
x_4 = BitVec('x_4', 32)
c_5 = c_4+c_4*32+x_4
x_5 = BitVec('x_5', 32)
c_6 = c_5+c_5*32+x_5
x_6 = BitVec('x_6', 32)
c_7 = c_6+c_6*32+x_6

solver.add(c == 1337)
solver.add(c_7 == 0xEF2E3558)
for x in [x_0, x_1, x_2, x_3, x_4, x_5, x_6]:
    solver.add(x & 0xFFFFFF00 == 0)
    solver.add(x != 0)
solver.check()
m = solver.model()
print m

s = ''
for x in [x_0, x_1, x_2, x_3, x_4, x_5, x_6]:
    print m[x]
    s += chr(int(str(m[x])))

print repr(s), check(s)

#running this gave me the string '\t\x8b\xff\x89\x9eq\xf4' which i then submitted using this script:

#!/usr/bin/env python
from pwn import *

s='\t\x8b\xff\x89\x9eq\xf4\n'
r = remote("128.238.66.218", 54321)
print r.recv()
r.send(s)
print r.recv()
print r.recv()
print r.recv()