Kuru, Ismail, Gordon, Colin S.
Proceedings of the ACM on Programming Languages, volume 9, number OOPSLA2, October 2025, doi: 10.1145/3763134
Abstract
Bibtex
@article{oopsla25,
abbr = {PACMPL},
title = {{Modal Abstractions for Virtualizing Memory Addresses}},
author = {Kuru, Ismail and Gordon, Colin S.},
journal = {Proceedings of the ACM on Programming Languages},
year = {2025},
volume = {9},
number = {OOPSLA2},
note = {To Appear..},
doi = {10.1145/3763134},
abstract = {
Virtual memory management (VMM) code is a critical piece of general-purpose OS kernels, but verification of
this functionality is challenging due to the complexity of the hardware interface (the page tables are updated
via writes to those memory locations, using addresses which are themselves virtualized). Prior work on
verification of VMM code has either only handled a single address space, or trusted significant pieces of
assembly code.
In this paper, we introduce a modal abstraction to describe the truth of assertions relative to a specific virtual
address space: [r]P indicating that P holds in the virtual address space rooted at r. Such modal assertions allow
different address spaces to refer to each other, enabling complete verification of instruction sequences manipulating
multiple address spaces. Using them effectively requires working with other assertions, such as points-to
assertions about memory contents — which implicitly depend on the address space they are used in. We therefore
define virtual points-to assertions to definitionally mimic hardware address translation, relative to a page
table root.We demonstrate our approach with challenging fragments of VMM code showing that our approach
handles examples beyond what prior work can address, including reasoning about a sequence of instructions
as it changes address spaces. Our results are formalized for a RISC-like fragment of x86-64 assembly in Rocq.
}
}