Automated bug-finding tools such as KLEE have achieved mainstream success over the last decade, and have proved capable of finding deep bugs even in programs that have received significant manual testing. Some recent works have demonstrated techniques for finding bugs in these bug-finding tools themselves; however, it remains unclear whether these correctness issues have any practical impact on their ability to uncover serious bugs. In this paper, we study this issue by conducting experiments with KLEE 1.4 and 2.2 on several corpora of memory safety bugs. Using automated bug injection, we can automatically find false negatives (i.e., bugs missed by KLEE); moreover, because the bugs we inject come with triggering inputs, we can then use concolic execution to tell which bugs were missed due path explosion and which are caused by soundness issues in KLEE. Our evaluation uncovers several sources of unsoundness, including a limitation in how KLEE detects memory errors, mismatches in the modeling of the C standard library, lack of support for floating point and C++, and issues with calls to external functions. Our results suggest that bug injection and other synthetic corpora can help highlight implementation issues in current tools and illuminate directions for future research in automated software engineering.

Use-after-free (UAF) vulnerabilities, in which dangling pointers remain after memory is released, remain a persistent problem for applications written in C and C++. In order to protect legacy code, prior work has attempted to track pointer propagation and invalidate dangling pointers at deallocation time, but this work has gaps in coverage, as it lacks support for tracking program variables promoted to CPU registers. Moreover, we find that these gaps can significantly hamper detection of UAF bugs: in a preliminary study with OSS-Fuzz, we found that more than half of the UAFs in real-world programs we examined (10/19) could not be detected by prior systems due to register promotion. In this paper, we introduce HeapExpo, a new system that fills this gap in coverage by parsimoniously identifying potential dangling pointer variables that may be lifted into registers by the compiler and marking them as volatile. In our experiments, we find that HeapExpo effectively detects UAFs missed by other systems with an overhead of 35% on the majority of SPEC CPU2006 and 66% when including two benchmarks that have high amounts of pointer propagation.