Rusty Rev 1 - Hacker's Odyssey CTF

Link to archived challenge

Description

This one seems a bit trickier than the last.

Good news though: I received word of a new form of black magic called “symbolic execution” - supposedly it can extract flags from even the trickiest of binaries!

Have fun!

Players are given two files to download: flag-checker and flag-checker-arm64.

There are also three hints available:

1. angr should prove useful.
2. Your script should not take more than a minute to find the solution.
3. If you know C, try testing your script out on a proof-of-concept C binary to better understand what’s happening.
   If you don’t know C, you can find practice examples online (with source code) for the same purpose.

Note: I will use the x86-64 flag-checker binary in this writeup, but my analysis and solution are valid for both binaries.

Analysis

The first few steps are very similar to Rusty Rev 0.
(these steps tend to be common across binary reverse engineering challenges)

In summary:

• We have a 64-bit dynamically-linked executable, including a symbol table.
• Running the executable gives a short error message: usage: ./flag-checker FLAG.
  If you pass a random variable as the first argument, you’ll get a "Flag is incorrect" message instead.

Decompiling the binary in Ghidra presents an identical main function.
After checking CLI arguments, it passes the first arg to verify_flag, and uses the return code to determine whether to print "Flag is correct" or "Flag is incorrect".

The verify_flag function contains the logic we’re interested in (I’ve renamed + retyped some variables):

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

bool verify_flag(char *flag)
{
  ulong uVar1;
  size_t flaglen;
  ulong uVar2;
  bool ret;

  flaglen = strlen(flag);
  if ((flaglen == 0x26) && ((*(ushort *)(flag + 4) ^ 0x6865 | *(uint *)flag ^ 0x62756c63) == 0)) {
    uVar1 = 0;
    while (uVar2 = uVar1, uVar2 != 0x13) {
      if (((char)(flag[uVar2 + 0x13] ^ flag[uVar2]) != (&DAT_00102032)[uVar2]) ||
         (uVar1 = uVar2 + 1, (char)(flag[uVar2 * 2 + 1] ^ flag[uVar2 * 2]) != (&DAT_00102045)[uVar2]
         )) goto LAB_001011de;
    }
    uVar2 = 0x13;
LAB_001011de:
    ret = 0x12 < uVar2;
  }
  else {
    ret = false;
  }
  return ret;
}

As with Rusty Rev 0, the first thing this function does is check the length of our input.
In this case, we know the flag must be 0x26 (38) bytes long.

To solve the challenge, we can either continue using static analysis, or we can use a symbolic execution tool called angr to automate the process.

Solution

The purpose of this challenge is to introduce players to symbolic execution, so that’s the route I will discuss.

First, install angr using pip/poetry/whatever tool you prefer.

If you’re not familiar with angr, I highly recommend checking out their documentation, especially the core concepts section.

Here’s a simplified version of my solve script:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

import angr
import claripy


FLAG_LEN = 38  # determined via static analysis


def check_found(state: angr.SimState) -> bool:
	return b"Flag is correct" in b''.join(state.posix.stdout.concretize())


def solve(exe: str):
	# initialize angr project - auto_load_libs is disabled to speed up 
	proj = angr.Project(exe, auto_load_libs=False)

	# create symbolic variable to represent our input
	flag_str = claripy.BVS("flag", 8 * FLAG_LEN)

	# create initial program state
	state = proj.factory.entry_state(
		args = [exe, flag_str],  # CLI arguments
		add_options = {
			# fill uninitialized memory with zeros
			angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS,
			angr.options.ZERO_FILL_UNCONSTRAINED_MEMORY,
		},
	)

	# create a new SimulationManager from the initial state
	simgr = proj.factory.simulation_manager(state)

	# search for a state where the flag is correct
	simgr.explore(find=check_found)

	assert len(simgr.found) > 0, "failed to locate any matching states!"

	# concretize up to 3 valid solutions (if there are multiple)
	results = simgr.found[0].solver.eval_upto(flag_str, cast_to=bytes, n=3)

	print(f"Results: {results}")


if __name__ == "__main__":
	solve("./flag-checker")

At a high-level, my script:

• creates a symbolic variable to represent our input: flag_str
• creates an initial program state, representing the state of the program before it begins execution
• searches for a state that matches our desired outcome: in this case, we check for "Flag is correct" in the stdout stream
• uses that program state to evaluate our flag_str variable into a concrete string (technically three)
• prints the evaluated string(s)

This is a basic example of using angr to solve a reverse engineering challenge.
Rusty Rev 2 ups the ante, requiring some optimization and a better understanding of angr and how symbolic execution works.