Smashing Flare-On #2 with Concolic Testing

17 Sep 2015 . reversing . Comments

#ctf #flareon

Prelude - Concolic Execution Tools

The idea of applying concolic execution to solving CTFs and crackmes is not new. Cr4sh solved an algebraic crypto-crackme with OpenREIL and Z3. Felipe and Artem demonstrated using KLEE (and McSema) to symbolically solve a maze. Michele recently created a keygen tool to break the serial validation process of a program using KLEE.

CTFs and crackmes have a common problem solving pattern: what inputs do you need to give to the program for it to do something. For example, what arguments do we need to supply to a crackme to display success! instead fail!? Or what key to input to the crackme to output a properly formatted image to disk? Typically, you want know what inputs can invoke the successful execution path of the program, while avoiding the failure execution path.

This pattern makes it especially amenable to the use of concolic testing to efficiently solve it. This typically involves a combination of:

  • IR lifting: Translates the program binary into a side-effects-free intermediate representation for program analysis. Examples of IRs are the BAP BIL, OpenREIL, Valgrind VEX and LLVM IR.
  • Symbolic execution: Expresses the constraints on the inputs needed to reach parts of a program and to aid in path exploration. Examples of symbolic execution engines can be found in KLEE, S2E and Triton.
  • Constraint solving: Determines the feasible range of inputs to reach a desired part of a program. Examples of constraint solvers are Z3 and STP.
  • Taint analysis: Tracks the data and control flows to determine constraints that can be be controlled by (parts of) user-controllable inputs.

I started Flare-On 2015 with the aim of trying my hand at applying concolic execution to solve the challenges. I wanted a framework/tool that allows me to jump straight into the heat of things, ideally as fuss-free as possible. After exploring a few tools, here are some thoughts.

First, I like OpenREIL for its simplicity and friendly Python bindings. It does not, however, have a full-fledged symbolic execution engine. Like Cr4sh, we could leverage OpenREIL’s internal IR emulation engine, pyopenreil.VM, to implement a simple symbolic execution engine with Z3. But depending on the operations used in the CTF binaries, we may need to extend the engine with operations to handle more complex symbolic execution, like branching with symbolic conditions.

Next, a PIN-based concolic testing framework, Triton has a nice taint analysis engine that can track at each program point user-controllable memory or registers. Like OpenREIL, it offers a user-friendly Python interface. But for now, it only works on 64-bit programs. It will be very useful to extend support for 32-bit instructions in Triton.

We could also use McSema to lift x86 programs to LLVM IR and use KLEE to symbolically execute the programs in LLVM bitcode. But KLEE works better (only?) with Linux binaries, and requires the development of an additional KLEE harness program to drive the symbolic execution. Furthermore, the current open-source KLEE applies to whole programs, and lacks the ability to restrict symbolic execution on a smaller subset of functions in the program. A recent extension of KLEE, UC-KLEE can limit execution to selected functions, but it is not available yet.

Last but not least, I stumbled upon angr, recently released at Blackhat 2015. This is an excellent binary analysis tool developed by the security researchers at UCSB, and has been used extensively by Shellphish in the DARPA Cyber Grand Challenge.

Powered by its concolic engine, angr offers users the ability to craft a script to solve for the following typical goal in CTF challenges like those in Flare-On:

What range of inputs is required to reach EIP_SUCCESS and avoid EIP_FAILURE?

And there, this becames my bin-ninjitsu swiss army knife of choice for this CTF.

I will describe the use of angr to efficiently perform path exploration with concolic execution to solve #2 without manual reverse engineering.

 

Identifying Code of Interest

Challenge #2, very_success (binary link), is a Windows binary that asks for a password. If the password is verified to be incorrect, it prints “You are failure”; if the password is correct, it prints “You are success”.

flare2 prompt

The disassembly is relatively straightforward. The function sub_401084 apparently takes some user input, performs verification and returns a result that determines if the program prints “success” or not. The goal is to input a password that allows us to take the branch at 0x40106B (“success”) and avoid the branch at 0x401072(“failure”).

flare2 control flow

Let’s zoom into and find out more about the function sub_401084. It takes three arguments, namely (1) address to a buffer of bytes at 0x4010E4, which is presumbly the reference key for verification, (2) address to a user input buffer at 0x402159, and (3) the length of the user password supplied to the program. The basic block, highlighted cyan, is likely performing the main computation used to verify the user password based on the reference key.

flare2 decoding func

Typically at this point, I would begin to reverse the function sub_401084 by hand, or run the Hex Ray decompiler on this function if I’m lazy.

 

Solving #2 Without Manual Reversing

This year, I experiment with using angr to solve this problem symbolically. In other words, I want to know what user password can get me to the successful execution path at 0x40106B. Assuming the password is a valid email address, we can choose to brute-force the password with a python script that iterates through the valid characters of an email address for increasing length of the password, and alerts us when the program execution reaches the desired code address. But this is inefficient.

Concolic execution in this case works nicely and elegantly in our path exploration to reach our desired code branch.

