Themis: A Filesystem Model Checker That Owns the Machine

Themis: A Filesystem Model Checker That Owns the Machine Daeyeon Son Independent Researcher Republic of Korea sdy1350@gmail.com August 2026

arXiv:2608.01135v1 [cs.OS] 2 Aug 2026

Abstract

runs across four days on an AMD Zen5 9800X3D. The mechanism is proven end-to-end: a real virtioblk filesystem write is served inside a fork window and then fully reverted—DRAM (a whole-working-set hash matches byte-for-byte), disk (a host-side overlay oracle reverts), and device state—in 9 µs for the dirtied set (O(dirtied)). The principal result is the clock. Themis drives a real ext2 filesystem across a clock sweep and witnesses a real Y2038 defect on silicon. A 128-byte-inode ext2 clamps any post-2038 timestamp to 0x7FFFFFFF, and the clamp persists across a remount—a property of the 128-byte inode, not of ext2: ext4 with 128-byte inodes clamps identically, and ext2 with 256-byte inodes does not. A byte-level whole-disk diff between two logically identical runs—after canonicalizing the filesystem’s randomidentity fields (s_uuid, s_hash_seed, i_generation) out—goes from three differing sectors to zero: the disk is deterministic modulo nuisance. Because the defect lives in the timestamps, a time-excluded fingerprint of the Metis kind does not register it; owning the clock is what makes it visible. Two further silicon results, both on real ext2, support that thesis. First, below-filesystem corruption microscopy: flipping a single bit in a file’s data block is read back wrong and reported by zero filesystem error (ext2 has no data checksums—invisible to any in-OS checker), while a single-bit flip of the superblock magic renders the whole filesystem unmountable—a demonstrated blast-radius spectrum from silent to fatal. Second, throughput, which I frame honestly as a backtrack cost model rather than a states/second count: Themis reverts only dirtied pages while Metis reloads the whole image, a gap that widens with image size (165× vs Metis’s ext4 remount, 2100× vs xfs), reported this way (a revert-only backtrack cost, not end-to-end throughput) because I estimate my bare-metal guest runs roughly an order of magnitude slower. I deliberately do not claim crash-consistency (a crowded corner I concede), and I drop attestation as a headline; I po-

File-system model checkers explore an unmodified inkernel filesystem’s state space to find bugs that escape unit tests. The state of the art, Metis [1], runs inside the operating system. It drives syscalls and reads their returns. Lacking a cheap way to snapshot in-kernel state from user space, it hand-codes a well-engineered reference filesystem, RefFS, to serve as its differential oracle. Where a checker sits shapes what it can see. Metis sits above the block device and above the clock: it observes the filesystem’s syscall interface rather than the device beneath it, and it sets time aside from its abstract state as noise. Both are documented choices. I present Themis, a filesystem model checker built beneath an unmodified in-kernel filesystem on a baremetal Type-1 AMD-V hypervisor. Themis owns the machine: it owns the virtual block device and the virtual clock underneath a stock Linux guest running a stock ext2 driver. Ownership buys four things. First, a machine-layer ε-copy fork: a VM/VMCB snapshot, nested-page-table write-protection of the guest working set, and a copy-on-write disk overlay. Its restore cost is proportional to dirtied pages, not filesystem image size, so every unmodified in-kernel filesystem becomes its own differential reference and a handcoded reference is no longer required. Second, machine-owned observation: per-operation belowFS write/read/location profiles, and byte-level wholedisk state diffs with nuisance-field normalization. Third, control of the clock, which turns time into an explored search dimension. Fourth, the same ε-copy fork doubles as a re-armable checkpoint for bit-exact deterministic replay: a real ext2 workload replays wholeDRAM and whole-disk bit-exact across nine passes, and a timing-dependent outcome that is flaky raw (nine distinct hashes) becomes reproducible when served (nine identical). This replay machinery is so far exercised on synthetic workloads rather than the filesystem headline. I report a silicon campaign of over 40 hardware

1

sition both as future cross-product work realizing the Metis group’s own dissertation §7.1.1.

1

• Own the block device ⇒ observe and inject below the filesystem. The checker measures, per operation, exactly how many sectors the filesystem wrote, how many it read, and where— reverseengineering the on-disk layout from beneath, and diffing whole-disk state at byte granularity. It can flip a single bit in a chosen on-disk structure and watch the blast radius. All of this follows from sitting beneath the driver rather than at the syscall boundary.

Introduction

A filesystem is a large, concurrent, crash-exposed state machine, and the bugs that matter most are the ones that survive years of production because no test drives the filesystem into the corner that triggers them. Model checking attacks this by systematically exploring the reachable states: from a state, apply each candidate operation, canonicalize the result into an abstract-state key, deduplicate against the visited set, and backtrack. The FAST’24 system Metis [1] showed this is practical against unmodified in-kernel filesystems and found real, long-lived bugs (including a 16-year-old JFFS2 defect). Metis pioneered versatile, in-OS filesystem model checking, and running inside the OS is a sound choice: the vantage is simple, portable, and fast, and it produced real results against real, unmodified filesystems. Metis makes two design choices that follow from its architecture, both stated in its own paper. First, running inside the OS as a userspace process, it does not have a cheap way to snapshot and restore the in-kernel state of the filesystem under test—the page cache, the inode cache, the journal, the block device. Metis reports that it “tried and evaluated . . . process snapshotting, VM snapshotting, and LightVM. None . . . were effective due to functional deficiencies or inefficient performance” [1], and, having found no suitable off-theshelf option, it builds RefFS, a purpose-built RAMFUSE reference filesystem (∼4,000 LoC) whose purpose is to be snapshottable, to serve as the differential oracle. Second, Metis sets time aside in its abstract state—atime, mtime, ctime are “noisy attributes”—and its §3.7 notes it “cannot detect atime-related bugs.” Both choices follow from where Metis sits: above the block device and above the clock. The idea is to move the checker beneath the filesystem. If the checker owns the machine—a Type-1 hypervisor that owns the virtual block device and the virtual clock under an unmodified in-kernel filesystem—then the two forced choices dissolve (Figure 1):

• Own the clock ⇒ time becomes a search axis. The checker drives the virtual wall clock through adversarial values (the 2038 overflow, rollback, nearequality) and folds the resulting on-disk timestamps into the abstract state—exactly the dimension Metis sets aside as noise. Of these three levers, the clock is this paper’s headline. It is the search axis an in-OS checker sets aside as noise, and it is where Themis witnesses a real Y2038 defect (§6). The below-filesystem observation and the deterministic replay support that result rather than share the billing. The honest core of the argument is this. The fork itself is not a contribution: lightweight VM snapshot/restore is commodity [2, 3, 4, 5, 6, 7, 8]. The contribution is what owning the machine enables. Above all it enables control of the clock; it also removes the need for a hand-coded reference and lets the checker see below the filesystem. And it demonstrates that a machine-layer fork serves, from beneath the OS, the snapshotting task the FAST’24 baseline evaluated and, within its in-OS architecture, found unsuitable. I am equally explicit about what this paper does not claim. It does not do crash-consistency testing—a crowded, conceded corner [9, 10, 11, 12, 13, 14, 15, 16, 17] where owning the machine adds little over an in-kernel bio log; I frame the crash × clock × corruption cross-product as future work that realizes the Metis group’s own dissertation §7.1.1 [18]. It does not lead with attestation; the hashchained write log is quiet infrastructure, pre-empted as a novelty by PeerReview [19]. And it does not yet report a previously-unknown reproduced bug—the Y2038 and coarse-timestamp results are real but known classes; the new-bug hunt is future work. This paper makes the following contributions. 1. A machine-layer ε-copy fork as the staterestore primitive for filesystem model checking. A whole-VMCB + GPR + XSAVE + device snapshot, nested-page-table write-protection of the guest working set, and a copy-on-write disk overlay, with restore in time O(dirtied pages) and O(1) backtracking. Silicon-proven end-to-end and reverting in 9 µs for the dirtied set (§9). This is what lets every unmodified in-kernel filesystem be its own reference, removing the need for a hand-coded one,

• Own the block device ⇒ every filesystem is its own reference. A machine-layer fork can snapshot and restore the entire in-kernel filesystem state cheaply, so an unmodified ext2/ext4/xfs can play the role RefFS was invented to play. Two forked instances (or one instance before and after a transformation) driven through the same operations are a differential oracle with no hand-built reference—an alternative route to the cheap snapshotting RefFS provides, reached by making the real filesystem itself cheap to restore.

2

and it realizes from beneath the OS the snapshot- herits a different set of trade-offs: more machine control ting Metis evaluated and set aside as unsuitable for at the cost of a heavier substrate and a slower guest. an in-OS checker. The two are complementary explorations of the same design space. Metis’s structure—which Themis reuses 2. Machine-owned below-filesystem observation. verbatim in its abstract-state policy—is: a fixed set of Per-operation write-amplification, write-localization filesystem operations (five metadata operations plus ten (from which I reverse-engineer the ext2 on-disk laysyscalls), argument binning into power-of-two partitions out without reading a line of filesystem source), and with per-argument-class distributions, and a bounded read-amplification profiles; and a byte-level wholedepth-first search (default depth 10,000, reduced for disk diff with nuisance-field normalization (§5). large-device filesystems) with an abstract-state finger3. The clock as a first-class explored dimension print for deduplication. Metis drives the real, unmod(the principal result). A differential clock sweep ified in-kernel filesystem via syscalls and compares it over a real filesystem that catches a real Y2038 times- against a differential reference. Its two design choices, tamp defect that a time-excluded (Metis-parity) fin- both stated in the paper and both reasonable within its gerprint does not register (§6). architecture, are the points where Themis’s beneaththe-OS vantage takes a different route: 4. Causal below-filesystem corruption microscopy. A single-bit flip beneath the filesystem • RefFS. Metis needs a snapshottable reference. Having evaluated process snapshotting, VM snapshotwhose blast radius spans a demonstrated spectrum ting, and LightVM and found them “not effecfrom silent to fatal (§7). tive due to functional deficiencies or inefficient 5. A backtrack cost model, honestly framed. performance” [1], it implements RefFS, a ∼4,000Themis reverts O(dirtied); Metis reloads O(image). LoC RAM-FUSE filesystem with ioctl SAVE/REThe gap widens with filesystem size—165× vs STORE/PICKLE/LOAD (∼12.5 KB per state), Metis’s published ext4 remount, 2100× vs xfs— purpose-built to be cheap to snapshot. RefFS is presented as a revert-only cost model, not a a well-engineered solution to a real problem—cheap states/second number, because I estimate my baresnapshotting under an in-OS checker; Themis reaches metal guest runs roughly an order of magnitude the same goal by a different route, making the real slower (§9). filesystem itself cheap to restore, so a hand-coded reference is not required. 6. Deterministic replay from the same rearmable fork. The machine-owned ε-copy fork • Time set aside. Metis’s abstract state excludes doubles as a re-armable checkpoint for bit-exact deatime/mtime/ctime as noisy attributes—a reasonterministic replay: a real ext2 create+write+fsync able simplification for a checker whose vantage does workload replays whole-DRAM and whole-disk bitnot read the on-disk timestamp path—and its §3.7 exact across nine passes, and a timing-dependent notes this leaves atime-related bugs out of scope. outcome that is flaky with the raw counter (nine disTime is the dimension Metis sets aside as noise, which tinct hashes) becomes reproducible when the counter Themis’s clock chapter re-examines. is served (nine identical) (§8). Metis’s published throughput—RefFS ∼830 ops/s The system is one component of AnimaOS, a bareand ∼349.9 states/s, ext4 ∼280.3 ops/s and ∼112.6 metal Rust operating system that includes the Typestates/s, xfs ∼29.2 ops/s and ∼8.8 states/s [1]—is the 1 AMD-V hypervisor Themis is built on. All silicon baseline for my backtrack cost model (§9). The tworesults are from a campaign of over 40 hardware runs order-of-magnitude gap between RefFS and xfs is preacross four days (July 13, 14, 15, and 18) on an AMD cisely the O(image) reload cost of using a real filesysZen5 9800X3D self-hosting from NVMe; bootlogs are tem as its own reference in an in-OS checker—the archived. cost Themis’s O(dirtied) fork removes. EXPLODE and FiSC [12, 13] are the model-checking ancestors 2 Background and Related Work and are worth positioning against precisely, because Themis inherits their core idea and moves only the Metis [1] is the immediate predecessor, and the sys- substrate. FiSC model-checked Linux filesystems from tem whose exploration approach Themis reuses and ex- inside a modified kernel, and EXPLODE generalized tends. Metis pioneered versatile in-OS filesystem model it to a lightweight, in-situ storage checker that snapchecking; its in-OS vantage is simple, portable, and shots and restores the running system to explore states fast, and its design choices—RefFS and setting time and found serious errors across a wide range of storaside—are reasonable engineering within that architec- age stacks. Both took the exploration approach Themis ture. Themis deliberately takes the opposite architec- reuses; both, however, did their checkpointing inside the tural bet, moving the checker beneath the OS, and in- machine they were testing, and neither observed below 3

