Modal Abstractions for Virtualizing Memory Addresses

TL;DR

This paper introduces modal abstractions for verifying virtual memory management code in operating systems, enabling reasoning about multiple address spaces and their interactions within a formal proof framework.

Contribution

It proposes a novel modal abstraction approach for verifying complex virtual memory operations, addressing limitations of prior methods.

Findings

Handles verification of multi-address space instruction sequences

Models hardware address translation relative to page tables

Mechanized proofs in Coq demonstrate effectiveness

Abstract

Operating system kernels employ virtual memory subsystems, which use a CPU's memory management units (MMUs) to virtualize the addresses of memory regions Operating systems manipulate these virtualized memory mappings to isolate untrusted processes, restrict which memory is accessible to different processes, hide memory limits from user programs, ensure process isolation, implement demand-paging and copy-on-write behaviors for performance and resource controls. 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. 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 in our separation logic, as relative to a given address space. We therefore define virtual points-to relations, which 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. All definitions and theorems mentioned in this paper including the operational model of a RISC-like fragment of x86-64, a simple language run on this operational model, and a logic as an instantiation of the Iris framework are mechanized inside Coq.