A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
summary
A dependent nominal physical type system called Typed C models contiguous memory regions with nesting, unions and mild update semantics to express pointer arithmetic, bit‑stealing, interior pointers and flexible array members; type checking is undecidable so rules are derived by abstract interpretation and embedded as an abstract domain in the Codeex verifier. The implementation analyzes unmodified C and binaries, uses only function prototypes, and on OOPSLA benchmarks generally proves spatial and type safety with far fewer manual annotations.
AI-written summary · about
chapters (9)
- 0:00Memory safety in low-level code
- 1:44Type C specification and invariants
- 3:51Type system constructs
- 7:06Dependent and union types
- 8:55Nominal typing and memory updates
- 10:41Abstract interpretation with types
- 12:54Experimental evaluation
- 15:45Summary and limitations
- 16:28Question and answer session
related talks
50mInside a static analyser: type system
51mThe C++ Type System is your Friend
25mC-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are(…)
01h 10mThe C++ Type System Is Your Friend
14mStatic Analysis of Endian Portability by Abstract Interpretation
23mFlexible Tag-based Policies for Compartmentalized C
19mA Library Modeling Language for the Static Analysis of C Programs
30mC to checked C by 3c