WhiteHat GrandPrix 2016 - RE200

Summary: Reverse engineering of a Game Boy ROM and computation of the key with Z3.

Tools:

This is a write-up for the “Com hen” challenge from WhiteHat GrandPrix 2016 CTF.

The provided binary is a Game Boy ROM prompting for a key:

bgb-rom-input

Inputting a wrong key results in this:

bgb-rom-fail

I started by looking at the strings:

rom-strings

This sure looks interesting but there is no xrefs for these strings. However, searching for immediate values leads us to an interesting function with two basic blocks at the end:

rom-strings-loading

Since each of these basic blocks are referencing respectively success and fail strings, we can safely assume that sub_1DDD is used to print strings.

After some renaming and immediate to offset conversions we end up with the following:

rom-success-fail

Let’s see the code path we need to follow to end in the success basic block:

rom-success-code-path

The first check is in the first basic block. In order to get some context, I am putting a breakpoint at 0x5A6 in BGB and provide the following input:

ABCDEFGHIJKLMNOPQRSTUVWXYZ

bgb-debugger-5a6

When the breakpoint triggers, we can see that the code is actually comparing the byte at 0xC0B7 to 0x45, ie, the 24th char of our input must be an ‘E’.

Also, we can see that our input is stored at 0xC0A0 and that there is the following 32 bytes string at 0xC0D2:

3YU8UV86XYZY4W4659756ZUY69582043

Back to our function, the second check depends on the “de” register which is set by sub_86A:

sub_86a

Which is nothing more than a string compare function, loading two strings from the stack and outputting the result in the “de” register.

Now let’s get some context with a breakpoint at 0x86A and the following input (‘E’ at the 24th position in order to pass the first check):

ABCDEFGHIJKLMNOPQRSTUVWEYZ

bgb-debugger-86a

The two compared strings are at 0xC0A0 and 0xC0D2, ie, our input and the mysterious 32 bytes string.

Moreover, our input changed, it is now:

VWXYZABCDEFGHIJKLMNOPQRZTU

Looks like a dumb ROT(21). However, trying to input ROT(-21, “3YU8UV86XYZY4W4659756ZUY69582043”) as key does not work.

I then started to look at sub_4E0 since it is the only function that is called between the first check and the strcmp.

The function is rather long, but after some RE, the algorithm is actually quite simple. Here is the equivalent C code:

// Check if c is a number
short sub_436(unsigned char c)
{
    return c <= '9' && c >= '0';
}

// Get distance between c1 and c2
short sub_40D(unsigned char c1, unsigned char c2)
{
    int ret = c1 - c2;
    return ret >= 0 ? ret : -ret;
}

// Do one hash round
void sub_457(unsigned char* key, unsigned char last, short distance)
{
    for (unsigned char* i = key; *i != 0; ++i) {
        if (sub_436(*i))
            continue;
        *i += distance;
        if (*i > 0x5A)
            *i += 0xE6;
    }
}

// Hash the key
void sub_4E0(unsigned char* key)
{
    unsigned char last = 0x41;
    for (unsigned char* i = key; *i != 0; ++i) {
        if (sub_436(*i))
            continue;
        short distance = sub_40D(last, *i);
        sub_457(key, last, distance);
        last = *i;
    }
}

Thus, the crackme is equivalent to the following C program:

#include <stdio.h>
#include <string.h>

short is_number(unsigned char c)
{
    return c <= '9' && c >= '0';
}

short get_distance(unsigned char c1, unsigned char c2)
{
    int ret = c1 - c2;
    return ret >= 0 ? ret : -ret;
}

void hash_round(unsigned char* key, unsigned char last, short distance)
{
    for (unsigned char* i = key; *i != 0; ++i) {
        if (is_number(*i))
            continue;
        *i += distance;
        if (*i > 0x5A)
            *i += 0xE6;
    }
}

void hash_key(unsigned char* key)
{
    unsigned char last = 0x41;
    for (unsigned char* i = key; *i != 0; ++i) {
        if (is_number(*i))
            continue;
        short distance = get_distance(last, *i);
        hash_round(key, last, distance);
        last = *i;
    }
}

int main(void)
{
    unsigned char key[50];
    gets(key);
    hash_key(key);
    if (!strcmp("3YU8UV86XYZY4W4659756ZUY69582043", key))
        puts("Success");
    else
        puts("Fail");
}

Let’s fire up Z3:

#! /usr/bin/env python2

from z3 import *

def abs(x):
    return If(x >= 0, x, -x)

def adjust(x):
    return If(x <= 0x5A, x, (x + 0xE6) & 0xFF)

def distance(x, y):
    return abs(x - y)

s = Solver()

ref = "3YU8UV86XYZY4W4659756ZUY69582043"
ref = [ord(x) for x in ref]

symvars = [BitVec(str(i), 32) for i in range(32)]
key = list(symvars)

# We only want printable ASCII
for i in range(32):
    s.add(key[i] <= 0x7e)
    s.add(key[i] >= 0x20)

# First condition
s.add(key[23] == ord("E"))

# Numbers are left unmodified
nan_idx = [i for i, j in enumerate(ref) if not "0" <= j <= "9"]

# Hash
last = 0x41
for i in nan_idx:
    d = distance(last, key[i])
    for j in nan_idx:
        key[j] = adjust(key[j] + d)
    last = key[i]

for i in range(32):
    s.add(key[i] == ref[i])

if s.check() == sat:
    m = s.model()
    print("".join([chr(m[x].as_long()) for x in symvars]))
else:
    print("unsat")

And after a couple of minutes we get the following:

3y[8'(86*_zy4]4659756zuE69582043

Which is accepted by the ROM :)

bgb-rom-success