Anger management. Welcome to Angr, a symbolic emulation framework

A symbolic emulator makes it possible to reverse the direction of searches for security holes. For instance, the AFL brute-force fuzzer tries all possible input data. By contrast, Angr, goes through all possible execution paths and recreates the input data required to reach the code section under investigation.

As an example, let’s examine the following piece of code:

A complete enumeration of six characters would take 256⁶ attempts. But for Angr, there is only one fork: go left or go right. And it goes in both directions! All you have to do is tell it when to stop and compute the input data.

You run the script and get the desired password in a second.

For more details, you can review the documentation; this article just explains what you need to get started.

First, install Angr (Python 3.8 or later is required):

Angr operates in interactive mode using console. In many situations, the documentation doesn’t cover all its functionality, and if you really want to master this tool, spend some time on fiddling around with it. For each item, you can get interactive help from docstring using the help(project) (or project? if you use iPython) command.

Help is navigated in the same way as man: you move using the arrow keys and exit with q.

Class fields and methods can be handily viewed using autocompletion: you add a period to the class name and press Tab several times.

Basic concepts

Everything begins with the Project class; you create it to start interacting with Angr. The project is responsible for file load and primary analysis.

You pass the path to the file under investigation and create a new state using factory.entry_state to start simulation. The factory creates instances of the main classes. The state is a SimState object, essentially a snapshot of a virtual machine. It contains a block of code, memory, registers, call stack and other elements implemented as plugins to SimState.

Data used in the simulation are stored in the bitvector bit array. It’s limited in length and can be overflowed (i.e. it behaves like a processor register). Its size is always specified in bits.

There are two main types: BVV (bit-vector value) and BVS (bit-vector symbol). The first type represents specific numerical values. The second one contains only name and size. This is the basis for symbolic execution, and there is no specific value there.

Basic Blocks

Each state is associated with a specific block of code. A local basic block is a set of instructions that ends with a control transfer instruction. Each emulation step takes you to the next block, thus, creating a new state.

The simulation manager operates only with block addresses, not with code contained in these blocks. This must be taken into account; otherwise, the manager won’t be able to find the desired state.

This is a disassembled basic block. Its assembler instructions are used to create intermediate VEX code. It can be said that this code is generated for the virtual processor used by analyzers.

The intermediate code is represented in the Intermediate Representation Super-Block. Let’s examine its contents:

• IMark indicates the size and address of the original instruction;
• PUT writes a value to a register;
• GET:I64 receives the register value; the postfix indicates its size in bits;
• t30 is a virtual variable (short for temp) and its number;
• LDle – Load in little-endian. Gets a value at the specified address;
• STle – Store in little-endian. Writes a value to the specified address;
• Add64 – addition operation;
• Sub64 – subtraction operation;
• And64 – logical AND operation; and 
• NEXT represents the transition to the next block and its type Ijk_Call.

The code is optimized, and the rip instruction counter doesn’t change with each instruction.

Instead of storing EFLAGS, the intermediate code records:

• cc_op – code of operation performed with flags; and 
• cc_dep1, cc_dep2 and cc_ndep – auxiliary values.

Based on the source code, VEX, 0x13 is X86G_CC_OP_DECB (i.e. a decrement of one byte). Specific flag values ​​are calculated as the need arises.

Simulation control

You can control the simulation manually, which is convenient for debugging.

The initial_state.step() function returns a SimSuccessors object that contains a list of states that occur after the emulation of the current block.

If a fork (i.e. conditional jump) occurs at the end of a block, two new states are created. This happens when the choice of path depends on a symbolic variable. If a jump depends only on known values, only one option is available (which is equivalent to an unconditional jump).

The simulation manager controls the code execution. The SimulationManager object is created in project.factory.simgr. In fact, this is a wrapper that runs step() in a loop. It decides in which branches to continue the emulation and in which branches to stop it.

In the course of execution, all states are stored in special ‘stashes’:

Stashes is a dictionary consisting of regular Python lists. Before the start, states are stored in stashed; during the simulation, in active; and after the code execution, in deadended. This list isn’t complete, and you can create new stashes for your needs.

When you start simulation using simulation.explore, the following arguments can be passed:

• find takes the address of the desired state or a function and returns Yes or No (in response to the question whether the desired state/function has been found); and 
• avoid works in a similar way, but takes addresses to be avoided.

The arguments below belong to simulation.step, but can be passed to simulation.explore. This isn’t explicitly stated in the documentation; so, I suggest reviewing the source code.