What Themis sees (beneath) below-FS I/O, whole-disk bytes, CPU/FPU state, the clock

What Metis sees (in-OS) the filesystem’s syscall interface

Unmodified Linux guest — busybox initramfs, real ext2 on /dev/vda, single-vCPU, no guest-side checker code

Owned resource #1: the guest clock the hypervisor is the time source

Owned resource #2: copy-on-write disk immutable base image + overlay stack

Bare-metal Type-1 AMD-V (SVM) hypervisor — the Themis checker lives here VMCB · nested page tables · traps the guest doorbell

AMD Zen5 9800X3D silicon — NVMe self-host, no host OS underneath

Figure 1: The ownership cascade. A bare-metal Type-1 AMD-V hypervisor—where the Themis checker lives— owns the guest’s copy-on-write block device and clock beneath an unmodified Linux guest that runs a stock ext2 driver with no guest-side checker code. The dashed columns contrast visibility: Metis, inside the OS, observes the syscall-return interface; Themis, beneath the guest, also observes below-FS I/O, whole-disk bytes, and CPU/FPU state. the filesystem or drove the clock. FiSC explicitly notes that “any VMM is a valid substitute” for its in-kernel checkpointing—a line that both anticipates and licenses the Themis substrate. Themis takes that license literally: it keeps the exploration engine and pushes the checkpoint down to a machine-layer fork, which is exactly what opens the below-FS and clock dimensions those ancestors left closed. I turn next to crash-consistency testing, positioning against that literature proactively so that no reviewer mistakes Themis for a crash tester. Crashconsistency is a mature, crowded area: CrashMonkey/ACE/B3 [9] systematically generate small workloads (ACE) and bounded-exhaustively test recovery from the crash states each one can reach (the B3 approach), catching real crash-consistency bugs in mature filesystems; dm-log-writes [10] is an in-tree devicemapper target that records every bio with FLUSH/FUA ordering and replays barrier-respecting prefixes under an unmodified filesystem; BOB/ALICE [11] reorder and drop writes at barriers to find application-level crash vulnerabilities against an abstract model of what each filesystem persists; Hydra [14] and Chipmunk [15] scale coverage; Vinter [16] does full-system crash testing of an unmodified kernel; and SnapCC [17] pairs a fuzzer with per-workload crash states. The critical point for Themis: on the crash

axis, “owning the machine” adds essentially nothing. dm-log-writes already sees every bio and every barrier beneath an unmodified filesystem, so a “hypervisor that logs writes and replays prefixes” is a re-implementation of an in-tree tool one layer down. Two adversarial design reviews independently reached a unanimous no-go on shipping crash consistency in this paper. Themis does not implement crash-consistency testing. The only non-derivative framing— per-node-of-theglobal -model-checker-graph crash enumeration, with the fork/replay substrate making it cheap and sound—is exactly the integration the Metis group’s own PhD dissertation §7.1.1 [18] lists as future work (“crash state must be considered as part of the overall state description”). I claim only to realize their open problem as future cross-product work (§10), not to compete with the crash-testing crowd here. On corruption injection and clock faking, the closest relative to the corruption experiments (below-FS corruption) is IRON [20], which taxonomizes per-blocktype detect/recover policies—but IRON is explicitly manual and policy-level, not a deterministic controlled experiment. Themis’s wedge is determinism makes n=1 causally sufficient: because the fork is a bit-exact εcopy, the unflipped counterfactual is identical modulo one bit, so every downstream divergence is provably caused by that bit—an exact causal blast radius rather 4

than a failure-policy fingerprint. For the clock experiments, a reviewer’s first instinct is that clock faking is solved by libfaketime [21]. It is not: LD_PRELOAD fakes what userspace reads via time()/fstat(); it never touches the inkernel timestamp-generation path that writes __le32 i_mtime to disk, and it provides no exploration and no oracle. Deterministic hypervisors such as Antithesis [22] virtualize the clock to remove time nondeterminism for reproducibility—the inverse posture; determinism is not exploration. No prior filesystem tester drives a virtual clock as an explored dimension over an unmodified in-kernel filesystem. The live, twice-reverted Linux multigrain-ctime defect of 2023–24 [23]—caught in the wild by make/rsync breakage, not by any tool—is the existence proof that this bug class is real and current. The fork substrate itself is commodity, and that is fine. Lightweight VM fork/snapshot with copy-onwrite or dirty-page reset is standard: Potemkin [2], SnowFlock [3], Remus [4], Firecracker snapshots [5], Xen fork-vm for fuzzing [6], Agamotto’s “lightweight VM checkpointing as a primitive” for a checker [7], and Nyx’s dirty-page reset [8]. Themis does not claim the fork. It claims (a) that a machine-layer fork serves this specific task from beneath the OS—where Metis, evaluating VM snapshotting within an in-OS architecture, found it unsuitable—and (b) everything the fork enables below and around an unmodified filesystem. Likewise, hash-chained tamper-evident logs are pre-empted by PeerReview [19]; my block-write chain is quiet infrastructure for future crash-epoch replay, not a headline.

3

the fork snapshot atomic (no live AP tears the snapshot) and sidesteps cross-CPU TLB coherence—it is also the regime a serial-console FS model checker wants. All silicon results are from a campaign of over 40 hardware runs across four days; each run is one physical boot of the machine with a specific build configuration, and the raw serial/NVMe bootlogs are archived alongside this draft. The choice to build on a Type-1 hypervisor that owns the machine— rather than QEMU/KVM—is the whole point: the checker is the most privileged software on the box, so the block device, the clock, the nested page tables, and the VMCB are directly under its control, with no host OS mediating. A companion QEMU “MockFs/MockNpt” harness proves every bit of pure logic without touching hardware; the hypervisor half, which cannot run nested under QEMU (no nested SVM), is proven on silicon.

4

Design: The ε-Copy Fork

The heart of Themis is a fork whose restore cost is proportional to the pages a branch dirtied, not the size of the filesystem image. I call it an ε-copy fork: the child branch shares the parent’s pages until it writes one, and a restore frees only what the child privately copied. This section describes the five pieces—the NPT write-protect + copy-up core, the CPU/device snapshot, the copy-onwrite disk overlay, the doorbell interface, the whole-set acceptance gate—and then why they together let every unmodified filesystem be its own reference. Figure 2 shows one fork’s lifecycle. At the core of the fork is NPT write-protection plus copy-up. On AMD-V, the guest’s physical memory is mapped through nested page tables (NPT). Themis installs guest DRAM as 4 KiB NPT leaves on demand (the platform does not use 2 MiB nested PDEs—a Zen5 consumer-silicon quirk means PS=1 in nested PD entries is not reliably honored, so all guest DRAM is 4 KiB leaves; this happens to make write-protection uniform). To fork, Themis walks the currently-installed DRAM leaves and clears the writable bit, recording each in a tracked set (CowForkState). Clearing W leaves the accessed/dirty bits untouched, so the fault that follows is a clean permission fault, not a dirty-bit walk pathology. A subsequent guest write to a write-protected present leaf raises a nested page fault with error bits P=1, R/W=1 (err & 0b11 == 0b11). Themis intercepts this at the top of the NPF handler, before MMIO dispatch (a tracked DRAM page is never MMIO), and performs a copy-up—reading the current page contents through the host mapping, allocating a fresh private frame, copying the 4 KiB, remapping the leaf to the private frame writable, recording the (gpa → private frame, parent frame) mapping, and resuming the guest without ad-

Threat Model, Scope, and Platform

Themis tests correctness and robustness properties of an unmodified in-kernel filesystem: the abstract filesystem state (path, kind, mode, uid, gid, nlink, size, content) reached by a sequence of operations; the belowfilesystem I/O behavior (what the driver writes/reads and where); on-disk state determinism modulo nuisance fields; timestamp behavior under an adversarial clock; and the blast radius of controlled below-filesystem corruption. It is equally important to say what Themis is not: it is not a crash-consistency tester (§2). It is not a fuzzer of the syscall ABI for memory-safety bugs. It runs single-node and single-vCPU. As for the platform, Themis is built on the AnimaOS bare-metal Type-1 AMD-V/SVM hypervisor. The host is an AMD Zen5 Ryzen 9800X3D, self-hosting from NVMe. The guest is a stock Linux kernel with a busybox initramfs, booted single-vCPU (maxcpus=1), running the stock in-kernel ext2 driver over a virtio-blk device whose backing store is a Themis copy-on-write overlay (§4). Single-vCPU is deliberate: it is what makes 5

1. Fork / snapshot snapshot CPU state + FPU/XSAVE

write-protect the in-use DRAM pages

fold the pre hash

4. Restore

unmodified guest runs one filesystem op

VMCB + registers

push a CoW disk overlay

2. Run the operation

write to a protected page ⇒ copy-up

3. Capture

free copied-up pages, rebind the originals

hash the (possibly-changed) state

restore the CPU snapshot pop the disk overlay

DRAM set + disk

private 4 KiB copy

fold the post hash

disk writes → overlay

cost ∝ dirtied pages

Copy-on-write memory: a write copies only that page, while unwritten pages stay shared (read-only) running branch

W

W copied on write (private, W)

base snapshot (write-protected)

shared, read-only (↓)

Acceptance gate: pre hash = post hash ⇒ the whole tracked set reverts byte-identically O(dirtied)

Themis revert — 38 pages in ∼9 µs O(image)

full-image reload — grows with FS size

