Solving Microcorruption Hollywood

2021-03-28

Microcorruption is a Capture The Flag (CTF) game created by Matasano Security and Square, Inc. in 2014, which is also referred to as "Embedded Security CTF". This CTF consists of multiple challenges where the goal is to find an input flag, which unlocks a door that is protected by software running on a microcontroller from the Texas Instruments MSP430 family.

This CTF works entirely in a web browser, providing access to a debugger for the microcontroller that allows one to view the assembly code, a live memory dump, register states, the current instruction executed, as well as the I/O console. The debugger supports stepping through instructions, setting breakpoints, inspecting memory sections, evaluating expressions, tracking registers in memory, writing to memory or registers, and going into "solve" mode where the input for unlocking the door can be supplied. Furthermore, the CTF comes with a simple assembler and disassembler: https://microcorruption.com/assembler.

If you haven't taken the time to go through the exercises yourself, now is the opportunity to stop reading and get started with the challenges. Working through these challenges is a great way to learn about reverse engineering and binary exploitation. Topics covered in this well-designed and simple training environment include stack and heap overflow exploitation. Some challenges require defeating protection mechanisms such as stack canaries, nonexectable stacks, and Address Space Layout Randomization (ASLR). To get a high-level description of these protection mechanisms and exploitation strategies with pointers to further information, check out Wikipedia. A practical introduction to Return-Oriented Programming (ROP) on 64-bit Linux, which is an exploitation approach that actually goes beyond the Microcorruption CTF, is provided by Ben Lynn. For a more advanced technique called Blind Return Oriented Programming (BROP), refer to this webpage by the authors who introduced this concept.

After attempting to solve these challenges yourself, it might be beneficial to review how others solved these problems. To this end, this blog post discusses two approaches to solve the final level in Microcorruption, which is called "Hollywood".

The major hurdle with Hollywood is that its code is obfuscated, aggravating analysis with the supplied debugger. To overcome this hurdle, others wrote an emulator for the MSP430 as well as a disassembler that can be used in conjunction with the emulator. To solve the challenge, Grazfather modified the emulator to obtain a ROM image that includes only the instructions actually executed by the challenge program and analyzed the resulting image using IDA.

The analysis by Grazfather reveals that at the core of Hollywood is a loop that hashes the input password. Register R5 holds the pointer to the beginning of the password in memory. An iteration of the Hollywood hashing function looks as follows:

add  @R5, R4
swpb R4
xor  @R5+, R6
xor  R4, R6
xor  R6, R4
xor  R4, R6

The syntax "@R5+" denotes that register R5 is used as a memory pointer and R5 is incremented after the instruction is executed. The machine word size of the MSP430 is 16 bits, and thus the password is iteratively hashed in 16-bit chunks. The final output as well as intermediate states of the hash function are stored in registers R4 and R6. The last three "xor" instructions of each iteration swap the values of registers R4 and R6. Using "xor" is a trick to avoid using a temporary register to perform the swap.

The Hollywood hashing function can be expressed as follows in Julia:

function hash(password::Vector{UInt16})
  r4 = 0x0000
  r6 = 0x0000

  for word in password
    (r4, r6) = (xor(r6, word), bitrotate(r4 + word, 8))
  end

  return (r4, r6)
end

Further analysis shows that the output of the Hollywood hash function stored in registers R4 and R6 is compared to constants as follows:

cmp #0xfeb1, R4
[...]
cmp #0x9298, R6
[...]

If the values in R4 and R6 are equal to 0xfeb1 and 0x9298, respectively, the door will be unlocked. Hence, the goal is to find a password that is hashed to these constants.

A straightforward approach that is detailed by Alex van Poppelen is to find a password via a brute-force search, i.e., to try all possible passwords in a systematic fashion until a password that results in the desired hash is found.

It turns out that the shortest password that unlocks the door is three machine words long. Instead of generating all passwords with this length, it is sufficient to enumerate candidates that are two machine words long, and compute the third machine word using the constraints imposed by comparison instructions.

Specifically, with [p1, p2, p3] denoting the password (each element of this array is a 16-bit machine word), and (r4, r6) representing the register state after computing hash([p1, p2]), the following constraints need to be satisfied for p3:

xor(r6, p3) == 0xfeb1
r4 + p3 == 0x9892 (this constraint is a simplification of bitrotate(r4 + p3, 8) == 0x9298)

To meet the first constraint, p3 can be computed as p3 = xor(0xfeb1, r6). Then, the password is valid if the second constraint is met. This exhaustive search for the password can be implemented in Julia as follows:

