针对NAND闪存硬件的形式化建模

杨龙婴，郭 宇

（1.中国科学技术大学计算机科学与技术学院，合肥230026；

2.中国科学技术大学苏州研究院软件安全实验室，江苏苏州215123）

针对NAND闪存硬件的形式化建模

杨龙婴1，2，郭 宇1，2

（1.中国科学技术大学计算机科学与技术学院，合肥230026；

2.中国科学技术大学苏州研究院软件安全实验室，江苏苏州215123）

为形式化地验证存储系统中软件的可靠性，引入NAND闪存硬件的形式化模型定义。根据NAND闪存接口标准ONFI，采用形式化语言对NAND闪存硬件的语义进行建模，包括ONFI定义的NAND闪存硬件的存储层次结构、闪存硬件芯片处理命令的内部工作流程、闪存硬件的命令集，以及在此基础之上定义的闪存等基本操作。该NAND闪存形式化模型在定理证明工具Coq中定义实现，其性质在Coq中得到完整证明，可以用于定义和验证基于NAND闪存的存储系统软件。

形式化验证；Coq证明工具；闪存设备；形式化建模；高可信软件；存储系统

1 概述

近年来NAND闪存（NAND Flash）以其高集成度、低成本、功耗小、抗震性好［1］的存储特点在从嵌入式系统到云计算平台上都得到了广泛的应用［2］。这其中包括了各种安全攸关的领域，例如航空航天、核电与医疗器械等。对于亟需高可信软件的领域来说，基于NAND闪存的存储系统也亟待进行形式化验证。比如美国宇航局的勇气号火星车曾因为基于闪存的文件系统算法出现了未被发现的设计缺陷的问题而停止运行了10 d［3］；大型云计算供应商亚马逊的数据中心也曾因为遭受断电而遗失了大量存储在闪存存储系统上的数据，并因此承受了经济和信誉方面的损失［4］。为了构建高可信的存储系统，需要对运行在存储介质之上的文件系统进行形式化验证。对于基于NAND闪存硬件的文件系统而言，验证文件系统需要一个可以真实地反映硬件行为的形式化的NAND闪存模型。

形式化模型应该能够真实地反映出NAND闪存硬件的结构、内部的状态转移及其与外界命令的交互。这样才能保证在该模型上经过验证的文件系统代码也能可靠地运行在真实的硬件上。

近年来已经逐渐有不少研究开始关注验证存储系统的可靠性问题。例如，文献［5］提出一个基于NAND闪存的文件系统，并对其进行形式化分析，澳大利亚NICTA（National ICT Australia）的研究组在形式化验证过内核seL4［6］之后，开始着手研究如何验证一个基于NAND闪存的文件系统BilbyFs［7］。但是他们的工作都基于过于简化的NAND硬件模型。例如文献［8］的简化NAND模型存在着以下与真实硬件不符的问题：（1）NAND闪存模型中的层次结构缺少plane层。（2）模型仅声明了3种NAND闪存上的驱动接口，即读、写、擦除，而不是真实芯片的（命令与数据）输入输出行为。（3）模型缺少对硬件操作失败状态的刻画。虽然Butterfield等人曾经利用Z Notation给出了一个在结构上接近真实的NAND闪存的硬件模型［9］，但是他们的NAND闪存模型仍然存在上述第（2）点、第（3）点描述的问题。

本文给出了一个能解决上述3个问题的模型。根据一个被多数主流闪存生产商广泛认可的NAND闪存接口规范ONFI（Open NAND Flash Interface）［10］，在形式化验证工具Coq［11］中对NAND闪存硬件进行了形式化建模。这个形式化模型的定义也能较为容易地移植到其他的形式化工具，如Isabelle/HOL［12］，PVS中。

2 闪存硬件与证明工具Coq

2.1 NAND闪存结构

一个闪存设备由一个或若干个Target组成，如图1所示。每个Target包含了一组逻辑单元（Logical UNit）。逻辑单元是NAND闪存中能够独立运行命令的最小单位。每个LUN有一个或多个Plane。每个Plane由1 024个～4 096个块（Block）组成。块是NAND闪存中最小的擦除单元，由若干个页构成。页由两部分结构组成：一部分是主数据区（Data Area），用来储存数据；另一部分是闲置区域（Spare Area），通常被用来存储校验码和一些标记位。

