Concolic Execution

In practice §1.1

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.

Some of this hazel is solved by libraries.

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

Now we can encode harder problems in our programming language of choice:

def at_most_one(props):
    import itertools

    conditions = []
    for p, q in itertools.permutations(props, 2):
        conditions.append(z3.Or(z3.Not(p), z3.Not(q)))
    return z3.And(*conditions)

import z3
import itertools


def at_most_one(props):
    conditions = []
    for p, q in itertools.permutations(props, 2):
        conditions.append(z3.Or(z3.Not(p), z3.Not(q)))
    return z3.And(*conditions)


columns = "abcd"
rows = "1234"

# Create a boolean for each possible queen location.
queen_on_square = [[z3.Bool(f"Q{c}{r}") for c in columns] for r in rows]
s = z3.Solver()

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

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

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

for diag in prim + secd:
    s.add(at_most_one(diag))

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

model = s.model()

for ir, r in reversed(list(enumerate(rows))):
    print(f" {r} ", end="")
    for ic, c in enumerate(columns):
        is_black = (ir + ic) % 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[ic][ir]])
        print("♛" if has_queen else " ", end="")
        print(" \033[0m", end="")  # ]
    print()
print(f"    {'  '.join(columns)}")

Even though it seems inefficient to solve these kinds of problems using a general tool. It is a very cool tool.

Symbolic Values §2.1

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

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

Path Constraints §2.2

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 $\psi ⊢\sigma$, where $\psi$ is the path constraints and $\sigma$ 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\le 10⊢a$. This means 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;
}

In Practice §2.3

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 paths. A path contains the next instruction to execute, a state, the path constraint, and the depth of current path.

stack : list[tuple[PC, SymState, SymPath, int]]

Below, we'll assume a stepping function over symbolic states:

def step(pc: PC, state: SymState) 
  -> Iterable[PC, SymState, SymPath]]: ...

When analysing the program, we pop 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 then end when the stack is empty.

def analyse(pc : PC, inputs : list[tuple[str, JvmType]], max_depth : 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[tuple[PC, SymState, SymPath]] = [(pc, state, [])]

  # As long as the stack is not empty
  while stack:
    # pop the end of the stack
    (pc, state, path, n) = stack.pop(-1)

    # 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 
    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

        # append stack if within limits
        if n < max_depth:
          stack.append((pc, state_, path_, n + 1))

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

Limitations §2.4

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).

Another big problem is memory aliasing and arrays. Since we can only access the arrays with concrete values we don't know what an access is pointing to.

Code Instrumentation §3.1

One big limitation of the dynamic techniques we have looked at so far is speed. Ideally, we would get all the information we needed while running the program instead of having to implement our own interpreter.

The way to get around this is by doing code instrumentation. Code instrumentation injects small instructions inside the code to track and trace what is happening.

To do concolic execution, you will have to instrument the code to keep track of the symbolic values of the entire memory, essentially keeping a shadow variable for each variable. And then update those accordingly. This is not trivial.