 ICACT20260385 Slide.01
[Big Slide]
[YouTube] |
Chrome  Click!! |
 |
Hi everyone, my name is Hripsime Hovhannisyan. Our presentation today is about Assessing Software Weakness Detection Capabilities: An Empirical Study of IKOS. |
| ICACT20260385 Slide.02
[Big Slide]
|
Chrome Click!! |
 |
The primary goal of this research was to evaluate the capabilities of IKOS—a static analysis tool developed by NASA—specifically in its ability to detect memory-related errors. While these vulnerabilities, such as use-after-free and double-free, are well-known, they remain difficult to catch. We evaluated how a state-of-the-art static analyzer handles these challenges. |
| ICACT20260385 Slide.03
[Big Slide]
|
Chrome Click!! |
 |
To understand why these errors are so dangerous, lets look at this C code snippet. Here, we have a classic bad function that demonstrates a Use-after-free vulnerability in three simple steps.
First, the program allocates memory for an integer using malloc. At this point, ptr owns a specific spot in the memory heap. Second, it performs a free(ptr). This is the correct way to release memory. Even though the memory is released, the variable ptr still holds the memory address. It has now become what we call a Dangling Pointer.
The error occurs at step three. When the program tries to print the value by dereferencing *ptr, by performing an illegal access. While the program might still print 42 by luck, that memory could have already been reassigned to a different, sensitive part of the program. |
| ICACT20260385 Slide.04
[Big Slide]
|
Chrome Click!! |
 |
This slide covers the second major category of memory vulnerabilities: the Double-free error. While it looks similar to the previous example, the impact on the system is quite different.
In this example, we see a typical Double-free scenario. It starts by allocating a small buffer of 10 characters. After checking that the allocation succeeded, the program correctly calls free(str) to release that memory back to the system.
The problem arises later in the programs logic, where free(str) is called a second time on that same pointer. |
| ICACT20260385 Slide.05
[Big Slide]
|
Chrome Click!! |
 |
Beyond the technical errors we just looked at, the real-world impact of these vulnerabilities typically manifests in three critical ways: arbitrary code execution, data corruption, and denial-of-service. Arbitrary code execution is perhaps the most severe, as it allows an attacker to hijack the programs control flow and run malicious commands by exploiting corrupted memory addresses. Alternatively, these bugs can lead to silent data corruption—where the system remains operational but produces incorrect or dangerous results—or a full denial-of-service where the application simply crashes and becomes unavailable. Ultimately, this illustrates that a single improperly managed pointer is not just a minor bug, but a major security gateway that can compromise the entire integrity and availability of a system. |
| ICACT20260385 Slide.06
[Big Slide]
|
Chrome Click!! |
 |
When choosing an analysis method, we face a fundamental trade-off between dynamic and static approaches. Dynamic analysis offers high precision by observing the program during execution, but it suffers from significant performance overhead and can only analyze the specific paths that are actually run. In contrast, static analysis provides full code coverage and allows for the early detection of bugs before the code ever executes. However, this method faces the challenges of false positives and the difficulty of accurately modeling complex memory behaviors, which is exactly why tools like IKOS are so critical to evaluate. |
| ICACT20260385 Slide.07
[Big Slide]
|
Chrome Click!! |
 |
IKOS is a static analyzer that accepts C/C++ source code as input and produces detailed reports on identified bugs as its output. |
| ICACT20260385 Slide.08
[Big Slide]
|
Chrome Click!! |
 |
To address the memory issues weve discussed, we evaluated IKOS, an open-source static analyzer developed by NASA specifically for certifying flight software in avionic systems. Its core strength lies in its foundation of Abstract Interpretation, a mathematical framework that guarantees soundness—meaning if a certain type of error exists, IKOS is mathematically designed to find it.
Architecturally, IKOS is built on the LLVM compiler infrastructure, allowing it to analyze standard C and C++ files as well as LLVM bitcode. Besides that, it uses dynamic inlining and interprocedural analysis, which allows the tool to track data not just within a single block of code, but across multiple functions, providing a more holistic view of the programs behavior. |
| ICACT20260385 Slide.09
[Big Slide]
|
Chrome Click!! |
 |
Flow sensitivity is the analyzers ability to track the specific order of operations. In this example, the pointer a is allocated, freed, and then re-allocated. A flow-insensitive tool might see these conflicting states and miss the bug, but IKOS follows the execution timeline. It understands that even though the pointer was valid at one point, it became invalid again after the second free(), allowing it to correctly flag the final line as a Use-after-free. |
| ICACT20260385 Slide.10
[Big Slide]
|
Chrome Click!! |
 |
