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验证的工作要么仅处理单一地址空间、信任大量汇编代码，要么直接基于机器语义进行推理，而非提供清晰的逻辑接口。本文提出了一种模态抽象，用于描述关于特定虚拟地址空间的断言的真值，使不同地址空间能够相互引用，并支持对操作多地址空间的指令序列的验证。有效使用这些模态抽象需要结合其他断言，例如分离逻辑中的指向断言（points-to assertions），并将其视为相对于给定地址空间。为此，我们定义了虚拟指向断言（virtual points-to assertions），其模仿硬件地址转换，并相对于页表根（page table root）进行表达。我们通过VMM代码中具有挑战性的片段展示了该方法，证明我们的方法能处理先前工作无法解决的示例，包括对改变地址空间的指令序列进行推理。本文中提及的所有定义和定理（包括权限模式x86-64中类RISC片段的操作模型，以及作为Iris框架实例化的逻辑）均在Coq中机械化实现。