  Despite significant research and engineering efforts, many of today's
important computer systems suffer from bugs. To increase the reliability of
software systems, recent work has applied formal verification to certify the
correctness of such systems, with recent successes including certified file
systems and certified cryptographic protocols, albeit using quite different
proof tactics and toolchains. Unifying these concepts, we present the first
certified file system that uses cryptographic primitives to protect itself
against tampering. Our certified file system defends against adversaries that
might wish to tamper with the raw disk. Such an "untrusted storage" threat
model captures the behavior of storage devices that might silently return
erroneous bits as well as adversaries who might have limited access to a disk,
perhaps while in transit. In this paper, we present IFSCQ, a certified
cryptographic file system with strong integrity guarantees. IFSCQ combines and
extends work on cryptographic file systems and formally certified file systems
to prove that our design is correct. It is the first certified file system that
is secure against strong adversaries that can maliciously corrupt on-disk data
and metadata, including attempting to roll back the disk to earlier versions of
valid data. IFSCQ achieves this by constructing a Merkle hash tree of the whole
disk, and by proving that tampered disk blocks will always be detected if they
ever occur. We demonstrate that IFSCQ runs with reasonable overhead while
detecting several kinds of attacks.
