Source-linked AI summary
CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives
Harshita Gupta, Mayank Kabra, Rakesh Nadig, Nika Mansouri Ghiasi, Sahand Divsalar, F. Nisa Bostanci, Ataberk Olgun, Konstantinos Kanellopoulos, Jisung Park, Haiyu Mao, Abdullah Giray Yaglikci, Mohammad Sadrosadati, Onur Mutlu
TL;DR
Existing FTL verification can leave security properties of modified designs unproved. CertiFlash uses a Rocq-mechanized framework to verify FTL correctness and security, and across four case studies designers added 27 to 3,231 lines.
Problem
Prior FTL verification largely checks functional correctness for fixed designs, without stating tenant isolation, integrity-tag coverage, or block-ownership properties.
Source: §4.2 · p. 6Method
CertiFlash is a Rocq-mechanized framework that proves invariant preservation and refinement for its FTL model, then lets designers verify customized operations against those guarantees.
Source: §1 · p. 2, §5 · p. 6, §9 · p. 14Results
Across four case studies, designers added 27 to 3,231 lines, and verified FTLs rule out all ten modeled failure states.
Source: §1 · p. 2, §7.2.2 · p. 11Takeaways & Limitations
A compliant FTL discharges five hypotheses rather than redoing the framework’s invariant-preservation and refinement proofs.
Source: §9 · p. 14Prior verification frameworks cover fixed, conventional FTLs and do not establish guarantees that survive modification.
Source: §4.2 · p. 6
Abstract
from arXiv · showhide
Data-intensive applications move large amounts of data from storage to the compute unit, incurring significant data movement overhead. Storage-centric computing reduces this overhead by moving computation near or inside solid-state drives (SSDs). Enabling it requires modifying SSD policies, e.g., address translation and garbage collection, which are part of the Flash Translation Layer (FTL), the SSD's firmware. Modifying the FTL is error-prone. Because FTL logic has direct access to security-critical device components, even a functionally correct FTL can leak data between tenants, drop integrity tags, or assign a flash block to the wrong tenant. We show that a faulty FTL can corrupt the device state at five surfaces inside the SSD, and demonstrate them on a DaisyPlus OpenSSD. Prior work verifies individual FTL designs, but has two limitations. (1) It establishes only functional correctness, so a modified FTL can violate isolation, integrity, and ownership and still pass verification. (2) It is tied to a single FTL design, so every modification requires redoing every proof. We propose CertiFlash, a formal verification framework for FTLs, mechanized in the Rocq proof assistant, that gives designers a machine-checked proof of security and correctness. CertiFlash models an FTL as a deterministic state machine with a single global invariant over mapping, isolation, integrity, ownership, and allocation. We prove once, over a general FTL model, that (i) every FTL operation preserves the invariant and (ii) the model refines an idealized block device. For a new design, a designer discharges five hypotheses about its own operations instead of redoing either proof. Across four case studies, a designer adds 27 to 3,231 lines against a 16,489-line framework, significantly reducing the verification effort. CertiFlash is open source.
1. Introduction
Storage-centric computing reduces data movement, but customizing the FTL introduces correctness and security risks. CertiFlash addresses gaps in prior verification with reusable proofs for customized FTLs.
1. Introduction
- A functionally correct FTL can still expose another tenant’s data, drop integrity tags, or assign a flash block to the wrong tenant.FTL logic accesses shared, security-critical components, and the FTL enforces tenant isolation boundaries.Source: §1 · pp. 1–2
- On a DaisyPlus OpenSSD, FTL-only attacks using ordinary host I/O can silently corrupt data, expose another tenant’s data, or misassign a block.The attacks require no privileged access, and corruption can persist in metadata before a host-visible failure.Source: §1 · p. 2
- Prior FTL verification establishes functional correctness but omits isolation, integrity, and ownership guarantees, while proofs must be rebuilt for each design.Testing and trace replay cover only part of reachable FTL states, and each customization changes which states can be reached.Source: §1 · p. 2
- CertiFlash is a Rocq formal-verification framework intended to give customized FTLs machine-checked proofs of correctness and security.It models shared FTL features and proves invariant preservation and refinement to an idealized block device.Source: §1 · p. 2
- A designer’s modular verification discharges five hypotheses about the FTL’s operations instead of redoing CertiFlash’s existing proofs.The interface includes the FTL state and operations, a refinement map, and proofs that operations preserve the invariant and writes do not lose or corrupt data.Source: §1 · p. 2
- Across four case studies, designers add 27 to 3,231 lines against a 16,489-line framework.The case studies span an orthogonal extension, DFTL, MegIS, and deduplication.Source: §1 · p. 2
2. Background
The background introduces SSD and FTL organization, storage-centric computing, and the ways prior designs customize FTL policies. These modifications span multiple FTL dimensions.
2. Background
- The background covers SSD architecture, the FTL, storage-centric computing, and prior designs’ FTL modifications.It also introduces NAND hardware constraints relevant to FTL operation.Source: §2 · p. 2, §2.1.1 · p. 3
2.1.1. SSD Architecture.
- NAND constraints require the FTL to manage out-of-place writes and their associated metadata.Reads and programs operate on pages, erases operate on whole blocks, and a programmed page cannot be programmed again until its block is erased.Source: §2.1.1 · p. 3
2.1.2. Flash Translation Layer (FTL).
- The FTL maps host logical addresses to NAND pages and manages caching, garbage collection, wear leveling, recovery, data layout, DRAM layout, and the flash controller.Garbage collection and wear leveling relocate live data and update mappings or metadata.Source: §2.1.2 · p. 3
2.2. Storage-Centric Computing
- Storage-centric architectures reduce data movement through in-storage processing near the SSD or in-flash processing inside NAND arrays.The described approaches support applications including genomics and machine learning.Source: §2.2 · pp. 3–4
2.2.1. FTL Modifications in Prior Designs.
- Prior storage-centric designs modify FTL policies across multiple dimensions, including mappings, garbage collection, data layout, and controller commands.The analysis covers 17 designs and records eight FTL dimensions; workloads motivate different combinations of changes.Source: §2.2.1 · p. 4
3. Threat Model
The threat model treats the FTL as untrusted in single- and multi-tenant SSD settings. CertiFlash verifies specified FTL state and operations while holding other device functions and behaviors fixed.
3. Threat Model
- The FTL is untrusted in both target settings: it may be modified to alter metadata or access flash in any order while tenants issue host I/O.The model considers both faulty and malicious modifications.Source: §3 · p. 4, §3.1.2 · pp. 4–5
3.1.1. Single-Tenant SSDs.
- In a single-tenant SSD, an FTL fault can corrupt address translation, silently lose data, or invalidate host integrity guarantees.The tenant owns the whole SSD, and the FTL manages its physical blocks.Source: §3.1.1 · p. 4
3.1. Target Settings
- Tenants share SSD resources, while NVMe namespaces and per-namespace keys express isolation boundaries that the FTL enforces.Sharing physical resources is described as improving utilization and cost efficiency.Source: §3.1.2 · p. 4
3.1.2. Multi-Tenant SSDs.
- In a multi-tenant SSD, each tenant owns a non-empty contiguous logical-address range, and a physical block belongs to the tenant whose address was programmed into it.No block holds data from two tenants; the FTL has direct access to DRAM metadata and flash commands.Source: §3.1.2 · p. 4
3.2. Scope of the Model
- CertiFlash verifies FTL state and six operations, including host I/O, integrity-metadata writes, garbage collection, and wear leveling.It excludes device management and NAND itself, assumes ECC-corrected reads return written data, and does not model concurrency, bad-block retirement, or timing side channels.Source: §3.2 · p. 5
4. Motivation and Our Goal
Custom FTLs can corrupt device state in ways that compromise tenant isolation, data integrity, and block ownership. The section demonstrates these risks on real hardware and motivates reusable verification that covers security as well as functional correctness.
4. Motivation and Our Goal
- The section identifies five failure surfaces and ten real-device failures, while explaining why prior verification does not rule them out.The failures affect tenant isolation, data integrity, or block ownership.Source: §4 · p. 5
4.1.1. Failure Surfaces.
- Across five SSD failure surfaces, faulty FTL actions can expose tenant data, omit integrity tags, or corrupt block ownership and allocation.The surfaces are the host-interface queue, internal DRAM, embedded compute units, flash controller, and NAND chips.Source: §4.1.1 · p. 5
4.1.2. Demonstration on a Real SSD.
- All ten failures were demonstrated on a DaisyPlus OpenSSD, including a remap that let an attacker read a victim’s secret through ordinary NVMe I/O.The attacker read’s SHA-256 matched the victim’s and differed from a control block; no privileged access was needed.Source: §4.1.2 · pp. 5–6
4.2. Limitations of Prior FTL Verification
- Prior FTL verification often checks only functional behavior, leaves isolation, integrity, and ownership unconstrained, and is tied to fixed designs.Existing models also omit storage-centric state and operations such as ownership metadata, garbage collection, and wear leveling.Source: §4.2 · p. 6
- A reusable framework should make customized FTLs inherit isolation, integrity, and ownership guarantees instead of requiring full proofs for every change.CertiFlash aims to provide designers with machine-checked proofs of correctness and security.Source: §4.2 · p. 6
5. CertiFlash: Formal Verification Framework
CertiFlash formalizes an FTL against a global invariant and an idealized block device. It proves these guarantees at both the operation and command levels, and defines failure as reaching a state that violates the invariant.
5. CertiFlash: Formal Verification Framework
- CertiFlash proves that FTL operations preserve a global invariant and that the FTL refines an idealized block device.The invariant is a conjunction of correctness and security properties; refinement makes host-visible reads match the idealized device.Source: §5 · p. 6
- The framework proves its model once at the operation level and carries guarantees down to the commands an FTL can issue directly.All proofs are mechanized in Rocq.Source: §5 · p. 6
- An FTL failure is reaching a state that violates the global invariant when execution starts from a well-formed state.The paper treats the components through which the FTL introduces such a state as failure surfaces.Source: §5 · p. 6
5.1. The FTL Model
CertiFlash models the FTL as a deterministic state machine and relates its concrete state to an abstract block-device specification. Its state, operations, and lower-level commands capture both host-visible behavior and FTL bookkeeping.
5.1. The FTL Model
- The FTL model is a deterministic state machine whose state records mappings, page metadata, ownership, allocation, and encryption keys.It has operations, a transition function, and a well-formed initial state; each operation expands into lower-level commands.Source: §5.1 · p. 6
5.1.1. Abstract Specification.
- The abstract specification tracks data by logical address and page offset, while abstracting away ownership, physical layout, and free-block management.Reads return stored data, writes update it, and invalidation makes it undefined.Source: §5.1.1 · pp. 6–7
5.1.2. Concrete State.
- The 16-field concrete state includes mappings, page state and metadata, ownership labels, allocation data, and device-global encryption-key metadata.The fields are grouped by role in Table 2.Source: §5.1.2 · p. 7, Table 2 · p. 7
5.1.3. Operation Semantics.
- Six operations cover reads, writes, invalidation, tag updates, garbage collection, and wear leveling; rejected operations leave the state unchanged.Operation-level theorems assume the transition succeeded and returned a successor state.Source: §5.1.3 · p. 7, Table 3 · p. 7
5.1.4. Command Semantics.
- Operations expand into flash and metadata commands, including programming pages with supplied reverse mappings and integrity tags.A fresh-address write uses a barrier, mapping command, program command, and closing barrier; invalid operations issue no commands.Source: §5.1.4 · p. 7
5.2. Global Security Contract
CertiFlash’s contract combines a global invariant over concrete FTL state with a refinement relation to an abstract device. The invariant supports both refinement and the stated security properties, while stronger threat models require additional preservation proofs.
5.2. Global Security Contract
- The contract pairs an invariant on internal FTL state with a refinement relation connecting concrete state to the abstract specification.The invariant has 27 clauses plus two well-formedness conjuncts.Source: §5.2 · p. 8
- The invariant clauses are derived from FTL designs and known failures, and support proofs of refinement, tenant isolation, data integrity, and block ownership.A stronger threat model adds clauses, whose preservation must be proved under all six operations; already-verified designs must re-discharge their hypotheses.Source: §5.2 · p. 8
- Refinement relates an abstract data value to a concrete live page that holds the same data, so reads return matching values on both devices.The two well-formedness conjuncts do not constrain an FTL.Source: §5.2 · p. 8
5.3. Proving the Global Security Contract
CertiFlash proves invariant preservation and refinement at the operation level, then connects those guarantees across traces and to NAND command execution. Command precondition bundles constrain individually issued commands.
5.3.1. Operation Level.
- Every operation preserves the invariant, preserves the refinement relation, and composes with other operations to provide both guarantees over whole traces.The trace-level simulation pairs each concrete operation with its abstract counterpart while R and the invariant hold throughout.Source: §5.3.1 · pp. 8–9, Figure 2 · p. 8
- Invariant preservation is proved by case analysis for each operation, with writes reestablishing all 27 clauses after invalidating the old page, programming a new one, repairing mappings, and advancing the write frontier.Maintenance operations rely particularly on Inv11, Inv15, Inv17, and Inv24.Source: §5.3.1 · p. 8
- Each valid execution from q0 preserves every global-invariant clause and refines the abstract device’s run of the same trace.The initial state is separately proved to satisfy every clause.Source: §5.3.1 · p. 9
- Operation expansions are connected to operation-level proofs by agreement, while realizability ensures each program targets an erased page when it executes.Agreement alone does not establish realizability.Source: §5.3.2 · p. 9
5.3.2. Command Level.
- Each command issued individually preserves the invariant when its precondition bundle holds; CertiFlash supplies decidable checks evaluated before execution.A faulty FTL can bypass verified operations by issuing commands directly; the final command restores the invariant, assuming each operation runs to completion.Source: §5.3.2 · p. 9, Table 5 · p. 9
6. FTL Verification Workflow
CertiFlash offers direct verification when a design changes the invariant and modular verification when it keeps it. The modular route projects a custom FTL onto the model and discharges five hypotheses to obtain a certificate.
6. FTL Verification Workflow
- Designers choose direct verification for a changed invariant or modular verification to reuse CertiFlash’s invariant-preservation proofs; the latter packages five discharged hypotheses into a certificate checked by Rocq and coqchk.The certificate adds no proof obligation; its status depends on whether the designer’s proofs introduce axioms.Source: §6 · p. 9, §6.2 · p. 10
6.1. Direct Verification
- Direct verification proves each operation preserves the invariant and refinement relation, and is required when a design changes the invariant.Deduplication changes injectivity and reverse mapping, so its operations must be proved against a modified invariant.Source: §6.1 · p. 9
6.2. Modular Verification
- For modular verification, designers supply custom state and operations, project that state onto FTLState, and prove five hypotheses: three invariant-preservation properties and two data-correctness claims.The two data claims are read-after-write correctness and that a write to one address does not disturb another.Source: §6.2 · p. 10, Figure 3 · p. 10
- New operations that change only a design’s own state can use the reuse library; operations that change CertiFlash’s state use command sequences whose precondition bundles preserve the invariant.CertiFlash supplies per-command results but does not generate the sequence.Source: §6.2 · p. 10
7. Evaluation
Across four FTL case studies, CertiFlash lets designers reuse proofs when they preserve its global invariant, while a changed invariant requires direct verification. The evaluation also proves ten failures reachable from well-formed states and shows how verified operations or checked preconditions rule them out.
7.1. Evaluation Methodology
- The evaluation builds and checks the Rocq proofs on an Apple M5 Pro; a clean build takes 93 seconds.The development comprises 28 Rocq files and 21,884 lines, with every listed definition and theorem statement closed with Qed.Source: §7.1 · p. 10
7.2. Reachability of Failures
- Ten failures across five attack surfaces are proved reachable from well-formed states by single commands issued without their precondition bundles.The proofs cover six distinct invariant clauses; the table lists each failure, its command, and a clause it falsifies.Source: §7.2 · p. 11, Table 7 · p. 11
7.2.1. An Example: L2P Aliasing at FS#2.
- L2P aliasing maps an attacker page to a victim’s physical page, violating mapping injectivity and enabling a read of the victim’s data.The PrimMapAddr bundle rejects the command when another logical page already maps to the target page.Source: §7.2.1 · p. 11
- Either using CertiFlash’s operations or gating direct commands on their bundles rules out all ten failures.The former preserves the invariant from a well-formed start; the latter relies on the bundles’ sufficiency to preserve it.Source: §7.2.2 · p. 11
7.3. Case Studies
- Designers add 27 to 3,231 lines against a 16,489-line framework across four case studies; effort tracks the local invariant a design adds.The read-disturb extension adds 27 lines; DFTL adds 844, MegIS adds 1,293 on top of DFTL, and deduplication adds 3,231.Source: §7.3 · pp. 11–12
- The read-disturb counter extension preserves the global invariant and leaves reads unchanged, so it needs no new global invariant.Nearly all its verification effort is defining the new state and operations.Source: §7.3 · p. 12
- DFTL reuses the global invariant but proves a local dftl_ok invariant connecting its cached mappings and translation-page image to the flash mapping.Its 844 added lines include 192 lines proving dftl_ok preservation and 143 lines discharging the five interface hypotheses.Source: §7.3 · p. 12
- MegIS adds range mappings and an Irange invariant; deduplication changes the global invariant to permit sharing only within a tenant’s namespace.MegIS proves its range mappings remain consistent after operations that can relocate pages. Deduplication adds 3,231 lines and re-proves results affected by its invariant changes.Source: §7.3 · p. 12
8. Related Work
Prior verification work covers fixed FTLs, functional behavior, or proofs within one storage stack, but generally does not give a differently designed FTL an inherited security contract. CertiFlash instead proves isolation, integrity-tag coverage, and ownership properties that compliant FTL designs inherit.
FTL and flash file-system verification
- Earlier FTL frameworks verify functional refinement or fixed implementations, while Qiao et al.’s framework requires a new FTL to re-prove its supplied invariant and omits garbage collection and wear leveling.CertiFlash fixes its invariant and allows a design implementing CUSTOM_FTL to inherit it.Source: §8 · p. 13
Verifying flash below the file system; File systems verified above a block device
- Other flash and file-system verification efforts check individual designs, and none of those described constrains tenant ownership.DiskSec’s confidentiality guarantee applies to one system rather than any FTL meeting an interface.Source: §8 · p. 13
Properties beyond functional correctness
- CertiFlash adds machine-checked proofs of tenant isolation, integrity-tag coverage, and block ownership, with a contract inherited by another FTL design.It also formalizes five failure surfaces and proves a reachable failure at each.Source: §8 · p. 13
Layered, concurrent, and crash-safe storage verification
- Layered storage proofs compose components within one stack, but do not transfer a guarantee between competing FTL implementations.Perennial is identified as infrastructure most directly applicable to adding concurrency to CertiFlash.Source: §8 · p. 13
- CertiFlash models one FTL invocation at a time, and timing contention and host-memory-buffer leakage are outside its model.The paper proves precondition bundles sufficient but does not build firmware that evaluates them.Source: §8 · pp. 13–14
9. Conclusion
CertiFlash provides a Rocq-mechanized framework for verifying customizable FTLs. It proves invariant preservation and refinement once, then lets compliant designs inherit those proofs by discharging five hypotheses; four case studies require 27 to 3,231 added lines.
9. Conclusion
- CertiFlash defines a global invariant over FTL state and proves both its preservation and refinement to an idealized block device.A compliant design discharges five hypotheses rather than redoing the proofs; the framework formalizes five failure surfaces and demonstrates failures on a DaisyPlus OpenSSD.Source: §9 · p. 14
- Across four case studies, designers add 27 to 3,231 lines against the framework’s 16,489 lines.The proofs rely on the Rocq kernel and standard library, with no admitted lemmas, classical reasoning, or axioms.Source: §9 · p. 14
- Each of the five failure surfaces has a failure shown reachable by a single command issued without its precondition bundle.The failures are demonstrated on a DaisyPlus OpenSSD.Source: §9 · p. 14