Questions: Symbolic Execution (Advanced)

Question 1

Path explosion in symbolic execution occurs because the number of paths grows exponentially with branches. A simple mitigation is state merging: combine multiple symbolic states that have reached the same program point. What does merging involve?

Model answer: State merging combines multiple states (with potentially different path constraints) into a single merged state. If one path has constraint C1 and another has constraint C2, the merged state has constraint (C1 OR C2). The merged state represents all paths that converged at that point. The tradeoff is that merged constraints become more complex (disjunctions are harder for SMT solvers than conjunctions), but fewer states are tracked overall. This reduces memory and exploration time, though some paths may be redundantly explored if the merged constraint is satisfiable in multiple ways.

State merging is a classic technique in program analysis. Instead of exploring one path with constraint {x > 5} and another with constraint {x <= 5} independently, you merge them into a single state with constraint {(x > 5) OR (x <= 5)} — which simplifies to true (always satisfiable). This reduces the state space, but if the merged constraint is complex, the SMT solver may take longer to solve it. The optimal choice of when to merge is a research problem: merge too aggressively and the SMT solver bogs down; merge too conservatively and you re-explore redundant paths.

Question 2

Directed symbolic execution prioritizes exploration toward a goal (e.g., reaching a specific program point or finding a specific bug). How does this differ from undirected symbolic execution?

Model answer: Undirected symbolic execution explores paths in some order (depth-first, breadth-first, coverage-driven) without targeting a specific goal. Directed symbolic execution assigns each state a distance or priority based on proximity to a goal. Heuristics might include: shortest path to the goal in the control flow graph, estimated distance in terms of branches, or anomaly likelihood (regions more likely to contain bugs). The executor prioritizes high-priority states, focusing computation on paths most likely to reach the goal. This is particularly effective when searching for specific vulnerabilities (division by zero at line 42) or maximizing coverage of a particular code region.

Directed symbolic execution brings goal-oriented search to program analysis. In security testing, you might direct execution toward potential vulnerabilities (null pointer dereferences, buffer overflows). In fuzzing, you direct it toward uncovered branches. The heuristics guide the search without guaranteeing the goal is reached, but they often dramatically reduce exploration time by avoiding irrelevant paths. This is the key to making symbolic execution practical on real code: instead of exploring all paths (infeasible), explore the most promising ones.

Question 3

Interprocedural symbolic execution reasons about programs with function calls. A naive approach is to inline all called functions, unrolling them completely. Why is this problematic for scalability?

• A. Inlining increases code size linearly with the number of calls
• B. If a function is called multiple times, inlining duplicates the exploration effort for each call. For recursive functions, inlining can be infinite. This leads to exponential blowup in the number of paths. Using function summaries instead allows the executor to reuse analysis results across multiple calls to the same function
• C. Inlining is not problematic
• D. Inlining prevents the SMT solver from running

Answer: (B)

Function inlining is simple but scales poorly. If a function f calls g which calls h, and you inline all calls, you get a monolithic expression with all the branches of h and g. If f is called 100 times and each call inlines g, and g calls h, you've explored the path through h one hundred times redundantly. Interprocedural analysis uses function summaries: after exploring all paths through g once, you save a summary (the mapping from inputs to possible outputs), and reuse this summary on subsequent calls to g. This amortizes the exploration cost across all calls.

Question 4

Whole-system symbolic execution (S2E) combines symbolic execution at the application level with OS-level analysis. What does this enable that application-level symbolic execution alone cannot?

Model answer: Application-level symbolic execution treats the OS as a black box — OS calls are modeled or stubbed out, not symbolically executed. Whole-system symbolic execution instruments the OS kernel itself, so system calls (open, read, write, fork, mmap) are symbolically executed alongside the application. This allows testing of: system call interaction bugs, race conditions involving the kernel, behavior depending on OS scheduling, and bugs in drivers and kernel modules. By symbolically executing the entire stack, whole-system analysis discovers bugs that OS-level or application-level analysis alone would miss.

This is a paradigm shift in scope. Traditional symbolic execution asks: 'What paths can the program take given all possible inputs?' Whole-system symbolic execution asks: 'What paths can the program and OS take given all possible inputs AND all possible system call returns AND all possible scheduling interleavings?' The added complexity is substantial, but the bugs found are often in the boundary between application and OS — race conditions, resource exhaustion, or incorrect assumptions about OS behavior. Tools like S2E and TriforceAFL use this approach to test entire software stacks including hypervisors, kernels, and user applications.