形式化建模运行在NAND闪存上的DFTL算法

• 作者: 张必红 李兆鹏 郭宇
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 形式化方法 形式化建模 Coq证明 闪存安全 信息安全 闪存转换层算法
• 年，卷（期）: 2018,（1）
• 所属期刊栏目: 计算机软件与数据库研究
• 页码范围: 89-94
• 页数: 6页
• 分类号: TP311
• 字数: 7234字
• 语种: 中文

摘要

为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性,对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计,我们以此为依据,对DFTL算法的基本数据结构,读写操作和垃圾回收操作以及基本性质进行了形式化的建模和验证,并对文中提出的垃圾回收算法进行了适当的修改和优化,以证明垃圾回收算法的正确性.最后我们针对DFTL算法,设计了一个验证框架,在这个验证框架和形式化的NAND闪存模型的基础上,对DFTL算法的的一些基本性质进行了验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李兆鹏	中国科学技术大学苏州研究院软件安全实验室	17	99	7.0	9.0
2	郭宇	中国科学技术大学苏州研究院软件安全实验室	12	38	3.0	6.0
3	张必红	中国科学技术大学苏州研究院软件安全实验室	1	0	0.0	0.0