结合有界模型检验与模糊测试技术发现并发程序中的软件漏洞
软件工程
2022-10-21 v4 系统与控制
系统与控制
摘要
由于状态空间探索的规模随程序线程和语句数量呈指数增长，在并发程序中寻找软件漏洞是一项具有挑战性的任务。我们提出并评估了 EBF（有界模型检验与模糊测试的集成）——一种结合有界模型检验（BMC）与灰盒模糊测试（GBF）以发现并发程序中软件漏洞的技术。由于目前没有公开可用的面向并发代码的 GBF 工具，我们首先提出 OpenGBF——一个新的开源并发感知灰盒模糊器，通过对被测代码插入随机延迟来探索不同的线程调度。随后，我们以如下方式构建 BMC 工具与 OpenGBF 的集成。一方面，当集成中的 BMC 工具返回反例时，将其用作 OpenGBF 的种子，从而提高执行由复杂数学表达式守护的路径的可能性。另一方面，我们使用决策矩阵聚合集成中 BMC 与 GBF 工具的结果，从而提升 EBF 的准确率。我们将 EBF 与最先进的纯 BMC 工具进行对比评估，结果表明其生成的正确验证见证比单独的相应 BMC 工具最多多 14.9%。此外，我们展示了 OpenGBF 的有效性：其能发现评估套件中 24.2% 的漏洞，而非并发感知的 GBF 工具仅能发现 0.55%。最后，得益于我们的并发感知 OpenGBF，EBF 检测到了开源 wolfMqtt 库中的数据竞争，并复现了多个其他真实程序中的已知缺陷，证明了其在发现真实世界软件漏洞上的有效性。
引用
@article{arxiv.2206.06043,
title = {Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent Programs},
author = {Fatimah K. Aljaafari and Rafael Menezes and Edoardo Manino and Fedor Shmarov and Mustafa A. Mustafa and Lucas C. Cordeiro},
journal= {arXiv preprint arXiv:2206.06043},
year = {2022}
}