CTF Writeup - Flare-On 2017 - 11: covfefe.exe

• Name - covfefe.exe
• Category - Reverse Engineering
• Points - 1
• Binary - Download here

The penultimate Flare-On challenge was, in hindsight, my absolute favourite. From the outside, the binary is just a basic command prompt that asks for a password:

Command Prompt

C:\>covfefe.exe Welcome to the magic box. Enter the password: random_stuff You did not guess the password. Consider brute-force guessing using a script, and letting it run for a few trillion years. C:\>

Looking at it under IDA, the binary's code is deceptively simple and doesn't do much. We only have 3 functions with the most important being sub_401000:

bool __cdecl sub_401000(int a1, int a2, int a3, int a4)
{
    bool result; // al@2

    *(_DWORD *)(a1 + 4 * a3) -= *(_DWORD *)(a1 + 4 * a2);
    if ( a4 )
        result = *(_DWORD *)(a1 + 4 * a3) <= 0;
    else
        result = 0;
    return result;
}

The function accepts a start position, a1, and 2 offsets, a2 and a3, and returns True if a1[a2] - a1[a3] is less than or equal to 0, else it returns False. The entire logic of this program is based solely on this instruction. We're hence dealing with a SUBLEQ VM.

For those of you who would like to see an elegant way of solving this challenge, please find another write-up. Here I'll be going through a very basic and manual way of how I solved it. The SUBLEQ VM is too complicated to go through instruction by instruction so, my technique was to put RW breakpoints on the memory region that holds our input and follow any transformations that happen to it. If parts of the input are copied to another memory region, we'll put RW breakpoints on those as well and monitor them.

So, let's get started by supplying the program with 'random' as input. After a few breakpoints we see that our input has been stored in location 0x40313C:

Add a new RW breakpoint to cover the 0x18-byte memory region starting from 0x40313C. After hitting the new breakpoint a few times we find that the first 2 chars of our input were copied to locations 0x406A68 and 0x406A6C respectively:

Put a RW breakpoint on these 2 new locations. Continuing with the execution we encounter the first operation on the first character:

The value 0x72, which is hex for 'r', the first character of our input, has been changed to 0x6AE. In other words, it has been multiplied by 0xF. The resultant value is then squared 7 times, which gives us 0x35700:

The focus now shifts to the 2nd char, which is 'a' in our case. This is copied to location 0x405FC4. At the same time, the value 0x7F is copied to location 0x405FC0. Both these values can be seen in the following screenshot:

By putting a breakpoint on each of these memory regions containing the 2 values we can see them change with each iteration. This part wasn't that straight forward to deduce using my method. After a while the values stop changing and we get the following scenario:

The original values, 0x7F and 0x61, which resided in locations 0x405FC4 and 0x405FC0 respectively, have been modified to show 0xFFFFFFFF. At the same time though, location 0x405FDC contains the value 0x20. This is a simple counter which tells the SUBLEQ VM to stop operating on these 2 values when it reaches 0x20. More importantly though is location 0x405FD0 which contains the value 0x1E. So which operation on values 0x7F and 0x61 gives 0x1E? Well, it's XOR of course.

The SUBLEQ VM now copies the resultant to where the original value was:

So at this point we have values 0x35700 and 0x1E. A few breakpoints later, we can see that the values have been OR'd and the result replaces the first value:

To be honest the operation could have been interpreted as an XOR as it produces the same result. In fact, it doesn't matter if we use OR or XOR, the challenge is still possible with either. Continuing, we encounter this situation:

The value 0x35E8A overwrites the second value. Then, our result, which resides at location 0x406A68, and this new value are subtracted from each other. If we continue execution we notice that the whole process is restarted with the next 2 characters of our input. This strongly suggests that the value 0x35E8A is what our result should have been.

The strategy to completing the challenge is now straight forward: collect all the comparison results and for each, reverse the algorithm to obtain 2 characters of the input each time. First, let us reiterate what the algorithm is for each 2 characters of our input:

1. Multiply the first char by 0xF and square the value 7 times
2. XOR the 2nd character by 0x7F
3. OR the 2 results together
4. Compare the final result to a fixed value

The following script bruteforces each 2 characters from the collected values by reversing the algorithm above:

import string, sys

sols = [0x35E8A,0x2DF13,0x2F58E,0x2C89E,0x3391B,0x2C88D,0x2F59B,0x36D9C,0x36616,0x340A0,0x2D79B,0x2C89E,0x2DF0C,0x36D8D,0x2EE0A,0x331FF]

def try_sol(c1, c2, sol):
    c1 *= 0xF
    for x in range(7):
        c1 += c1
    c2 ^= 0x7F
    c12 = c1 | c2
    if c12 == sol:
        return True
    return False

for sol in sols:
    for c1 in string.printable + '\x00':
        for c2 in string.printable + '\x00':
            if try_sol(ord(c1),ord(c2), sol):
                sys.stdout.write(c1)
                sys.stdout.write(c2)

Running the script:

Command Prompt

C:\>python covfefe_sol.py subleq_and_reductio_ad_absurdum C:\>