Modal Abstractions for Virtualizing Memory Addresses

Learn about a novel approach to verifying virtual memory management code through modal abstractions in this 15-minute conference presentation from OOPSLA 2025. Discover how researchers Ismail Kuru and Colin S. Gordon from Drexel University address the challenging problem of formally verifying virtual memory management (VMM) code in operating system kernels. Explore their innovative modal abstraction framework that uses assertions like [r]P to indicate that property P holds within a specific virtual address space rooted at r, enabling verification across multiple address spaces simultaneously. Understand how virtual points-to assertions mimic hardware address translation relative to page table roots, allowing for complete verification of instruction sequences that manipulate multiple address spaces. Examine challenging VMM code fragments that demonstrate capabilities beyond previous verification approaches, including reasoning about instruction sequences as they transition between different address spaces. See how this work advances the field by handling complex scenarios that prior research could only address partially or required trusting significant assembly code components, with results formalized using a RISC-like fragment of x86-64 assembly in Rocq.