Wednesday, September 23, 2015

CSAW CTF - RE300 - FTP

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
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

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)])
```
```con.write('USER blankwall' + chr(0xa))