Read the original article here.

---

Okay, here is the detailed educational resource on Symbolic Execution, reframed for the "Forbidden Code: Underground Programming Techniques They Won’t Teach You in School" context.

---

Symbolic Execution: Navigating the Labyrinth of Code

Welcome, initiates, to a dive into the deeper arts of code analysis – techniques often glossed over in standard curricula, yet essential for anyone seeking to truly understand software behavior, uncover hidden vulnerabilities, or craft sophisticated analysis tools. Today, we peel back the curtain on Symbolic Execution, a powerful method for understanding all possible execution paths a program can take, given any input.

While normal program execution is like walking a single, predetermined path through a maze (driven by specific inputs), symbolic execution is like mapping every single possible path simultaneously. It allows you to ask questions like: "What inputs would make the program reach this specific line of code?" or "Is there any input that could cause this crash?" These are questions vital to security researchers, advanced bug hunters, and those building serious software verification tools – areas residing firmly in the realm of "Forbidden Code."

The Core Ritual: Symbolic vs. Concrete Execution

To grasp symbolic execution, let's contrast it with what you're likely familiar with: concrete execution.

• Concrete Execution: This is standard program execution. You provide specific, concrete values as input (e.g., the number 5, the string "hello"). The program runs, performs computations on these concrete values, and follows a single path determined by the outcomes of conditions (if, while) based on those concrete values. The output is a single result corresponding to that specific input.

• Symbolic Execution: Instead of concrete values, the program is run with symbolic values representing the inputs. These symbols stand for any possible input value. As the program executes, variables and expressions don't hold concrete numbers or strings, but rather expressions involving these symbols. When the execution hits a conditional branch (like if (x > 10)), since x is symbolic, the condition doesn't evaluate to a simple true or false. Instead, the symbolic execution engine understands that both possibilities might be true for some input values. It "forks" the execution path, following both branches.

Symbolic Value: A placeholder representing an unknown input or state value, often denoted by a symbol (e.g., λ, α, Input_X). It stands for any possible concrete value the actual input could take.

Symbolic Expression: A mathematical or logical expression involving symbolic values. As a program executes symbolically, variables hold symbolic expressions derived from the initial symbolic inputs. Example: If input is λ, and y = λ * 2 + 5, then y holds the symbolic expression λ * 2 + 5.

Path Constraint: A logical condition or set of conditions on the initial symbolic inputs that must be true for execution to follow a particular path through the program. These constraints accumulate as symbolic execution traverses conditional branches. Example: If an if (x > 10) branch is taken, the path constraint for that path includes Input_X > 10.

At each conditional branch where the outcome depends on a symbolic value, symbolic execution:

1. Evaluates the condition symbolically, resulting in a symbolic expression (e.g., λ * 2 == 12).
2. Forks into multiple execution paths (typically two for a simple if/else).
3. Assigns a copy of the current program state (symbolic values of variables, memory) to each new path.
4. Adds a new constraint (the condition or its negation) to the set of path constraints for that specific path.

When a symbolic execution path terminates (either normally or due to an error like a crash), the engine has accumulated a complete set of path constraints describing the inputs required to reach that termination point. To find actual concrete inputs that trigger this path, a constraint solver is invoked.

Constraint Solver (or SMT Solver): A powerful tool that takes a set of logical and mathematical constraints involving symbolic variables and determines if there exists a set of concrete values for those variables that satisfies all constraints simultaneously. If a solution exists, it provides those concrete values. If no solution exists, the path is infeasible (cannot be reached by any input).

The constraint solver finds a concrete input (or shows that none exist) that satisfies the accumulated path constraints, revealing exactly what input triggers that specific behavior, whether it's printing "OK" or hitting a dreaded fail() state.

An Illustrative Example: Unmasking the Forbidden Input

Let's look at a simple program that might contain a hidden failure mode:

int main() {
    int y, z;
    // Assume input() reads an integer from the user
    y = input();
    z = y * 2;
    if (z == 12) {
        fail(); // This is the forbidden state we want to find inputs for
    } else {
        print("OK");
    }
    return 0;
}

Concrete Execution (Example Input: 5):

1. y = 5;
2. z = 5 * 2 = 10;
3. if (10 == 12) evaluates to false.
4. The else branch is taken.
5. print("OK");
6. Program exits. Analysis: For input 5, the program is fine. A simple test with 5 tells you nothing about the fail() condition.

