Finding real bugs in big programs with incorrectness logic

File Description SizeFormat 
3527325.pdfPublished version789.99 kBAdobe PDFView/Open
Title: Finding real bugs in big programs with incorrectness logic
Authors: Le, QL
Raad, A
Villard, J
Berdine, J
Dreyer, D
O'Hearn, PW
Item Type: Journal Article
Abstract: 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.
Issue Date: 29-Apr-2022
Date of Acceptance: 1-Apr-2022
URI: http://hdl.handle.net/10044/1/97408
DOI: 10.1145/3527325
ISSN: 2475-1421
Publisher: Association for Computing Machinery (ACM)
Start Page: 1
End Page: 27
Journal / Book Title: Proceedings of the ACM on Programming Languages
Volume: 6
Issue: OOPSLA1
Copyright Statement: © 2022 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
Sponsor/Funder: UK Research and Innovation
Funder's Grant Number: MR/V024299/1
Publication Status: Published
Open Access location: https://doi.org/10.1145/3527325
Online Publication Date: 2022-04-29
Appears in Collections:Computing



This item is licensed under a Creative Commons License Creative Commons