虚拟化内存地址的模态抽象
摘要：虚拟内存管理子系统是操作系统内核中的关键部分。它通过虚拟化内存区域的地址来隔离不受信任的进程，确保进程的隔离性，并实现按需分页和写时复制行为以实现性能和资源控制。对于这些系统中的错误可能导致内核崩溃。虚拟内存管理的代码是通用操作系统内核中的关键部分，但由于硬件的接口问题（映射是通过对内存位置的写入来更新的，这些位置本身已经被虚拟化），其验证工作具有挑战性。之前的虚拟内存管理验证工作该只处理单个地址空间，信任重要的汇编代码部分，或者采用直接对机器语义进行推理而不是公开一个干净的逻辑接口。在本文中，我们引入了一种模态抽象来描述相对于特定虚拟地址空间的断言的真实性，允许不同的地址空间相互引用，并且能够验证操纵多个地址空间的指令序列。要有效地使用它们，需要处理其他断言，例如我们分离逻辑中的点指向断言，相对于给定的地址空间来说。因此，我们定义了虚拟指向断言，其模拟了硬件地址转换，相对于页面表根。我们使用具有挑战性的VMM代码片段展示了我们的方法，证明了我们的方法处理的示例超出了之前的工作范围，包括对指令序列进行推理时地址空间的变化。本文提到的所有定义和定理，包括RISC-like型号的片段的操作模型和Iris框架的逻辑的实例，均在Coq中实现机械化。
作者：Ismail Kuru and Colin S. Gordon
论文ID：2307.14471
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-08-15