Figure 2: One fork’s lifecycle, left to right: fork/snapshot, run one filesystem operation, capture, and restore. The center panel shows the copy-on-write memory—a write copies only that one page, while unwritten pages stay shared read-only. The acceptance gate is PRE-hash = POST-hash: the whole tracked set reverts byte-identically, so the revert is O(dirtied) (38 pages in ∼9 µs) rather than a full-image reload. §4 details each stage. vancing RIP so it retries the write against the nowprivate page. The parent frame is never mutated—that immutability is what makes the fork revertible. Two subtleties cost real time on hardware. First, clearing the writable bit in an NPT leaf does not evict a cached writable TLB entry on AMD SVM. Without a TLB flush at fork time, every page whose translation was TLB-resident-writable at the fork point (the hot working set—kernel stack, current, live page tables) is written with no fault, no copy-up, and the write lands in the shared parent frame and is never reverted. This silently corrupts the reference for all later branches, and it is invisible to any test that only touches cold pages. The fix is a one-shot FLUSH_ALL_ASID in the fork path. Second, the on-demand install of a page first touched after the fork (page-cache growth—the commonest FS side effect) has no parent version; restore must unmap it, free it, and untrack it, not merely free a frame. The restore action set therefore carries four lists—copyups to free-and-rebind, and fresh pages to unmap— validated by a MockNpt replay in software before any hardware run. Restore reverts the NPT: free the child’s private frames, rebind the parent leaves, unmap fresh installs, one-shot TLB flush. Because it touches only what the branch dirtied, it is O(dirtied).

Beyond memory, a fork must capture all machine state that carries across a branch. On AMD-V the minimal correct set is four things: the whole 4 KiB VMCB page (the instruction pointer, the control and segment registers, and the segment bases), the host-managed general-purpose registers (which, on AMD-V, live outside the VMCB and so must be captured separately), the shadow CR2 the run loop reloads each iteration, and the guest XSAVE area (the 4032-byte block of FPU/AVX state)—the piece a naive “copy the VMCB” misses, producing the classic “fork looks fine, then floats diverge” bug. Missing any one of these four is a silent state leak across a branch: the memory reverts, but a register, a segment base, or a float lane carries a value forward from the wrong branch, so I snapshot and restore all four as a unit. Snapshotting the whole VMCB page is safe because the host’s own save area sits elsewhere and the fork-invariant control structures do not change underneath it. Once a branch performs real I/O, device state must also snapshot and revert (gated behind a compile-time flag so a pure-compute fork pays nothing): the whole virtio-blk device struct including last_avail_idx (the host’s consume cursor—omitting it desynchronizes the virtqueue rings across a restore, the classic ring-desync

6

bug), both LAPICs (pending IRR, timer fields), the IOAPIC redirection table, and the block completionIRQ latches. I snapshot whole structs, not register subsets, because the guest-visible ring indices in DRAM and the host-shadow cursor in the device struct must revert in lockstep. The fork is taken only at a clean VMEXIT boundary with no in-flight virtio-blk descriptor (used == avail) and guest interrupts sane, so no request is mid-flight when the snapshot is taken. The disk side of the fork is copy-on-write ownership. The virtual block device is backed by a copy-on-write structure (CowDisk): an immutable base image plus a stack of overlay layers. fork() pushes a layer (O(1)); the running branch’s writes land only in the top layer; discard() pops it (O(1) backtrack); a read walks the stack top-down, returning the first hit, else the base. The base image is never mutated, so it is the permanent root of the exploration tree. This is the disk-side ε-copy: a branch’s disk footprint is exactly the sectors it wrote, and reverting it is a pop. The disk overlay and the DRAM tracked set are kept in lockstep—a fork pushes both, a restore pops both, and the code asserts equal depth—because a filesystem write dirties both DRAM (buffer heads, page cache) and disk (the eventual bio), and both must revert together or the branch leaks state forward. Because the checker owns this structure, it is also the instrument for §5–§7: the top layer’s key set is the below-FS write set and its LBAs; an interior read counter is the below-FS read amplification; a wholeimage fold is the disk oracle for the fork’s revert proof and for the byte-level state diff; and a direct sector write is the below-FS corruption injector. The guest agent and the host checker rendezvous through a port-I/O doorbell: the guest issues an OUT to the reserved port 0xD0, which VMEXITs straight to the hypervisor, and the command byte in the accompanying register selects the action. This is the entire guest-to-host interface—no shared memory region, no paravirtual driver, nothing the unmodified filesystem can see—which is what keeps the guest genuinely unmodified apart from a thin agent that rings the bell. The commands the mechanism needs are minimal: fork (snapshot + write-protect + push overlay), restore (revert), a disk-mid capture (the guest signals its write is durable so the host can sample the in-window disk state as a positive control), and an exit that tears down to the host shell and resets fork state. Table 1 is the full command map, verified byte-for-byte against the dispatcher. A restore is a single-pass terminate: it reverts DRAM + disk + devices and sets RIP past the doorbell, then tears down—it does not loop the guest back to re-run the op (an earlier two-pass design re-ran the FS op against a popped overlay and corrupted the shared baseline; the revert proof is host-side, so the guest re-run is pure liability). A fork-window watchdog bounds VMRUN iterations so a wedged guest yields a log, not a bricked

machine. The host-driven exploration loop that would inject operations and read back guest fingerprints over a shared channel (needed for the at-scale throughput pillar—scaling the backtrack cost across a large exploration) is designed but deferred (§10); a guest-scripted driver realizes the eval results in this paper without it. The payoff of owning the block device is that every filesystem becomes its own reference, removing the need for a hand-coded one. Metis builds RefFS because cheap snapshotting of a real filesystem’s in-kernel state is not available to an in-OS process. Themis can: the ε-copy fork snapshots and restores the whole machine—page cache, inode cache, block device—in time proportional to the dirtied set. So the abstract state can be read by observing the real filesystem rather than by consulting a hand-coded model. The checker walks the mounted filesystem (readdir + stat + content read) and folds each entry into a Merkle-style fingerprint—a sorted path → leaf-hash map whose fold is a single deterministic root—over exactly Metis’s policy fields (path, kind, mode, uid, gid, nlink, size, content), excluding time by default so that the substrate delta is isolated from the clock delta (a config folds mtime in for the clock experiments). Two questions a checker lives on both reduce to this fingerprint: “have we seen this state?” is a lookup in a visited set keyed by root hash (O(states), not O(image)); “do two implementations agree?” is a root comparison, and the first sorted path where they differ is the localized differential bug. That second question is what removes the need for a hand-coded reference: drive two unmodified filesystem instances (two implementations, or one instance versus its remounted self) through the same deterministic operation sequence; a root divergence at any step is a bug in one relative to the other, found with no hand-built oracle. The exploration driver is a bounded DFS: at each state, apply next_command from a deterministic policy (same seed ⇒ same exploration ⇒ replayable), fork before each op, recurse if the op changed the abstract state, restore after—every op is fork/restore-bracketed, and the tree unwinds fully (Figure 3). The DFS, the visited-set dedup, the differential comparison, and the fingerprint are all pure logic, proven in software under QEMU against an inmemory MockFs/RealisticFs; the real checker swaps the mock for the hypervisor fork plus a guest readoracle whose content digest is a blake3 over the file’s real bytes (the model carries the actual content), so a size-preserving content corruption changes the fingerprint and is caught—an earlier draft digested only path ∥ size and was blind to it, and that gap is now closed.

7

Table 1: The doorbell command interface. Each command is a guest OUT to a reserved port that traps to the hypervisor. command

what it does

0xE0 0xE1 0xE2 0xE3 0xE4 0xE5 0xE6 0xE7 0xE8 0xE9 0xEA 0xEB 0xF1 0xF2 0xF3 0xFF 0x00–0xFE

Flip one bit in a marked file data block (the silent-corruption injector). Push a disk overlay and reset the read counters, establishing a per-operation baseline. Report the number of sectors the operation wrote below the filesystem. Report the sorted list of disk locations the operation wrote. Report the number of sectors read below the filesystem since the baseline. Hash the entire disk image. Snapshot the entire disk for a later diff. Report the disk sectors that differ from the snapshot. Report the differing byte ranges, then mask the nuisance fields and recount. Flip a bit of the superblock magic at LBA 2 (the fatal-corruption injector). Corrupt an inode-table byte. Corrupt a directory-block byte. Fork: snapshot the CPU, write-protect the working set, and push a disk overlay. Restore: revert memory, disk, and CPU to the fork point. Capture the in-window disk state as a positive control. Tear down fork state and return to the host shell. Progress marker, no side effect.

5

Table 2: Below-FS write amplification for real ext2.

Machine-Owned Observation

An in-OS checker reads syscall arguments and returns. Themis owns the block device, so for every filesystem operation it measures the below-filesystem consequences directly. These are not incidental metrics; they are a data class the beneath-the-device vantage makes available, and they let Themis reverse-engineer the on-disk layout and compare whole-disk states at byte granularity. The first data class is the below-FS I/O profile of each operation—its write amplification, its write localization, and its read amplification. Consider write amplification first. For each operation Themis counts the sectors written beneath the filesystem (the top overlay layer’s key set). Table 2 shows the profile for real ext2. A 1-byte write costs 16 sectors (8192× amplification); the amplification falls toward ∼1× as the write grows past the block size; and metadata operations that a syscall-return checker sees as “returned 0” have a hidden, non-zero below-FS cost (create/mkdir = 14 sectors, chmod/chown = 2, hardlink/rename/unlink = 6). What this profile means is that the syscall return code is a lossy summary of what the filesystem actually did: a metadata operation the guest reports as a bare success in fact commits a fixed, characteristic set of sectors below the driver, and the amplification curve—8192× for a sub-block write, decaying to unity once the write spans whole blocks—directly traces the block-size quantum and the read-modify-write it forces. Each operation therefore has a below-FS write signature, and that signature is a first-class observable Themis can key on, deduplicate against, and diff—a dimension of behavior that the syscall return value does not by itself express.

op write 1 B write 512 B write 4 KB write 64 KB write 1 MB create / mkdir chmod / chown hardlink / rename / unlink

bytes

sectors written

amplification

1 512 4096 65536 1048576 0 0 0

16 16 20 ∼130 2070 14 2 6

8192× 16× 2.5× ∼1.02× ∼1.01× — — —

Write localization reverse-engineers the ext2 layout from beneath. Because Themis sees which LBAs each op writes, it derives the on-disk layout without reading a line of filesystem source (Table 3). From these I read off, over the 8192-sector 4 MiB image: LBA 2–3 = superblock, 4–11 = group descriptors + bitmaps, 14–17 = inode table, 522–523 / 548–549 = directory blocks, 6146+ = file data. A chmod touches only the inode table (LBAs 14–15); a create touches the superblock, bitmaps, inode table, a directory block, and a data block; a mkdir additionally allocates a new directory block (548–549). What makes this more than a curiosity is that the entire on-disk format—region boundaries, which structure each operation mutates, and where— falls out purely from watching below-FS writes, and the same map then tells the corruption experiments (§7) exactly which LBA and byte offset to target. Figure 4 draws the full reverse-engineered map. Read amplification is the mirror of the write set: cold reads beneath the filesystem, minus a 70-sector mount baseline (Table 4). A stat reads 2 sectors (the inode); a small cat reads 4 (inode + data); a 64 KB cat reads 132 (inode + 128 data + indirect block); a full find over 8

