Sunday, 23 December 2018

Friedrich's Christmas Hangover - X-MAS CTF 2018

The binary provided to us in the challenge is an ELF binary however it has an encrypted file header due to which it will not execute. We need to fix the binary header.

So, how do we know that the binary header is encrypted?

We can first run the file command on the binary and we can see that the OS tells us it is a data file and does not recognize it as an ELF file.

$ file chall
chall: data

Next, we check the binary header using hexdump. We notice that the binary header begins with rHAK. We also notice that there are a large number of 0xd bytes in the binary header.

We can now run hexdump on an ELF file and view the first 250 bytes to compare the headers as shown below:

We can quickly confirm that the binary header is encrypted using the byte, 0xd by XOR'ing the first 4 bytes of the file with 0xd and we obtain the bytes {0x7f 0x45 0x4c 0x46} which corresponds to ELF header.

So, to fix the binary, we need to XOR the first 0xc8 bytes of the binary with a single byte key, 0xd.

Once, we have fixed the binary we can run the file command to confirm that it is a 64-bit ELF file.

It also executes properly now.

Let's check the main() subroutine of the binary now:

Quick observations from the main() subroutine:

1. The binary is using the ptrace() anti debugging technique. However, it's important to note that the binary invokes ptrace() two times consecutively. This is done to detect if the return value of ptrace() was patched.
2. Binary expects an input and calculates the length of the input.

Further in the main() subroutine, we observe that the binary is using conditional jump instructions to jump in between the code. This is a common anti disassembly technique. As you can see, IDA did not disassemble the complete code correctly due to this technique:

Let's debug the binary to understand how it processes the input and performs validation.

We can observe from the above screenshot:

1. Calculates the length of the input.
2. Checks if the length is 0x24 bytes.

The screenshot below shows how the input is processed by the binary:


1. There are two loops. An outer loop and an inner loop.
2. In the inner loop, it calculates an offset and use it to read a DWORD from an array (at address: 0x601100).
3. Multiplies the DWORD from step 2 with a byte of the input (at address: 0x602560). The result is added to the total sum.

The screenshot below shows how the sum is validated:

At memory address, 0x601060, there is an array of DWORDs. Each time the outer loop is executed, the sum is compared with the corresponding DWORD from the array at address: 0x601060.


1. Outer loop executes 0x24 times.
2. Each time the outer loop executes, it will compare the calculated sum with a corresponding DWORD from the array at address:  0x601060.

So, we have 0x24 equations which need to be satisfied.

Now, let's have a look at the array at address: 0x601100 which was used to calculate the offsets in the inner loop.

The interesting thing about this array is that it contains 1296 elements as shown below:

1296 = 36 * 36

The calculation of the sum can be represented as shown below:

def gen(input, outer_counter):

    result = 0
    for counter in range(len(input)):
        outer_counter = outer_counter + (outer_counter << 3)
        outer_counter = (outer_counter << 2) + counter
        a = offset[outer_counter]
        b = ord(input[counter])
        result = result + (a * b)
    return result

After analysing the above array more, I observed that it is a collection of 36 arrays. Each of those 36 arrays is used to compute a sum which is later compared by the outer loop.

So, we have:

1. 36 Arrays
2. 36 Sum values calculated using the bytes of input (whose length is also 36 bytes)
3. Each value of Sum is compared with the corresponding DWORD from an array consisting of 36 elements.

We can solve this using Z3 now.

Here is the code to solve it:


No comments:

Post a Comment