maybe-checker [175 Points] (53 Solves)

Your average flag checker with a twist.

Attached is maybe-checker.

---

TL;DR

1. Dump the function decompilation with ida
2. Calculate the offsets into the input
3. Format into a z3 script
4. Profit Submit

Writeup

Opening the attached binary in Ghidra, we find the following main:

seed = time((time_t *)0x0);
srand((uint)seed);
printf("Enter the flag: ");
__isoc99_scanf("%s",str);
rnd = rand();
res = (**(code **)(&DAT_00402041 + ((ulong)(long)rnd % 0x3c) * 9))
              (str + (byte)(&DAT_00402040)[((ulong)(long)rnd % 0x3c) * 9]);
__s = "Wrong flag";
if (res != 0) {
__s = "MAYBE correct flag";
}
puts(__s);
return res ^ 1;

The code takes our flag, then randomly offsets into a an array of functions of length 60 (0x3c). If the function returned 1 (true), then it says our flag is "MAYBE correct".

But first, how does it know what to call?

//    ↓              function address               ↓
//    ↓ the array ↓     ↓         the offset        ↓
res = (&DAT_00402041 + ((ulong)(long)rnd % 0x3c) * 9)(...);

Notice that the offset is multiplied by 9, thus the size of an array element is 9 bytes:

• 8 bytes - the function pointer
• 1 byte - ???

Let's investigate the parameter of the function

//  ↓ our input ↓  ↓       once again offset into the same array      ↓
         str     + (byte)(&DAT_00402040)[((ulong)(long)rnd % 0x3c) * 9]

Because str is a pointer, the value from the array this time will offset the input by some amount.

But wait! Before that, the array was DAT_00402041, in Ghidra this means that its address is at 0x402041. This time it's DAT_00402040!
So 1 byte less than for the function. Thus the array looks like

1 byte - offset for func1
8 byte - address of func1
1 byte - offset for func2
8 byte - address of func2
...
1 byte - offset for func60
8 byte - address of func60

Alright, let's dump this array into something we could work with.

from pwn import u64

BINARY = open("./maybe_checker", "rb").read()

FUNCS_START = 0x2040  # The address the array in the binary
FUNC_COUNT = 0x3c

for arr_idx in range(FUNC_COUNT):
    bin_idx = FUNCS_START + arr_idx * 9

    offset = BINARY[bin_idx]
    addr = BINARY[bin_idx + 1 : bin_idx + 9]

    print(hex(u64(addr)), offset)

And run it

Great! What now?

Ideally, we get the decompilation of each of the functions, and the easiest way to do so, is scripting!
I wrote an IDA script (although it's probably possible with Ghidra too) to do just that:

import idaapi
import ida_hexrays
import idc

func_addresses = [0x401210, ..., 0x401770] # The addresses we dumped


def define_function_at(addr):
    return idaapi.get_func(addr) or not idc.add_func(addr)

assert not ida_hexrays.init_hexrays_plugin(), "init_hexrays_plugin: Failed"

for addr in func_addresses:
    if not define_function_at(addr):
        continue

    try:
        print(ida_hexrays.decompile(addr))
    except ida_hexrays.DecompilationFailure:
        print(f"decompile({addr:#x}): Failed")

ida_hexrays.term_hexrays_plugin()

In the end we get the following:

One annoying thing is that the decompilation has stuff like

(*((_BYTE *)flag + 10)

But we want

flag[10]

for the z3 python script. Luckily, a simple regex like (vim sed (:%s) syntax)

:s/\V*((_BYTE *)flag + \(\d\+\)/flag[\1]

fixes the issue.

Alright, now, all is left is to extract the function content, and add the offset from array to the indexes in the function.

Using a couple of regexes and vim macros I merged all the data we have, into python-syntax array:

[
    flag[0 + 0] == 98,
    flag[1 + 0] == 119,
    flag[2 + 0] == 99,
    # ...
    (flag[10 + 9] ^ flag[27 + 9]) == 12,
    (flag[4 + 6] ^ flag[8 + 6]) == 100,
    flag[21 + 10] + flag[36 + 10] == 150,
]

Btw, looking at the very first function in the array, we see

bool FUN_00401210(char *flag)
{
  return *flag == 'b' && flag[1] == 'w' && flag[2] == 'c' &&
     flag[3] == 't' && flag[4] == 'f' && flag[5] == '{' &&
    flag[47] == '}';
}

And because it checks that flag[47] is }, we know the total length of the flag is 48

So now we can write a z3 script!

from z3 import *

FLAG_LEN = 48
flag = [BitVec("flag_%d" % i, 32) for i in range(FLAG_LEN)] # NOTE: See footnote [1]

conditions = [
    flag[0 + 0] == 98,
    # ...
    flag[21 + 10] + flag[36 + 10] == 150,
]

solver = Solver()
solver.add(conditions)

# Make sure all the characters are ascii characters
for ch in flag:
    solver.add(z3.And(ch >= 32, ch <= 126))

solution_history = set()

while solver.check() == sat:
    model = solver.model()
    result = [chr(model[flag[i]].as_long()) for i in range(FLAG_LEN)]
    result_str = str("".join(result))

    # Skip existing solutions
    if result_str in solution_history: continue

    solution_history.add(result_str)
    print(result_str)

¹

Running the script we get the flag

Success!

Flag: bwctf{WE1C0-M3T0B-1U3W4-T3RCT-FH0P3-Y0UH4-VEFUN}

For the full scripts see dump.py, solve.ida.py and solve.z3.py

Footnotes

1. as SuperFashi (the author of the chal) pointed out after the CTF, the multiplication is done on 32 bit values, not on 8 bit! If we used 8 bit, we would get 4 solutions instead of 1. ↩