Concolic Execution

Christian Gram Kalhauge

The goal of this chapter is to ask and answer the following questions:

What are some good uses for SMT Solving?
What are the big limitations of Symbolic Execution?
Why would you use Concolic execution?

In this section, we are going to cover a powerfull dynamic technique called symbolic execution, how to reason about symbolic values using a SMT solver, as well as showing how to combine it with fuzzing to get very precise coverage.

1. SMT Solving

The most revolutionary technology in the field of program analysis, in my opinion, is the ability to routinely and effectively solve NP-hard problems.

SMT stands for satisfiability modulo theories, and is essentially a solver of mathematical equations. And, since most of program analysis is essentially solving equations, this is a total game changer for our field.

Install Z3 for you favorite language

Install bindings to Z3 for your favorite language. If you use Python, you can simply install z3-solver==4.13.3.0 package with pip (in your virtual environment).

After which you should be able to run the following example:

>>> from z3 import *
>>> s = Solver()
>>> a = Int("a")
>>> s.add(a > 10)
>>> s.check()
sat
>>> s.model()
[a = 11]

We are not going into how SMT solvers work. Consider them black magic -- they are solving NP-hard problems rutinely after all. Sometimes the black magic works and sometimes it doesn't, and even something as benign as renaming your variables might anger the shadow creatures. Now let's swing that Wand!

When using a SMT solver you have to do 3 steps,

Encode your problem as a proposition that the SMT solver can check.
Run the SMT solver, by checking if the proposition is satisfied.
If that is true, then a model (a truth assignment) is found, you should now turn that back into a (counter -) solution the user can understand.

While this seems simple, we often tend to over complicate the problem, making it hard for the SMT solver to check, or we get some subtle details of the problem work. It is paramount that we are precise when we defined our proposition.

N-Queens

Exercise taken from CSC410

Your goal is to solve the N-Queens problem. Given an N x N chessboard, place N queens so than none can take each other. There are three rules

There must be exactly one queen on each row,
There must be exactly one queen on each column, and
There can be no more than one queen on each diagonal.

First try to solve the 4-Queens problem, using your bindings to Z3. Some small hints:

Make a boolean for whether or not each square contains a queen: Qa1, Qa2, ...
Write up logical constraints for the rules above using those booleans

In Python, you can write at most one element must be true like this:

def at_most_one(probs):
  return Or(
    And(*[Not(q) for q in props]),
    *[
        And(p, *[Not(q) for iq, q in enumerate(props) if iq != ip])
        for ip, p in enumerate(props)
    ],
    )

Hower to see an implementation

from z3 import *

columns = "abcd"
rows = "1234"
squares = [(c, r) for r in rows for c in columns]
inv = {sq: i for i, sq in enumerate(squares)}

queen_on_square = [f"Q{c}{r}" for r in rows for c in columns]
at_most_one = lambda props: Or(
    And(*[Not(q) for q in props]),
    *[
        And(p, *[Not(q) for iq, q in enumerate(props) if iq != ip])
        for ip, p in enumerate(props)
    ],
)

s = Solver()

# Create a boolean for each possible queen location.
queen_on_square = Bools(" ".join(queen_on_square))

# There need to be exactly one queen per row.
for r in rows:
    s.add(And(*[Or(*[queen_on_square[inv[(c, r)]] for c in columns]) for r in rows]))
    s.add(at_most_one([queen_on_square[inv[(c, r)]] for c in columns]))

# There can be at most one queen per column.
for c in columns:
    s.add(at_most_one([queen_on_square[inv[(c, r)]] for r in rows]))

# There can be no more than one queen per diagonal.
prim, secd = dict(), dict()
for ir, r in enumerate(rows):
    for ic, c in enumerate(columns):
        # primary diagonals are constant over substraction
        prim.setdefault(ir - ic, []).append((c, r))
        # secondary diagonlas are constant over summation
        secd.setdefault(ir + ic, []).append((c, r))

for d in list(prim.values()) + list(secd.values()):
    s.add(at_most_one([queen_on_square[inv[dcor]] for dcor in d]))

# This is kind of an ugly hack.
assert str(s.check()) == "sat"

model = s.model()
for irow, row in enumerate(rows):
    print(f" {row} ", end="")
    for icol, col in enumerate(columns):
        is_black = (irow + icol) % 2 == 0
        if is_black:
            print("\033[40m\033[37m ", end="")  # ]]
        else:
            print("\033[47m\033[30m ", end="")  # ]]
        has_queen = bool(model[queen_on_square[inv[col, row]]])
        print("♛" if has_queen else " ", end="")
        print(" \033[0m", end="")  # ]
    print()
