Finding real bugs in big programs with incorrectness logic
Finding real bugs in big programs with incorrectness logic
复制标题
通过不正确的逻辑在大型程序中查找真正的错误
DOI：
10.1145/3527325
复制
发表时间：
2022
影响因子：
--
通讯作者：
Le Q
中科院分区：
文献类型：
--
作者：
Le Q
不正确逻辑(IL)最近作为一种逻辑理论被提出，用于从成分上证明错误的存在--对偶到Hoare逻辑，后者被用来从成分上证明错误的存在。尽管IL在很大程度上是为了为错误捕获程序分析提供一个逻辑基础，但它仍然是一个悬而未决的问题：IL是只用于回溯(解释现有分析)，还是实际上在开发能够捕获大型程序中真实错误的新分析时有用？在这项工作中，我们开发了Pulse-X，这是一种新的、自动的程序分析，用于捕获内存错误，基于ISL，它是IL和分离逻辑的最新综合。使用Pulse-X，我们在OpenSSL中发现了15个新的真实错误，我们已经向OpenSSL维护人员报告了这些错误，并已修复。为了不被潜在的错误报告淹没，我们提出了一种基于潜在错误和显性错误区分的组合错误报告标准，该标准参考了Pulse-X计算的欠近似ISL抽象，并研究了该标准的应用所产生的固定率。最后，为了探索我们的缺陷发现方法的潜在实用性，我们将其与在工业工程实践中被证明有用的广泛使用的分析器INFER进行了比较。
Incorrectness Logic (IL) has recently been advanced as a logical theory for compositionally proving the presence of bugs—dual to Hoare Logic, which is used to compositionally prove their absence. Though IL was motivated in large part by the aim of providing a logical foundation for bug-catching program analyses, it has remained an open question: is IL useful only retrospectively (to explain existing analyses), or can it actually be useful in developing new analyses which can catch real bugs in big programs?In this work, we develop Pulse-X, a new, automatic program analysis for catching memory errors, based on ISL, a recent synthesis of IL and separation logic. Using Pulse-X, we have found 15 new real bugs in OpenSSL, which we have reported to OpenSSL maintainers and have since been fixed. In order not to be overwhelmed with potential but false error reports, we develop a compositional bug-reporting criterion based on a distinction between latent and manifest errors, which references the under-approximate ISL abstractions computed by Pulse-X, and we investigate the fix rate resulting from application of this criterion. Finally, to probe the potential practicality of our bug-finding method, we conduct a comparison to Infer, a widely used analyzer which has proven useful in industrial engineering practice.
登录
查看更多内容
DOI：
10.1109/icst.2015.7102580
发表时间：
2015-04
期刊：
2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST)
影响因子：
--
作者：
M. Harman;Yue Jia;Yuanyuan Zhang
通讯作者：
M. Harman;Yue Jia;Yuanyuan Zhang
DOI：
--
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Fraser Brown;D. Stefan;D. Engler
通讯作者：
Fraser Brown;D. Stefan;D. Engler
DOI：
10.1007/978-3-030-53291-8_14
发表时间：
2020-06-16
期刊：
Computer Aided Verification
影响因子：
--
作者：
Raad A;Berdine J;Dang HH;Dreyer D;O’Hearn P;Villard J
通讯作者：
Villard J
Gillian，第一部分：用于符号执行的多语言平台
DOI：
10.1145/3385412.3386014
发表时间：
2020
期刊：
--
影响因子：
--
作者：
Fragoso Santos J
通讯作者：
Fragoso Santos J
使用用于测试输入生成的分离逻辑增强基于堆的程序的符号执行
DOI：
10.1007/978-3-030-31784-3_12
发表时间：
2017
期刊：
Inf. Softw. Technol.
影响因子：
--
作者：
Long H. Pham;Quang Loc Le;Quoc;Jun Sun;S. Qin
通讯作者：
S. Qin