Wednesday, September 23, 2015


The challenge binary is a 64 bit executable. The objective was to login as user blankwall by finding the password. The supplied password is processed using a hash function at 0x00401540. Below is the decompiled code of the function:
uint32_t calc_hash(char *input)
  int counter; 
  uint32_t state; 

  state = 5381;
  for (counter = 0; input[counter]; ++counter)
    state = 33 * state + input[counter];
  return state;
The output of this function must be equal to 0x0D386D209. The length of the password is not known and state variable is 32-bit, hence modulo 0xffffffff. I used Z3 to solve this and multiple solutions are possible. Below is the solver:
#!/usr/bin/env python

from z3 import * 

# >>> (0x1505 * 0x21 * 0x21 * 0x21) < 0xD386D209
# True
# minimum length of password
passlen = 4

def init_solver(passlen):
    s = Solver()
    vectors = {}
    for c in range(passlen):
        vec = BitVec(str(c), 8)
        vectors[c] = vec
        s.add(And(0x20 < vec, vec < 0x7F))
    return s, vectors

while True:
    s, vectors = init_solver(passlen)
    state = 0x1505 
    for i in range(passlen):
        vec = ZeroExt(24, vectors[i])
        state = state * 0x21 + vec
    s.add(state == 0xD386D209)

    if s.check() == sat: break
    passlen += 1

m = s.model()
c = lambda m, i: chr(m[vectors[i]].as_long())
print ''.join([c(m,i) for i in range(passlen)])
This gives the password UIcy1y. Login using the password as
con.write('USER blankwall' + chr(0xa))
password = 'PASS UIcy1y\x00' + chr(0xa)
The file re_solution had the flag, flag{n0_c0ok1e_ju$t_a_f1ag_f0r_you}

No comments :

Post a Comment