图1 NAND闪存设备存储结构

NAND闪存设备还具有数据传输总线、地址传输总线、命令传输总线、输入输出控制、控制逻辑单元和各类寄存器，如图2所示。地址传输总线分为行地址总线和列地址总线2种。这是由于在ONFI中，在NAND闪存上寻址，地址需要分为行地址和列地址2种。行地址包含了LUN号、块号和页号；列地址则为页内偏移。为了暂时存储数据、地址和命令，NAND闪存提供了多种寄存器。每个Plane有一个页寄存器（Page Register）。每个LUN有一个命令寄存器（Command Register）和一个地址寄存器（Address Register）。页寄存器用来暂时存储页数据。命令寄存器和地址寄存器分别用来暂时存储最后获得的命令和地址。此外，每个LUN会有一个状态寄存器（Status Register）来储存一些必要的状态值。当设备允许多个Plane并行处理命令的时候，每个Plane会有一个独立的状态寄存器的结构。

图2 NAND闪存设备工作结构

2.2 NAND闪存操作

一个典型的NAND闪存操作的工作流程是由若干个输入部分，包括命令输入、地址输入、数据输入，以及数据输出部分组成。以读操作为例，首先输入输出控制部分将发送一个30H命令到命令寄存器，然后发送列地址和行地址到地址寄存器，继而发送一个读确认命令00H到命令寄存器，然后等待设备将指定存储单元的页内容读取到页寄存器中，在控制逻辑单元得到一个就绪信号之后，则开始从总线上向外输出数据。图3给出了一个在读操作中会出现的状态转换图作为状态转移的例子。

图3 NAND闪存读操作的状态转换示意图

由上述读写操作的工作流程可以发现：（1）NAND闪存操作并不是一步完成的。一个操作会被拆分为命令传输、地址传输和数据传输3个部分；（2）NAND闪存操作需要等待设备发出就绪信号，并不是一个不间断的单向的往NAND闪存发送地址命令并进行处理的过程；（3）NAND闪存操作的工作不仅仅涉及NAND设备存储结构本身，也涉及了各类寄存器。除此之外，NAND闪存操作可以被主动打断。重置命令（Reset）就是用来打断读、写和擦除操作的。如果命令寄存器在读写和擦除操作中接收到了重置命令，那么读写和擦除就都会被强制中断。

2.3 形式化验证工具Coq

定理证明辅助工具Coq［10］不仅提供了一个交互式的证明环境，用来进行逻辑推理，还提供了一个强大的形式化语言——Gallia语言。该语言基于一种名为归纳构造演算CiC（Calculus of inductive Constructions）的高阶多态类型化lam bda演算。采用Gallia定义的NAND闪存模型，不仅可以形式化地定义闪存的存储结构、操作接口、模型规范，还可以在Coq中对模型的一些基本性质进行严格的证明。

3 NAND闪存的内部结构

本节根据ONFI规范真实地定义了NAND闪存的层次化结构。

3.1 数据单元定义

在NAND闪存中，数据存储的最小单位是字节（Byte）。NAND闪存中存储的字节可能为空（擦除状态），也可以为其他值：

在Coq中，用Inductive类型来刻画一个具有多种取值的数据类型。由上在Coq中定义数据如下：

这个定义表示数据为一个字节的有序列表。

3.2 NAND闪存架构定义

如2.1节中所述，ONFI中NAND闪存的架构分为6层，本文在Coq中由下至上对它们进行了定义。3.2.1 页

页是NAND闪存读写的基本单位，由相连的主数据区和备用区域组成。

下面以一个具体的NAND设备为例来描述如何定义NAND架构。在Coq中在配置文件里分别定义了页的主数据区和备用区域的大小：

在NAND中，页的状态有空页、有效页和无效页（写入失败的页）3种状态：

在Coq中，Record关键字可以定义一个具有多个域的结构体。这里page就是具有page-data和page-state2个域的结构体，它的构造函数是m kpage。page-data不仅包含了页的主要数据，也包括了闲置区域内的数据信息。

当需要定位一个页时，可以先由行地址找到页所在的块，再由列地址找到页在该块中的具体偏移。以下分别是页内偏移、块号和页号的Coq定义。其中页内偏移和块号都是一个自然数，而页号则是由块号和页内偏移组成的二元组。

