PlaidCTF 2020: reee

Published in

The BKPT

5 min readApr 21, 2020

Alice and I recently participated in PlaidCTF 2020 and solved the challenge reee. You can download the binary here: reee.zip.

You can also view this post on Notion for better code highlighting.

Setup

reee is a reversing challenge / crackme. Run the program with the flag as input, and you're told if you got it right or wrong:

root@4cc0f48f74a2:/ctf/reee# ./reee 'AAAA'
Wrong!

We used Docker on macOS — see here for more on how to effectively use Docker for CTFs.

The flag format is pctf{$FLAG}.

Reverse Engineering

We began by opening the binary in IDA. Our goal was to trace the input to determine how it affects the result. Interestingly, only argc is checked to ensure an argument is supplied — the input buffer isn't touched by main otherwise.

At this point, we ran the program in GDB and located our buffer on the stack, then setting a watchpoint to see which instruction accessed our buffer. This location turns out to be 0x40071a; which, in IDA, appears as a mix of garbage instructions and data. Looking more carefully, we realized that 0x40071a is inside an encrypted function that is decrypted at runtime.

With this context, we can then build a better understanding of main:

int main(int argc, char **argv, char **envp)
{
  int result; // eax
  int byte_offset; // [rsp+18h] [rbp-28h]
  int i_loop; // [rsp+1Ch] [rbp-24h]  if ( argc <= 1 )
    puts("need a flag!");  for ( i_loop = 0; i_loop <= 31336; ++i_loop )
  {
    for ( byte_offset = 0; byte_offset <= 551; ++byte_offset )
      *((_BYTE *)&oracle + byte_offset) = decrypt_byte_of_oracle(*((_BYTE *)&call_me + byte_offset));
  }  if ( ((__int64 (*)(void))oracle)() )
    result = puts("Correct!");
  else
    result = puts("Wrong!");
  return result;
}

Extracting the runtime-decrypted code

We ran the program under GDB and dumped the decrypted function with:

dump binary memory oracle.bin 0x4006E5 0x40090C

oracle was our name for the validation routine. The starting address was determined by looking at where oracle begins. The size of oracle is 551 (decimal). Thus, the end address is start + len.

We then created a new IDA project with oracle.bin. When loading the function, we had to configure the segment offset of 0x4006E5 to preserve the original addresses from reee.bin.

Anti-disassembler techniques

oracle contained anti-disassembler techniques which had to be dealt with.

There were a number of “jump-in-the-middle” instructions, which is a jmp that targeted itself. The jump instruction jumps to the middle of the jmp itself, throwing off linear disassembly. To fix this, nop out the first byte of the jmp
The binary was littered with opaque predicates like:

seg000:0000000000400889 mov eax, 3B4AD836h 
seg000:000000000040088E xor eax, 0F1D7DBEAh 
seg000:0000000000400893 jns short near ptr loc_400816+2

In this case, the xor always results in a signed value, and thus the jump will never be taken. We chose to ignore these. We did not need to tell IDA anything in these cases.

Interestingly, Ghidra’s decompiler dealt far better with these techniques than IDA: it was able to detect and ignore any unreachable code without any manual fixups.

Solving

With the reverse engineering complete, we now have the following pseudocode for the oracle subroutine.

char target[] = {
	0x48, 0x5f, 0x36, 0x35, 
	0x35, 0x25, 0x14, 0x2c,
	0x1d, 0x01, 0x03, 0x2d,
	0x0c, 0x6f, 0x35, 0x61,
	0x7e, 0x34, 0x0a, 0x44,
	0x24, 0x2c, 0x4a, 0x46,
	0x19, 0x59, 0x5b, 0x0e,
	0x78, 0x74, 0x29, 0x13,
	0x2c
};bool do_i_win(char *input_buffer, size_t buffer_len)
{
  // Encrypt user input
  int i;
  int round = 0;
  byte key = 0x50;  while (round < 1337) {
    i = 0;
    while (buffer_index < buffer_length) {
      input_buffer[i] ^= input_buffer[i] ^ key;
      key ^= input_buffer[buffer_index];
      i++
    }
    round++;
  }  // Check user input against fixed target data
  i = 0;
  bool result = false;
  while (i < buffer_len) {
      result = input_buffer[index] == target[index];
      if (!result) {
          break;
      }
    }
    i++;
  }  return result;
}

The initial key is 0x50. The inner loop is like a block cipher mode (sort of like CBC, but not exactly) that operates on single byte blocks. The outer loop applies the inner encryption routine multiple times. The output key of one round of encryption is used as the starting key for the next.

We initially tried to write a decryption function — this works for one round, but falls apart when applying 1337 iterations — because we only know the starting key, not the final one. Additionally, brute forcing is not feasible.

Solving with Z3py

After discussing with a teammate, we decided to use Z3py to solve the problem. We started with simpler test cases that we control. Specifically, we:

Encrypt a known input without any outer loops (one round)
Write z3 code to solve that
Encrypt a known input with multiple rounds
Update z3 code

The solution is below.

#!/usr/bin/env pythonfrom z3 import *
import syssolver = Solver()target_ciphertext = [
    0x48, 0x5f, 0x36, 0x35, 0x35, 0x25, 0x14, 0x2c,
    0x1d, 0x01, 0x03, 0x2d, 0x0c, 0x6f, 0x35, 0x61,
    0x7e, 0x34, 0x0a, 0x44, 0x24, 0x2c, 0x4a, 0x46,
    0x19, 0x59, 0x5b, 0x0e, 0x78, 0x74, 0x29, 0x13,
    0x2c
]target_ciphertext_array = Array('target_ciphertext', BitVecSort(8), BitVecSort(8))
constraints = {}# Define our expected output
plaintext_len = len(target_ciphertext)
for i in xrange(plaintext_len):
    constraints['b%i' % i] = BitVec('b%i' % i, 8)
    # Ensure only ASCII input
    solver.add(constraints['b%i' % i] >= 33)
    solver.add(constraints['b%i' % i] <= 126)# These clauses are redundant with some from line 28, but whatever
solver.add(constraints['b0'] == ord('p'))
solver.add(constraints['b1'] == ord('c'))
solver.add(constraints['b2'] == ord('t'))
solver.add(constraints['b3'] == ord('f'))
solver.add(constraints['b4'] == ord('{'))
solver.add(constraints['b%i' % (plaintext_len - 1)] == ord('}'))for i in range(0, len(target_ciphertext)):
    solver.add(target_ciphertext_array[i] == target_ciphertext[i])# Model the encryption function
key = BitVecVal(0x50, 8)for k in xrange(1337):
    for i in xrange(len(target_ciphertext)):
        constraints['b%i' % i] ^= key
        key ^= constraints['b%i' % i]for i in range(len(target_ciphertext)):
    solver.add(constraints['b%i' % i] == target_ciphertext_array[i])print("Solving...")# Solve the equations
if solver.check():
    modl = solver.model()    sorted_output = {}
    for d in modl.decls():
        name = d.name()
        if name.startswith('b'):
            idx = int(name[1:len(name)])
            sorted_output[idx] = modl[d].as_long()    for k, v in sorted_output.items():
        sys.stdout.write('%s' % chr(v))
    print
else:
    print('unsat')

Let’s try it out…

~/D/c/p/reee ❯❯❯ python solve.py
Solving...
pctf{ok_nothing_too_fancy_there!}

Solved!

root@4cc0f48f74a2:/ctf/reee# ./reee 'pctf{ok_nothing_too_fancy_there!}'
Correct!