Themis: A Filesystem Model Checker That Owns the Machine
Themis is presented, a filesystem model checker built beneath an unmodified in-kernel filesystem on a bare-metal Type-1 AMD-V hypervisor and the principal result is the clock: Themis drives real ext2 across a clock sweep and witnesses a real Y2038 defect, a 128-byte-inode clamp that a time-excluded fingerprint cannot r...