Read-oracle fingerprint: walk names → stat inode → hash content; leaf = path | kind | mode | uid | gid | nlink | size | content (mtime folded only in the time mode); Merkle-fold to a root; dedup against the visited set

mke2fs a real ext2 in the guest, then a deterministic, replayable operation sequence

Below-FS observers (own the device): write amplification, write localization, read amplification (below-the-device measurements)

Every filesystem is its own reference: drive two instances through the same sequence; the diff localizes the first divergence (no hand-coded reference)

Whole-disk snapshot, diff, and nuisance normalization

Exploration DFS loop: fingerprint → dedup → fork → apply op → restore Verdict: divergence path · below-FS footprint tables · deterministicmodulo-nuisance normalization · corruption blast radius

Figure 3: The data-collection loop. A run creates a real ext2 with mke2fs and drives a deterministic, replayable operation sequence through two parallel planes—the below-FS observers and the whole-disk snapshot/diff/normalize path—while the read-oracle fingerprint dedups states and the exploration loop brackets every operation with fork/apply/restore. Driving two unmodified instances through the same sequence localizes the first divergent path, removing the need for a hand-coded reference (§4). All paths converge on a verdict. Table 3: Below-FS write localization, and the reverse-engineered ext2 layout. op chmod / chown create mkdir write 64 KB

sectors 2 16 14 142

LBAs touched

ext2 structure

14–15 2–11, 14–15, 522–523, 6146–47 4–11, 16–17, 522–523, 548–549 . . . 6148–8129

inode table only sb → bitmaps → inode → dir → data + new dir block data region

Table 4: Below-FS read amplification (marginal cold The three profiles compose into a 3-D fingerprint reads over a 70-sector mount baseline). per operation— reads ⊕ writes ⊕ location. For example, chmod = read 2 / write 2 / at LBA 14–15. This is op marginal cold reads a below-FS behavioral signature that the beneath-thedevice vantage provides. stat 2 (inode) The filesystem can also serve as its own transition cat small 4 (inode + data) model. Owning the block device lets Themis derive cat 64 KB 132 (inode + 128 data + indirect) the abstract-state transition model by observing the ls dir 4 find tree 28 (full walk) real filesystem rather than hand-coding it in a referchmod 2 ence. Table 5, the operation–field footprint, records for each operation exactly which of the eight abstractstate fields it changes, measured against the real driver a tree reads 28. An honesty note: drop_caches was a rather than posited. It reads as a compact behavioral no-op on this guest, so cold reads were forced by umount contract: chmod, chown, setuid, rename, and hardlink + remount rather than by dropping caches—a coverage all touch ctime (a metadata change always bumps the gap (§10) but not an inaccuracy in the reported counts. change time), while only the size-changing operations 9

boot 0–1

superblock 2–3

group-desc +bitmaps 4–11

Corruption targets (own the dev): 0xE9 superblock s_magic @LBA2:56 (FATAL) 0xEA inode-table byte @LBA15:0 0xEB directory block @LBA522:0

inode table 14–17

dir block 522–523

new dir 548–549

file data 6146 .. 8191

Which op touches what (from write localization, doorbell 0xE3): chmod/chown → 14–15 (inode table only, 2 sec) create → 2–11 + 14–15 + 522–523 + 6146–47 = 16 sec mkdir → 4–11 + 16–17 + 522–523 + new 548–549 = 14 sec write 64 KB → 6148–8129 (data region)

Figure 4: The ext2 layout, reverse-engineered without reading a line of filesystem code. Every region boundary is derived from watching which LBAs each operation dirties (Table 3); the corruption doorbells (§7) target exactly these structures. Owning the block device recovers the on-disk format from below—a view available from beneath the device, complementary to the syscall interface an in-OS checker reads. (append, truncate) also touch mtime, and only touch moves atime and mtime together. Two entries carry a value beyond the check mark: setuid sets mode = 4755, and hardlink’s nlink changes from 1 to 2—transitions a hand-coded reference must encode explicitly, whereas Themis observes the real filesystem make them. Table 6, the timestamp-semantics matrix, records the measured timestamp semantics—and from it Themis reads, directly from the running mount, a real mount property: this mount is strictatime (read updates atime), not relatime/noatime. The point of both tables is that the transition model is observed, so it is correct by construction for whatever driver, version, and mount options are actually running, and it needs no maintenance as the filesystem evolves—which is the precise burden RefFS carries in Metis. A state-space battery of measured properties (Table 7) confirms the checker’s abstract-state machinery on a real filesystem: directory scaling is linear (∼1 KB/file); hardlink refcounts follow the exact trajectory create=1 → link×3 = 2,3,4 → unlink ×2 = 3,2; limits hold (255-char names, dotfiles, depth5); a 6-op sequence run three times from a fresh mkfs yields an identical fingerprint b4bb1041b38d (the checker is reproducible); commutativity is non-trivial (chmod;chown, chmod;write, trunc;chmod all commute, but write;truncate does not); idempotency splits state from return code (mkdir is state-idempotent but its second return code is an error); six error paths return the correct errno; and symlink semantics hold. The sharpest expression of owning the block device is a byte-level whole-disk state diff. Themis folds the entire overlay-resolved disk into a snapshot, runs a filesystem operation, and reports the exact LBAs—and 10

within them the exact byte ranges—that changed. Between two logically identical runs this is the raw material for a disk-level determinism check—one phrased in on-disk bytes rather than syscall returns. The subtlety, which I get exactly right and report honestly (§6), is nuisance. Two logically identical mkfs + op runs, even with a pinned clock and a fixed UUID request, differ in a handful of sectors—not only in timestamps but in the filesystem’s random-identity fields: the superblock s_uuid and htree s_hash_seed, and each inode’s i_generation (an NFS version counter seeded randomly). A model checker must canonicalize these out of the abstract state—exactly as it excludes atime. Themis does this at byte granularity: it masks the known ext2 nuisance offsets (superblock s_mtime/s_wtime/s_lastcheck/s_uuid/ s_hash_seed; per-inode i_atime/i_ctime/i_mtime/i_dtime/ i_generation, plus the extra timestamp fields for 256-byte inodes) in both images before comparing, and counts the sectors that still differ. This “normalized diff” is the disk-level analogue of the fingerprint’s abstract-state canonicalization, and it is what makes the clock-chapter result (§6) a clean 3 → 0.

6

The Clock Chapter

Metis sets time aside from its abstract state, treating it as noise, and notes that atime bugs fall outside its scope—a reasonable choice for a checker that reads syscall returns rather than the on-disk timestamp path. Themis owns the clock, so time is a dimension it explores. This is the paper’s principal result because it is un-preempted ground: no prior filesystem tester drives

Table 5: The operation–field footprint (measured on real ext2): op × 8-field metadata footprint, where a check mark means the field changed. op

mode

chmod chown setuid append truncate touch rename hardlink

uid

gid

✓

✓

size

read write chmod stat

atime

mtime

✓ ✓ ✓ ✓ ✓

Table 6: The timestamp-semantics matrix (canonical POSIX, measured on real ext2). op

nlink

atime

mtime

ctime

✓ — — —

— ✓ — —

— ✓ ✓ —

a virtual clock over an unmodified in-kernel filesystem, and the bug class is live (the 2023–24 multigrain-ctime defect, §2). I should be precise about what “owning the clock” means here in mechanism, because it is easy to overread. Themis does not run a bit-exact virtual clock, and it does not intercept the guest’s timestamp counter: the TSC runs free. I drive time instead by having the guest agent call settimeofday to advance CLOCK_REALTIME in the guest timekeeper to each adversarial value, then read back what the unmodified filesystem chooses to persist to disk. The hypervisor is the ultimate time source in that it presents the platform timers the guest calibrates against, but the exploration lever is the ordinary POSIX wall clock, not the raw RDTSC—freezing which would be the wrong instrument (§6). What owning the machine adds is not a faked clock; it is the vantage beneath the driver to read exactly what the filesystem wrote in response to that clock, at byte and, later in this section, nanosecond granularity—something no in-guest test can see. The principal silicon result is a real Y2038 defect, witnessed on real ext2: a guest mounts a real, unmodified in-kernel ext2, sets its wall clock past 2038 (date -s @2147483648— settimeofday into the guest timekeeper; no hypervisor clock trickery), touches a file, and reads back the on-disk __le32 i_mtime via stat. Real ext2 clamps the post-2038 timestamp to 0x7FFFFFFF (i32::MAX = 2038-01-19 03:14:07): it cannot represent 2038-01-19 03:14:08 or later. The Linux ext2 driver itself declares this limit at mount (“supports timestamps until 2038-01-19 (0x7fffffff)”)—irrefutable ground 11

✓ ✓ ✓

ctime ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓

truth—and the clamp persists across a remount, i.e. it is a real on-disk value, not a page-cache artifact. The same clamp fires for a year-2106 timestamp. Table 8 is the differential clock sweep, and it pins the causal variable: the clamp is a property of the 128-byte inode, not of ext2 versus ext4. A 128-byte inode has no i_[cma]time_extra epoch bits, so it stores a bare signed __le32 second and wraps at 231 (2038); a 256byte inode carries the extra epoch bits and represents past it (to the ∼2446 ceiling). A host-side byte-parse cross-check—re-mkfsing the same formats and reading the on-disk inode bytes directly—isolates this cleanly: ext4 formatted -I 128 clamps at 2038 identically to ext2, and ext2 formatted -I 256 stores post-2038 correctly. So the filesystem type is not the variable; the inode size is. The silicon differential drives a 128-byteinode lane (clamps) against a 256-byte-inode lane (represents). A time-included fingerprint (Themis) catches and localizes the divergence at the affected file; a timeexcluded (Metis-parity) fingerprint hashes the correct and clamped states identically and so does not register it. The coarse-granularity probe (Table 9) is itself a finding: four rapid touches produce one distinct stored timestamp, and in the multi-state exploration (§9) two rapid touches received the identical nanosecondprecision timestamp. On real silicon the kernel timestamp is coarse, so two distinct operations are temporally indistinguishable—the multigrain-timestamp class ground truth. A checker that relies on time to order operations is fooled; a time-included fingerprint sees them as time-identical; a time-excluded (Metis-parity) fingerprint does not track time at all. The determinism result is a 3 → 0 byte-diff, with an honest correction. Two logically identical runs (pinned clock, requested fixed UUID) differ raw in three sectors—the superblock plus inode-table sectors. Themis’s byte-diff localizes the differing bytes and—this is the honest correction I make prominently—they are not (only) timestamps. The residue is the filesystem’s random-identity fields: s_uuid (the -U flag did not fully pin it), s_hash_seed, and i_generation. An

Table 7: The state-space battery: measured state-space structure (summary). property

result

directory scaling hardlink refcount trajectory limits determinism commutativity idempotency error paths

∼1 KB/file, linear (10/100/500 files → 11/103/510 KB on disk) create=1 → link×3=2,3,4 → unlink×2=3,2 (exact) 255-char name OK, dotfile OK, depth-5 OK same 6-op seq ×3 (fresh mkfs) → fingerprint b4bb1041b38d identical chmod;chown, chmod;write, trunc;chmod = yes; write;truncate = no chmod/truncate/chown = yes; mkdir state-idempotent but rc2 = err 6, correct errno (rmdir-nonempty, rmdir-a-file, unlink/rename/link-missing, mkdir-existing) to-file deref yes, dangling no, to-dir is-dir yes, self-loop ELOOP (no)