Symbolic Execution:

1. Input is a symbolic value, let's call it λ.
2. y = λ; (y now holds symbolic value λ)
3. z = λ * 2; (z now holds symbolic expression λ * 2)
4. Execution reaches if (z == 12), which is if (λ * 2 == 12). The condition is symbolic.
5. Forking occurs:
   • Path 1 (The 'if' branch): Assumes λ * 2 == 12 is true.
     • Current state: y=λ, z=λ * 2.
     • Path constraints: { λ * 2 == 12 }.
     • Execution proceeds into the if block: fail().
     • Path terminates (with failure). The engine takes the path constraints { λ * 2 == 12 } and sends them to the constraint solver.
     • Solver: Finds that λ = 6 satisfies λ * 2 == 12.
     • Result for Path 1: Input 6 leads to the fail() state. Forbidden input found!
   • Path 2 (The 'else' branch): Assumes λ * 2 == 12 is false.
     • Current state: y=λ, z=λ * 2.
     • Path constraints: { λ * 2 != 12 }.
     • Execution proceeds into the else block: print("OK").
     • Path terminates (normally). The engine sends path constraints { λ * 2 != 12 } to the solver.
     • Solver: Finds that any λ not equal to 6 satisfies λ * 2 != 12 (e.g., λ=5, λ=0, λ=-100).
     • Result for Path 2: Any input other than 6 leads to the "OK" state.

Through symbolic execution, without guessing random inputs, we systematically explored both possibilities at the branch and precisely identified the input 6 that triggers the hidden fail() condition. This is the power: systematic exploration and constraint solving to find inputs for any reachable code.

The Serpent's Scales: Challenges of Symbolic Execution

While immensely powerful, symbolic execution isn't a magic bullet. Applying it to large, complex, real-world programs reveals significant challenges, often requiring deep technical knowledge and sophisticated tools to mitigate. These limitations are part of why it remains an "underground" technique for many.

1. Path Explosion: The most notorious challenge. The number of possible execution paths in a program can grow exponentially with the number of conditional branches and loop iterations. A program with just 20 independent binary if statements can have up to 2^20 (over a million) paths. Loops with symbolic bounds can lead to infinitely many paths. Exploring all feasible paths quickly becomes computationally impossible for non-trivial programs.

   • Mitigation Tactics:
     • Heuristics: Instead of brute-forcing all paths, use strategies to guide the exploration towards interesting areas (e.g., prioritizing paths that increase code coverage, paths that reach specific functions, or paths that seem likely to trigger errors).
     • Parallelization: Execute independent paths on different CPU cores or machines.
     • Path Merging: Identify paths that converge or become sufficiently similar (e.g., their states and future constraints are equivalent) and merge their symbolic states to reduce redundancy. Techniques like "veritesting" combine static analysis with dynamic symbolic execution to amplify merging.

2. Program-Dependent Efficiency: Symbolic execution's efficiency comes from analyzing paths rather than individual inputs. If a program is structured such that almost every unique input follows a different path (which is rare, but possible in highly data-dependent control flow), the savings over traditional testing might be minimal. The greatest benefit is found when many diverse inputs exercise the same core logic paths.

3. Memory Aliasing: In languages like C/C++, different pointers or variable names can refer to the same memory location (aliasing). If a symbolic execution engine doesn't correctly identify that *p and array[i] refer to the same memory when p points to array[i], it might miss updates or read stale symbolic values, leading to incorrect analysis. Statically determining all possible aliases is a hard problem.

4. Arrays and Complex Data Structures: Handling operations on arrays or complex structures with symbolic indices or offsets is difficult. If you have A[i], where i is a symbolic value, a read x = A[i] means x could be any element of the array. A write A[i] = value means some element is updated, but which one depends on i. Representing and efficiently reasoning about updates and reads on large arrays with symbolic indices requires advanced techniques (often relying on specific "array theories" within constraint solvers).

