Symbolic Execution — KLEE, Angr and Path Exploration

In this tutorial, you'll learn about Symbolic Execution. We cover key concepts, practical examples, and best practices to help you understand and apply this topic effectively.

Symbolic Execution analyzes programs by using symbolic values instead of concrete inputs, enabling exploration of all execution paths and automated test case generation.

Learning Path

flowchart LR
  A["Bounded Model Checking"] --> B["Symbolic Execution
KLEE, Angr & Paths"]
  B --> C["Satisfiability & SMT"]
  B --> D["Industrial Formal Verification"]
  style B fill:#f90,color:#fff,stroke-width:2px

Prerequisites

Basic compiler concepts, SAT/SMT solving, and C or Python programming.

What Is Symbolic Execution?

Instead of running a program with concrete values, Symbolic Execution assigns symbolic values to inputs. When the program branches on a symbolic condition, execution forks, and each path gets a path constraint capturing the branch condition.

The solver checks if each path is feasible. At the end, you get concrete inputs for each explored path.

Step-by-Step: Simple Symbolic Interpreter

Step 1: Symbolic Variables

class SymbolicExpr:
    def __init__(self, name):
        self.name = name

    def __repr__(self):
        return self.name

def symbolic(name):
    return SymbolicExpr(name)

x = symbolic("x")
y = symbolic("y")
print(f"Symbolic variables: x={x}, y={y}")

Expected output:

Symbolic variables: x=x, y=y

Step 2: Track Path Constraints

class PathState:
    def __init__(self, constraint=[]):
        self.constraint = constraint

    def branch(self, condition, take_true):
        if take_true:
            new_c = self.constraint + [condition]
        else:
            new_c = self.constraint + [f"not({condition})"]
        return PathState(new_c)

    def __repr__(self):
        return f"Path: {' AND '.join(self.constraint)}"

state = PathState()
state_t = state.branch("x > 0", True)
state_f = state.branch("x > 0", False)
print(f"True branch:  {state_t}")
print(f"False branch: {state_f}")

Expected output:

True branch:  Path: x > 0 AND ...
False branch: Path: not(x > 0) AND ...

Step 3: Symbolic Execution of a Function

def symbolic_eval_max(a, b):
    start = PathState()
    # branch: if a > b
    path_gt = start.branch(f"{a} > {b}", True)
    result_gt = a, path_gt

    path_le = start.branch(f"{a} > {b}", False)
    result_le = b, path_le

    return [result_gt, result_le]

a = symbolic("a")
b = symbolic("b")
results = symbolic_eval_max(a, b)
for val, path in results:
    print(f"Result = {val}, {path}")

Expected output:

Result = a, Path: a > b
Result = b, Path: not(a > b)

Step-by-Step: Using KLEE

Step 1: Install KLEE

sudo apt-get install klee

Step 2: Write a Symbolic Program

#include <klee/klee.h>
#include <assert.h>

int abs(int x) {
    if (x < 0) return -x;
    return x;
}

int main() {
    int x;
    klee_make_symbolic(&x, sizeof(x), "x");
    int result = abs(x);
    klee_assert(result >= 0);
    return 0;
}

Step 3: Compile and Run

clang -I /usr/include/klee -emit-llvm -c abs.c -o abs.bc
klee abs.bc

Expected output:

KLEE: output directory = "klee-out-0"
KLEE: done: total instructions = 12
KLEE: done: completed paths = 2
KLEE: done: generated tests = 2

KLEE generates test cases covering both branches (positive x and negative x).

Common Errors

1. Path Explosion

The number of paths grows exponentially with branch count. Mitigate with path merging, state pruning, and execution time limits.

2. External Function Calls

Symbolic Execution cannot model system calls or library functions not compiled to LLVM bitcode. Use KLEE's klee_assume to constrain external behavior.

3. Infinite or Very Deep Loops

Loops create infinite paths if unconstrained. Use symbolic loop bounds or KLEE's --max-loop-iterations.

4. Constraint Solving Timeout

Complex constraints slow the SMT Solver. Use simpler symbolic representations or reduce path complexity.

5. Memory Model Complexity

Symbolic pointers and complex data structures create ambiguous memory accesses. Use concrete pointers where possible.

Practice Questions

Q1: What is a path constraint?

The logical conjunction of branch conditions along a particular execution path. A satisfiable path constraint means the path is feasible.

Q2: How does KLEE handle symbolic files?

KLEE provides klee_make_symbolic for marking arbitrary memory as symbolic, including file buffers.

Q3: What is concolic execution?

A hybrid of concrete and Symbolic Execution that runs the program concretely while collecting symbolic constraints along the actual path.

Q4: Why does Symbolic Execution use SMT solvers?

To check whether path constraints are satisfiable and to produce concrete test inputs.

Q5: What limits KLEE to C programs?

KLEE operates on LLVM bitcode. Languages that compile to LLVM IR (C, C++, Rust) can be analyzed.

Challenge

Write a C function that takes three integers representing side lengths and determines if they form a valid triangle. Use KLEE to generate test inputs covering all paths: invalid triangle, equilateral, isosceles, and scalene.

FAQ

Built by the developers of Doda Browser, DodaZIP, and Durga Antivirus Pro.