Black-Box Cooperative Verification Framework for Finding Software Vulnerabilities in Concurrent Programs

Abstract

Detecting software vulnerabilities in concurrent programs poses a significant challenge due to the extensive state-space exploration required, with interleavings growing exponentially as the number of program threads and statements increases. Combining different verification and testing techniques, at least in theory, achieves better results than individual use. In theory, combining different verification and testing techniques to detect software vulnerabilities can improve results compared to using them individually. We propose and evaluate EBF (Ensembles of Bounded Model Checking with Fuzzing) – a technique that combines Bounded Model Checking (BMC) and Gray-Box Fuzzing (GBF) to detect software vulnerabilities in concurrent programs. Given the lack of publicly available GBF tools for concurrent programs, we first propose OpenGBF, a new open-source concurrency-aware gray-box fuzzer that explores different thread interleavings by instrumenting the program under test (PUT) with random delays. Then, we develop a cooperative framework that combines the BMC tool and OpenGBF as follows. On the one hand, we force the BMC tool to provide seed values to OpenGBF by injecting additional vulnerabilities (error statements) in the PUT, thus increasing the likelihood of OpenGBF executing paths guarded by complex mathematical expressions. On the other hand, we aggregate the results of the BMC and OpenGBF tools in the framework using a decision matrix, thus improving the accuracy of EBF. We evaluate the performance of EBF compared to state-of-the-art pure BMC tools and demonstrate that it can produce up to 14.9% more correct witnesses than the corresponding BMC tools alone. Moreover, we show the effectiveness of OpenGBF by illustrating its capability of finding 41.9% of the vulnerabilities within our evaluation suite, while non-concurrency-aware GBF tools can only find 0.55%. Finally, thanks to our concurrency-aware OpenGBF, EBF successfully detects a data race in the open-source wolfMqtt library and reproduces known bugs in several other real-world concurrent programs, which shows its efficacy in finding vulnerabilities in real-world concurrent software.