Close Encounters with Symbolic Execution

Artem Dinaburg

November 25, 2014

compilers, darpa, mcsema, symbolic-execution

At THREADS 2014, I demonstrated a new capability of mcsema that enables the use of KLEE, a symbolic execution framework, on software available only in binary form. In the talk, I described how to use mcsema and KLEE to learn an unknown protocol defined in a binary that has never been seen before. In the example, we learned the series of steps required to navigate through a maze. Our competition in the DARPA Cyber Grand Challenge requires this capability — our “reasoning system” will have no prior knowledge and no human guidance, yet must learn to speak with dozens, hundreds, or thousands of binaries, each with unique inputs.

Symbolic Execution

In the first part of this two part blog post, I’ll explain what symbolic execution is and how symbolic execution allows our “reasoning system” to learn inputs for arbitrary binaries. In the second part of the blog post, I will guide you through the maze solving example presented at THREADS. To describe the power of symbolic execution, we are going to look at three increasingly difficult iterations of a classic computer science problem: maze solving. Once I discuss the power of symbolic execution, I’ll talk about KLEE, an LLVM-based symbolic execution framework, and how mcsema enables KLEE to run on binary-only applications.

Maze Solving

One of the classic problems in first year computer science classes is maze solving. Plainly, the problem is this: you are given a map of a maze. Your task is to find a path from the start to the finish. The more formal definition is: a maze is defined by a matrix where each cell can be a step or a wall. One can move into a step cell, but not into a wall cell. The only valid move directions are up, down, left, or right. A sequence of moves from cell to cell is called a path. Some cell is marked as START and another cell is marked as END. Given this maze, find a path from START to END, or show that no such path exists.

An example maze. The step spaces are blank, the walls are +-|, the END marker is the # sign, and the current path is the X’s.

The typical solution to the maze problem is to enumerate all possible paths from START, and search for a path that terminates at END. The algorithm is neatly summarized in this stack overflow post. The algorithm works because it has a complete map of the maze. The map is used to create a finite set of valid paths. This set can be quickly searched to find a valid path.

Maze Solving sans Map

In an artificial intelligence class, one may encounter a more difficult problem: solving a maze without the map. In this problem, the solver has to discover the map prior to finding a path from the start to the end. More formally, the problem is: you are given an oracle that answers questions about maze paths. When given a path, the oracle will tell you if the path solves the maze, hits a wall, or moves to a step position. Given this oracle, find a path from the start to the end, or show there is no path.

The solution to this problem is backtracking. The solver will build the path one move at a time, asking the oracle about the path at every move. If an attempted move hits a wall, the solver will try another direction. If no direction works, the solver returns to the previous position and tries a new direction. Eventually, the solver will either find the end or visit every possible position. Backtracking works because with every answer from the oracle, the solver learns more of the map. Eventually, the solver will learn enough of the map to find the end.

Maze Solving with Fake Walls

Lets posit an even more difficult problem: a maze with fake walls. That is, there are some walls that are really steps. Since some walls are fake, the solver learns nothing from the oracle until it asks about a complete solution. If this isn’t very clear, imagine a map that is made from completely fake walls: for any path, except one that solves the maze, the oracle will always answer “wall.” More formally, the problem now is: given an oracle that will verify only a complete path from the start to the end, solve the maze.

This is vastly more difficult than before: the solver can’t learn the map. The only generic solution is to ask the oracle about every possible path. The solver will eventually guess a valid path, since it must be in the set of all paths (assuming the maze is finite). This “brute force” solver is even more powerful than the previous: it will solve all mazes, map or no map.

Despite its power, the brute force solver has a huge problem: it’s slow and impractical.

Cheat To Win

The last problem is equivalent to the following more general problem: given an oracle that verifies solutions, find a valid solution. Ideally, we want something that finds a valid solution faster than brute force guessing. Especially when it comes to generic problems, since we don’t even know what the inputs look like!

So lets make a “generic problem solver”. Brute force is slow and impractical because it tries every single concrete input, in sequence. What if a solver could try all inputs at once? Humans do this all the time without even thinking. For instance, when we solve equations, we don’t try every number until we find the solution. We use a variable that can stand in for any number, and algorithmically identify the answer.

So how will our solver try every input at once? It will cheat to win! Our solver has an ace up its sleeve: the oracle is a real program. The solver can look at the oracle, analyze it, and find a solution without guessing. Sadly, this is impossible to do for every oracle (because you run into the halting problem). But for many real oracles, this approach works.

For instance, consider the following oracle that declares a winner or a loser:

x = input();
if(x > 5 && x &lt; 9 && x % 4 == 0) {
  winner();
else {
  loser();
}

The solver could determine that the winner input must be a number greater than 5, less than 9, and evenly divisible by 4. These constraints can be turned into a set of linear equations and solved, showing the only winner value is 8.

A hypothetical problem solver could work like this: it will treat input into the oracle as a symbol. That is, instead of picking a specific value as the input, the value will be treated as a variable. The solver will then apply constraints to the symbol that correspond to different branches in the oracle program. When the solver finds a “valid solution” state in the oracle, the constraints on the input are solved. If the constraints can be solved, the result will be a concrete input that reaches the valid solution state. The problem solver tries every possible input at once by converting the oracle into a system of linear equations.

This hypothetical problem solver is real: the part that discovers the constraints is called a symbolic execution framework, and the part that solves equations is called an SMT solver.

The Future Is Now

There are several software packages that combine symbolic execution with SMT solvers to analyze programs. We will be looking at KLEE because it works with LLVM bitcode. We can use KLEE as a generic problem solver to find all valid inputs given an oracle that verifies those inputs. KLEE can solve a maze with hidden walls: Felipe Manzano has an excellent blog post showing how to use KLEE to solve exactly such a maze.

So what does mcsema have to do with this? Well, KLEE works on programs written in LLVM bitcode. Before mcsema, KLEE could only analyze programs that come with source code. Using mcsema, KLEE can be a problem solver for arbitrary binary applications! For instance, given a compiled binary that checks solutions to mazes with hidden walls, KLEE could find all the valid paths through the maze. Or it could do something more useful, like automatically generate application tests with high code coverage, or maybe even find security bugs in binary programs.

But back to maze solving. In Part 2 of this blog post, we’ll take a binary that solves mazes, use mcsema to translate it to LLVM, and then use KLEE to find all valid paths through the maze. More specifically, we will take Felipe’s maze oracle and compile it to a Linux binary. Then, we will use mcsema and KLEE to find all possible maze solutions. Everything will be done without modifying the original binary. The only thing KLEE will know is how to provide input and how to check solutions. In essence, we are going to show how to use mcsema and KLEE to identify all valid inputs to a binary application.