Modal Abstractions for Virtualizing Memory Addresses
summary
Introduces a modal assertion [r]P that ties assertions to a particular page‑table root and a definition of virtual points-to that splits page‑table traversal tokens from physical page ownership, enabling verification of instruction sequences that switch CR3 and mutate shared page tables without trusting large assembly fragments. Claims complete verification for multi‑address‑space VMM code beyond prior single‑space work, demonstrates tricky allocation/traversal examples on a RISC‑like x86‑64 fragment, and mechanizes the soundness proof in Rocq mechanization.
AI-written summary · about
chapters (6)
- 0:00Memory virtualization intro
- 3:23Virtualized memory in kernel
- 6:17Address translation verification
- 9:59Fixing translation with tokens
- 11:25Address space switch example
- 13:54Paper overview and future
related talks
17mModular Verification of Safe Memory Reclamation in Concurrent Separation Logic
15mThread-modular Analysis of Release-Acquire Concurrency
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
57mInvited Talk: Bridging Safety and Performance
19mPete's Footprints
01h 03mPrinciples of Persistent Programming
16mA metalanguage for multi-phase modularity
19mLeaf: Modularity for Temporary Sharing in Separation Logic