print(f"   ", end="")
for icol, col in enumerate(columns):
    print(f" {col} ", end="")
print()

(Optional) Try to be faster than Z3

N-Queens is a known (and hard) search problem, try to see if you can outperform Z3 with your own implementation.

2. Symbolic Execution

Symbolic execution, Wikipedia.
Various youtube vidoes here, and here

The advent of SMT solvers suddenly made a new kind of analysis possible, called Symbolic Execution. Instead of running the program with concrete values, this technique builds up symbolic values. A symbolic value is a value which can contain formulas over input symbols. This is clearly very useful when analysing programs:

int incr(int a) { 
  int x = a;        // x := a
  x =+ 1;           // x := a + 1
  x =+ 3;           // x := a + 1 + 3 = a + 4
  return x;         // return (a + 4)
}

In the example above, we do a simple symbolic execution to see that the program is in fact just adding 4 to the input. This would have been very hard to detect using regular testing and even with some kinds of static analysis.

2.1. Symbolic Values

As mentioned above, a symbolic value is a formulae explaining how to calculate a value from inputs. We use symbols to indicate an input.

\begin{matrix} s_{1}, s_{2} \in 𝐒 𝐲 𝐦 𝐕 𝐚 𝐥 & := & v & – a symbol \\ | & s_{1} + s_{2} & – operations on the symbols \\ | & \dots & – and so on \end{matrix}

You can consider symbolic values as very simple programs or expressions, which are easy to do further analysis on.

For example, assuming the input $i$ is 42, then the concrete value of $i + 2 - 10$ is $34$ , while the symbolic value is $i - 8$ . We can use z3 to simplify symbolic values for us using the z3.simplify command.

>>> import z3
>>> i = z3.Int("i")
>>> e = i + 2 - 10
>>> print(e)
i + 2 - 10 
>>> print(z3.simplify(e))
-8 + i

This is very useful as for loops can add a lot of $((x + 1) + 1) + 1$ to your symbolic expressions:

>>> i = z3.Int("i")
>>> for r in range(10):
...     i = i + 1
... 
>>> print(i)
i + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1

>>> i = z3.Int("i")
>>> for r in range(10):
...     i = z3.simplify(i + 1)
... 
>>> print(i)
10 + i

2.2. Path Constraints

When analysing real program we quickly face a problem, executions have context. If we first check if a variable $x$ is less than $10$ , and it is true then we know that in this branch $x < 10$ . This is called a path constraint, as individual values does not hold this information, but the full context of the path does. We can denote a symbolic execution like $ψ ⊢ σ$ , where $ψ$ is the path constraints and $σ$ is the symbolic state, which is often a mapping from variables to symbolic values.

The procedure is illustrated by the following program:

int incr(int a) { 
  int x = a;          // []                    |- x := a
  if (x > 10) {       // [a > 10]              |- x := a
    x =+ 1;           // [a > 10]              |- x := a + 1
    if (x < 10)       // [a > 10, a + 1 < 10]  |- UNSAT
      assert false;   // never executed
  }
  return x;           // returns [ a  > 10 |- a + 1 
                      //         , a <= 10 |- a      ]
}

When we get to the second branch, we need to figure out if we would enter it and raise an assertion error. Since we already know that $a > 10$ , we can see that that $\neg (x < 10)$ , when $x = a + 1$ . This what we use our SMT solver for. In Python, we can use z3 to build up symbolic values, add the path constrains as context and then check if the current branch is satisfiable.

>>> import z3
>>> a = z3.Ints("a")[0]
>>> s = z3.Solver()
>>> path = []

>>> x = a
>>> path.append(x > 10)
>>> print(path, s.check(path), s.model())
[a > 10] sat [a = 11]

>>> x += 1
>>> print(x) 
a + 1
>>> path.add(x < 10)
>>> print(path, s.check(path))
[a > 10, a + 1 < 10] unsat

After iterating over all branches of the program to some depth, we get that the program can be described using two paths: $a > 10 ⊢ a + 1$ and $a \leq 10 ⊢ a$ . This actually also mean that we can re-implement the program like this equivalent and much simpler program:

int incr(int a) {
  if (a > 10) return a + 1;
  if (a <= 10) return a;
}

2.3. In Practice