3.2.2 块

块是由一组连续的页构成的，是NAND闪存进行擦除的基本单位。

块的状态有3种：有效块，无效块（即擦除失败的块）以及坏块：

除了块的状态之外，块的另一个重要参数是块的擦除次数。NAND闪存的主要特性之一就是它不支持原地写入（in-place update）。在写入一个已经存在的物理页时，必须先擦除包含此页的整个块。这种特性也被称为擦后写（Erase Before W rite）。然而对于一个NAND闪存中的块来说，可擦写次数是有限的。如果擦写次数超过硬件所能接受的上限，那么块的工作就会不正常。由上，在Coq中定义块为如下结构：

其中，block-pages表示了块内的所有页；blocknext-page是一个指向块内第一个空页的位置的指针；block-erase-count记录了当前该块的擦写次数；block-state是块的状态记录。

3.2.3 Plane构成

Plane由一组块构成，每个Plane具有一个独立的页寄存器，因此多个Plane可以并行进行读写操作。

页寄存器是用来暂时存储向plane内部发送或从plane中取出的页数据的。

3.2.4 逻辑单元

逻辑单元是NAND闪存中独立执行命令的最小单位，由若干个plane构成，这些plane共享一个状态寄存器、一个地址寄存器和一个命令寄存器。

在ONFI中，一个状态寄存器由8位组成。由于篇幅有限、为增加易读性，本文略去了一些繁琐的硬

件规范，只模拟了Ready/Busy状态位和Success/ Fail状态位。本文的形式化方法可以很容易地扩展成完整的ONFINAND硬件规范。

在本文的Coq实现中，设定每个逻辑单元具有2个plane。LUN在Coq中的定义如下：

lun-status-RB表示Ready/Busy状态位；lunstatus-SF表示Success/Fail状态位；lun-cm d-reg表示命令寄存器；lun-addr-reg表示地址寄存器；lunintern-state标识了lun所在的状态。其中，Success/ Fail状态位描述硬件操作是否成功。需要注意的是，按照大多数厂商提供的硬件规格和本文所遵从的ONFI规范，在真实的NAND闪存硬件操作的流程中，只有写和擦除操作会失败，读操作不会失败，只会读到空数据。因此，Success/Fail位会真实地反映出诸如写入非法地址、擦除非法地址等硬件操作失败的情况。在本文模型中，可以通过读状态命令来从数据总线上得到状态寄存器包含的内容。

3.2.5 Target构成

一个Target是由若干个逻辑单元（LUN）构成的。如果是在一个具有多个Target的NAND闪存中，每一个Target会具有一个独立的片选信号。本文只考虑具有一个逻辑单元的Target的NAND闪存。

3.2.6 设备

一个设备是由一个到多个Target组成的完整NAND闪存系统。在本文的例子中，每个设备只有一个Target。

4 NAND闪存设备的命令处理

NAND闪存设备操作如2.2节所述，是一种会经过多个状态，涉及一个或更多命令码的接收，并且可能出现操作失败的复杂逻辑。为了能够真实地在硬件行为层面对NAND闪存进行建模，在定义了所涉及的命令集合和寄存器的基础上，本文详细定义了发送命令、发送地址、等待设备就绪、数据输入输出的操作语义。

NAND闪存操作可被进一步区分为基础操作和高级操作2种。基础操作指每一种闪存设备都必须实现的操作，比如读写操作，没有这些基础操作NAND闪存就会无法工作；高级操作的实现要依赖厂商对于硬件的优化设计，比如对于同一个LUN的多个p lane进行写入的命令，如果闪存设备的LUN仅有一个plane，就不能支持这一类高级操作。通常高级操作是用来提升闪存操作效率的，没有这些高级操作，闪存依然能够正常工作。为简化起见，只考虑基础操作。

在真实的闪存时序操作中，一个基本的操作可能涉及多于一个的具体命令。本文所模拟的命令集合如表1所示。

表1 NAND闪存命令

在表1中，命令码是指NAND闪存从总线上接收的16进制命令代码。这些命令码分别对应到不同的命令，用于在操作流程中控制和标示下一个要进行的步骤。这些命令码的操作语义在Coq中描述。发送命令的操作语义在Coq中定义如下：

