该论文聚焦于以存储为中心的计算（storage-centric computing）场景下固态硬盘（SSD）固件——闪存转换层（FTL）——的安全与正确性问题。研究背景是：数据密集型应用需要把大量数据从存储搬运到计算单元，产生显著的数据移动开销；把计算下沉到 SSD 内部或近端可以缓解该开销，但这要求修改 FTL 中的地址转换、垃圾回收等策略。作者指出，FTL 属于设备固件，其逻辑直接访问安全关键的设备组件，因此即便功能上完全正确的 FTL，也可能在租户之间泄漏数据、丢弃完整性标签，或把闪存块错误地分配给其他租户。论文首先证明一个有缺陷的 FTL 可以在 SSD 内部的五个“表面”（surfaces）上破坏设备状态，并在 DaisyPlus OpenSSD 平台上进行了演示。作者进一步指出现有 FTL 验证工作的两大局限：(1) 只验证功能正确性，被修改的 FTL 即使违反隔离性、完整性与归属（ownership）约束仍能通过验证；(2) 验证与某一具体 FTL 设计绑定，任何改动都要重做全部证明，代价高昂。为此作者提出 CertiFlash：一个在 Rocq（Coq）证明助理中机械化的 FTL 形式化验证框架。CertiFlash 把 FTL 建模为确定性状态机，并在映射、隔离、完整性、归属和分配五个维度上建立单一全局不变式；在该通用 FTL 模型上一次性证明两件事：(i) 每个 FTL 操作都保持该不变式，(ii) 该模型细化了理想化的块设备语义。对新设计，开发者只需为其自身操作消解五条假设（hypotheses），而无需重做上述两个证明。在四个案例研究中，设计者只需在 16,489 行的框架之上新增 27 至 3,231 行代码，验证工作量显著降低。框架已开源。适合关注存储安全、SSD 固件、多租户隔离以及形式化验证的研究者与工程人员阅读。