Lightweight Resource Leak Verification and Inference
summary
Presents a modular, type-based verifier that proves resource-leak absence without whole-program alias analysis by treating leaks as an accumulation property and using annotations like owning and resource aliasing to regain precision. Implementation (Checker Framework RLC; rlcp on CodeQL for C) finds 49 real leaks, runs in minutes where whole-program tools (Grapple) take hours, averages one annotation per 1,500 LOC, and uses optimistic inference that recovers roughly 75–80% of hand-written specs (100% on some C services).
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:03Resource leak problem in Java
- 8:46Detecting resource leaks
- 11:34Sound verification with properties
- 15:49Lightweight ownership
- 18:40Resource aliasing for wrappers
- 23:15Annotations and stub files
- 28:13Evaluation results
- 35:52Manual annotation burden
- 36:56Automated inference
- 41:58Optimistic inference rules
- 43:26Inference results
- 47:19Limitations and future work
- 49:04Conclusion
- 50:07Q&A
related talks
12mLeakage models are a leaky abstraction (...)
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
04mAutomatically Eliminating Speculative Leaks with Blade
20mAutomatic and Incremental Repair for Speculative Information Leaks
30mLightweight Runtime Security Policy Verification Using an Embeddable C++ miniKanren
12mMemory-Safety Verification of Open Programs With Angelic Assumptions
31mA Small Leak Can Sink A Great Ship
17mFoundations for a Rust-Like Borrow Checker for C