WolvCTF2022 Atari Magic

Problem statement

I don’t remember, sorry.

Binary

We are given a binary that is a TOS file. The magic is 0x601a, which means it is a program for the Atari ST that runs on the TOS operating system. So, I found a Ghidra loader and decided to take a look.

And so it loaded. It even had symbols in it. In order to debug it and understand what was going on I found someone had made a Hatari fork with a debugger, so I decided to give this emulator fork a try. This is a TOS program (or PRG like they seem to be called here), so I you need to have a copy of TOS to run it. For legal reasons, I cannot provide you with a way to get your hands on one other than getting an Atari ST. However, I managed to get the emulator up and running in the end.

Now, I open the so called TOS PRG aaaand…

We even got the magical debugger to attach, perfect! Now, to find the ROM in memory I was lucky hitting CTRL+F in memory tab actually worked. There we go, a perfect match according to Ghidra if we believe the entry point is correct. So, yeah… Entry at 0xf176. I even put a breakpoint there just to test and reopened the program and it seems to stop immediately there and be static.

So, now to rev the code… Hmm… Ghidra is not so happy about plotting the control flow graph…

Compact hierarchical mode already gives us something but there seems to be something peculiar…

There are opaque predicates. But they seem pretty simple though. Like, straight up just constant moves and comparisons. I decided to switch to Binary Ninja (or Binja) nevertheless, because I prefer working with it and I am quite fond of their API for these situations.

So, I grepped the part of the bytes in GEF and did a dump according to both PRG logic implemented in the emulator and what Ghidra mapped in its segment. It was just a hunch but it seemed to match perfectly and if I were doing an incorrect dump I could come back nevertheless. Anyway, I thought I’d probably have enough to be happy in Binja, so I aligned the size with Ghidra’s segment and dumped it.

Perfect, now we just load it in Binary Ninja, map the code at the 0xf176 base and give names to things. We use the m68k plugin to be able to decompile the code.

This is the graph spat out by Binary Ninja. It looks like a bunny. To patch simple opaque predicates, the MLIL representation seems good enough. Binary Ninja lifts the instructions to an internal intermediate representation and it can spit decompilation in low, medium, high level ILs and even more… It’s a really complete tool.

@ 0000f1d8  if (1) then 21 else 23

@ 0000f186  d2 = (0xffff0000 & arg2) | (0xffff & arg2 << 6)
@ 0000f188  jump(&data_f132)

@ 0000f1ec  d6_1 = (0xffff0000 & d6) | (0xffff & __return_addr:2.w)
@ 0000f1ee  call(NewLine, stack = &arg13)
@ 0000f1f4  call(NewLine, stack = &arg13)
@ 0000f1fa  call(NewLine, stack = &arg13)
@ 0000f206  if (true) then 25 else 26 @ 0xf20a

As we can see, Binja can recognize the absurd tautologies with the medium level IL (MLIL) and we know the branch it will take. The official OpaquePredicatePatcher patches opaque predicates and removes the noise. It walks the MLIL and patches accordingly. It’s pretty intuitive to follow because Binja already did the evaluation and lifting behind the scenes.

# All credit goes to Vector35 for this code.

def patch_opaque_inner(bv, status=None):
    patch_locations = []
    for i in bv.mlil_instructions:
        # Allow the UI to cancel the action
        if status is not None and status.cancelled:
            break

        if i.operation != MediumLevelILOperation.MLIL_IF:
            continue
        # Get the possible_values of the condition result
        condition_value = i.condition.possible_values
        # If the condition never changes then its safe to patch the branch
        if condition_value.type == RegisterValueType.ConstantValue:
            if condition_value.value == 0 and bv.is_never_branch_patch_available(i.address):
                patch_locations.append((i.address, True))
            elif bv.is_always_branch_patch_available(i.address):
                patch_locations.append((i.address, False))

    return patch_locations


def patch_opaque(bv, status=None):
    analysis_pass = 0
    while True:
        analysis_pass += 1
        patch_locations = patch_opaque_inner(bv, status)
        if len(patch_locations) == 0 or analysis_pass == 10 or (status is not None and status.cancelled):
            break
        for address, always in patch_locations:
            if always:
                log_info("Patching instruction {} to never branch.".format(hex(address)))
                bv.never_branch(address)
            else:
                log_info("Patching instruction {} to always branch.".format(hex(address)))
                bv.always_branch(address)
        bv.update_analysis_and_wait()

Let’s run it aaaaaaannd…

A snake. It looks easier to rev now. Let’s have a look in high level IL, rename the vars and understand what the code is doing…

Trivial! Our code just reads an input with a TOS read syscall, checks string len and performs assertions char by char. There aren’t even dependencies between the chars. We could even blackbox the binary by scripting something in the emulator if we wanted. Let’s ask Z3 to solve all the equations.

from z3 import *

flag = [BitVec('flag_%d' % i, 8) for i in range(25)]

s = Solver()

s.add((flag[8] - 6) == 0x2a)
s.add((flag[0x11] - 0x77) == 0xbd)
s.add((flag[0x13] ^ 0xba) == 0xde)
s.add(RotateRight(flag[0xa], 7) == 0xd6)
s.add(RotateLeft(flag[0xf], 3) == 0x9b)
s.add((flag[0xc] + 0x62) == 0xdb)
s.add((flag[0x16] - 0x32) == 2)
s.add(RotateLeft(flag[0xb], 3) == 0x99)
s.add((flag[0x10] ^ 0x93) == 0xff)
s.add(RotateRight(flag[0xe], 6) == 0xc4)
s.add((flag[9] ^ 0xb1) == 0xdf)
s.add(RotateLeft(flag[0xd], 2) == 0x7d)
s.add((flag[0x17] + 0x52) == 0xc0)
s.add(RotateRight(flag[7], 5) == 0x6b)
s.add((flag[0xb] - 0x32) == 1)
s.add((flag[0x15] - 0x11) == 0x55)
s.add((flag[0x12] ^ 0x67) == 9)
s.add((flag[0x14] - 0x32) == 0x2d)
s.add(RotateLeft(flag[0x18], 1) == 0xfa)
s.add(RotateRight(flag[0x6], 4) == 0xb7)
s.add((flag[0x3] ^ 0x72) == 0x11)
s.add((flag[5] - 0x36) == 0x30)
s.add((flag[4] + 0x71) == 0xe5)
s.add(RotateRight(flag[2], 5) == 0xbb)

if s.check() == sat:
    m = s.model()
    print(''.join(chr(m[flag[i]].as_long()) for i in range(2, 25)))

And we get the flag: wctf{m0nk3y_1sl4nd_f4n}! Yaaay! I 2nd blooded it back then!

Conclusion

I really think this challenge is a nice introduction to opaque predicates and a fun way to learn reverse. I really really love when the challenges are all retro or about consoles. I hope you enjoyed it as much as I did. See you next time! <3