[Write-up] Free Madame De Maintenon – CTF Challenge

May 25, 2023

Free Madame De Maintenon – CTF Challenge was a linux reverse engineering challenge from HexRays you can read more about here.

The challenge is a GUI application that uses SDL2 as a GUI backend.

Using IDA Free we can decompile its main function, which is pretty straightforward. There are a bunch of checks on an user input that looks like constraints we could provide to z3. If all constraints are satified, we should be granted with a win message.

char user_input[24];
if ( *(unsigned __int16 *)&user_input[16]
       + *(unsigned __int16 *)&user_input[22]
       - *(unsigned __int16 *)&user_input[8]
       - *(unsigned __int16 *)&user_input[14] != 7380 )
    goto error;

if ( *(unsigned __int16 *)&user_input[20]
    + *(unsigned __int16 *)&user_input[6]
    + *(unsigned __int16 *)&user_input[2]
    - *(unsigned __int16 *)&user_input[10] != 55449 )
    goto error;

[...]

if ( (*(_QWORD *)&user_input[16] ^ *(_QWORD *)user_input) != 0xA04233A475D1B72LL )
    goto error;

[...]

if ( *(_DWORD *)&user_input[20]
    + 2 * *(_DWORD *)user_input
    - 4 * *(_DWORD *)&user_input[8]
    - (*(_DWORD *)&user_input[16] >> 3)
    - (*(_DWORD *)&user_input[4] >> 3) != 78988956 )

[...]

if ( (*(_QWORD *)&user_input[8] ^ *(_QWORD *)&user_input[16]) == 0x231F0B21595D0455LL )
    goto win;

Transcribing those constraints to z3 could be tedius, because we are comparing different sizes of integers (WORDS, DWORDS, BYTES, QWORDS…). To solve this, I choosed to have a single BitVec (size 8 * 24) from which I will be extracting specific parts when I need them. This should allow me to extract BYTES, WORDS, DWORDS or QWORDS from wherever I want.

Then we should just keep in mind that bitvec constraints have to be of the same size. This means that if you do this :

from z3 import *

x = BitVec("X", 8)
y = BitVec("Y", 8)

s = Solver()
s.add(x + y == 0x1BB)
print(s)

The resulting constraint from z3 point of vue is :

[X + Y == 187]

As you can see, it did truncate the compared value to the source operands size : it compared X + Y which are 8 bits long to an 8 bit long value : 0xBB.

To avoid that behavior when additioning bits, we can zero extend our operations to larger interger:

from z3 import *

def _toval(val, sz):
    num = val.size()
    if num == sz:
        return val
    return z3.ZeroExt(sz - num, val)

def toword(val):
    return _toval(val, 16)

x = BitVec("ARG1", 8)
y = BitVec("ARG2", 8)

s = Solver()
s.add(toword(x) + toword(y) == 0x1BB)
print(s)

Which results in :

[ARG2 = 192, ARG1 = 251]

Representing constraints with proper type casts give the following script :

from z3 import *


def _toval(val, sz):
    num = val.size()
    if num == sz:
        return val
    return z3.ZeroExt(sz - num, val)


def toqword(val):
    return _toval(val, 64)


def todword(val):
    return _toval(val, 32)


def toword(val):
    return _toval(val, 16)


def tobyte(val):
    return _toval(val, 8)


def extract_bytes(_from, _to, val):
    return Extract(_to * 8 - 1, _from * 8, val)

def bitvec_bytes_between(s, bitvec, size, min, max):
    """Constrains every byte of bitvec

    Args:
        s : z3 solver to add constaints to
        bitvec
        size : BitVec size in bytes
        min : minimal value of each bytes
        max : maximal value of each bytes
    """
    for i in range(size):
        s.add(
            And(
                tobyte(extract_bytes(i, i + 1, p)) >= 0x20,
                tobyte(extract_bytes(i, i + 1, p)) <= 0x7F,
            )
        )


if __name__ == "__main__":
    KEY_SZ = 24
    p = BitVec("ARG", KEY_SZ * 8)
    s = Solver()
    bitvec_bytes_between(s, p, KEY_SZ, 0x20, 0x7F)

    # if ( (*(_QWORD *)&dest[16] ^ *(_QWORD *)dest) != 0xA04233A475D1B72LL )
    s.add(
        toqword(toqword(extract_bytes(0, 8, p)) ^ toqword(extract_bytes(16, 24, p)))
        == 0xA04233A475D1B72
    )

    # if ( (*(_QWORD *)&dest[8] ^ *(_QWORD *)&dest[16]) == 0x231F0B21595D0455LL )
    s.add(
        toqword(toqword(extract_bytes(8, 16, p)) ^ toqword(extract_bytes(16, 24, p)))
        == 0x231F0B21595D0455
    )

    # if ( *(unsigned __int16 *)&dest[16]
    #    + *(unsigned __int16 *)&dest[22]
    #    - *(unsigned __int16 *)&dest[8]
    #    - *(unsigned __int16 *)&dest[14] != 0x1CD4 )
    s.add(
        toword(
            toword(extract_bytes(16, 18, p))
            + toword(extract_bytes(22, 24, p))
            - toword(extract_bytes(8, 10, p))
            - toword(extract_bytes(14, 16, p))
        )
        == 0x1CD4
    )

    # if ( *(unsigned __int16 *)&dest[20]
    #    + *(unsigned __int16 *)&dest[6]
    #    + *(unsigned __int16 *)&dest[2]
    #    - *(unsigned __int16 *)&dest[10] != 0xD899 )
    s.add(
        toword(
            toword(extract_bytes(20, 22, p))
            + toword(extract_bytes(6, 8, p))
            + toword(extract_bytes(2, 4, p))
            - toword(extract_bytes(10, 12, p))
        )
        == 0xD899
    )

    # if ( *(_DWORD *)&dest[20]
    #    + 2 * *(_DWORD *)dest
    #    - 4 * *(_DWORD *)&dest[8]
    #    - (*(_DWORD *)&dest[16] >> 3)
    #    - (*(_DWORD *)&dest[4] >> 3) != 0x4B5469C )
    s.add(
        todword(
            todword(extract_bytes(20, 24, p))
            + 2 * todword(extract_bytes(0, 4, p))
            - 4 * todword(extract_bytes(8, 12, p))
            - (todword(extract_bytes(16, 20, p)) >> 3)
            - (todword(extract_bytes(4, 8, p)) >> 3)
        )
        == 0x4B5469C
    )

    print(s)
    assert s.check() == sat
    hex_result: str = hex(s.model()[p].as_long())[2:]
    print(f'Flag: {bytes.fromhex(result)[::-1]}')

writeup

CTF