Lightweight Shape Analysis based on Physical Types
summary
Defines a new abstract-interpretation memory analysis that summarizes the heap with physical types encoding byte-level layouts and pairs that with a focusing abstraction to refine active regions and enable strong updates without disjunctions. Implements the domain in the Codex library and runs it on standard shape benchmarks and a full commercial microkernel, proving spatial memory safety and absence of privilege escalation on the kernel binary with few annotations and practical runtime.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:10Why Do We Need Automatic Memory Analysis
- 3:13Abstract Interpretation Based on Types
- 13:03Structural Environments
- 18:04Experiments
- 19:17Benchmarks
- 21:37Conclusion
related talks
01h 02mThe MemCAD static analyser: shape, value and collection abstraction and application to(…)
34mSymbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
38mTaking Kernel Hardening to the Next Level
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
18mScalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)
35mTalk by Adria Gascon (Google)
36mA Hybrid Alias Analysis Framework and Its Application to Protecting the Linux Kernel
35mDeep-Kernel Treasure Hunt: Finding exploitable structures in the Linux kernel