CSAW CTF 2015 - Reverse 300 - FTP

Breaking a cryptographically weak hash function to generate a valid password and bypass authentication of a FTP server.

Introduction

This writeup is about how we solved the "FTP" Reverse Engineering challenge using Z3 The Theorem Prover.

Context

A custom FTP service is running on the the port 12012 of the target, we have to find a way to bypass the authentication mechanism.

The binary is an ELF 64-bit, with a simple static analysis we find out that to authenticate a user the FTP service compare the username with the string "blankwall" and generate a 32 bits hash for the submitted password, this hash must equal to the value 0xD386D209 to grant access to the FTP commands.

Hash function

Understanding the function responsible for the hash generation is quite simple, here is what the disassembly looks like.

hash proc
input = qword -0x18
index = dword -0x08
check = dword -0x04
    push    rbp
    mov     rbp, rsp
    mov     [rbp + input], rdi
    mov     [rbp + result], 0x1505
    mov     [rbp + index], 0x00
    jmp     loop_start

loop_continue:
    mov     eax, [rbp + result]
    shl     eax, 0x05
    mov     edx, eax
    mov     eax, [rbp + result]
    lea     ecx, [rdx + rax]
    mov     eax, [rbp + index]
    movsxd  rdx, eax
    mov     rax, [rbp + input]
    add     rax, rdx
    movzx   eax, byte [rax]
    movsx   eax, al
    add     eax, ecx
    mov     [rbp + result], eax
    add     [rbp + index], 0x01

loop_start:
    mov     eax, [rbp + index]
    movsxd  rdx, eax
    mov     rax, [rbp + input]
    add     rax, rdx
    movzx   eax, byte [rax]
    test    al, al
    jnz     loop_continue

    mov     eax, [rbp + result]
    pop     rbp
    retn
hash endp

Generating a valid password

Basically what we need to do now is to find a string for which the hash function will generate the value 0xD386D209.
To do so we used Z3 The Theorem Prover, it's an excellent tool for key generation algorithms.

First we have to transcribe the hash algorithm to Python. Note that although this a 64 bit binary we can fit the algorithm of the hash function on 32 bit registers.

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

def display_model(m):
    block = {}
    for x in m:
        if "b" in str(x):
            block[ord(str(x)[-1:])] = int(str(m[x]))

    password = "".join(map(chr, block.values()))
    print password

def get_models(F):
    s = Solver()
    s.add(F)
    while True:
        if s.check() == sat:
            m = s.model()
            display_model(m)
            block = []
            for d in m:
                if d.arity() > 0:
                    raise Z3Exception("uninterpreted functions are not supported")
                c = d()
                if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                    raise Z3Exception("arrays and uninterpreted sorts are not supported")
                block.append(c != m[d])
            s.add(Or(block))
        else:
            break

def is_alphanum(x):
    return Or(And(x >= 0x41, x <= 0x5a), And(x >= 0x61, x <= 0x7a), And(x >= 0x30, x <= 0x39))

def calculate(password):
    ret, ecx, edx = BitVecs("ret ecx edx", 32)
    i = BitVec("i", 8)
    ret = 0x1505

    for i in range(len(password)):
        edx = (ret << 5)
        ecx = (edx + ret)
        ret = (password[i] + ecx)

    return ret

if __name__ == "__main__":
    F = []
    length = 10
    hash = BitVec("hash", 32)
    password = [BitVec("b{0:02d}".format(i), 32) for i in range(length)]

    F.extend([is_alphanum(password[i]) for i in range(length)])
    F.extend([
        hash == 0xD386D209,
        calculate(password) == hash
    ])

    get_models(F)

We decided to generate an alphanumeric string of 10 chars, in a very short amount of time some valid passwords will satisfy our conditions and appear in the terminal.

Getting the flag

Now getting the flag is trivial, a simple netcat command would do the job but it's more explicit in Python.
The script sends the username, the password and the RDF command which order the server to read the file containing the flag.

#!/usr/bin/env python
import sys
import socket

HOST = "54.175.183.202"
PORT = 12012

username = "blankwall"
password = "erh6clKoae"

s = socket.socket(socket.AF_INET, socket.SOCK_STREAM)
s.connect((HOST, PORT))
s.recv(1024)

s.send("USER " + username + "\n")
s.recv(1024)

s.send("PASS " + password)
s.recv(1024)
s.recv(1024)

s.send("RDF")
data = s.recv(1024)
sys.stdout.write(data)

s.close()

Conclusion

Automated theorem proving can be very handful for reverse engineering.
Mixing satisfiability modulo theories and symbolic execution is trending you should look at KLEE a symbolic virtual machine built on top of the LLVM compiler infrastructure.

Unfortunately this year we haven't spent much time participating to the CSAW CTF due to other occupations during the event.
But we couldn't completely ignore this event so we tried a few challenges on our free time.

Share