Bridging the Gap For Security Analysis In Infer
summary
Infer gets extended with pulse infinite, an under-approximate termination checker built on Pulse and Infer’s separation-logic core that analyzes millions of lines in minutes. Implementation adds raw path equations, k-bounded unrolling and a widen-state hash to detect lassos; evaluation finds 21 bugs with ~30% signal rate so far. Work exposes missing support for bounded integer/bit arithmetic and recursive nontermination and shows the extension is fast and practically effective.
AI-written summary · about
chapters (10)
- 0:00Infer security analysis intro
- 2:10Non-termination bugs matter
- 7:34Pulse Infinite and HTER logic
- 10:47Real-world non-termination bugs
- 17:43Pulse Infinite implementation
- 19:13Future Infer improvements
- 25:39Integer overflow challenges
- 31:00Scalability and evaluation
- 33:27Future plans and open-source
- 34:30Q&A
related talks
59mUnder-approximation for Scalable Bug Detection
19mNon-Termination Proving at Scale
29mFinding real bugs in big programs with incorrectness logic
24mInception: System-Wide Security Testing of Real-World Embedded Systems Software
31mEthainter: A Smart Contract Security Analyzer for Composite Vulnerabilities
01h 05mTheory and Security
26mVerification of Programs with Concealed Components
18mEnhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach