Lecture 10: Symbolic Execution

What this lecture covers

Guest lecturer Armando Solar-Lezama (MIT CSAIL) introduces symbolic execution, a program analysis technique used in tools like Microsoft's SAGE to find security bugs by reasoning about entire classes of inputs rather than testing one input at a time. The lecture builds up from ordinary concrete execution to symbolic execution, explains how program paths turn into logical formulas, and then explains how SAT and SMT solvers decide whether those formulas have a solution.

After watching, you can explain why symbolic execution can prove a branch unreachable when testing cannot, describe how a path condition is built while walking a control-flow path, and outline how SAT solvers propagate assignments and learn conflict clauses, and how SMT solvers extend SAT with theories like bit-vectors and arrays to model integers and heap memory.

Key ideas

• Symbolic execution: instead of running a program on one concrete input, it tracks each variable as a symbolic formula over the unknown inputs, letting a single run reason about many (or infinite) concrete inputs at once.
• Path condition: the set of constraints (from branch decisions and assumptions) that must hold for execution to reach a given point along a specific path; if the path condition is unsatisfiable, that path is provably unreachable.
• Precondition / contract: an assumption about valid inputs to a function; without it, symbolic execution may report failures on inputs the function was never meant to handle.
• SAT solver: given a Boolean formula in conjunctive normal form, it tries variable assignments, propagates their consequences, and on a contradiction derives a new conflict clause, until it finds a satisfying assignment or proves none exists.
• SMT (satisfiability modulo theories) solver: builds on a SAT solver by separating a formula's Boolean structure from domain-specific reasoning (theories such as bit-vectors, linear arithmetic, arrays, or uninterpreted functions), going back and forth between the SAT solver and theory solvers.
• Theory of bit-vectors: models machine integers with a fixed width, which matters because machine integers can overflow in ways mathematical integers cannot.
• Theory of arrays: models heap memory as one large array from addresses to values, which is how symbolic execution handles pointers and heap-allocated data.
• Path-by-path exploration: because it does not scale to explore all paths of a large program simultaneously, most symbolic execution tools generate a separate, simpler formula for each path and prune paths early once a path condition becomes unsatisfiable.

Walkthrough

Why symbolic execution matters (1:00)

Symbolic execution is described as a workhorse of modern program analysis, used at Microsoft in a tool called SAGE to find security bugs across products like PowerPoint and Windows. Compared to random testing, it can reason about effectively infinite sets of inputs; compared to purely static analysis, when it finds a bug it produces a concrete input and trace that reproduces the failure, so developers can distinguish real bugs from false positives.

From concrete to symbolic execution (5:33)

Using a small program with an assert false guarded by branches, the lecture first runs it with concrete inputs (x=4, y=4 and x=2, y=2), showing that individual test runs say nothing about other inputs. Symbolic execution instead tracks each variable as a symbolic value (a formula), and at a branch where the direction is unknown, both branches are followed, merging the resulting formula for a variable like t into a single expression (t0) with logical conditions describing when it equals each branch's value. Solving the resulting equation shows the assertion is unreachable. The lecture also discusses preconditions: a branch that looks reachable in isolation may be provably unreachable once a function's documented assumptions about its inputs are added as constraints.

SMT solvers and theories (24:52)

An SMT solver takes a logical formula and returns a satisfying assignment, a proof of unsatisfiability, or (for hard cases) "I don't know" - many of the underlying problems are NP-complete or worse. The "modulo theories" part means solvers can be extended with domain-specific theories: fixed-width bit-vectors (which force a choice of bit width and capture overflow behavior), linear integer arithmetic (efficient but not overflow-aware), and uninterpreted functions (used when only input/output consistency of a function like sin matters, not its actual behavior).

How SAT solvers work (34:41)

SMT solvers rely on SAT solvers to handle formulas in conjunctive normal form. A SAT solver picks a variable, guesses a value, propagates the logical consequences through the remaining clauses, and repeats. When it hits a contradiction (a variable forced both true and false), it analyzes which assignments caused it and records a new conflict clause so it never repeats that mistake, continuing until every variable is assigned or a top-level contradiction is proven.

Combining SAT with theory solvers (40:49)

An SMT solver splits a formula's Boolean skeleton from its theory-specific subformulas (such as x > 5), asks the SAT solver for a candidate assignment to the Boolean skeleton, and checks that assignment against a theory solver (for example, a linear arithmetic solver). If the theory solver rejects the assignment, it returns a summary constraint (a conflict) that the SAT solver incorporates before trying again. This back-and-forth continues until a jointly satisfying assignment is found or proven impossible.

From programs to formulas: paths and the heap (54:52)

Because exploring all paths simultaneously does not scale well with modern solvers, most tools explore one path at a time: for a chosen path through the control-flow graph, they build up a symbolic state and an accumulating path condition, checking early whether that condition is still satisfiable so infeasible paths can be pruned without further exploration. The lecture then extends this to programs with heap-allocated memory and pointers, modeling memory as one large array from addresses (just integers) to values, so pointer reads, writes, and arithmetic become array operations that SMT solvers' theory of arrays can reason about directly. A simplified malloc model that ignores freeing and safety regions is shown as a common trade-off between analysis precision and scalability - richer models of library functions catch more bug classes but cost more performance.

Before you watch

• This is a guest lecture within MIT 6.858 on program analysis for security; no earlier lecture is a strict prerequisite, but familiarity with basic programming (branches, pointers, control flow) and discrete math (Boolean logic, conjunctive normal form) helps.
• Some background in what a control-flow graph is will make the path-exploration discussion easier to follow.

Check your understanding

1. Why can testing a program on a handful of concrete inputs never prove a branch is unreachable, while symbolic execution sometimes can?
2. What is a path condition, and why does an unsatisfiable path condition let a tool prune that path without exploring it further?
3. How does an SMT solver divide labor between a SAT solver and a theory solver, and what happens when the theory solver rejects a candidate assignment?
4. Why does choosing between the theory of bit-vectors and the theory of linear integer arithmetic involve a trade-off, particularly with respect to integer overflow?
5. How does modeling the heap as a single large array let symbolic execution reason about pointer reads and writes, and why might a simplified malloc model miss certain classes of bugs?