symlinks

Table 8: Clock sweep: the Y2038 clamp tracks inode size, not filesystem type. The silicon differential drives ext2 (128-byte inode) against ext4 (256-byte inode); a host-side byte-parse cross-check adds the diagonal (ext4 -I 128 clamps, ext2 -I 256 represents), isolating the 128-byte inode’s missing i_[cma]time_extra epoch bits—not the filesystem type—as the causal variable. filesystem

inode size

post-2038 timestamp

provenance

ext2 ext4 ext4 ext2

128-byte 256-byte 128-byte 256-byte

clamps to 0x7FFFFFFF (2038) represents (to ∼2446) clamps to 0x7FFFFFFF (2038) represents (to ∼2446)

silicon silicon host parse host parse

result

granularity (4 rapid touches) post-2038 store

1 distinct stored time (coarse, 1 s)

clamp mount

across

re-

0xE8 byte-diff localizes the bytes: superblock: s_mtime@44 s_wtime@48 s_lastcheck@64, s_uuid@104(16), s_hash_seed@236(16) (random identity) inode: i_atime@8 i_ctime@12 i_mtime@16 i_dtime@20, i_generation@100(4), *_extra@132 (256B inode)

0xE8 normalize (mask_nuisance_fields): sectors still differing = 0 ⇒ deterministic modulo nuisance (3→0 by canonicalization, NOT by freezing the clock)

Table 9: Y2038: timestamp granularity and the persisted clamp. probe

0xE7 raw diff: 3 sectors differ — LBA 2 (superblock), LBA 15,16 (inode table)

Figure 5: The byte-diff and normalize step (the 3→0 result). Two logically-identical runs differ in three raw sectors; localizing the differing bytes shows the residue lands on the filesystem’s random-identity fields (s_uuid, s_hash_seed, i_generation), not only on timestamps. Masking those nuisance fields drops the count to 0—deterministic modulo nuisance, by canonicalization, not by freezing the clock (§6).

0x7FFFFFFF clamp; kernel declares “until 2038-01-19” persisted (real on-disk value)

earlier framing of this result as “the only difference is time” was wrong, and the byte-diff is what disproved it. Normalizing those nuisance fields (§5) drives the still-differing sector count to zero: the disk is deterministic modulo nuisance (Figure 5). This is exactly what a model checker does— canonicalize nuisance out of the abstract state—performed at byte granularity on a real disk, at the below-device level the machine owner observes. I stress that the 3 → 0 was achieved by canonicalization, not by freezing the clock.1 Two adversarial design reviews unanimously 1 These raw and normalized sector counts come from a wholedisk byte-diff of the two runs’ dumped disk images (the 0xE7/0xE8 observation path, §5), recorded in the evaluation dataset— an offline comparison of on-silicon runs, as distinct from the timestamp-clamp witness (§6), which prints directly to the guest

rejected a clock-freeze feature: ext2 timestamps come from CLOCK_REALTIME/settimeofday, not raw RDTSC (freezing the TSC is the wrong lever); Linux’s clocksource watchdog defeats a frozen TSC within a second (operation windows are multi-second); and reaching diff=0 by freezing would be circular. Freezing belongs instead to the deterministic-replay engine (§8), where a masked-timer freeze makes ext2 timestamps bit-exact at no additional cost. The result stands because it is a canonicalization, the same move the abstract state makes for atime. A closing extension of the clock chapter turns the same vantage on sub-second time, and it makes vivid both what owning the machine buys and—just as honestly—what it does not. Because Themis owns the serial log.

12

Table 10: Nanosecond ctime read from the raw on-disk ext4 inode across eight rapid appends, beside the flat whole second the guest’s stat reports (§6). modification

on-disk ctime (ns)

creation append 1 append 2 append 3 append 4 append 5 append 6 append 7 append 8

.013921066 .018000001 .022000002 .027000002 .031000003 .036000003 .044000004 .048000004 .053000005

forces, rather than closes, the honest note in the limitations (§10): a previously-unknown reproduced bug remains the single strongest sentence the evaluation still lacks, and the search—across other filesystems and kernels—continues.

guest stat

7 one second (flat)

block device, it can read the nanosecond ctime of a file straight from the raw on-disk ext4 inode: a granularity available from beneath the device, whereas the second-resolution stat a stock guest’s userspace offers is all that is visible from inside. I parse the ext4 superblock and group descriptor to locate the inode, then read i_ctime together with the i_ctime_extra field whose upper bits carry the sub-second nanoseconds. On a modern Linux guest (kernel 6.17) I made eight rapid appends to a single file, querying and flushing between each, and read the on-disk nanosecond ctime after every modification. The two vantages tell opposite stories (Table 10). From inside the guest, stat reported a flat, unchanging whole second throughout: the entire run fell within one wall-clock second, so at second resolution the file never appears to change time. Read from below, the on-disk nanosecond ctime advanced strictly and monotonically on every single modification—from .013921066 at creation, through .018000001, .022000002, .027000002, .031000003, .036000003, .044000004, .048000004, to .053000005 at the last append. The low-order digits even expose the kernel’s multigrain floor counter—the mechanism that guarantees each observed timestamp is distinct within a single coarse tick [23]. This is exactly the sub-second time behavior that is not visible from inside the guest and lies outside Metis’s abstract state, which sets time aside: a class of observation, and a class of data, that the machine-owner vantage makes available. I am scrupulous about what this is and is not. It is a capability-and-data demonstration, not a newly discovered bug. On this kernel the multigrain implementation is correct: every rapid modification advanced the nanosecond ctime, and I observed no missed-change anomaly, because the earlier multigrain-ctime defects (§2) are fixed in kernel 6.17. What the experiment establishes is therefore the observation vantage and a data class the machine owner alone can produce—not the reproduction of a previously-unknown defect. It rein13

Causal Below-Filesystem Corruption

Themis owns the block device, so it can flip a single bit in a chosen on-disk structure—a controlled fault injection performed from beneath the device—and the guest’s re-mount/re-read reveals the blast radius. Because the fork is a bit-exact ε-copy, the unflipped counterfactual is identical modulo the one bit, so every downstream difference is provably caused by that bit: determinism makes a single run a complete causal experiment (n=1 is sufficient), in contrast to IRON’s manual, policy-level failure fingerprints. I demonstrate a blast-radius spectrum (Table 11). At the silent end, flipping one bit in a file’s data block: the file reads back wrong (a byte changes, e.g. - → ,), the filesystem reports zero error, and other files are intact. ext2 has no data checksums, so the read returns success with wrong bytes—a corruption for which a checker reading syscall returns has no signal to key on. At the fatal end, flipping one bit of the superblock magic (LBA 2, byte 56): the whole filesystem becomes unmountable—maximum blast radius from a single bit. The spectrum is the result: the same one-bit perturbation ranges from completely undetectable to total loss of the volume purely as a function of which on-disk structure it lands in. Because the fork makes the unflipped counterfactual bit-exact, each blast radius is measured rather than estimated—I can point at the one bit that caused it—and the silent endpoint is the sharpest lesson: a filesystem without data checksums cannot notice its own file contents rotting, and a checker reading the same corrupted bytes back through the same driver sees the same success the guest does. A single bit flip thus spans the full range purely by the layer I aim it at: a silently wrong file, a file with corrupt metadata, a directory that loses its named entries, and a filesystem that will not mount. Themis places each flip precisely because it locates the target structure by parsing the on-disk geometry—the same superblockand-group-descriptor walk the timestamp probe uses— so the offset lands on the live image’s inode or directory block rather than a hardcoded guess. (An earlier attempt with LBAs hardcoded from a different file set missed the live structures; parsing the geometry of the image under test fixes that.) A checker above the block device can inject none of these, which is what makes the spectrum a Themis-specific measurement. The corruption injector is a direct sector write

Table 11: Single-bit below-FS corruption blast radius. corruption

mount

blast radius

data block (a bit in a file’s data)

OK

inode field (a file’s i_size)

OK

directory block (an entry’s record length)

OK

superblock magic (LBA 2 @ byte 56)

FAIL

one file’s content—the file reads back wrong, the fs reports no error, other files intact; ext2 has no data checksums, so a checker reading syscall returns has no signal to key on one file’s metadata—the reported size flips (22 to 233 bytes), the fs raises no error, sibling files and the directory listing intact one directory’s entries—the entry chain breaks, so the directory’s named children vanish from a listing while the fs stays mounted and other files are intact the whole fs—one bit renders it unmountable (the maximum blast radius)

into the CoW overlay (corrupt_lba(lba, off, xor) / corrupt_canary), and because it lands in a fork branch’s overlay, the flip is reverted by the same O(dirtied) restore as any other branch write—the corruption experiment is a fork/restore bracket like every other explored node.

8

Deterministic Replay

Everything so far uses the fork to backtrack : run an operation, then restore to the state before it. The same machine-owned fork buys a second capability that a beneath-the-OS vantage makes uniquely cheap—bitexact deterministic replay. Record the nondeterministic inputs of one execution once; then, from the same starting state, feed those same inputs back and the execution re-derives itself bit-for-bit. The classic single-core replay systems—ReVirt [24] on a para-virtual guest, rr [25] as a ptrace tool—run above a shared kernel: the replayer competes with the very software it replays for control of the machine, and recovers determinism from an external interface. PANDA [27] records and replays a full system for reverse engineering, but atop a QEMU emulator rather than on the metal, as does QEMU’s own icount record/replay [30] and the Simics full-system simulator’s reverse execution [29]: all three reproduce a model of the machine, not its real silicon. The closest relative on real hardware is VMware’s deterministic replay [28], a hosted-VMM feature that logged an unmodified single-vCPU guest at ∼5 % record overhead—and was later withdrawn from the product. I do not claim to be the first hypervisor to replay an unmodified guest: ReVirt and VMware established that a decade ago. Themis inverts the vantage. Because the checker is ring 0 of the host world and owns ring −1 of a single-vCPU guest, the guest’s nondeterminism is not something to recover from outside—it is something Themis produces, and can therefore pin. What distinguishes Themis from all of these is not the replay mechanism but the fidelity metric: rather than demonstrate replay by re-running and observing that 14

Table 12: The deterministic record/replay landscape. Themis occupies a distinct cell: a Type-1 hypervisor on real silicon, verifying whole-machine replay fidelity by hashing all of DRAM and disk bit-identical across passes. System

Layer

Real HW

Scope / fidelity

Themis

Type-1

yes

rr [25] ReVirt [24]

user hyperv.

yes yes

SMP-ReVirt [26]

hyperv.

yes

VMware [28]

host VMM

yes

QEMU r/r [30]

emulator

no

PANDA [27]

emulator

no

Simics [29]

simulator

no

Antithesis [22]

host VMM

yes

whole machine, bit-exact (9× hash) one process tree whole OS, uniproc; no machine hash multiproc. via logged interleave 1-vCPU; withdrawn model of the machine model; REfocused model; reverse exec det. by construction