Field sensitivity allows the analyzer to distinguish between different fields of a structure. In this example, the struct c2 contains two separate pointers: a and b. A tool without field sensitivity might treat the entire structure as one single block of memory, potentially missing the error. However, IKOS tracks these fields individually. It recognizes that even though c2.b is still valid and safe to use, c2.a has already been freed, allowing the tool to precisely flag the Use-after-free. |
| ICACT20260385 Slide.11
[Big Slide]
|
Chrome Click!! |
 |
Context sensitivity is the analyzers ability to distinguish between different calls to the same function. In this snippet, the function foo is called twice: first with a valid pointer b, and then with a freed pointer a. Without context sensitivity, the tool might get confused and report an error for both calls or neither. IKOS is context sensitive and analyzes foo within the specific context of each call site, correctly identifying that the second call is a Use-after-free while recognizing the first call is safe. |
| ICACT20260385 Slide.12
[Big Slide]
|
Chrome Click!! |
 |
Path sensitivity enables the analyzer to track different execution branches based on specific conditions. In this code, the pointer "a" is used inside an if statement that depends on the value of x. For the path where x is equal to zero, the analyzer recognizes that the pointer "a" is freed and subsequently dereferenced, correctly flagging a use-after-free error. Conversely, it identifies that on the alternate path, the memory remains valid, ensuring that safe operations are not incorrectly reported as bugs. |
| ICACT20260385 Slide.13
[Big Slide]
|
Chrome Click!! |
 |
We did empirical testing to confirm if IKOS actually satisfies these critical properties in practice. To do this, we utilized test cases from the GSAC repository, which has a specialized collection designed to evaluate static analysis sensitivities. Our testing confirms that IKOS successfully satisfies all four requirements: Flow, Field, Context, and Path sensitivity. |
| ICACT20260385 Slide.14
[Big Slide]
|
Chrome Click!! |
 |
To rigorously test IKOS, we used the Juliet Test Suite version 1.3, a massive industry-standard benchmark. We specifically isolated over 1,400 test cases targeting CWE-415 (Double-free) and CWE-416 (Use-after-free). What makes our methodology unique is our strict evaluation criteria: we only counted explicit Errors as True Positives. Any Warnings—where the tool is unsure—were excluded. |
| ICACT20260385 Slide.15
[Big Slide]
|
Chrome Click!! |
 |
Our results from the Juliet Test Suite show that IKOS is an reliable tool. Across all four categories—spanning both C and C++—IKOS achieved a perfect Precision score of 100%. This means that when the tool flagged a bug, it was a confirmed vulnerability every single time, with zero false positives.
Looking at the F1 scores, we see high performance across the board, particularly with Double-Free errors, which reached over 97% in C. While the Recall for C-Use After Free was slightly lower at 78%, this is largely due to our strict methodology of only counting explicit errors. Overall, these metrics demonstrate that IKOS is a highly trustworthy analyzer. |
| ICACT20260385 Slide.16
[Big Slide]
|
Chrome Click!! |
 |
While IKOS achieved perfect precision, it’s just as important to understand the False Negatives—the bugs the tool missed. We identified four main coding patterns that caused these misses.
First, Wide Characters: IKOS failed to detect errors involving wchar_t because it lacks internal library definitions for these specific types. Second, Global Variables proved challenging; if a bugs logic depended on a value stored globally, the tool sometimes lost track of that state.
We also saw issues with Multiple Loops. To prevent the analysis from running forever, IKOS uses a technique called Widening. While this keeps the tool fast, it can sometimes over-generalize a pointers state, causing the tool to miss a specific error. Finally, Complex C++ Containers, like std::vector or std::map, presented lifecycles that were simply too complex for the tools current memory modeling. |
| ICACT20260385 Slide.17
[Big Slide]
|
Chrome Click!! |
 |
To examine the performance of IKOS on real-world vulnerabilities, we collected CVEs from www.cve.org website for each memory error type. To ensure fair evaluation, we searched for CVEs using the respective keywords "use after free" and "double free", sorted the results by date, and sequentially selected the most recent CVEs. |
| ICACT20260385 Slide.18
[Big Slide]
|
Chrome Click!! |
 |
As a result, IKOS can find 1 double-free and 1 use-after-free vulnerability, showing a low 5% detection rate. |
| ICACT20260385 Slide.19
[Big Slide]
|
Chrome Click!! |
 |
In summary, while the evaluation identified critical limitations in detecting memory errors within real-world code patterns, the analyzers strength remains its reliability, evidenced by a zero false positive rate under strict testing conditions on the Juliet Test Suite. To address current deficiencies, future development should prioritize modeling C++ Standard Template Library (STL) internals and refining widening strategies to improve precision across complex loops. |
| ICACT20260385 Slide.20
[Big Slide]
[YouTube] |
Chrome Click!! |
 |
Thank you! |