function findPassword()
  # The password consists of three 16-bit words [p1, p2, p3] such that the
  # following constraints are satisfied:
  # xor(r6, p3) == 0xfeb1
  # r4 + p3 == 0x9892 # simplification of bitrotate(r4 + p3, 8) == 0x9298
  #
  # Enumerate all values of p1 and p2, hash this partial password, and then
  # compute xor(0xfeb1, r6) to obtain p3. p3 must meet the constraint
  # r4 + p3 == 0x9892 for the password to be valid.
  #
  # For a Ruby implementation of this brute-force search, see
  # https://unorde.red/microcorruption-ctf-hollywood/

  for p1=0x0000:0xffff
    for p2=0x0000:0xffff
      (r4, r6) = hash([p1, p2])
      p3 = xor(0xfeb1, r6)

      if (r4 + p3) == 0x9892
        # solution found
        password = [p1, p2, p3]

        # double-check that the solution is correct
        (r4, r6) = hash(password)
        if r4 == 0xfeb1 && r6 == 0x9298
          println(string("password: ", password))
        else
          error("computation incorrect")
        end
      end
    end
  end

  return 0
end

findPassword()

Running the Julia program above with our prior definition of the hash function, we receive many passwords that solve the Hollywood challenge:

password: UInt16[0x0010, 0x5ca5, 0x4bed]
password: UInt16[0x0010, 0x7cc5, 0x2bcd]
password: UInt16[0x0012, 0x5ca5, 0x49ed]
[...]

The byte order of the MSP430 architecture is little endian, meaning that bytes with less significance are located at lower addresses in memory than bytes with higher significance. The Julia output shows each word in big endian notation. Thus, it's necessary to swap the bytes of each word in the Julia output to obtain an input for the microcontroller in hexadecimal format that will be accepted. For example, the hexadecimal input "1000 a55c ed4b" is interpreted by the microcontroller as desired.

The exhaustive search approach is sufficient to solve the Hollywood challenge. However, it is not the most efficient way to find a solution. A more efficient approach is to leverage a Satisfiability Modulo Theories (SMT) solver such as the Z3 Theorem Prover developed by Microsoft Research. Others including Grazfather, W. J. van der Laan, and Guillaume Vigeant pursued the same approach.

Fortunately, Z3 has bindings for Julia. Reading up on the documentation of the underlying Julia package, we can implement a solver for the Hollywood challenge in Julia as follows:

using Z3

function hash(ctx::Z3.ContextAllocated, password::Vector{Z3.ExprAllocated})
  r4 = bv_val(ctx, 0, 16)
  r6 = bv_val(ctx, 0, 16)

  for word in password
    (r4, r6) = (xor(r6, word), rotate_right(r4 + word, 8))
  end

  return (r4, r6)
end

function findPassword(numWords::Int)
  ctx = Context()
  password = Vector{Z3.ExprAllocated}(undef, numWords)

  # password consists of machine words where each word is a bitvector of size 16:
  for i=1:length(password)
    password[i] = bv_const(ctx, string("p", i), 16)
  end

  (r4, r6) = hash(ctx, password)

  s = Solver(ctx)

  # 16-bit words of password need to satisfy the following constraints:
  add(s, r4 == 0xfeb1)
  add(s, r6 == 0x9298)

  if check(s) == Z3.sat
    # solution found
    m = get_model(s)

    res = consts(m)
    for (k, v) in res
      println("$k = $v")
    end

    return 0
  end

  return 1
end

function main()
  for numWords=1:8
    res = findPassword(numWords)
    if res == 0
      # solution found
      return 0
    end
  end

  return 1
end

main()

The code above attempts to find a password with a length ranging from one to eight machine words, and displays the solution as soon as it finds one. The password is represented as an array of bit vector constants that Z3 solves for where each bit vector consists of 16 bits. Each bit vector has a unique name. While the name format is arbitrary, this implementation uses "p<index>" as the format where "<index>" denotes the position in the password array. The hash function above declares the 16-bit bit vectors r4 and r6 that represent the corresponding registers. These bit vectors are initialized to zero. This function then declares how these variables arithmetically depend on the bit vectors from the password. In addition, the solver is provided with the two constraints on r4 and r6, i.e., the requirements that these values need to be equal to given constants. Finally, the findPassword function calls check to probe for satisfiability, and prints the solution if the check is successful.

Running the code above, we obtain a password consisting of three machine words:

p3 = #x71c5
p1 = #xfc5e
p2 = #x7831

As the output above uses big endian notation, and MSP430 is a little endian architecture, the hexadecimal password "5efc 3178 c571" clears the Hollywood level.

If you enjoy these type of challenges and have an interest in cryptography, you might like the Cryptopals Crypto Challenges by Matasano Security. These challenges inspired me to write a Julia package for the AES symmetric-key algorithm supporting several cipher modes of operation. Another recommended resource is the tutorial series by Azeria Labs that is geared towards ARM exploitation. For these tutorials, check out my macos-qemu-rpi project that provides scripts for setting up QEMU on macOS in order to simulate Raspberry Pi OS (previously called Raspbian) for the ARM architecture.

Fabian's Lines of Thought

Solving Microcorruption Hollywood

2021-03-28