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

论文面向企业数据丢失防护(DLP)与存储介质安全删除难以统一的现实问题，提出一种带“保留感知”语义的版本化固态硬盘(Versioning SSD)。传统 DLP 通常依赖上层应用拦截和文件系统快照，面临性能开销大、回收不彻底、数据残留等挑战；本文把版本管理和保留期控制下沉到SSD内部，每当主机发生覆盖或删除操作时，底层存储控制器不仅记录新版本的映射，也会按策略保留旧版本生命周期，使合法的误删恢复和勒索软件事件取证得以实现，同时通过感知每个版本的最小保留期、最长保留期，让垃圾回收在保证有效版本的前提下尽量缩减对空闲块的消耗，避免写入放大和磨损加剧。文章还着重探讨安全删除语义：达到保留期限的版本应被不可逆擦除，甚至可用物理擦除或密钥销毁机制保证敏感数据不会残留在闪存中。若用于 DLP 策略，还可增加审计契约，使管理员能够以可证明方式确认过期数据已删除。文中很可能设计了某种原型，通过盘内固件或 FPGA 平台测量多工作负载下的吞吐、延迟与回收效率，并与常规快照、Copy-on-Write 文件系统做对比。该项工作的启示是系统安全可进一步“下沉”到存储硬件，把版本控制转化为稳定可信的安全基座，同时兼顾主机侧不可信运行环境。

本文提出了一种名为 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 存储接口的可扩展性和可编程性。

研究者提出了一种基于持久存储 fsync 系统调用的新型隐蔽信道 Sync+Sync。此前已有利用 CPU 缓存和主存构建隐蔽信道的研究，本文则将目光转向内存层次更底层的持久存储。大多数程序会将中间或最终结果以文件形式保存，并可能调用 fsync 将文件同步持久化到存储设备。定量研究发现，即使两个程序不共享任何数据，若同时调用 fsync，其中一方经历的响应时间会显著变长。进一步分析表明，并发 fsync 调用在存储栈的多个层级发生资源争抢，包括共享软件结构（如 Ext4 日志）和硬件资源（如磁盘 I/O 调度队列）。基于此，作者构建了名为 Sync+Sync 的隐蔽信道。在普通固态硬盘上，Sync+Sync 能够以约 0.40% 的错误率实现每秒 20,000 比特的传输带宽，并支持跨磁盘分区、跨文件系统、跨容器、跨虚拟机甚至跨磁盘驱动器的工作方式，无需程序间共享数据。作者还利用 Sync+Sync 发起侧信道攻击，能够精确检测目标数据库的操作（如插入/更新和 B-Tree 节点分裂）。此外，通过检测和分析应用的 fsync 调用频率及刷新数据量，Sync+Sync 可以高精度地区分不同应用程序和网站。这些攻击能力可支持更细粒度的信息泄露。该研究对存储堆栈安全性、云环境隔离机制及系统侧信道防护提出了新的挑战，适合存储系统研究员、安全分析师和云基础设施安全团队阅读。