send-cmd的操作语义表示从一个设备状态下，发送命令到设备之后，设备转移到另一个状态。输入device是一个设备。cm d是设备从总线上接收的命令，根据不同的命令，省略部分的代码执行不同的操作和状态转移。最后send-cm d函数返回一个达到一个新状态的设备device或者一个处于未定义状态的设备device。未定义状态描述和概括了一种情况：设备得到的输入不是期待的输入，比如一个已经得到了读取目标页地址的设备所期望的输入是一个读确认命令，那么如果在这个时候发送一个写开始命令给设备，就会造成一种未定义的结果。这个可能包含未定义状态的返回值由以下Coq定义描述：

在send-cmd函数中，A这个类型变量就是device。因此当设备所到达的状态是一个合法的确定状态时，send-cm d会返回一个Ok device；当设备所到达的状态是一个非法状态的时候，会返回一个Unknow n。

大部分的NAND闪存操作都需要通过总线传输地址来指定具体操作执行的位置。发送地址的操作分为发送行列地址和仅发送行地址2种。这种区分来自于有些操作仅仅需要指明块所在的位置而不需要指定页和页内偏移。这2种发送地址的操作语义在Coq中的定义如下：

在这2个函数中，函数接收一个设备和一个地址作为输入，根据当前的设备状态，进行状态转移和操作，最后返回一个新的设备状态或者一个未定义状态。

在一部分NAND闪存操作中，会出现需要等待设备准备好数据的情况，必须要等待状态寄存器显示设备是Ready的，方能进行下一步子操作。这种等待设备就绪后进行状态转移的操作语义在Coq中被定义如下：

这个操作语义的定义仅仅允许状态寄存器显示设备Ready时进行下一步的状态转移。

输出数据的操作语义在Coq中被定义如下：

5 NAND闪存设备的工作流程及性质

本节将使用上一节定义的NAND闪存设备的命令来刻画闪存的工作流程。由于篇幅所限，在这里只列举读操作、写操作和擦除操作的流程和在Coq中的形式化定义。

5.1 读操作

读操作的目的是从NAND闪存中的某个页内读出这个页所保存的全部或部分数据。读操作的执行流程如下：

（1）发送读开始命令（00H）到设备；

（2）发送列地址和行地址到设备，设备找到对应读取起点；

（3）向设备发送一个读确认命令（30H），设备在接收到读确认命令之后会按照行地址和列地址读出由列地址开始到页末的所有数据到页寄存器中，并设Ready/Busy标志位为true；

（4）在等待设备读取数据到页寄存器就绪期间，设备并不向数据总线传输任何数据；

（5）当设备就绪之后，开始通过数据总线向输出端发送数据。

读操作在Coq中的形式化定义如下：

5.2 写操作

写操作的目的是向NAND闪存中的某个页写入数据。写操作在Coq中定义如下：

该定义与读操作类似。

5.3 擦除操作

擦除操作被用来擦除某个块的数据，该操作以块为基本单位。擦除操作在Coq中的定义如下：

5.4 NAND闪存设备模型的性质

本文中的形式化闪存模型满足真实NAND闪存工作流程的常见的性质，由于篇幅所限，仅列部分性质如下：

性质1 在执行了正确的读、写或擦除操作后，设备一定会进入空闲状态。

性质2 擦除或写操作正确执行后，设备中的状态寄存器R/B位为Ready，S/F位为Success。

性质3 对设备中的某一块进行擦除后，该块中的每一页中的数据都为空（OxFF）、且块擦写次数加1。

性质4 对某一块进行擦除或写入后，其他所有块，其各状态均与操作执行前完全相同。

性质5 当给出的擦除地址超出寻址空间时，擦除失败，状态寄存器中S/F位为Fail，R/B位为Ready。

这些性质均可在Coq中被证明。

6 结束语

NAND闪存硬件规格各异，内部状态转换复杂，因此对于NAND闪存之上运行的嵌入式软件是否可靠进行验证一直是一个难点。本文以ONFI规范所刻画的一类典型NAND闪存为对象，对NAND闪存的真实层次结构和操作中硬件层面的行为进行了建模，能够描述硬件操作是否成功，并已经能够得到证明其上驱动命令的方法。本文的贡献在于：

（1）本文根据ONFI进行建模，不仅描述了带有Plane的NAND闪存结构，还描述了现实NAND闪存中存在的逻辑单元、Target、设备等结构。

