用于虚拟化内存地址的模态抽象

《Proceedings of the ACM on Programming Languages》：Modal Abstractions for Virtualizing Memory Addresses

虚拟内存管理代码验证面临硬件接口与多地址空间复杂性挑战，本研究提出模态抽象[r]P描述特定虚拟地址空间断言，结合虚拟点对断言模拟硬件地址转换，在RISC-like x86-64汇编示例中验证了多地址空间指令序列的完整性和跨地址空间推理能力。

　　

摘要

虚拟内存管理（VMM）代码是通用操作系统内核中的关键组成部分，但由于硬件接口的复杂性（页面表是通过写入这些内存位置来更新的，而这些地址本身也是虚拟化的），因此对其功能的验证具有挑战性。以往对VMM代码的验证工作要么仅处理单一地址空间，要么依赖于部分可信的汇编代码。

在本文中，我们引入了一种模态抽象方法来描述与特定虚拟地址空间相关的断言：[r]P 表示在以 r 为根的虚拟地址空间中 P 成立。这种模态断言允许不同的地址空间相互引用，从而实现对操作多个地址空间的指令序列的完整验证。有效使用这些断言需要结合其他断言，例如关于内存内容的指针断言——这些断言隐含地依赖于它们所使用的地址空间。因此，我们定义了虚拟指针断言，以在定义上模拟相对于页面表根的硬件地址转换。我们通过具有挑战性的VMM代码片段来演示我们的方法，证明了该方法能够处理以往工作无法处理的示例，包括在指令序列切换地址空间时的推理过程。我们的结果针对Rocq中的x86-64汇编代码（类似RISC架构）进行了形式化描述。