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

作     者：张必红 郭宇 李兆鹏 ZHANG Bi-hong;GUO Yu;LI Zhao-peng

作者机构：中国科学技术大学苏州研究院软件安全实验室江苏苏州215123 中国科学技术大学软件学院江苏苏州215123 

基　　金：国家自然科学基金项目(61202052 61103023 61632005 61229201)资助 

出 版 物：《小型微型计算机系统》 (Journal of Chinese Computer Systems)

年 卷 期：2018年第39卷第1期

页      码：89-94页

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

主 题 词：形式化方法 形式化建模 Coq证明 闪存安全 信息安全 闪存转换层算法 

学科分类：08[工学] 0835[0835] 081202[081202] 0812[工学-测绘类] 

D　O　I：10.3969/j.issn.1000-1220.2018.01.019

馆 藏 号：203282003...