We begin by initializing the angr environment in Python, and loading the challenge binary.

In [1]: import angr

In [2]: p = angr.Project('very_success')

We localize our analysis to the specific function sub_401084. After initializing the engine to begin the concolic execution at an initial code address 0x401084, we need to set up the arguments for this function accordingly. We know from the instruction at 0x401093 that the function is looking for a password of 0x25 bytes long. We hardcode this, as well as the address offsets for the various arguments on the stack.

In [3]: initial_state = p.factory.blank_state(addr=0x401084)

In [4]: initial_state.stack_push(0x25)                  # arg_8__len_password

In [5]: initial_state.stack_push(0x402159)              # arg_4__user_password

In [6]: initial_state.stack_push(0x4010e4)              # arg_0__ref_key

In [7]: initial_state.stack_push(0x401064)              # return addr

To guide the concolic execution, we need to represent the buffer containing user input password symbolically as a BitVector expression consisting of 8 * 0x25 bits. We do that with the state.BV class.

In [8]: PW_LEN = 0x25

In [9]: initial_state.mem[0x402159:] = initial_state.BV('password', 8 * PW_LEN)

Furthermore, since we know that the password should consist only of printable characters, we add these constraints to the initial state. These constraints will guide the concolic execution during the path exploration.

In [10]: for i in xrange(PW_LEN):
   ....:     char = initial_state.memory.load(0x402159 + i, 1)
   ....:     initial_state.add_constraints(char >= 0x21, char <= 0x7e)

With the constraints and initial state configured, we are one step away from the concolic execution. We initialize a path using our initial state. To begin the path exploration with concolic testing, we rely on the angr.surveyors.Explorer class. We specify the desired code address to reach and the one we want to avoid. Note that the display output of concolic_run indicates that one path (“1 found”) satistifies our requirement during the path exploration.

In [11]: initial_path = p.factory.path(state=initial_state)

In [12]: ex = angr.surveyors.Explorer(p, start=initial_path, find=(0x40106b,), avoid=(0x401072,), enable_veritesting=True)

In [13]: concolic_run = ex.run()

In [14]: concolic_run
Out[14]: <Explorer with paths: 1 active, 3 spilled, 1 deadended, 0 errored, 0 unconstrained, 1 found, 1 avoided, 0 deviating, 0 looping, 0 lost>

Finally, we extract the password from this found state, and voila!

In [15]: final_state = concolic_run.found[0].state

In [16]: final_state.se.any_str(final_state.memory.load(0x402159, PW_LEN))
Out[16]: 'a_Little_b1t_harder_plez@flare-on.com'
 

Optimization

Documentation on angr API and various classes is lacking. So the instructions above are found through the existing documentation and some example scripts on the github site. Incidentally, after I had struggled to piece together various parts of angr to solve this challenge, an example angr script to solve challenge #2 was then added to the github repo.

It turns out that we can remove the option simuvex.o.LAZY_SOLVES when creating the blank_state. This makes the path exploration more efficient by ensuring that we do not traverse paths that are unsatifiable.

Furthermore, instead of the angr.surveyors.Explorer that I used, the example angr script uses the PathGroup class. It seems to be a more elegant and better approach to managing the explored paths.

... <snip> ...
initial_state = p.factory.blank_state(addr=0x401084, remove_options={simuvex.o.LAZY_SOLVES})
... <snip> ...
paths = p.factory.path_group(state, immutable=False)
paths.explore(find=0x40106b, avoid=0x401072)
 

Full angr Script

Here is the full listing of python script to solve Flare-On #2 with angr.

import angr, simuvex

# Load binary
p = angr.Project('very_success')

# Start with a blank state at the function sub_401084
initial_state = p.factory.blank_state(addr=0x401084, 
                                      remove_options={simuvex.o.LAZY_SOLVES})

# Populate stack to simulate calling function with required args
initial_state.stack_push(0x25)                  # arg_8__len_password
initial_state.stack_push(0x402159)              # arg_4__user_password
initial_state.stack_push(0x4010e4)              # arg_0__ref_key
initial_state.stack_push(0x401064)              # return addr

# Set the user input password as a symbolic buffer of bytes
PW_LEN = 0x25
initial_state.mem[0x402159:] = initial_state.BV('password', 8 * PW_LEN)

# Assume that the password consists of only printable bytes
for i in xrange(PW_LEN):
    char = initial_state.memory.load(0x402159 + i, 1)
    initial_state.add_constraints(char >= 0x21, char <= 0x7e)

# Create an execution path with our initial state
initial_path = p.factory.path(state=initial_state)

# Perform the path exploration using concolic execution
ex = angr.surveyors.Explorer(p, start=initial_path, find=(0x40106b,), 
                             avoid=(0x401072,), enable_veritesting=True)
concolic_run = ex.run()

# Extract the password that got us to the desired execution path
final_state = concolic_run.found[0].state
print final_state.se.any_str(final_state.memory.load(0x402159, PW_LEN))
 

Useful References

Here are the links to several good references to the use of concolic testing applied to security: