CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives
CertiFlash provides machine-checked formal verification of SSD flash translation layers, proving isolation, integrity, and ownership invariants to prevent tenant data leaks.
CertiFlash is an open-source formal verification framework for Flash Translation Layers (FTL) in computational SSDs, mechanized in the Rocq proof assistant. It shows that a faulty FTL can corrupt device state at five surfaces (e.g., leaking data between tenants or dropping integrity tags), demonstrated on a DaisyPlus OpenSSD. Designers prove once that every operation of a general FTL model preserves a global invariant covering mapping, isolation, integrity, ownership, and allocation; new designs need only discharge five hypotheses. Across four case studies, added effort was 27-3,231 lines against a 16,489-line framework.