5. Environment Interactions (The Untamed Wilderness): Real-world programs don't exist in a vacuum. They interact with the operating system, file system, network, databases, hardware, and external libraries. These external components often perform concrete operations (e.g., writing to a file, making a network request, getting the current time) outside the control and visibility of the symbolic execution engine. How do you handle read(file_descriptor, buffer, count) when the file_descriptor contents are unknown/symbolic or when the read has side effects?

   • Approach 1: Direct Execution: Execute the environment call concretely whenever it's encountered. Simple to implement. Downside: The side effects are concrete and global. If multiple symbolic paths hit a concrete file write, they might all clobber or interfere with each other's view of the file state, destroying the isolation of symbolic paths. This breaks the core premise of exploring independent paths.
   • Approach 2: Modeling the Environment: Create symbolic "models" for critical environment interactions (system calls, library functions). Instead of executing the real call, the engine executes the model, which updates the symbolic state of files, sockets, etc., specific to the current path. Upside: Maintains path isolation and correctness. Downside: Requires writing and maintaining complex symbolic models for a vast number of system and library calls, which is a huge effort. Tools like KLEE often use this approach for common system calls (like file operations).
   • Approach 3: Forking the Entire System State: Run the symbolic execution within a virtual machine or container. When a path forks, fork the entire VM snapshot. Environment interactions still happen concretely within the VM, but each path gets its own isolated copy of the complete system state. Upside: Handles any environment interaction naturally without needing specific models. Much broader compatibility. Downside: High memory and storage overhead due to managing potentially many large VM snapshots. Tools like S2E use this VM-based approach.

Mastering symbolic execution involves understanding these limitations and employing sophisticated techniques to work around them, tailoring the analysis to the specific target program and the desired outcome.

The Forge of Analysis: Tools of the Trade

Developing a robust symbolic execution engine is a significant undertaking, requiring expertise in compilers, operating systems, constraint solving, and program analysis. However, several powerful tools exist that allow practitioners to leverage this technique:

• KLEE: A widely-used symbolic execution engine built on top of the LLVM compiler infrastructure. Known for its focus on finding bugs and generating test cases. It employs environment modeling. (EXE was an earlier version).
• S2E: (Symbolic Execution Engine) Built on the QEMU emulator, S2E forks the entire virtual machine state, offering broad compatibility with arbitrary binaries and complex environment interactions.
• Cloud9 / Otter: Other examples of symbolic execution tools, often built for specific domains or using particular underlying technologies.

These tools are complex frameworks requiring careful setup and configuration, but they provide the necessary infrastructure to perform deep symbolic analysis on real-world software.

Echoes from the Past: A Glimpse at History

The core ideas behind symbolic execution aren't new. They were first explored academically in the 1970s with systems like Select, EFFIGY, DISSECT, and early work by Clarke. The major advances that made it practical for complex programs in recent decades have been driven by vast improvements in computing power and, crucially, the development of highly efficient Satisfiability Modulo Theories (SMT) solvers capable of handling the increasingly complex constraints generated by real-world code.

Related Underground Arts

Symbolic execution is one technique in a family of powerful program analysis methods used in the "forbidden code" landscape:

• Concolic Testing (Concrete + Symbolic): A popular hybrid approach that alternates between concrete execution and symbolic execution. It starts with a concrete input, performs symbolic execution along that single concrete path, collects constraints, and then uses the solver to generate a new concrete input that steers execution down a different path. This iterative process can be more scalable than pure symbolic execution for increasing code coverage.
• Abstract Interpretation: A technique for discovering properties of program execution (like variable value ranges) without executing the program. It's typically faster than symbolic execution but provides less precise results. Often used for high-level analysis or finding potential issues quickly.
• Control-Flow Graph (CFG): A fundamental representation of all possible paths a program can take. Symbolic execution engines heavily rely on CFGs to understand the program structure and identify branching points.
• Symbolic Simulation / Computation: Applying similar symbolic reasoning concepts to hardware design (simulation) or mathematical expressions (computation) respectively.

Conclusion: Embracing the Symbolic Path

Symbolic execution is a formidable technique for anyone seeking to move beyond surface-level code understanding. It provides a systematic way to explore program behavior, find inputs that trigger specific code paths (including those leading to vulnerabilities or crashes), and generate comprehensive test cases.

While challenging due to path explosion, aliasing, and environment interactions, mastering the principles and tools of symbolic execution equips you with the ability to delve into the deepest corners of software, uncover secrets hidden from casual inspection, and understand code in a way few others can. It is a technique for the dedicated few who dare to navigate the full labyrinth of possibility within a program – a true art of the forbidden code.