• step_func is called after each step (useful for debugging);
• filter_func specifies the stash to put the found state into; and 
• selector_func asks whether to execute the current state.

Simulation ends when the state from find is found or the code from all branches has been executed. Then simulation.explore returns control. If the desired state has been found, it’s placed into the found stash.

For clarity, let’s slightly alter the code:

Now you can see the state at each step:

After reaching the fork, the emulator went both ways. And it finished its job after filling the found stash.

Automatic path selection

The ‘normal’ explore goes ‘broadwise’ by placing all forks to the stash for simultaneous execution. However, loops and forks create many possible routes; as a result, the number of potential paths can increase exponentially. To solve this problem, you can use exploration techniques: search strategies that decide where to go and in what order.

The Depth first search technique deals with only one state at a time and places the rest of them to a queue. The deferred stash acts as such a queue.

This search technique limits the maximum emulation depth for each path (i.e. performs a fast, but shallow emulation).

There are plenty of ready-made techniques, but they are poorly documented; so, check the original scripts for more info.

Symbolic execution

Symbolic variables are computed using the Z3 library. As you remember, symbolic variables don’t contain specific values. The emulator only knows their size and constraints imposed in the course of execution. For instance, let’s create a 64-bit variable called x and add the following constraint: x + 2 == 5.

If you ask the program to calculate a feasible solution, you’ll get 0x3. Similar constraints are imposed on symbolic variables after each block. As an example, let’s examine simple branching.

After finding the address in the debugger, you emulate the beginning of this function. The argument is passed using EDI substitution, and a 32-bit symbolic variable is placed to it.

There is a constraint: to go left, the variable must be less than or equal to five.

For comparison, let’s try to pass a specific value.

No doubt, 1337 is greater than 5. In such a case, there is only one possible choice without any constraints.

Symbolic functions also impose certain constraints, but sometimes it’s difficult to comprehend them.

Suffice it to know that this is a mathematical formula, and a possible solution has to be found for it.

Symbolic functions

So, Angr emulates the application code, but what about external modules? The emulator uses hooks to substitute calls of library functions with Python SimProcedures stubs simulating the execution of the required functions. The same thing happens in case of a syscall. If the required stub cannot be found, the standard ReturnUnconstrained stub is executed.

By default, all external functions are intercepted. Angr’s behavior can be configured when you create a new project. If necessary, you can emulate individual functions or all external code, but this adversely affects performance.

Let’s examine the list of set hooks.

Ready-made stubs inherit the SimProcedure class; see the original scripts for examples.

Hooks can be set by specifying the address:

Or the symbol name:

In Angr, symbols tie names to specific addresses. They are created when the executable file is loaded.

Out of curiosity, you can list them all:

For example, those listed below were taken from debug symbols of an ELF file:

Serial number recovery

To ensure a fair game, let’s take the real crackme for Windows.

The challenge is to generate the serial number for a specific username. After reconstructing the pseudocode in Binary Ninja, you can see the buffer size and input method.

The fgets function takes both strings to a buffer 0x20 bytes in length. It computes the string size and writes a zero byte at the end (i.e. at the address computed as BEGINNING + SIZE). The real fgets returns a string with two bytes at the end: a line break character and a zero. Remember addresses of the blocks that display the success and failure messages.

Symbolic variables aren’t explicitly defined; by default, the standard input stream is implemented as SimPacketsStream. It can be treated as a set of variables created as the need arises.

To pass the username, replace the original fgets hook with your own one that returns the desired string bypassing STDIN. As soon as your hook is triggered, you restore the old one. It’s more convenient to substitute function results than the input stream. As soon as the simulation manager finds a block whose address is 0x004012e3, you specify the STDIN value using posix.dumps.

The solution seems to be simple, but I had to spend plenty of time on debugging. First, I didn’t immediately notice that fgets preserves the line break. Second, sprintf from Angr returns a lowercase string; while sprintf from Wine, an uppercase string. After checking the code in Windows, you can see that Wine was right. I have already reported this bug. As you can see, even the original Angr stubs can contain errors.

Conclusions

Angr is an amazingly powerful tool, but symbolic execution has its limitations. I managed to ‘crack’ the CRC32 key in a couple of minutes, but the formula used to recover data from an MD5 hash turned out to be beyond the Z3 capacity;

Of course, Angr cannot simulate large applications. But if you find a weak place in a program, it will help you to find the ‘right’ input data required for fuzzing.

Now you are aware of the basic Angr functionality. In the next article, I will provide practical examples to give an insight into vulnerability identification and exploitation.