We can implement symbolic execution to depth $n$ , like the following python pseudo-code. The fundamental idea is to do a depth-first search through the program down to depth $n$ . To do this we maintain a stack of steps. Since the state after step might be multiple different states, one per branch, we keep a list of branches at each stack point. A branch contains the next instruction to execute, a state, and the path constraint. When analysing the program we pop the leftmost branch of the top of the stack, and then compute the steps from there. We then add a new stack entry containing all the branches that have satisfiable path constraints. We pop a stack entry when there is no more branches in it, and end when the stack is empty.

# This method is implemented so the operations are done symbolically instead.
def step(pc : PC, state : SymState) -> list[tuple[PC, SymState, SymPath]]:
  ...

def analyse(pc : PC, inputs : list[tuple[str, JvmType]], n : int):
  # assuming only integers, create symbolic vars for all input
  locals = z3.Ints(" ".join(i_name for i_name, _ in inputs))
  # create state.
  state = SymState.from_locals(locals)

  # Create a stack to do depth first search with.
  stack : list[list[tuple[PC, SymState, SymPath]]] = [ [(pc, state, [])] ]

  # As long as the stack is not empty
  while stack:
    # pop the end of the stack, containing a list of branches
    branches = stack.pop(-1)

    # if no branches left, go op the stack
    if not branches:
       continue

    # look at the first branch, putting the rest back to the stack.
    (pc, state, path), *rest := branches
    stack.append(rest)
   
    # Check if state does something we want to warn the user about.
    if interesting(state):
      return "found interesting state"

    # otherwise create the list of next branches:
    next_branches = []
    for (pc, state_, pathc) in step(pc, state):
        # add new path constraints to the path
        path_ = path + pathc

        # check if path is reachable
        if str(z3.check(path_)) != "sat": 
          continue


        # add new branch to list of branches
        next_branches += (pc, state_, path_)

    # push the set of branches to the stack, if withing limits
    if len(stack) < n:
      stack.append(next_branches)

  return f"all is fine, uptil depth {n}"

It is now your turn to try to implement symbolic execution.

Implement symbolic execution

Implement symbolic execution and try to run it on JPAMB. Tag your solution with dynamic and symbolic.

Upload your results to LEARN.

3. Concolic Execution

Concolic testing, Wikipedia.
The original papers on concolic execution [ 1, 2 ]

One big flaw in symbolic execution is that you have to be able to create a symbolic expression over the entire program. This can be problematic if we use builtin methods like malloc, one-way-functions like hashing or string manipulation methods (which are notoriously hard to model in SMT solvers).

One solution to this is to simulate the different builtin methods, however this mean we might over- or under-estimate the real behaviour of the code. The alternative solution is to additionally to the symbolic values also maintain the concrete values. By having a concrete value, we avoid having to simulate the builtin methods as we can simply use the concrete values instead. We might lose our symbolic value doing that, but it is better than giving up. This is concolic execution. Concolic is just the concatenation of the words Concrete and Symbolic.

To do concolic execution, we first run the program with a random and concrete input. For each concrete value we also keep the symbolic value. Every time we branch on a value, emit the symbolic value as path constraint if the concrete value was true, else emit the negated symbolic value. When we are done we have a list of path constraints which we can use to generate new concrete inputs we can run the program with. We can see a single concolic run as a function from a program and a concrete input to a list of path constraints.

c o n c o l i c (P, i) = ψ_{0}, ψ_{1}, \dots, ψ_{n}

To get a new input, we can simply negate one of the path constraints:

i' \in 𝐬 𝐨 𝐥 𝐯 𝐞 (ψ_{0} \land ψ_{1} \land \dots \land \neg ψ_{n})

Interestingly we actually know that running $c o n c l i c (P, i')$ will produce a prefix of the same path constraints $ψ_{0}, ψ_{1}, \dots, \neg ψ_{n}, ψ_{n + 1}, \dots$ , but might be extended, by new ones. This means, that if we keep track of which path constraints we have already negated (and have infinite time) we can do a depth first search through all possible paths of the program.

Implement concolic execution

Implement concolic execution and try to run it on JPAMB. Tag your solution with dynamic and concolic.

Upload your results to LEARN.

References

1. Gul Agha, Darko Marinov , and Koushik Sen. 2005. CUTE: a concolic unit testing engine for C.
2. Koushik Sen, Nils Klarlund , and Patrice Godefroid. 2005. DART: Directed Automated Random Testing.