Operating system kernels employ virtual memory management (VMM) subsystems to virtualize the addresses of memory regions in order to to isolate untrusted processes, ensure process isolation and implement demand-paging and copy-on-write behaviors for performance and resource controls. Bugs in these systems can lead to kernel crashes. VMM code is a critical piece of general-purpose OS kernels, but their verification is challenging due to the hardware interface (mappings are updated via writes to memory locations, using addresses which are themselves virtualized). Prior work on VMM verification has either only handled a single address space, trusted significant pieces of assembly code, or resorted to direct reasoning over machine semantics rather than exposing a clean logical interface. In this paper, we introduce a modal abstraction to describe the truth of assertions relative to a specific virtual address space, allowing different address spaces to refer to each other, and enabling 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 assertions, 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 supervisor-mode x86-64, and a logic as an instantiation of the Iris framework, are mechanized inside Coq.

翻译：操作系统内核采用虚拟内存管理（VMM）子系统来虚拟化内存区域的地址，以实现对不可信进程的隔离、确保进程间的隔离性，并执行按需分页和写时复制等行为，从而提升性能和控制资源。这些系统中的缺陷可能导致内核崩溃。VMM代码是通用操作系统内核的关键组成部分，但由于其硬件接口的复杂性（通过写入内存位置更新映射，且这些地址本身是虚拟化的），对其验证面临挑战。此前关于VMM验证的研究要么仅处理单个地址空间，要么信任大量汇编代码，要么直接基于机器语义进行推理，而未提供清晰的逻辑接口。本文提出一种模态抽象，用于描述相对于特定虚拟地址空间的断言真实性，使不同地址空间能够相互引用，并支持对操作多个地址空间的指令序列进行验证。有效使用这种抽象需要将其他断言（如分离逻辑中的指向断言）视为相对于给定地址空间成立。因此，我们定义了虚拟指向断言，它模仿硬件地址转换机制，且相对于页表根节点。我们通过VMM代码中具有挑战性的片段展示了该方法，表明其能处理先前工作无法解决的示例，包括在地址空间切换时对指令序列进行推理。本文中涉及的所有定义和定理（包括监权模式下x86-64的RISC类片段的操作模型，以及作为Iris框架实例化的逻辑）均在Coq中机械化实现。