behaviour recurs, Themis hashes the entire physical machine—the whole guest DRAM working set and the whole disk—and shows the two hashes byte-identical across nine passes. A process-scoped recorder (rr) cannot make a whole-machine claim; an emulator or simulator (QEMU, PANDA, Simics) makes it only about its model; and a deterministic-by-construction platform (Antithesis) removes the nondeterminism rather than faithfully reproducing it, so it cannot witness a real hardware-timing artifact such as the Y2038 defect of §6. Single-vCPU is a deliberate scope—the same one VMware shipped and rr accepts—and §10 owns it as such. Table 12 places these systems. This section reuses the ε-copy fork of §4 as a rearmable replay checkpoint and adds only what replay needs on top of it. For a single-vCPU guest with its application proces-

sors held offline, the set of nondeterministic inputs is closed for the evaluated workloads: every one is either produced by Themis or intercepted by it. Every asynchronous interrupt (timer, virtio-blk completion, IPI) is delivered by a host EVENTINJ write, so its vector and instruction-stream position are Themis’s to choose; every byte the guest reads from a device is produced by the virtio and disk backends, and the copy-on-write disk overlay pins the base image; and RDTSC/RDTSCP are intercepted from the VMCB and served. CPUID is intercepted and constant, the LAPIC timer is under host control, and pvclock is a fixed function of a pinned timeline. There is no shared host kernel racing the guest, no second core mutating shared memory, and no external scheduler—the three sources ReVirt and rr work hardest to tame, and that multiprocessor replay pays for by logging the shared-memory interleaving [26], are absent by construction here. The one general input the engine does not yet close is hardware randomness: an intercept-and-serve path for RDRAND/RDSEED is not yet built, a known input-recording hole (§10); the evaluated workloads consume no in-window randomness, so the gap is unexercised but flagged rather than hidden. The checkpoint is exactly the ε-copy fork of §4: a whole-VMCB + GPR + CR2 + XSAVE snapshot, nested-page-table write-protection of the guest working set with copy-up, and a copy-on-write disk overlay, restored in time proportional to dirtied pages, not memory or image size. Replay needs one property backtracking did not: the fork must be re-armable. Recording forks once; every replay pass must restore, re-execute, and restore again from the identical snapshot. I untangle the single-shot fork lifecycle so a restore does not tear the snapshot down, honoring the pending-flush / stalewritable-TLB discipline (§4) on every iteration—a leaf made writable by a copy-up in one pass must be reprotected before the next, or the next pass would see the previous pass’s write. Each restore also re-hashes the working set and asserts it equals the snapshot, so a checkpoint that failed to revert byte-identically cannot masquerade as a stable replay.

8.1

The instruction clock: a determinism gate and a positioner

To replay an asynchronous event I need a deterministic measure of guest progress. I program a performance counter (PERF_CTL0, MSR 0xC0010200; count in 0xC0010201) to the Zen5 retired-conditional-branch event (ex_ret_cond, event 0xD1) with USR, OS, En, and—decisively—GuestOnly (bit 40), so it advances only while the guest runs and freezes across the VMEXIT/VMRUN boundary while my handler runs. This is the clock rr uses on x86, and the one it found needs careful per-microarchitecture validation. It serves as the determinism gate: a fixed guest loop re-run from 15

one snapshot retires the same number of conditional branches, bit-identically, run after run—establishing directly on the target part that a Zen5 PMC is a usable, deterministic replay clock. But the conditional-branch count is piecewise-constant: it does not change across straight-line code, and a rep movsb moving 512 bytes retires zero conditional branches at one repeated RIP. So it names a range, not a point. For positioning I therefore use the monotone retired-instruction counter (ex_ret_instr, event 0xC0), equally deterministic on this silicon, which advances once per instruction: counting to just short of the target gets the replay close.

8.2

Landing at a coordinate

A monotone count still does not, by itself, name a landing spot: a count-then-step lands within a small skid window, and a rep op repeats an RIP. So the landing is decided by a coordinate tuple ⟨RIP, RCX, register-hash⟩—RIP and the register-hash pin the instruction, RCX disambiguates rep iterations—and the replay stops only when all three match. The instruction count gets it close; the tuple lands it. I record a coordinate for asynchronous events only (interrupt vectors); deterministic faults are never logged, because they reproduce on their own and re-injecting one would doublefault. To reach a coordinate I count the retired-instruction PMC to just short of the target and single-step the remaining window: set the #DB exception intercept in the VMCB, set the guest EFLAGS.TF, and add a dispatch arm for #DB (SVM exit code 0x41). Each singlestep trap sets DR6.BS (bit 14); the handler confirms the #DB is its own via DR6.BS, clears only that bit, and— critically—does not advance RIP (the VMCB RIP already points at the next instruction; advancing it would skip an instruction per step and corrupt the count). The guest’s own DR6/DR7 are saved and restored. Two corners make this sound. First, I aim not for transparency but for record/replay symmetry: the CPU pushes the live EFLAGS.TF onto exception frames with no PUSHF to intercept, an irreducible leak, so I ensure stepping is identical in record and replay and scrub pushed frames afterward. I intercept PUSHF and POPF only and merge a shadow-TF so a guest POPF that clears TF does not stop my step clock; IRET emulation (a full frame plus segment reload) is deferred, so the recorded window is kept IRET- and SYSCALL-free (the guest does its one iopl before arming, and SYSCALL’s SFMASK would clear TF and silently stop the step clock). Second, injection honors the interrupt shadow: I read the VMCB interrupt-state field, so an injection whose coordinate lands in a MOV SS shadow would be deferred exactly as silicon defers it (the shadow read is validated; the deferral path is implemented but unexercised by the evaluated injection).

Table 13: Bit-exact replay across nine re-runs. “wholeDRAM” and “whole-disk” state are identical on every Every input is recorded against a coordinate and served pass; the non-vacuity guard proves the workload actuon replay. Asynchronous interrupts are logged as vec- ally ran each pass. tor plus coordinate at each injection. Timestamps are served deterministically: I intercept RDTSC/RDTSCP and workload passes non-vacuity return a pure function of the per-window read index, compute (served TSC) 9 hashes identical served(seq) = ANCHOR + K · seq; the exact constants + free-run injected #DB 9 inject-ctr = 1, ×9 do not matter, only that the served sequence is identi- + single-step-landed #DB 9 inject-ctr = 1, landing logged cal across record and replay. Device bytes need no byte 9 wrote-each, blklog—the virtio-blk backend produces all disk input and raw block write (O_DIRECT) served = 9 the copy-on-write overlay pins the base image, so iden- mounted ext2 create+write+fsync 9 wrote-each, blktical bytes are delivered without one. Hardware ranserved = 54 domness (RDRAND/RDSEED) has no serve path yet (§8). For a workload that reads no timestamp and no randomness in-window and whose only asynchronous event core result (Table 13) is that the engine reproduces a self-lands (a disk completion delivered at the fsync idle recorded execution bit-for-bit across nine record/replay point), the log is essentially empty: the determinism re-runs, with non-vacuity guards proving the workload then comes from freezing plus the checkpoint, not from actually ran each pass. The workloads climb in machina large log. ery: a compute workload reading a served counter; the same plus a free-running injected asynchronous excepThe delivery-fault gate (an implementation les- tion; the same with that exception single-step-landed at son). One hazard appears only once the checkpoint’s its recorded coordinate; a raw block write; and a real write-protection and event injection meet. To replay an ext2 create+write+fsync. The headline is the last row: a real Linux ext2 asynchronous #DB I write EVENTINJ and VMRUN; delivering the #DB pushes an interrupt frame onto the guest filesystem workload—inode allocation, block-bitmap kernel stack, which inside the fork window is write- update, directory entry, data block, and timestamps— protected, so the frame push itself takes a nested-page reproduces bit-exact in whole-DRAM and whole-disk fault in the middle of delivery. A handler that naively across nine re-runs, non-vacuously (the write hit the re-injects on “the exit was an NPF” re-injects the #DB disk every pass) and soundly (the checkpoint reverts on every later write-protected NPF too, a storm that byte-identical each pass: the working-set pre-hash triple-faults the machine; conversely, capping the write- equals its post-hash, and the disk restores Dpost = protection so the push does not fault makes the injection Dpre ). The single-step row is the proof that the coorsilently fail to deliver—a vacuous pass that looks bit- dinate landing (§8.2) and the EXITINTINFO gate (§8.3) exact only because nothing was injected. The fix is to work: an injected #DB is landed at its recorded RIP ask the hardware whether an event is still in flight. On and the replay is bit-exact, with the injection counter an NPF during delivery the VMCB EXITINTINFO field reading 1 on all nine passes. The reproducibility payoff. The point of replay (0x088) records the interrupted event: valid bit (31) set, type field = 3 (exception), vector = 1 (#DB). I re- is to make a nondeterministic outcome reproducible, inject only when EXITINTINFO shows the #DB in flight and the sharpest demonstration is a two-configuration (and copy up the faulting frame page); a post-delivery contrast of the same workload (accumulate one hunkernel NPF has valid = 0 and is handled as an ordinary dred in-window rdtsc reads into a tracked page, then copy-up with no re-injection. This is textbook SVM—a nine record/replay passes, whole-set hash per pass). production VMM such as KVM re-injects interrupted The two differ by a single instruction: whether the events the same way; the lesson specific to replay is RDTSC intercept-and-serve is armed (Table 14). Left only that the checkpoint’s write-protection makes the raw, the nine whole-set hashes are all distinct on real mid-delivery frame-push fault unavoidable, so the gate silicon—3cbd...d2b6, 6983...ab37, 2eec...cdfe, 7660...5d33, 9ed9...603e, is mandatory here rather than incidental. It is what 5a25...e40e, 58b4...a367, 232e...9c32, 7efb...dbff—so the makes the injected-interrupt replay both non-vacuous outcome is flaky. Served from the log, all nine are (the event really lands) and storm-free. identical. Because the two runs are the same workload 8.4 Results: bit-exact replay of a real minus one armed intercept, the difference isolates the mechanism: replay makes a timing-dependent filesystem workload whole-system state bit-exact reproducible, which forkAll data are from the same silicon campaign (AMD Zen5 from-root alone cannot do (restoring the same memory 9800X3D, single-vCPU stock Linux 6.17 guest). The does not stop a raw RDTSC returning a new value each

8.3

Input recording and serving

16

Table 14: Reproducibility contrast. The same workload; the only difference is whether the timestamp counter is served from the log. Serving it makes a timing-dependent whole-system state bit-exact; leaving it raw makes it flaky.

