💻 computer science

Directed Symbolic Execution for Path Feasibility Analysis]{Directed Symbolic Execution for Path Feasibility Analysis in Software Security Testing

This paper presents a directed symbolic execution method that enhances static security analysis by efficiently verifying interprocedural path feasibility through automated symbolization and loop iteration limits, thereby significantly improving precision while preserving recall on real-world benchmarks.

Original authors: Hovhannes Movsisyan, Hripsime Hovhannisyan, Tigran Avagyan, Hayk Aslanyan

Published 2026-10-22

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Hovhannes Movsisyan, Hripsime Hovhannisyan, Tigran Avagyan, Hayk Aslanyan

Original paper licensed under CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Software security is a constant battle against hidden flaws, much like a city planner trying to ensure every bridge and tunnel in a sprawling metropolis can withstand an earthquake. To do this, engineers use automated tools that scan code without actually running it, mapping out every possible route a program could take. These maps, known as control flow graphs, are incredibly detailed, showing how a program jumps from one instruction to another. However, these maps are often too thorough; they highlight paths that look dangerous on paper but are physically impossible to travel in the real world. This creates a flood of false alarms, forcing human experts to waste time investigating ghosts in the machine. The challenge, then, is to build a system that can quickly distinguish between a path that is merely possible in theory and one that is actually executable, without getting lost in the sheer volume of possibilities.

A team of researchers at the Russian-Armenian University has developed a new method to solve this problem, using a technique called directed symbolic execution. Imagine a traveler trying to verify if a specific route through a complex city exists. A standard approach would be to send out explorers to walk every single street in the city to see where they lead, a task that would take forever and overwhelm the team. Instead, the researchers' method acts like a guided tour. It takes a specific route reported by a security scanner and directs a virtual explorer to follow only that path, ignoring every other street that does not lead to the destination. This "directed" approach allows the system to check if the reported danger is real without wasting energy on irrelevant detours.

The core of this work lies in how the system handles the unknown. In real software, programs often deal with data that hasn't been set yet, or they call functions from outside libraries where the internal code is hidden. A traditional explorer might get stuck or give up when faced with these blanks. The researchers' system, however, is designed to treat these unknowns as flexible variables. If a program reads a memory location that hasn't been filled, the system assigns it a symbolic value, allowing it to explore every possible outcome that value could take. It does the same for the results of external functions and complex pointer arguments, which act like dynamic addresses that can point to different places depending on the situation. By automatically filling in these gaps with possibilities rather than concrete guesses, the system can trace the path through the code even when the full picture isn't visible.

Another major hurdle in navigating software is the loop, a section of code that repeats itself. In a real program, a loop might run a few times or millions of times, and in a symbolic analysis, it can trap the explorer in an infinite cycle. The researchers introduced a strategy to handle this by setting a limit on how many times the system will follow a loop before forcing it to exit. This is not a random cut-off; the system carefully records what happened during those iterations and then jumps to the point where the loop would naturally end. This allows the analysis to continue past the repetitive section without getting stuck, ensuring that the tool can reach the end of the path it is investigating.

To test their method, the team applied it to real-world software and a standard collection of test cases known as the Juliet suite. They first checked their system against paths extracted from the GNU Coreutils, a fundamental set of tools for the Linux operating system. The system successfully verified that 95.3% of these real-world paths were indeed feasible, proving it could handle complex, interwoven code. They then integrated their method with an existing security tool called MLH. Before this addition, the tool flagged 666 false alarms out of thousands of reports. After applying the new path feasibility analysis, those false alarms disappeared completely, while the tool continued to catch every single real vulnerability it had found before. This meant the precision of the security check jumped from 56.6% to 100% on the tested subset, with no loss in the ability to find real bugs.

The researchers also compared their approach against KLEEF, another specialized tool designed for similar tasks. When tested on reports generated by two other major security scanners, Infer and Clang Static Analyzer, the results were stark. KLEEF struggled significantly, failing to verify most of the true positive reports and causing its performance scores to plummet. In contrast, the new method maintained or slightly improved the performance of the original scanners. It successfully verified all the true vulnerabilities reported by the Infer tool and handled the vast majority of the Clang reports, demonstrating that it is robust enough to work with industrial-grade code.

The findings suggest that this directed approach offers a practical way to clean up the noise in software security testing. By focusing only on the paths that matter and automatically handling the complexities of memory and external functions, the method filters out impossible scenarios that waste human time. While the system does make a calculated trade-off by limiting loop iterations to keep things moving, the results show that this does not come at the cost of missing real dangers. The work provides a clear path forward for making automated security tools more reliable, ensuring that when a warning is raised, it is a genuine threat worth investigating.

Technical Summary: Directed Symbolic Execution for Path Feasibility Analysis in Software Security Testing

Problem Statement

Static analysis is a scalable technique for identifying software vulnerabilities by analyzing code without execution. However, a significant limitation of static analyzers is the generation of false-positive reports. These reports often stem from the analysis of infeasible control flow paths—sequences of basic blocks that appear valid in the Interprocedural Control Flow Graph (ICFG) but cannot be executed at runtime due to semantic constraints.

While symbolic execution can theoretically determine the feasibility of such paths by constructing and solving path constraints, its practical application is hindered by the "path explosion" problem. Standard symbolic execution attempts to explore all reachable paths, leading to exponential resource consumption. Furthermore, existing tools often lack the automation required to handle real-world complexities such as uninitialized memory, external function calls, symbolic pointers, and loops without manual intervention or specific instrumentation.

Methodology

The authors propose a Directed Symbolic Execution method designed specifically to verify the feasibility of a pre-defined set of ICFG paths. Unlike traditional symbolic execution that explores the entire state space, this approach directs execution strictly toward a target path, pruning branches unrelated to the verification goal.

Core Algorithm

The algorithm operates on a set of allowed basic blocks ( $S_{allowed}$ ) and a set of required milestones ( $S_{req}$ ) that must be traversed to reach a target block ( $B_{target}$ ).

Directed Pruning: At every branching point, the engine explores a successor block only if it belongs to $S_{allowed}$ . This eliminates the exploration of irrelevant program regions.
Loop Bounding: To prevent non-termination in loops, the method limits the number of loop iterations ( $C_{max}$ ). If a loop exceeds this bound, the engine forces the symbolic state to exit the loop via available exit edges, symbolizing only the memory locations written during the loop's execution. This allows the analysis to continue beyond the loop rather than terminating.
Verification: A path is deemed feasible if the symbolic execution reaches $B_{target}$ having visited all blocks in $S_{req}$ while remaining within $S_{allowed}$ .

Automatic Symbolization Strategies

To enable fully automated analysis without manual configuration, the paper introduces several symbolization approaches:

Entry-Point Parameters: All parameters of the function where the path analysis begins are symbolized, regardless of whether the function is the program's main entry point.
Uninitialized Memory: Uninitialized local variables and dynamically allocated memory regions are treated as symbolic objects with unconstrained values, ensuring that paths dependent on undefined behavior are not prematurely discarded.
External Functions:
- Return Values: Return values from external functions (e.g., dynamic libraries) are symbolized.
- Pointer Arguments: Memory regions referenced by non-constant pointer arguments of external calls are re-symbolized to account for potential side effects.
- Special Globals: Specific handling is applied to errno (re-symbolized after external calls) and environ (modeled as a fixed set of symbolic variables with fixed lengths to avoid non-termination in environment manipulation functions).
Function Pointers and Virtual Functions: The system resolves symbolic function pointers by matching signatures and, for virtual functions, by analyzing virtual tables to identify all possible derived class overrides, forking states for each candidate.

Memory Model

The paper proposes a flexible memory model for symbolic pointers with unknown sizes (e.g., arrays passed to functions). Instead of allocating fixed-size arrays, the model creates memory objects on demand upon the first dereference.

On-Demand Allocation: A memory object is created only when a symbolic pointer is accessed.
Aliasing Resolution: When a pointer is dereferenced, the engine checks for existing memory objects with the same offset. If an alias is possible, the engine forks the symbolic state to explore scenarios where the pointer references an existing object versus a new, distinct memory location. This supports the analysis of complex data structures like linked lists and trees without pre-defined size constraints.

Key Contributions

Directed Symbolic Execution Algorithm: A method to determine the feasibility of specific ICFG paths by restricting exploration to a defined scope.
Fully Automatic Symbolization: Strategies for handling entry-point parameters, uninitialized variables, external function returns, and pointer arguments without user intervention.
Symbolic Memory Modeling: A memory model that supports symbolic pointers and aliasing scenarios, enabling the analysis of arbitrary data structures.
Loop Bounding Strategy: An algorithm that limits loop iterations to ensure termination while allowing symbolic execution to proceed to subsequent code blocks.
Empirical Evaluation: A comprehensive assessment using real-world software (GNU Coreutils) and the NIST Juliet Test Suite.

Experimental Results

The method was implemented as an extension of the KLEE symbolic execution engine (v3.1) and evaluated in three contexts:

Scalability on Real-World Paths:
- Tested on 234 ICFG paths extracted from GNU Coreutils (ranging from 22 to 1,218 basic blocks).
- Achieved a 95.3% recall, successfully verifying 223 paths.
- 49 paths required the loop bounding strategy (threshold set to 3), while 174 were verified without it.
- Execution times varied from under a minute for simple paths to approximately 30 minutes for complex paths involving heavy symbolic pointer arithmetic.
Integration with MLH Static Analyzer:
- Evaluated on the Juliet Test Suite (CWE-401: Memory Leak subset).
- Integration increased the precision of the MLH tool from 56.6% to 100% by filtering out false positives.
- Recall was preserved at 100%, confirming that no true vulnerabilities were discarded.
Comparison with KLEEF:
- Compared against KLEEF (a KLEE derivative for industrial code) using reports from Infer and Clang Static Analyzer (CSA) on Juliet subsets (CWE-415 and CWE-416).
- KLEEF Performance: Significantly degraded performance. For Infer, KLEEF reduced the F1-score from 1.0 to 0.0 (classifying all true positives as infeasible or crashing). For CSA, the F1-score dropped from 0.766 to 0.074.
- Proposed Method Performance: Maintained the baseline F1-scores for Infer (1.0) and slightly improved CSA (0.767). The method successfully verified all true positives and correctly identified feasible paths for false positive reports (which can be further filtered by additional checks).

Significance and Claims

The paper claims that the proposed method effectively bridges the gap between the high precision of symbolic execution and the scalability required for practical software security testing. By directing execution and automating symbolization, the approach successfully filters infeasible paths from static analysis reports, thereby eliminating false positives without sacrificing the detection of true vulnerabilities.

The authors acknowledge that the loop bounding strategy introduces a trade-off between completeness and scalability, potentially allowing some logically unreachable paths to be explored. However, they argue this is an acceptable trade-off in the context of validating static analysis reports, where the priority is ensuring the reachability of the target defect location rather than exhaustive exploration of all loop behaviors. The method is presented as a robust post-processing step that enhances the reliability of existing static analysis tools.