 ICACT20260382 Slide.01
[Big Slide]
[YouTube] |
Chrome  Click!! |
.jpg) |
Hello everybody, my name is Hovhannes. I am a researcher at Center of Advanced Software Technologies. My presentation is about control flow path feasibility analysis through symbolic execution.
|
| ICACT20260382 Slide.02
[Big Slide]
|
Chrome Click!! |
 |
Often, static analyzers report issues without performing path sensitive analysis. For example, a tool might flag a NULL dereference on line 8, but in reality, that path is logically impossible—making it a false positive. This highlights why path feasibility analysis is so critical: it allows us to filter out these non-existent issues and focus only on real bugs.
|
| ICACT20260382 Slide.03
[Big Slide]
|
Chrome Click!! |
 |
Determining whether a control flow path is feasible is a critical challenge in program analysis, and it serves several purposes. First, it is essential for reducing false positives provided by static analysers. Second, it can be used to verify that there is no feasible path leading to problematic program points. Finally, it enables dead path elimination.
|
| ICACT20260382 Slide.04
[Big Slide]
|
Chrome Click!! |
 |
So, the goal of this work is to check the feasibility of the given control flow path.
To achieve this, we introduce a solution powered by symbolic execution. |
| ICACT20260382 Slide.05
[Big Slide]
|
Chrome Click!! |
 |
Now, let’s talk about symbolic execution. What is symbolic execution?
|
| ICACT20260382 Slide.06
[Big Slide]
|
Chrome Click!! |
 |
It’s an analysis technique that uses symbolic variables instead of fixed, concrete values. |
| ICACT20260382 Slide.07
[Big Slide]
|
Chrome Click!! |
 |
As the program runs, it translates the code’s logic into a system of mathematical equations and inequalities. By solving these using SMT solvers, we can automatically identify every possible execution path and the exact inputs needed to reach them. |
| ICACT20260382 Slide.08
[Big Slide]
|
Chrome Click!! |
 |
Let’s look at this example. On line 3, the make symbolic call transforms variable a into a symbolic value. This allows the symbolic executor to explore all three execution paths. For instance, it might generate one input where a is 0, another where its 20, and a third where its 10—effectively covering every possible branch of the code. |
| ICACT20260382 Slide.09
[Big Slide]
|
Chrome Click!! |
 |
Here, we can compare a feasible path with an infeasible one. In the first example, the highlighted lines show a clear, valid route to line 6. However, in the second example, line 5 is unreachable because the conditions on lines 3 and 4 are logically contradictory. Our primary goal is to use symbolic execution to determine path feasibility. |
| ICACT20260382 Slide.10
[Big Slide]
|
Chrome Click!! |
 |
Here is how our algorithm works. We start symbolic execution at the beginning of the path, treating the initial function arguments as symbolic variables. To stay focused, we prune any branches that lead outside our target path, preventing unnecessary execution. If the execution reaches the endpoint and verifies that every required block was executed, it reports the path as feasible. However, if the execution finishes without reaching the endpoint—or if blocks are skipped—we know the path is infeasible. |
| ICACT20260382 Slide.11
[Big Slide]
|
Chrome Click!! |
 |
To achieve full automation, we’ve developed a suite of automatic symbolization techniques. These allow the system to handle unknowns without manual intervention—including function parameters, external return values, and reference arguments. Crucially, it also manages uninitialized memory and pointer-referenced locations. |
| ICACT20260382 Slide.12
[Big Slide]
|
Chrome Click!! |
 |
To understand the automatic symbolization approaches, lets discuss the following examples.
First, we have an uninitialized local variable, a, on line 2. According to C and C++ standards, its value is indeterminate. To ensure the executor can explore every possible path, our approach automatically marks these uninitialized variables as symbolic.
Second, in this example, we see a function call where the source code isnt available to the executor. In these cases, our method automatically symbolises the return value.
Finally, consider a symbolic pointer, p. Rather than allocating memory undera pointer, we use a lazy approach. When the code accesses an index—like p[5] on line 2—we create a single symbolic memory object. This specific object is then used for any subsequent operations. |
| ICACT20260382 Slide.13
[Big Slide]
|
Chrome Click!! |
 |
We implemented our method within the KLEE symbolic execution engine, which is built on the LLVM compiler infrastructure for C and C++. The algorithms and methods are implemented using KLEE and LLVM API. |
| ICACT20260382 Slide.14
[Big Slide]
|
Chrome Click!! |
 |
To evaluate our method, we integrated it into Memory Leak Hunter, a static analyzer designed for memory leak detection. Path feasibility analysis provides path sensitivity for Memory Leak Hunter. |
| ICACT20260382 Slide.15
[Big Slide]
|
Chrome Click!! |
 |
We evaluated the effectiveness of our approach using the Juliet Test Suite, comparing Memory Leak Hunter both with and without path verification. The results were clear: by applying our path feasibility method, we were able to filter out all false positives and keep all true positives. |
| ICACT20260382 Slide.16
[Big Slide]
|
Chrome Click!! |
 |
When we look at the core metrics—Precision, Recall, and the F1-score—the results are exceptional. On the Juliet test suite, Memory Leak Hunter with path feasibility achieved a perfect score of 1.0 across all categories. |
| ICACT20260382 Slide.17
[Big Slide]
|
Chrome Click!! |
.jpg) |
Moving on to the computational costs, lets look at how path feasibility impacts our Juliet test suite benchmarks.
In terms of speed, we see a 10% time overhead. The memory overhead is roughly 80%. While that might sound high at first glance, its important to remember that these percentages are relative to the Memory Leak Hunter performance. For this specific test suite, 80% is actually well within an acceptable range.
Furthermore, the process is highly scalable. If MLH identifies multiple issues, we can run the path feasibility analysis for each one in parallel. |
| ICACT20260382 Slide.18
[Big Slide]
|
Chrome Click!! |
 |
Beyond tests, we evaluated the integration on several real-world projects. Every report presented here was accepted by the project maintainers. |
| ICACT20260382 Slide.19
[Big Slide]
|
Chrome Click!! |
.jpg) |
So, in this work, we have introduced several methods for enhancing symbolic execution to support fully automatic control-flow path feasibility analysis. By developing automatic symbolization techniques for variables with unknown values, function arguments, return values, and pointer-referenced memories, we have developed a control flow path verification algorithm. |
| ICACT20260382 Slide.20
[Big Slide]
|
Chrome Click!! |
 |
As loops often lead to the path explosion problem in symbolic execution, our future research will focus on mitigating the path explosion problem caused by loops, exploring loop abstraction and induction techniques to keep symbolic execution tractable. We also plan to investigate advanced path-selection heuristics to prioritize high-probability branches and reach the paths endpoint faster. |
| ICACT20260382 Slide.21
[Big Slide]
|
Chrome Click!! |
 |
Thank you for your attention! Any questions?
|