reverted with everything else each pass. (ext4’s multigrain ctime reads the live counter and would drift— documented, not worked around; that drift is exactly what the served-RDTSC path above pins.) This closes a loop with the clock chapter. The Y2038 witness of §6— a 128-byte-inode ext2 clamping any post-2038 timesconfig nine whole-set hashes verdict tamp to 0x7FFFFFFF—is produced by a mount/setserved (from log) all identical reproducible clock/read-back workload, exactly the FS-touching kind unserved (raw TSC) all distinct flaky that Table 13 shows replays whole-DRAM and wholedisk bit-exact, and the same masked-timer freeze that Table 15: Checkpoint cost. Arming (write-protect the gives ext2 timestamps bit-exact at no additional cost 1 GiB working set) is one-time and constant; revert is is what would make that divergence a replayable object: the ⟨checkpoint, served-input⟩ pair would re-materialize O(dirtied). Times at the guest’s 4.7 GHz. the clamp on demand, and the single-step machinery workload arm (once) revert/pass dirtied/pass could land on the instruction where it originates. I state this as a composition argument from results each raw block write 13.85 ms 14 µs few ext2 single op 13.77 ms 26 µs 1 op already on silicon—the Y2038 witness (§6) and the bitext2 nine passes 13.88 ms 27 µs 127 (508 KiB) exact FS replay (Table 13)—not as an end-to-end run: I have not yet executed the single experiment that replays that divergence and single-steps to the clamp, and pass). I scope the causal claim to what the whole-set that unification is the natural next step (§10). hash proves—that the guest’s whole-system state depends on the raw counter and is made deterministic by serving it, with the harness localizing the drift to a 9 Evaluation concrete page in the guest’s timekeeping region (gpa 0x3400000)— not the stronger, unlocalized claim that The evaluation has three legs, fused where possible into the drift is uniquely the accumulator page. The nine single silicon runs: the mechanism (the fork serves distinct unserved hashes also make the FAIL non- and reverts real filesystem I/O on silicon), the checker coincidental, which is what validates the served PASS logic (the DFS/differential/lenses, proven in software as genuine rather than a hash over counter-independent under QEMU), and real-filesystem witnesses (the clock chapter, the corruption experiments, multi-state memory. Cost. The working set is 261,888 present 4 KiB leaves exploration on real ext2). §5–§7 reported the observa(≈1.0 GiB of guest DRAM). Arming the checkpoint— tion and bug-class results; this section reports the fork write-protecting that working set—costs ≈13.8 ms, paid cost and the Themis-vs-Metis backtrack cost model, and once and constant across workloads (it is the working summarizes the mechanism proof. The mechanism itself is proven on silicon. The set, not the workload). The larger arm cost here than in §9 (≈13.8 ms vs ≈10.3 ms) is simply the larger work- fork/restore cycle with real filesystem I/O is siliconing set of this campaign (261,888 vs ∼200,000 leaves); proven in stages, each isolating one variable (one variper-leaf the write-protect cost is the same ∼52 ns, able per hardware run): confirming the O(working-set) arm and O(dirtied) re- • Compute fork (whole-set revert). A multi-pagevert. Reverting each pass is O(dirtied): a full ext2 dirtying compute branch forks and reverts with the create+write+fsync dirties 127 pages and reverts in whole tracked working set (200,000 write-protected ∼27 µs (≈0.2 µs/page), copying up 508 KiB while the DRAM leaves) hashing byte-identically before and 1.0 GiB working set stays shared and is never copied. after (pre == post, match=true), with zero I/O viThe input log is essentially empty for this workload olations (a tripwire confirms no host/device DRAM (no in-window RDTSC exits, no logged interrupt, timer write bypassed the copy-up set) and zero unsound masked), so the determinism comes from freezing plus (drained/alloc-fail) pages. This is the hardware run the checkpoint, not from a large log. that closed the hot-page TLB-bypass hole (§4). A filesystem clock at no extra cost, and a tie to the Clock Chapter. A replay engine must re- • Real FS write served in a fork window. A guest agent mounts real ext2 and issues one produce the guest’s timestamps, and for classic ext2 pwrite(O_DIRECT|O_SYNC) inside a fork window; I get them bit-exact with no clock serving and no field the virtio-blk write is served, the completion IRQ masking. ext2’s coarse i_ctime/i_mtime come from the is injected, and fsync returns (the agent makes kernel wall clock, latched on the timer tick; inside the progress past it—proof the completion was delivered fork window the timer is masked, so the coarse clock through a freshly copied-up used-ring, not a stale is frozen, its state lives in tracked DRAM, and it is 17

Table 16: ε-copy fork revert cost (O(dirtied)). The 38page revert is a real ext2-write branch; the 265-page revert is a synthetic compute-dirty branch (its run’s soundness tripwire is set). # dirtied pages

revert time

µs/page

38 265

9 µs 54 µs

0.24 0.20

base frame). The host disk oracle sees Dmid ̸= Dpre — the write really hit the disk (a positive control).

Table 17: Backtrack cost model: Themis ε-copy revertonly vs Metis end-to-end per-state. Metis costs are derived from its published states/second (parenthesized). The axes differ deliberately—the Themis column is the isolated revert time, the Metis column a full per-state cost (op + fingerprint + reference-compare + restore)— so this isolates the backtrack primitive and is not an end-to-end throughput comparison (where the slower guest, §9, would reverse the ranking). The 265-page Themis point is a synthetic compute-dirty branch. system

• Real FS write fully reverted. The full write+revert cycle: the real FS write’s dirtied pages (37 in the run) plus the used-ring host-write all revert byte-identically (whole-set hash match=true), the disk overlay discards back to the pre-fork image (Dpost = Dpre , reverted=true), and device state restores—via a single-pass-terminate restore (no root-corrupting guest re-run). This is the modelchecker’s core primitive—fork → run an FS op → restore → byte-identical—working end-to-end on silicon. The fork cost is O(dirtied). Restore reverts only what a branch dirtied. Table 16 shows the revert cost scaling with the dirtied-page count: 38 pages (a real ext2-write branch) in 9 µs, 265 pages (a synthetic compute-dirty branch) in 54 µs—∼0.2 µs/page (7× the pages ⇒ 6× the time). Backtracking is the most frequent model-checker operation, and it is silicon-fast because it is O(dirtied), not O(image). The honest bottleneck is the fork side: writeprotecting all ∼200,000 installed DRAM leaves costs a fixed ∼10.3 ms per fork (O(working-set)). This dominates a naive per-fork cost, but it is a one-time cost under re-run-from-root amortization: fork once at the root, then restore-to-root many times, so the 10.3 ms is amortized over the whole campaign and the per-state cost is op-replay plus the 9 µs revert. (A lazy/incremental write-protect is a further optimization, §10.) Themis and Metis are best compared through a backtrack cost model rather than a states/second count— the central quantitative claim—and I am deliberate about not reporting it as states/second. Themis reverts a filesystem state in time proportional to dirtied pages (9–54 µs, independent of filesystem image size); Metis, using a real filesystem as its own reference, must unmount and remount and reload the whole image, i.e. O(image). Table 17 places Themis’s measured 54 µs backtrack (for a 265-page synthetic compute-dirty branch) against Metis’s published backtrack costs derived from its states/second numbers: Metis RefFS 2.86 ms (349.9 states/s), Metis ext4 remount 8.9 ms (112.6 states/s), Metis xfs remount 114 ms (8.8 states/s). The relative advantage is 53× vs RefFS, 18

Themis ε-copy (265-page op) Metis RefFS Metis ext4 remount Metis xfs remount

backtrack cost

relative

0.054 ms 2.86 ms 8.9 ms 114 ms

1× 53× 165× 2100×

165× vs Metis’s ext4 remount, and 2100× vs xfs—and it widens with image size, because Themis reverts only the dirtied set while Metis reloads the whole image. These multipliers compare Themis’s revert-only backtrack against Metis’s end-to-end per-state cost (op + fingerprint + reference-compare + restore), so they isolate the backtrack primitive rather than end-to-end throughput—on a states/second count the slower guest would reverse the ranking (below). This O(dirtied)-vsO(image) gap is exactly the reload cost that makes a real filesystem impractical as its own reference for an in-OS checker, and the reason Metis introduced RefFS; Themis’s fork removes that cost, which is the mechanism behind “every filesystem is its own reference.” It is worth stating why not states/second. A raw states/second campaign would undersell Themis and, worse, rebut the thesis: my end-to-end per-state cost is dominated by the bare-metal guest executing the filesystem operation, which I estimate runs roughly an order of magnitude slower (a bring-up estimate I have not measured directly, and an artifact of the guest bring-up, not the fork mechanism), so a states/second number is guest-bound and would lose to Metis’s native RefFS. The correct claim is the mechanism’s cost model—the fork’s O(dirtied) backtrack—not an end-to-end count on an unoptimized guest. I report the mechanism cost (Tables 16–17) and am explicit about the guest overhead so the number is not misread. Beyond the mechanism, Themis drives an 8-state exploration over a real, unmodified ext2 (S0 empty → S7 mkdir), each state a unique find + stat + contenthash fingerprint—the abstract-state key working on a real filesystem (the dedup and differential source). This is the multi-state demonstration realized as a guestscripted sequence over the proven mount path (no hostdriven DFS yet, §10). The coarse-timestamp finding (§6) surfaced here: two rapid touches receiving the identical nanosecond timestamp. The full checker logic—

bounded DFS with visited-set dedup and fork/restore bracketing, the differential comparison, the clock and corruption lenses, the read-oracle catching an nlinkrefcount leak and a non-atomic rename in the inodelevel model—is proven in software under QEMU; the silicon runs prove the mechanism and the real-filesystem witnesses. In summary, the dataset comprises ∼20 tables and graphs—the machine-owned below-FS measurements (write amplification, write localization, and read amplification), the clock-chapter byte-diff and normalization, the corruption blast radius, and the fork-cost curve; the filesystem-as-reference matrices (the operation–field footprint and the timestamp-semantics matrix); the state-space battery; the clock sweep, granularity, and Y2038 tables; and the backtrack cost model. Critically, it includes data classes—below-FS profiles, byte-level whole-disk diffs, clock sweeps, below-FS corruption— that the beneath-the-device vantage makes available.

10

Limitations and Future Work

The machine-level vantage that yields Themis’s unique capabilities is the same property that makes each of those capabilities a deliberate, silicon-verified increment rather than a barrier the approach runs into: because the checker owns the machine, adding an ability is a matter of building it beneath the guest and proving it on hardware, one variable at a time. What remains is therefore largely a roadmap the substrate enables, not a wall the design hits, and I separate the two below— the genuine, approach-level limitations from the scope I have simply not built yet—and record, for completeness, the capabilities that were limitations in an earlier draft and are now closed. Two of those earlier gaps are now closed and bootverified. The differential read-oracle no longer digests a hash of path ∥ size; it hashes the file’s real content (the model carries the actual bytes), so a sizepreserving content corruption changes the fingerprint and is caught, closing the size-blind gap. And the attested write chain now carries an external length-andtip commitment, so suffix truncation—dropping the tail of the log—is detected, closing the truncation gap. The attestation chain itself remains deliberately quiet infrastructure rather than a headline— PeerReview [19] preempts hash-chained tamper-evidence as a novelty—now with truncation detection added. Turning to the genuine limitations, there are three, and each is a property of the vantage rather than a defect to be patched away. The first concerns deterministic replay, which is now built and demonstrated (§8): the same ε-copy fork, made re-armable, replays a real ext2 workload bit-exact in whole-DRAM and whole-disk across nine passes, and turns a timing-flaky 19

