Finding real bugs in big programs with incorrectness logic
summary
Pulse-X applies ISL (a synthesis of Incorrectness Logic and separation logic) to build an automatic under-approximate analyzer for memory errors, inferring function summaries compositionally and classifying reports as latent vs manifest errors to reduce false positives. It finds 15 real OpenSSL bugs that are reported and fixed, scales to tens of thousands of functions and whole repositories in under 30 minutes, and compares favorably in precision and scalability to Infer while explicitly leveraging Pulse-X’s ISL-based proofs and a compositional reporting criterion.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:19Presentation
- 3:37Overview
- 5:05Foundations
- 7:17Choice
- 7:58Analysis
- 11:18Inference
- 13:19Mercury Blockchain
- 17:15Implementation Evaluation
- 23:16Conclusion
related talks
59mUnder-approximation for Scalable Bug Detection
40mBridging the Gap For Security Analysis In Infer
42mContemporary Automatic Program Analysis
23mAutomatically Detecting Error Handling Bugs Using Error Specifications
16mFIXX: FInding eXploits from eXamples
24mSymbiotic: finding bugs in C programs
34mHow To Find And Prevent Entire Classes Of Security Vulnerabilities
40mEnterprise-scale static analysis: A Pinpoint experience