## Ghost in the Android Shell: Pragmatic Test-oracle Specification of a Production Hypervisor

> Kayvan Memarian, Ben Simner, David Kaloper-Meršinjak, Thibaut Pérami, Peter Sewell (University of Cambridge)

### 一、背景

在现代操作系统和虚拟化平台中，**hypervisor（虚拟机监控器）** 是实现安全隔离的核心组件。本文的讨论的对象 **pKVM**（protected KVM）是 Google 在 Android 上部署的生产级 hypervisor，用于保护 Android host 与 guest 虚拟机之间的隔离。传统的 hypervisor 开发通常依赖**测试 + 手工推理**；而要实现严格的安全性保障，过去的做法是**形式化验证**，但如 seL4、CertiKOS、IronFleet 等方法对大多数生产环境对开发团队来说成功过高。因此，本文提出了一种更轻量的中间方案：通过“**可执行规范 + 运行时测试**”的方式构建对生产 hypervisor 的信任。

### 二、问题与挑战

要在真实的生产 hypervisor（pKVM）中使用“定义规范 + 运行时测试”方法，存在一系列的挑战：

- pKVM 的行为与底层 Arm 硬件架构（页表、异常处理）密切绑定，规范必须能描述这种隐式行为（如硬件页表 walk）。
- 多个硬件线程可能同时进入 hypervisor；规范需要正确处理锁和状态的所有权。
- 规范需要松弛，例如，pKVM 对 host 内存映射采用按需映射机制，无法精确指定每一步行为；必须在规范中抽象掉不必要的实现细节。
- 运行环境受限，由于 pKVM 运行在 EL2，无常规测试工具（如 coverage、调试器）可用，使用随机的错误输入可能导致整个系统崩溃。
- 规范需要直接在 C 语言中实现（pKVM 所用语言），而不是在 Coq、Lean 之类的形式化语言中；C 缺乏代数数据类型、纯函数子集、pattern matching、泛型等高层特性。

### 三、设计

论文的核心设计是定义“可执行的 test-oracle 规范”，从而能够根据规范：1. 生成符合运行环境规范的随机测试输入，避免纯随机的测试输入导致系统完全 crash；2. 通过 oracle 得到运行测试后 pKVM 的状态，与实际 pKVM 运行后的状态进行比较进行测试。

1. 定义一个抽象状态（Ghost state），作为 hypervisor 真实状态的高层数学模型；ghost state 包含如下的信息。在抽象时过滤掉内存分配、页表内部结构等与外部可观察行为无关的实现细节。
	- pkvm 自身 stage-1 映射
	- host stage-2 映射
	- 每个 VM 的 stage-2 映射与元信息
	- 全局常量（物理 CPU 数、地址偏移等）
	- 每个 CPU 的本地状态
	![[251014-144626.png]]
2. 通过一组抽象函数在运行时从 pKVM 的真实状态生成 ghost state，同时保证抽象与锁的持有状态严格对应（只有在持锁时才能抽象相关状态）。
3. 使用 C 语言实现 hypercall 的“纯函数”规范，在 hypercall 执行前后分别记录 pre/post ghost state，然后比较与规范计算结果是否一致。例如 `host_share_hyp`：
	- 输入：抽象 pre-state + 调用参数 + 环境信息
	- 输出：抽象 post-state
	- 只依赖 ghost state，不依赖真实实现
4. 松弛规范与非确定性：
	- 对于内存不足错误（`ENOMEM`）等不影响核心语义的行为，规范不强制实现；
	- 规范参数化于实现返回值，以支持松弛匹配；
	- 对 host 与 pKVM 共享内存的交互，通过记录实际读取的值来消除非确定性。
5. 检查抽象状态在 hypercall 之间不发生“锁外干扰”；检查页表 footprint 不被越界修改，实现 separation logic 风格的隔离保证。

### 四、测试与评估

本工作通过修改 Linux 内核引入 “hyp-proxy” 接口，使 pKVM 的 hypercall 能在用户态直接调用，并配合自研的覆盖率工具，对实现与规范的行、分支和函数进行监测。测试主要包括三类：
1. 手写测试，共 41 个用例，覆盖所有 hypercall 的正常与错误分支
2. 随机测试，基于 ghost state 生成高质量随机输入以避免系统崩溃
3. 合成 bug 测试，通过注入错误验证测试框架的有效性
实际测试中共发现 5 个 pKVM 的真实 bug，包括 allocator 内存对齐、memcache 越界访问、竞争条件和 IO 映射重叠等问题，其中第 4 个是通过规范对比发现的。此外，规范规模约 8.4K 行，接近实现的 11K 行，在 QEMU 环境下内存占用约 18MB，启动时间增加 3.2 倍，测试时间增加 11.5 倍，测试速率达每小时约 20 万次 hypercall。作为总结，本工作提出并验证了一种用“可执行规范”动态对比实现的轻量级验证方法，在不依赖繁重形式化工具的前提下，对生产级 hypervisor（pKVM）实现了实用、低成本的高可信度保障。