CertiFlash：计算固态硬盘中闪存转换层的正式验证框架
CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives
浏览论文内容
中文总结 AI 辅助
针对计算SSD中FTL修改易出错且现有验证仅覆盖功能正确性的问题，提出CertiFlash框架，基于Rocq证明助手，通过单一全局不变量和细化证明，提供机器检查的安全与正确性验证，显著降低新设计的验证成本。
中文摘要 AI 辅助
数据密集型应用将大量数据从存储移动到计算单元，导致显著的数据移动开销。存储中心计算通过将计算移动到固态硬盘（SSD）内部或附近来减少这种开销。实现这一目标需要修改SSD的策略，例如地址转换和垃圾回收，这些是闪存转换层（FTL）的一部分，即SSD的固件。修改FTL容易出错。由于FTL逻辑可以直接访问安全关键的设备组件，即使功能正确的FTL也可能在租户之间泄漏数据、丢弃完整性标签或将闪存块分配给错误的租户。我们展示了有缺陷的FTL可以在SSD内部的五个界面破坏设备状态，并在DaisyPlus OpenSSD上进行了演示。先前的工作验证了单个FTL设计，但有两个局限性。（1）它仅建立功能正确性，因此修改后的FTL可能违反隔离、完整性和所有权，但仍能通过验证。（2）它绑定到单个FTL设计，因此每次修改都需要重做每个证明。我们提出了CertiFlash，一个用于FTL的正式验证框架，在Rocq证明助手中机械化，为设计者提供机器检查的安全性和正确性证明。CertiFlash将FTL建模为确定性状态机，并在映射、隔离、完整性、所有权和分配上具有单一全局不变量。我们在通用FTL模型上证明了一次：（i）每个FTL操作都保持不变量，并且（ii）模型细化了理想化的块设备。对于新设计，设计者只需对其自身操作提出五个假设，而无需重做任一证明。在四个案例研究中，设计者添加了27到3,231行代码，而框架为16,489行，显著减少了验证工作。CertiFlash是开源的。
英文摘要
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.
发表机构
- ETH Zürich（苏黎世联邦理工学院）
- POSTECH（浦项科技大学）
- King’s College London（伦敦国王学院）
- CISPA（信息安全与隐私保护中心）
机构由 AI 辅助整理，请以论文原文为准。
