Under-approximation for Scalable Bug Detection
summary
Presents a concrete under‑approximate program logic, Incorrectness Separation Logic, and an automated analyzer Pulse‑X that targets memory‑safety bugs (null dereference, use‑after‑free, leaks). Pulse‑X is interprocedural, bi‑abductive, uses bounded loop unrolling and branch caps, and is deployed at Meta where it finds real OpenSSL bugs that are fixed; performance is comparable to Infer and fix‑rate sometimes exceeds Infer. Guarantees no false positives by construction except when facing unknown code, imprecise arithmetic solving, or bounded analysis; distinguishes manifest vs latent errors.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:08Speaker introduction
- 2:11Under-approximation in bug detection
- 8:32Incorrectness logic benefits
- 15:57Separation logic extension
- 22:46PulseX under-approximate analysis
- 27:47Memory safety with PulseX
- 33:07Manifest vs latent errors
- 35:37Limitations of under-approximation
- 37:00Concurrency and security extensions
- 39:25Non-termination detection
- 45:05Summary and future work
- 46:52Closing and Q&A
related talks
29mFinding real bugs in big programs with incorrectness logic
19mNon-Termination Proving at Scale
40mBridging the Gap For Security Analysis In Infer
23mAutomatically Detecting Error Handling Bugs Using Error Specifications
18mEnhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach
20mAutomatic and Incremental Repair for Speculative Information Leaks
42mContemporary Automatic Program Analysis
18mPreview: Verification (Correctness & Debugging)