The Design and Implementation of a Verified File System with End-to-End Data Integrity

TL;DR

This paper introduces IFSCQ, a formally verified cryptographic file system that ensures data integrity against malicious tampering and rollback attacks using Merkle trees, enhancing reliability in untrusted storage environments.

Contribution

It presents the first certified file system combining cryptographic primitives with formal verification to guarantee detection of tampering and rollback attacks.

Findings

IFSCQ effectively detects disk tampering and rollback attacks.

The system maintains reasonable performance overhead.

It provides strong integrity guarantees against malicious adversaries.

Abstract

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.