In SAST (static application security testing), source code is analyzed without being executed. SAST can be used to detect buffer overflows, injection flaws, and other common vulnerabilities that attackers could exploit. SAST is a fast, cost-effective, and scalable approach to security testing; however, it is not without its flaws. Many SAST tools are considered “noisy”: their high false-positive rate often results in hours of sifting to discover one notable finding. This blog post explores the limits of SAST – why this high false-positive rate exists and how we can combat it.

We will explore an example where SAST fails to report a memory-safety issue, illustrating how runtime behavior (unknown before execution) can influence the presence and detectability of certain vulnerabilities. We illustrate how symbolic execution is a powerful alternative approach to software vulnerability detection, especially in cases where SAST falls short.

Static Analyzers

We will be experimenting with two static analysis tools: Cppcheck and Snyk Code. Cppcheck detects a slew of syntax issues and software vulnerabilities in C/C++ source code. Cppcheck reports array index out of bounds exceptions, which will be our focus. Snyk Code also reports array index out of bounds exceptions, labeling them as “User Controlled Pointers”.

These two static analysis tools were selected not because they are weak examples. Quite the contrary, these tools are some of the best SAST performers available in both the open source and commercial market today. Cppcheck has been downloaded from SourceForge over 800,000 times. Snyk is used by over a million developers.

Symbolic Executor

We will compare static analysis against symbolic execution: a software testing technique that substitutes normal inputs into a program for symbolic values. This lets a symbolic executor model the program’s dynamic runtime behavior, simulating the paths of execution the program could take under different user-input conditions. Symbolic execution can be used to explore a set of possible states the program can be in, determining if any of these states are vulnerable, behave in an undefined manner, or violate memory safety.

The symbolic executor we will be experimenting with is ObjectSecurity’s BinLens (Formerly ObjectSecurity OT.AI Platform). BinLens uses symbolic execution to explore, detect, and report vulnerable program states. Like Cppcheck and Snyk, BinLens can find array index out of bounds exceptions (also called CWE-129: Improper Validation of Array Index).

Samples

We have created two small program samples with which SAST and symbolic execution will be compared. The first sample is called detected.c, and contains a hard-coded array index out of bounds exception:

void foo(int x) {
    char buf[10];
    buf[x] = 'D'; // <- ERROR
    printf("%c", buf[x]);
}

int main() {
    foo(64);
}

The buf buffer contains 10 characters and is therefore 10 bytes long. The program writes the character ‘D’ to index 64 of the buffer. Index 64 is outside of the bounds of the buffer; buf should be indexed using 0-9 (arrays start at 0).

The second sample is called undetected.c, and also contains an array index out of bounds exception, albeit under different conditions:

void foo(int x) {
    char buf[10];
    buf[x] = 'D'; // <- ERROR
    printf("%c", buf[x]);
}

int main(int argc, char** argv) {
    if (argc != 2) {
        return 0;
    }
    foo(atoi(argv[1]));
}

In this sample, the index ‘D’ is written to within buf is determined by user input, as a command line argument. The index chosen is arbitrary: it may be within the allowed bounds of buf (0-9), or outside of them, comprising a memory-safety violation.

Findings

Running Cppcheck on detected.c yields the following findings:

$ cppcheck detected.c
Checking detected.c ...
detected.c:6:8: error: Array 'buf[10]' accessed at index 64, which is out of bounds. [arrayIndexOutOfBounds]
    buf[x] = 'D'; // <- ERROR
       ^
detected.c:11:9: note: Calling function 'foo', 1st argument '64' value is 64
    foo(64);
        ^
detected.c:6:8: note: Array index out of bounds
    buf[x] = 'D'; // <- ERROR
       ^
detected.c:7:21: error: Array 'buf[10]' accessed at index 64, which is out of bounds. [arrayIndexOutOfBounds]
    printf("%c", buf[x]);
                    ^
detected.c:11:9: note: Calling function 'foo', 1st argument '64' value is 64
    foo(64);
        ^
detected.c:7:21: note: Array index out of bounds
    printf("%c", buf[x]);
                    ^

Cppcheck successfully detects the array index out of bounds issue, even associating it with the index 64. However, running Cppcheck on undetected.c only yields the following:

$ cppcheck undetected.c
Checking undetected.c ...

The output from Cppcheck ends here: no results were found. Why is this? Because Cppcheck (and static analysis generally) cannot predict what value(s) the user will enter on the command line. This input is determined dynamically, at runtime.

Using symbolic execution, BinLens can find the array index out of bounds exception, because during symbolic execution, unconstrained user inputs like this are considered and modeled appropriately.

To analyze undetected.c using BinLens, we must first compile the file to undetected.out, as BinLens expects a binary file as input. Then, running BinLens against undetected.out yields the following result:

Moving on to Snyk: it seems to be incapable of detecting the vulnerability in detected.c, but capable of detecting the vulnerability in undetected.c, reporting it as a “User Controlled Pointer”:

Snyk analyzes multiple files at once: both detected.c and undetected.c were analyzed in the test shown above. No findings were produced for detected.c.

In undetected.c, Snyk correctly determines that an argument from the command line is used to access and write a value to a buffer. Tracking how untrusted input flows throughout a program is an approach commonly called taint analysis or taint checking and can be used to great effect for detecting vulnerabilities. Note however that Snyk states “…an attacker might be able to control where the pointer is pointing…”. All Snyk knows is that an untrusted pointer reaches a buffer, not that the buffer is accessed in a vulnerable manner. We can demonstrate this by modifying undetected.c slightly:

Now, although the program still uses a user-controlled pointer to modify the buffer, the access to this buffer is bounded between only allowable values (indices 0-9 specifically). The program is no longer vulnerable, yet Snyk still reports the “User Controlled Pointer” as a Medium-tier issue:

This shows that Snyk does not actually check to see if the value from the command line can be used in a dangerous way, just that this value can be used in general. This understandably results in many false positive results. Analyzing the new, safe version of undetected.c with BinLens produces proper results: not reporting any false positives.

Conclusion

SAST succeeds in providing fast, cost-effective results that aid developers in identifying and fixing syntax issues in their source code. However, because the input a user provides to a program cannot be predicted before runtime, SAST is limited in what it can accomplish. SAST doesn’t account for the full picture. Symbolic execution, although more performance intensive, considers user input conditions and how they can affect a program’s state, ultimately supporting the identification of a larger set of vulnerabilities with a higher degree of accuracy.

ObjectSecurity’s BinLens (formerly ObjectSecurity OT.AI Platform) utilizes symbolic execution to detect memory-safety violations such as stack-based buffer overflow, heap-based buffer overflows, double-frees, and others. ObjectSecurity’s BinLens (formerly ObjectSecurity OT.AI Platform) performs post-build binary analysis, inspecting a program’s runtime behavior as it would occur on the CPU. By inspecting the “ground-truth” of program behavior in this way, BinLens can find the tricky vulnerable states missed by most SAST tools. BinLens’ vulnerability analysis capabilities can be integrated directly into your CI/CD pipeline.