AI 中文总结
本文提出Themis，一款基于AMD-V hypervisor的文件系统模型检查器，通过掌控机器资源实现低开销差分参考、时间维度探索与确定性重放，成功发现ext2的2038年问题缺陷并实现结果可复现。
AI 中文摘要
文件系统模型检查器会探索未修改的内核态文件系统的状态空间，以发现单元测试遗漏的漏洞。当前的技术水平代表工具是Metis，它运行在操作系统内部：它驱动系统调用，由于缺乏从用户空间低成本快照内核态的方法，它手动编码了一个参考文件系统（RefFS）作为其差分预言机，并将时间视为噪声。检查器的部署位置决定了它能观测到的内容。本文提出Themis，一款构建于未修改的内核态文件系统之下、运行在裸金属Type-1 AMD-V hypervisor上的文件系统模型检查器。Themis拥有机器控制权：在标准Linux/ext2客户机中，它控制着虚拟块设备和虚拟时钟。这种控制权带来四项优势：（1）机器层的epsilon-copy fork，其恢复成本与脏页数量成正比，而非文件系统镜像大小，因此每个未修改的文件系统都能成为自身的差分参考，无需手动编码参考；（2）文件系统底层的观测能力以及带干扰字段归一化的字节级整盘差异；（3）对时钟的控制，将时间转化为可探索的搜索维度；（4）可重新激活的同一fork，兼作位精确确定性重放的检查点。在AMD Zen5 9800X3D上进行的40余次硬件运行实验中，该机制被证明是端到端可行的：在fork窗口内处理一次真实的ext2写操作，脏页集的DRAM、磁盘和设备状态可在9微秒内完全恢复。主要成果与时钟相关：Themis驱动真实ext2遍历时钟扫描，发现了一个真实的2038年问题缺陷——128字节inode的限制，该缺陷在排除时间因素的指纹中无法被检测到；真实ext2工作负载在9次运行中实现了整DRAM和整盘的位精确重放，原本因时间波动导致的9种不同哈希值结果，在时钟可控后变为9种相同的可复现结果。
英文摘要
Filesystem model checkers explore an unmodified in-kernel filesystem's state space to find bugs that escape unit tests. The state of the art, Metis, runs inside the OS: it drives syscalls, and, lacking a cheap way to snapshot in-kernel state from user space, it hand-codes a reference filesystem (RefFS) as its differential oracle and sets time aside as noise. Where a checker sits shapes what it can see. I present Themis, a filesystem model checker built beneath an unmodified in-kernel filesystem on a bare-metal Type-1 AMD-V hypervisor. Themis owns the machine: the virtual block device and the virtual clock under a stock Linux/ext2 guest. Ownership buys four things. (1) A machine-layer epsilon-copy fork whose restore cost is proportional to dirtied pages, not filesystem image size, so every unmodified filesystem becomes its own differential reference and no hand-coded reference is required. (2) Below-filesystem observation and byte-level whole-disk diffs with nuisance-field normalization. (3) Control of the clock, turning time into an explored search dimension. (4) The same fork, made re-armable, doubling as a checkpoint for bit-exact deterministic replay. Over a campaign of 40+ hardware runs on an AMD Zen5 9800X3D, the mechanism is proven end-to-end: a real ext2 write is served inside a fork window and fully reverted (DRAM, disk, and device state) in 9 microseconds for the dirtied set. The principal result is the clock: Themis drives real ext2 across a clock sweep and witnesses a real Y2038 defect, a 128-byte-inode clamp that a time-excluded fingerprint cannot register. A real ext2 workload replays whole-DRAM and whole-disk bit-exact across nine passes, and a timing-flaky outcome (nine distinct hashes raw) becomes reproducible when the clock is served (nine identical).
