Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
Fatimah Aljaafari, Rafael Menezes, Edoardo Manino, Fedor Shmarov, Mustafa Mustafa, Lucas Carvalho Cordeiro · IEEE Access · 2022
Finding software vulnerabilities in concurrent programs is a challenging task due to the size of the state-space exploration, as the number of interleavings grows exponentially with the number of program threads and statements. 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 find software vulnerabilities in concurrent programs. Since there are no publicly-available GBF tools for concurrent code, we first proposeOpenGBF– a new open-source concurrency-aware gray-box fuzzer that explores different thread schedules by instrumenting the code under test with random delays. Then, we build an ensemble of a BMC tool andOpenGBFin the following way. On the one hand, when the BMC tool in the ensemble returns a counterexample, we use it as a seed forOpenGBF, thus increasing the likelihood of executing paths guarded by complex mathematical expressions. On the other hand, we aggregate the outcomes of the BMC and GBF tools in the ensemble using a decision matrix, thus improving the accuracy ofEBF. We evaluateEBFagainst state-of-the-art pure BMC tools and show that it can generate up to 14.9% more correct verification witnesses than the corresponding BMC tools alone. Furthermore, we demonstrate the efficacy ofOpenGBF, by showing that it can find 24.2% of the vulnerabilities in our evaluation suite, while non-concurrency-aware GBF tools can only find 0.55%. Finally, thanks to our concurrency-awareOpenGBF,EBFdetects a data race in the open-sourcewolfMqttlibrary and reproduces known bugs in several other real-world programs, which demonstrates its effectiveness in finding vulnerabilities in real-world software.