（2）该模型在声明了读、写、擦除、读ID、读状态和重置这几个操作的基础上，切实地描述了这些操作中所涉及的硬件层面的行为，比如命令码的接收、地址的传送、数据的输入输出、寄存器的控制和NAND闪存的状态转移等。这些描述均严格遵守真实的闪存操作流程。

（3）本文模型能够反映硬件操作失败或成功的状态。这个状态在模型中由状态寄存器的Success/ Fail位进行描述。

下一步将在该模型的基础上，针对并行的NAND闪存高级操作进行扩展，证明更多的在此类NAND闪存上运行的嵌入式软件。

［1］ Hasegawa T，Ogiwara R.An Experimental DRAM with a NAND-structured Cell［J］.IEEE Journal of Solid-State Circuits，1993，28（11）：1099-1104.

［2］ 李胜广，张其善.闪存设备在嵌入式Linux系统中的应用［J］.计算机工程，2007，33（2）：191-193.

［3］ Reeves G，Neilson T.The M ars Rover Spirit FLASH Anomaly［C］//Proceedings of IEEE Aerospace Conference. Los Angeles，USA：IEEE Press，2005：4186-4199.

［4］ Zheng M，Tucek J，Qin F，et al.Understanding the Robustness of SSDS Under Power Fault［C］//Proceedings of IEEE FAST'13.Washington D.C.，USA：IEEE Press，2013：271-284.

［5］ Schellhorn G，Ernst G，Pfähler J，et al.Development of a Verified Flash File System［M］.Berlin，Germany：Springer，2014.

［6］ K lein G，Elphinstone K，Heiser G，et al.seL4：Form al Verification of an OS Kernel［C］//Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles.New York，USA：ACM Press，2009：207-220.

［7］ Keller G，Murray T，Am ani S，et al.File System s Deserve Verification Too！［J］.ACM SIGOPS Operating System s Review，2014，48（1）：58-64.

［8］ Kang E，Jackson D.Form al Modeling and Analysis of a Flash Filesystem in Alloy［M］.Berlin，Germany：Springer，2008.

［9］ Butterfield A，Freitas L，Woodcock J.Mechanising a Form al Model of Flash Memory［J］.Science of Computer Programming，2009，74（4）：219-237.

［10］ Semiconductor H.Open NAND Flash Interface Specification［EB/OL］.（2006-06-30）.http：//www. onfi.org.

［11］ The Coq Development Team.The Coq Proof Assistant Reference Manual［EB/OL］.（2011-10-20）.http：// coq.inria.fr.

［12］ Isabelle/HOL：A Proof Assistant for Higher-order Logic［M］.Berlin，Germany：Springer，2002.

编辑 索书志

Formal Modeling for NAND Flash Hardware

YANG Longying1，2，GUO Yu1，2
（1.School of Computing Science and Technology，University of Science and Technology of China，Hefei 230026，China；2.Software Security Laboratory，Suzhou Institute for Advanced Study，University of Science and Technology of China，Suzhou 215123，China）

In order to verify the reliability of the software running on storage system formally，a formal model of NAND flash hardware is needed.According to an interface specification named ONFI that is recognized by many companies，a formal model for the semantics of NAND flash hardware is built in formal language.It includes the storage architecture of NAND flash defined by ONFI，the inner work flow of the commands，the command set of the NAND flash and several flash operations defined upon the model.The model is defined in a popular theorem proof assistant，Coq.This model can be used to define and verify the software based on NAND flash storage system.

formal verification；Coq proof tool；Flash device；formal modeling；high confidence software；storage system

10.3969/j.issn.1000-3428.2015.11.017

杨龙婴，郭 宇.针对NAND闪存硬件的形式化建模［J］.计算机工程，2015，41（11）：94-99.

英文引用格式：Yang Longying，Guo Yu.Formal Modeling for NAND Flash Hardware［J］.Computing Engineering，2015，41（11）：94-99.

1000-3428（2015）11-0094-06

A

TP391

国家自然科学基金青年基金资助项目（61202052，61103023）；国家自然科学基金海外及港澳学者合作研究基金资助项目（61229201）。

杨龙婴（1988-），女，硕士研究生，主研方向：形式化验证，软件安全；郭 宇，副教授。

2014-10-31

2014-12-22 E-m ail：vittayang@gmail.com