outcome (nine distinct hashes raw) into a reproducible one (nine identical, served). Its residual limitations are honest and bounded. The engine replays a single vCPU; multi-vCPU replay requires logging the sharedmemory access interleaving [26], exactly the cost the single-vCPU scope avoids, and is future work. The single-step skid is bounded but its magnitude is not yet measured across workloads. Hardware-randomness serving (RDRAND/RDSEED) is not yet built—a known input-recording hole the evaluated workloads do not exercise. And because a bare-metal SVM hypervisor cannot run nested under a second hypervisor, every replay result is a physical hardware burn, so I report a curated campaign rather than a statistical sweep. Finally, the replay machinery new to this system—the instruction clock, the coordinate tuple, the single-step, the EXITINTINFO gate—is exercised by the injected-#DB and served-RDTSC paths, not yet by the filesystem headline, whose determinism comes from freezing plus the fork; a single workload that both touches a real filesystem and requires the full machinery would unify the two and is the highest-value next step. The second is crash consistency, where the machine vantage honestly adds essentially nothing that dm-log-writes [10]— which already sees every block write and every barrier beneath an unmodified filesystem—does not; a hypervisor that logged writes and replayed prefixes would merely re-implement an in-tree tool one layer down. I therefore do not claim crash-consistency testing (§2), and the only non-derivative version—pernode-of-the-global-model-checker-graph crash enumeration on the fork/replay substrate—is exactly the integration the Metis group’s own dissertation §7.1.1 [18] lists as an open problem, which I frame (with the crash × clock × corruption cross-product) as collaborative future work rather than a claim here. The third is cost: the bare-metal guest runs the filesystem operation an estimated order of magnitude slower than a native host (a bring-up estimate I have not measured directly), a real price of putting the checker beneath the machine, and it is precisely why I report a backtrack cost model (§9) rather than a states/second figure—a raw throughput count would be guest-bound and would misrepresent the fork mechanism, whose O(dirtied) backtrack is the quantity that actually scales. The rest is roadmap the substrate makes buildable, not weakness. Host-driven exploration at scale—the throughput pillar, scaling the backtrack cost across a large exploration—is designed but deferred as a substantial build: the host acts as the outer driver, rerun-from-root serves as the physical backtrack, and an untracked command-and-report channel survives the revert so the driver can inject operations and read back guest fingerprints across it. The results in this paper are realized instead by a guest-scripted driver over the proven mount path; three earlier candidates for

a backtracking restore proved unsound before I settled on single-pass-terminate, so the at-scale loop remains a substantial, strategic build. The previouslyunknown-bug hunt is the next concrete target, and here the mechanism is already proven—what remains is to point it at a live class. The immediate step is a rapidtouch / near-equality time probe for the multigrainctime class [23] over real ext4, a guest-scripted experiment that needs no new hypervisor code and exploits the coarse-granularity ground truth the clock chapter (§6) already witnessed. A host-side companion to the below-FS instrument—byte-parsing ten on-disk formats without a hypervisor burn— already maps each filesystem’s below-FS time range as a measurement study: FAT and exFAT are immune to the Unix 2038 and 2106 wraps (they store a broken-down date, not a Unix counter) yet hard-cap at 2107, and minix’s unsigned32 seconds clamp at both 1970 and 2106—evidence that the below-FS temporal observation generalizes across filesystems and points toward a broader characterization study. A handful of minor residuals were recorded during development and are noted for completeness. drop_caches was a no-op on the eval guest, so cold reads were forced by umount+remount rather than by dropping caches—a coverage detail, not an inaccuracy in the reported counts. Low guest RAM below the loaded image (the BIOS area and the guest’s own page tables) is outside the tracked range, which is a whole-machine-determinism gap rather than a filesystem-content one. And the copy-on-write disk read is O(overlay-depth), a scaling cliff at large exploration depths that re-run-from-root (depth 1) avoids.

11

Conclusion

Metis showed that model checking finds real bugs in unmodified in-kernel filesystems, and it does so from inside the OS—a simple, portable, and fast vantage that yielded real results. Two of its choices follow from that vantage: it hand-codes a reference filesystem, because cheap snapshotting of in-kernel state is not available to an in-OS process, and it sets time aside as noise. Themis takes the opposite architectural bet, moving the checker beneath the filesystem, onto a bare-metal Type1 AMD-V hypervisor that owns the machine—trading a heavier substrate and a slower guest for more machine control. Owning the machine buys a machine-layer εcopy fork whose restore is O(dirtied)—proven on silicon to serve and fully revert a real virtio-blk filesystem write in 9 µs for the dirtied set—which lets every unmodified in-kernel filesystem be its own differential reference and removes the need for a hand-coded one. It buys belowfilesystem observation: write/read/location profiles and byte-level whole-disk state diffs with nuisance normal20

ization, from which I reverse-engineer the ext2 on-disk layout and prove the disk deterministic modulo nuisance (a clean 3 → 0). And it buys control of the clock, which I foreground: a real Y2038 defect witnessed on real ext2, clamped to 0x7FFFFFFF and persisted across remount, invisible to a time-excluded checker. The same fork, made re-armable, also buys bit-exact deterministic replay (§8): a real ext2 workload replays wholeDRAM and whole-disk across nine passes, and a timingflaky whole-system state (nine distinct hashes raw) becomes reproducible (nine identical, served). I concede crash-consistency to a crowded field and drop attestation as a headline, and I am explicit that the previouslyunknown-bug hunt and the at-scale host-driven exploration remain future work. The claim I make is narrow and, I believe, defensible: when the checker owns the machine, an unmodified filesystem becomes its own reference, and whole classes of below-filesystem and temporal behavior—beneath the syscall vantage an in-OS checker reads—become first-class, silicon-demonstrated objects of test.

Acknowledgments I am grateful to a co-author of Metis for generously sharing the system and its model-checking approach, which sparked this work.

References [1] Y. Liu et al., “Metis: File System Model Checking via Versatile Input and State Exploration,” USENIX Conference on File and Storage Technologies (FAST), 2024. [2] M. Vrable et al., “Scalability, Fidelity, and Containment in the Potemkin Virtual Honeyfarm,” ACM Symposium on Operating Systems Principles (SOSP), 2005. [3] H. A. Lagar-Cavilla et al., “SnowFlock: Rapid Virtual Machine Cloning for Cloud Computing,” European Conference on Computer Systems (EuroSys), 2009. [4] B. Cully et al., “Remus: High Availability via Asynchronous Virtual Machine Replication,” USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2008. [5] A. Agache et al., “Firecracker: Lightweight Virtualization for Serverless Applications,” USENIX Symposium on Networked Systems Design and Implementation (NSDI), 2020.

[6] T. K. Lengyel, “VM Forking and Hypervisor-based Fuzzing with Xen,” Xen Developer and Design Summit, 2020.

[18] Y. Liu, “Advancing File System Model Checking: Coverage, Framework, and Scalability,” Ph.D. dissertation, Stony Brook University, 2025.

[7] D. Song et al., “Agamotto: Accelerating Kernel [19] A. Haeberlen, P. Kouznetsov, and P. Druschel, “PeerReview: Practical Accountability for DisDriver Fuzzing with Lightweight Virtual Machine tributed Systems,” ACM Symposium on Operating Checkpoints,” USENIX Security Symposium, 2020. Systems Principles (SOSP), 2007. [8] S. Schumilo et al., “Nyx: Greybox Hypervisor Fuzzing using Fast Snapshots and Affine Types,” [20] V. Prabhakaran et al., “IRON File Systems,” ACM Symposium on Operating Systems Principles USENIX Security Symposium, 2021. (SOSP), 2005. [9] J. Mohan et al., “Finding Crash-Consistency Bugs with Bounded Black-Box Crash Testing,” USENIX [21] W. Hommel (wolfcw), “libfaketime: A Library to Fake the System Clock,” open-source software Symposium on Operating Systems Design and Improject. plementation (OSDI), 2018. (CrashMonkey and ACE tools; the B3 approach.) [22] A. Pshenichkin, “So You Think You Want to Write a Deterministic Hypervisor?,” Antithesis [10] Linux Kernel, “dm-log-writes: Device-Mapper Log blog, 2024. Writes Target,” Linux kernel device-mapper documentation. [23] J. Layton, “Multigrain Timestamps,” Linux kernel documentation, 2024; see also “The multigrain [11] T. S. Pillai et al., “All File Systems Are Not timestamp saga,” LWN.net, 2024. Created Equal: On the Complexity of Crafting Crash-Consistent Applications,” USENIX Sympo- [24] G. W. Dunlap, S. T. King, S. Cinar, M. A. Basrai, and P. M. Chen, “ReVirt: Enabling Intrusion sium on Operating Systems Design and ImplemenAnalysis through Virtual-Machine Logging and Retation (OSDI), 2014. play,” USENIX Symposium on Operating Systems [12] J. Yang, C. Sar, and D. Engler, “EXPLODE: Design and Implementation (OSDI), 2002. A Lightweight, General System for Finding Serious Storage System Errors,” USENIX Symposium [25] R. O’Callahan, C. Jones, N. Froyd, K. Huey, A. Noll, and N. Partush, “Engineering Record and Reon Operating Systems Design and Implementation play for Deployability,” USENIX Annual Technical (OSDI), 2006. Conference (ATC), 2017. [13] J. Yang, P. Twohey, D. Engler, and M. Musuvathi, “Using Model Checking to Find Serious File Sys- [26] G. W. Dunlap, D. G. Lucchetti, M. A. Fetterman, and P. M. Chen, “Execution Replay of Multiprocestem Errors,” USENIX Symposium on Operating sor Virtual Machines,” ACM SIGPLAN/SIGOPS Systems Design and Implementation (OSDI), 2004. International Conference on Virtual Execution Environments (VEE), 2008. [14] S. Kim et al., “Finding Semantic Bugs in File Systems with an Extensible Fuzzing Framework,” [27] B. Dolan-Gavitt, J. Hodosh, P. Hulin, T. Leek, and ACM Symposium on Operating Systems Principles R. Whelan, “Repeatable Reverse Engineering with (SOSP), 2019. PANDA,” Program Protection and Reverse Engineering Workshop (PPREW), 2015. [15] H. LeBlanc et al., “Chipmunk: Investigating CrashConsistency in Persistent-Memory File Systems,” [28] M. Xu, V. Malyugin, J. Sheldon, G. VenkitachaEuropean Conference on Computer Systems (Eulam, and B. Weissman, “ReTrace: Collecting ExroSys), 2023. ecution Trace with Virtual Machine Deterministic Replay,” Workshop on Modeling, Benchmarking [16] S. Kalbfleisch, L. Werling, and F. Bellosa, “Vinand Simulation (MoBS), 2007. ter: Automatic Non-Volatile Memory Crash Consistency Testing for Full Systems,” USENIX An- [29] P. S. Magnusson et al., “Simics: A Full System Simnual Technical Conference (ATC), 2022. ulation Platform,” IEEE Computer, vol. 35, no. 2, pp. 50–58, 2002. (Reverse execution added in Sim[17] J. Liu, Y. Shen, Y. Xu, H. Sun, and Y. Jiang, ics 3.0, 2005.) “SnapCC: Effective File System Consistency Testing Using Systematic State Exploration,” ACM Transactions on Software Engineering and Methodology (TOSEM), 2025.

[30] QEMU Project, “Record/Replay,” QEMU System Emulation Documentation; icount-based deterministic full-system record and replay.

21

Related documents

• The Logic of Machine Self-Preservation#662129
• The Logic of Machine Self-Preservation#661079
• Qubes OS Security in the Public Record#373334
• SFDS: Selective File Disclosure System#361408
• Generalizing and accelerating consistency checking for non-transactional distributed storage systems#463199