Logo image
Back
Modal Abstractions for Virtualizing Memory Addresses
Conference proceeding   Open access

Modal Abstractions for Virtualizing Memory Addresses

Ismail Kuru and Colin Stebbins Gordon
Proceedings of the ACM on Programming Languages, v 9(OOPSLA2), pp 2338-2366
09 Oct 2025
DOI: https://doi.org/10.1145/3763134
Featured in Collection :   Research Supported by Drexel Libraries' OA Programs
url
https://doi.org/10.1145/3763134View
Published, Version of Record (VoR)Open Access via Drexel Libraries Read and Publish Program 2025CC BY V4.0,  Open

Abstract

program verification virtual memory modal logic
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.

Metrics

10 Record Views
1 citations in Web of Science

Details

InCites Highlights

Data related to this publication, from InCites Benchmarking & Analytics tool:

Web of Science research areas
Computer Science, Software Engineering
Logo image