Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs
复制标题
DOI：
10.1109/access.2022.3223359
复制
发表时间：
2022-06
期刊：
影响因子：
3.9
通讯作者：
Fatimah Aljaafari;R. Menezes;Edoardo Manino;F. Shmarov;Mustafa M. Mustafa-Mustafa-M.-Mustafa-2170073934;L. Cordeiro
中科院分区：
文献类型：
--
作者：
Fatimah Aljaafari;R. Menezes;Edoardo Manino;F. Shmarov;Mustafa M. Mustafa-Mustafa-M.-Mustafa-2170073934;L. Cordeiro
在并发程序中发现软件漏洞是一项具有挑战性的任务，因为状态空间探索的规模很大，因为交织的数量随着程序线程和语句的数量呈指数级增长。我们提出并评估了EBF(有界模型检测与模糊集成)--一种结合了有界模型检测(BMC)和灰盒模糊(GBF)来发现并发程序中的软件漏洞的技术。由于目前还没有公开可用的用于并发代码的GBF工具，我们首先提出了OpenGBF--一种新的开源、支持并发的灰盒模糊器，它通过用随机延迟检测被测代码来探索不同的线程调度。然后，我们以以下方式构建BMC工具和OpenGBF的集成。一方面，当集成中的BMC工具返回反例时，我们将其用作OpenGBF的种子，从而增加了执行复杂数学表达式保护的路径的可能性。另一方面，我们使用决策矩阵将BMC和GBF工具的结果聚合在集成中，从而提高了EBF的准确性。我们对比最先进的纯BMC工具对EBF进行了评估，结果表明，与相应的BMC工具相比，EBF可以生成高达14.9%的正确验证证人。此外，我们还展示了OpenGBF的有效性，它可以发现我们评估套件中24.2%的漏洞，而非并发感知的GBF工具只能找到0.55%。最后，由于我们的并发感知OpenGBF，EBF可以检测到开源wolfMqtt库中的数据竞争，并在其他几个真实世界的程序中复制已知的错误，这证明了它在发现现实世界软件中的漏洞方面的有效性。
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 propose OpenGBF – 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 and OpenGBF in the following way. On the one hand, when the BMC tool in the ensemble returns a counterexample, we use it as a seed for OpenGBF, 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 of EBF. We evaluate EBF against 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 of OpenGBF, 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-aware OpenGBF, EBF detects a data race in the open-source wolfMqtt library and reproduces known bugs in several other real-world programs, which demonstrates its effectiveness in finding vulnerabilities in real-world software.