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

Formal Modeling of the DFTL Algorithm for Based on the NAND Flash

作　　者：张必红 郭宇 李兆鹏 

机构地区：[1]中国科学技术大学苏州研究院软件安全实验室,江苏苏州215123 [2]中国科学技术大学软件学院,江苏苏州215123

出　　处：《小型微型计算机系统》2018年第1期89-94,共6页Journal of Chinese Computer Systems

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

摘　　要：为了保证一种非常经典的适用大规模存储地NAND闪存上的DFTL算法的正确性,对DFTL算法采用了形式化建模的方法来建立一个高可信的形式化模型.根据DFTL算法提出者的设计,我们以此为依据,对DFTL算法的基本数据结构,读写操作和垃圾回收操作以及基本性质进行了形式化的建模和验证,并对文中提出的垃圾回收算法进行了适当的修改和优化,以证明垃圾回收算法的正确性.最后我们针对DFTL算法,设计了一个验证框架,在这个验证框架和形式化的NAND闪存模型的基础上,对DFTL算法的的一些基本性质进行了验证.In this paper, in order to guarantee the correctness of a very classical algorithm DFTL which based on the mass storageNAND flash, we use the formal methods to analysis and model a high trustworthy model of the DFTL algorithm. According to the au-thor＇ s design, we model the basic data structure, the read-write operation, the garbage collection operation and the nature of the DFTLalgodthra. And then in order to prove the correctness of garbage collection algorithm, we model the garbage collection algorithm whichwe have taken some measures to optimize and improve. At last, we design a erification framework and we have proved some basicproperties of the DFTL algorithm based on this framework and a formal model of NAND flash.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]