一句话：基于不正确性逻辑与分离逻辑的融合 ISL 实现自动分析器 Pulse-X，在 OpenSSL 中发现 15 个真实内存错误。
不正确性逻辑（IL）此前被提出作为组合式证明 bug 存在的逻辑理论，与 Hoare 逻辑对偶，但其能否真正用于开发新分析、在大程序中捕获真实 bug 仍是未决问题。本文基于 IL 与分离逻辑的融合 ISL，实现自动内存错误检测分析 Pulse-X，并针对误报过多的问题提出基于潜在错误（latent）与显式错误（manifest）之分的组合式报错准则，该准则引用 Pulse-X 计算的下近似 ISL 抽象。作者用 Pulse-X 在 OpenSSL 中发现 15 个新的真实 bug，已报告给维护者并得到修复，还分析了该准则带来的修复率；最后与工业界广泛使用的分析器 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.
@article{paperbot1519,
title = {Finding real bugs in big programs with incorrectness logic},
author = {Quang Loc Le and Azalea Raad and Jules Villard and Josh Berdine and Derek Dreyer and Peter W. O'Hearn},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA1},
year = {2022},
doi = {10.1145/3527325}
}