The Downgrading Semantics of Memory Safety
summary
Proposes gradual allocator independence: a semantic property saying program traces must not distinguish allocator implementations except where explicitly allowed. Defines a small flat-memory language (noac) parameterized by allocator state, traces and malloc/free events, and an epistemic allocator-impact set that must not shrink during execution. Treats out-of-memory checks and pointer-to-int casts as controlled declassification via cast, proves translation from MemSafe preserves the property, artifacts available and reusable.
AI-written summary · about
chapters (12)
- 0:00Memory safety semantics intro
- 1:04Allocator independence defined
- 3:29Traditional limits
- 4:50Borrowing non-inference
- 6:55Semantic safety with downgrading
- 7:58Weakening non-inference
- 9:45Downgrading with declassification
- 11:50Formalizing note tech language
- 13:33Event traces and allocators
- 14:56Non-inference formalized
- 17:43Case study: memsafe language
- 18:26Q&A
related talks
26mMemory Safety Preservation for WebAssembly
35m"Memory Safety is Merely Table Stakes [...]"
12mMemory-Safety Verification of Open Programs With Angelic Assumptions
22mReconciling Progress-Intensive Noninterference and Declassification
18mBlame-aware Recomposition for Formally Secure Low-level Compiler Backends
17mSealed with a Library Call: Memory Allocators Should Track Capability Seal Opera...
22mQuest Complete: The Holy Grail of Gradual Security
08mShort Talk: Generalising secure compilation criteria