该论文聚焦于以存储为中心的计算（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 固件、多租户隔离以及形式化验证的研究者与工程人员阅读。

本文提出了一种名为 SxSSD 的安全且可扩展的软件定义固态硬盘（SSD）设计。传统 SSD 基于 NAND 闪存，通过块存储接口向操作系统暴露存储功能，但由于 NAND 闪存存在硬件层面的读写约束，需要闪存转换层（FTL）在操作系统 I/O 与原始闪存 I/O 之间进行转换。传统 FTL 固件在物理上与操作系统隔离，形成一种可信计算基，许多安全设计（如抵御恶意软件攻击的数据恢复）可借此在操作系统被攻破时仍保证数据安全属性。然而，这些安全设计通常需要修改 FTL 固件代码，而传统块接口 FTL 不提供修改其内部功能的接口，导致实际实施困难。新兴的闪存存储接口设计（如开放通道 SSD 或分区命名空间）将关键 FTL 功能移入操作系统，虽然简化了 FTL 功能的修改，但模糊了可信边界，使 FTL 不再与操作系统隔离。SxSSD 通过将内部策略定义与原始 FTL 机制解耦，允许可信应用程序动态且安全地定义 FTL 策略和暴露的存储接口，相比开放通道和分区命名空间 SSD 提供了更高的灵活性。更重要的是，SxSSD 保留了传统 FTL 执行隔离性，实现了与传统块接口 SSD 类似的安全性。作者识别并解决了在操作系统被攻破场景下引入的关键安全挑战，并实现了 SxSSD 原型，评估了不同 FTL 策略和存储接口下的开销。实验结果表明，与原生 FTL 实现相比，SxSSD 引入的开销较小。该工作主要面向存储系统安全、操作系统安全领域的研究者和开发者，尤其关注如何在不牺牲安全性的前提下提升 SSD 存储接口的可扩展性和可编程性。