基于SMT的Clang静态分析器中伪漏洞报告反驳
计算机科学中的逻辑
2018-12-03 v2 编程语言
软件工程
摘要
我们描述并评估了Clang静态分析器（CSA）的一个漏洞反驳扩展，该扩展解决了现有内置约束求解器的局限性。具体而言，我们补充了CSA现有的用于移除伪漏洞报告的启发式方法。我们将CSA产生的路径约束编码为可满足性模理论（SMT）问题，使用SMT求解器精确检查其可满足性，并移除那些关联路径约束不可满足的漏洞报告。我们的反驳扩展在12个广泛使用的开源应用中的8个里反驳了伪漏洞报告；平均而言，它反驳了约7%的所有漏洞报告，且从未反驳任何真实漏洞报告。它仅带来可忽略的性能开销，平均使完整Clang/LLVM工具链的运行时长增加1.2%。演示视频见{\tt https://www.youtube.com/watch?v=ylW5iRYNsGA}。
引用
@article{arxiv.1810.12041,
title = {SMT-Based Refutation of Spurious Bug Reports in the Clang Static Analyzer},
author = {Mikhail R. Gadelha and Enrico Steffinlongo and Lucas C. Cordeiro and Bernd Fischer and Denis A. Nicole},
journal= {arXiv preprint arXiv:1810.12041},
year = {2018}
}
备注
4 pages