針對(duì)NAND閃存硬件的形式化建模

楊龍嬰，郭 宇

（1.中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥230026；

2.中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室，江蘇蘇州215123）

針對(duì)NAND閃存硬件的形式化建模

楊龍嬰1，2，郭 宇1，2

（1.中國(guó)科學(xué)技術(shù)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，合肥230026；

2.中國(guó)科學(xué)技術(shù)大學(xué)蘇州研究院軟件安全實(shí)驗(yàn)室，江蘇蘇州215123）

為形式化地驗(yàn)證存儲(chǔ)系統(tǒng)中軟件的可靠性，引入NAND閃存硬件的形式化模型定義。根據(jù)NAND閃存接口標(biāo)準(zhǔn)ONFI，采用形式化語(yǔ)言對(duì)NAND閃存硬件的語(yǔ)義進(jìn)行建模，包括ONFI定義的NAND閃存硬件的存儲(chǔ)層次結(jié)構(gòu)、閃存硬件芯片處理命令的內(nèi)部工作流程、閃存硬件的命令集，以及在此基礎(chǔ)之上定義的閃存等基本操作。該NAND閃存形式化模型在定理證明工具Coq中定義實(shí)現(xiàn)，其性質(zhì)在Coq中得到完整證明，可以用于定義和驗(yàn)證基于NAND閃存的存儲(chǔ)系統(tǒng)軟件。

形式化驗(yàn)證；Coq證明工具；閃存設(shè)備；形式化建模；高可信軟件；存儲(chǔ)系統(tǒng)

1 概述

近年來NAND閃存（NAND Flash）以其高集成度、低成本、功耗小、抗震性好［1］的存儲(chǔ)特點(diǎn)在從嵌入式系統(tǒng)到云計(jì)算平臺(tái)上都得到了廣泛的應(yīng)用［2］。這其中包括了各種安全攸關(guān)的領(lǐng)域，例如航空航天、核電與醫(yī)療器械等。對(duì)于亟需高可信軟件的領(lǐng)域來說，基于NAND閃存的存儲(chǔ)系統(tǒng)也亟待進(jìn)行形式化驗(yàn)證。比如美國(guó)宇航局的勇氣號(hào)火星車曾因?yàn)榛陂W存的文件系統(tǒng)算法出現(xiàn)了未被發(fā)現(xiàn)的設(shè)計(jì)缺陷的問題而停止運(yùn)行了10 d［3］；大型云計(jì)算供應(yīng)商亞馬遜的數(shù)據(jù)中心也曾因?yàn)樵馐軘嚯姸z失了大量存儲(chǔ)在閃存存儲(chǔ)系統(tǒng)上的數(shù)據(jù)，并因此承受了經(jīng)濟(jì)和信譽(yù)方面的損失［4］。為了構(gòu)建高可信的存儲(chǔ)系統(tǒng)，需要對(duì)運(yùn)行在存儲(chǔ)介質(zhì)之上的文件系統(tǒng)進(jìn)行形式化驗(yàn)證。對(duì)于基于NAND閃存硬件的文件系統(tǒng)而言，驗(yàn)證文件系統(tǒng)需要一個(gè)可以真實(shí)地反映硬件行為的形式化的NAND閃存模型。

形式化模型應(yīng)該能夠真實(shí)地反映出NAND閃存硬件的結(jié)構(gòu)、內(nèi)部的狀態(tài)轉(zhuǎn)移及其與外界命令的交互。這樣才能保證在該模型上經(jīng)過驗(yàn)證的文件系統(tǒng)代碼也能可靠地運(yùn)行在真實(shí)的硬件上。

近年來已經(jīng)逐漸有不少研究開始關(guān)注驗(yàn)證存儲(chǔ)系統(tǒng)的可靠性問題。例如，文獻(xiàn)［5］提出一個(gè)基于NAND閃存的文件系統(tǒng)，并對(duì)其進(jìn)行形式化分析，澳大利亞NICTA（National ICT Australia）的研究組在形式化驗(yàn)證過內(nèi)核seL4［6］之后，開始著手研究如何驗(yàn)證一個(gè)基于NAND閃存的文件系統(tǒng)BilbyFs［7］。但是他們的工作都基于過于簡(jiǎn)化的NAND硬件模型。例如文獻(xiàn)［8］的簡(jiǎn)化NAND模型存在著以下與真實(shí)硬件不符的問題：（1）NAND閃存模型中的層次結(jié)構(gòu)缺少plane層。（2）模型僅聲明了3種NAND閃存上的驅(qū)動(dòng)接口，即讀、寫、擦除，而不是真實(shí)芯片的（命令與數(shù)據(jù)）輸入輸出行為。（3）模型缺少對(duì)硬件操作失敗狀態(tài)的刻畫。雖然Butterfield等人曾經(jīng)利用Z Notation給出了一個(gè)在結(jié)構(gòu)上接近真實(shí)的NAND閃存的硬件模型［9］，但是他們的NAND閃存模型仍然存在上述第（2）點(diǎn)、第（3）點(diǎn)描述的問題。

本文給出了一個(gè)能解決上述3個(gè)問題的模型。根據(jù)一個(gè)被多數(shù)主流閃存生產(chǎn)商廣泛認(rèn)可的NAND閃存接口規(guī)范ONFI（Open NAND Flash Interface）［10］，在形式化驗(yàn)證工具Coq［11］中對(duì)NAND閃存硬件進(jìn)行了形式化建模。這個(gè)形式化模型的定義也能較為容易地移植到其他的形式化工具，如Isabelle/HOL［12］，PVS中。

2 閃存硬件與證明工具Coq

2.1 NAND閃存結(jié)構(gòu)

一個(gè)閃存設(shè)備由一個(gè)或若干個(gè)Target組成，如圖1所示。每個(gè)Target包含了一組邏輯單元（Logical UNit）。邏輯單元是NAND閃存中能夠獨(dú)立運(yùn)行命令的最小單位。每個(gè)LUN有一個(gè)或多個(gè)Plane。每個(gè)Plane由1 024個(gè)～4 096個(gè)塊（Block）組成。塊是NAND閃存中最小的擦除單元，由若干個(gè)頁(yè)構(gòu)成。頁(yè)由兩部分結(jié)構(gòu)組成：一部分是主數(shù)據(jù)區(qū)（Data Area），用來儲(chǔ)存數(shù)據(jù)；另一部分是閑置區(qū)域（Spare Area），通常被用來存儲(chǔ)校驗(yàn)碼和一些標(biāo)記位。

圖1 NAND閃存設(shè)備存儲(chǔ)結(jié)構(gòu)

NAND閃存設(shè)備還具有數(shù)據(jù)傳輸總線、地址傳輸總線、命令傳輸總線、輸入輸出控制、控制邏輯單元和各類寄存器，如圖2所示。地址傳輸總線分為行地址總線和列地址總線2種。這是由于在ONFI中，在NAND閃存上尋址，地址需要分為行地址和列地址2種。行地址包含了LUN號(hào)、塊號(hào)和頁(yè)號(hào)；列地址則為頁(yè)內(nèi)偏移。為了暫時(shí)存儲(chǔ)數(shù)據(jù)、地址和命令，NAND閃存提供了多種寄存器。每個(gè)Plane有一個(gè)頁(yè)寄存器（Page Register）。每個(gè)LUN有一個(gè)命令寄存器（Command Register）和一個(gè)地址寄存器（Address Register）。頁(yè)寄存器用來暫時(shí)存儲(chǔ)頁(yè)數(shù)據(jù)。命令寄存器和地址寄存器分別用來暫時(shí)存儲(chǔ)最后獲得的命令和地址。此外，每個(gè)LUN會(huì)有一個(gè)狀態(tài)寄存器（Status Register）來儲(chǔ)存一些必要的狀態(tài)值。當(dāng)設(shè)備允許多個(gè)Plane并行處理命令的時(shí)候，每個(gè)Plane會(huì)有一個(gè)獨(dú)立的狀態(tài)寄存器的結(jié)構(gòu)。

圖2 NAND閃存設(shè)備工作結(jié)構(gòu)

2.2 NAND閃存操作

一個(gè)典型的NAND閃存操作的工作流程是由若干個(gè)輸入部分，包括命令輸入、地址輸入、數(shù)據(jù)輸入，以及數(shù)據(jù)輸出部分組成。以讀操作為例，首先輸入輸出控制部分將發(fā)送一個(gè)30H命令到命令寄存器，然后發(fā)送列地址和行地址到地址寄存器，繼而發(fā)送一個(gè)讀確認(rèn)命令00H到命令寄存器，然后等待設(shè)備將指定存儲(chǔ)單元的頁(yè)內(nèi)容讀取到頁(yè)寄存器中，在控制邏輯單元得到一個(gè)就緒信號(hào)之后，則開始從總線上向外輸出數(shù)據(jù)。圖3給出了一個(gè)在讀操作中會(huì)出現(xiàn)的狀態(tài)轉(zhuǎn)換圖作為狀態(tài)轉(zhuǎn)移的例子。

圖3 NAND閃存讀操作的狀態(tài)轉(zhuǎn)換示意圖

由上述讀寫操作的工作流程可以發(fā)現(xiàn)：（1）NAND閃存操作并不是一步完成的。一個(gè)操作會(huì)被拆分為命令傳輸、地址傳輸和數(shù)據(jù)傳輸3個(gè)部分；（2）NAND閃存操作需要等待設(shè)備發(fā)出就緒信號(hào)，并不是一個(gè)不間斷的單向的往NAND閃存發(fā)送地址命令并進(jìn)行處理的過程；（3）NAND閃存操作的工作不僅僅涉及NAND設(shè)備存儲(chǔ)結(jié)構(gòu)本身，也涉及了各類寄存器。除此之外，NAND閃存操作可以被主動(dòng)打斷。重置命令（Reset）就是用來打斷讀、寫和擦除操作的。如果命令寄存器在讀寫和擦除操作中接收到了重置命令，那么讀寫和擦除就都會(huì)被強(qiáng)制中斷。

2.3 形式化驗(yàn)證工具Coq

定理證明輔助工具Coq［10］不僅提供了一個(gè)交互式的證明環(huán)境，用來進(jìn)行邏輯推理，還提供了一個(gè)強(qiáng)大的形式化語(yǔ)言——Gallia語(yǔ)言。該語(yǔ)言基于一種名為歸納構(gòu)造演算CiC（Calculus of inductive Constructions）的高階多態(tài)類型化lam bda演算。采用Gallia定義的NAND閃存模型，不僅可以形式化地定義閃存的存儲(chǔ)結(jié)構(gòu)、操作接口、模型規(guī)范，還可以在Coq中對(duì)模型的一些基本性質(zhì)進(jìn)行嚴(yán)格的證明。

3 NAND閃存的內(nèi)部結(jié)構(gòu)

本節(jié)根據(jù)ONFI規(guī)范真實(shí)地定義了NAND閃存的層次化結(jié)構(gòu)。

3.1 數(shù)據(jù)單元定義

在NAND閃存中，數(shù)據(jù)存儲(chǔ)的最小單位是字節(jié)（Byte）。NAND閃存中存儲(chǔ)的字節(jié)可能為空（擦除狀態(tài)），也可以為其他值：

在Coq中，用Inductive類型來刻畫一個(gè)具有多種取值的數(shù)據(jù)類型。由上在Coq中定義數(shù)據(jù)如下：

這個(gè)定義表示數(shù)據(jù)為一個(gè)字節(jié)的有序列表。

3.2 NAND閃存架構(gòu)定義

如2.1節(jié)中所述，ONFI中NAND閃存的架構(gòu)分為6層，本文在Coq中由下至上對(duì)它們進(jìn)行了定義。3.2.1 頁(yè)

頁(yè)是NAND閃存讀寫的基本單位，由相連的主數(shù)據(jù)區(qū)和備用區(qū)域組成。

下面以一個(gè)具體的NAND設(shè)備為例來描述如何定義NAND架構(gòu)。在Coq中在配置文件里分別定義了頁(yè)的主數(shù)據(jù)區(qū)和備用區(qū)域的大?。?/p>

在NAND中，頁(yè)的狀態(tài)有空頁(yè)、有效頁(yè)和無效頁(yè)（寫入失敗的頁(yè)）3種狀態(tài)：

在Coq中，Record關(guān)鍵字可以定義一個(gè)具有多個(gè)域的結(jié)構(gòu)體。這里page就是具有page-data和page-state2個(gè)域的結(jié)構(gòu)體，它的構(gòu)造函數(shù)是m kpage。page-data不僅包含了頁(yè)的主要數(shù)據(jù)，也包括了閑置區(qū)域內(nèi)的數(shù)據(jù)信息。

當(dāng)需要定位一個(gè)頁(yè)時(shí)，可以先由行地址找到頁(yè)所在的塊，再由列地址找到頁(yè)在該塊中的具體偏移。以下分別是頁(yè)內(nèi)偏移、塊號(hào)和頁(yè)號(hào)的Coq定義。其中頁(yè)內(nèi)偏移和塊號(hào)都是一個(gè)自然數(shù)，而頁(yè)號(hào)則是由塊號(hào)和頁(yè)內(nèi)偏移組成的二元組。

3.2.2 塊

塊是由一組連續(xù)的頁(yè)構(gòu)成的，是NAND閃存進(jìn)行擦除的基本單位。

塊的狀態(tài)有3種：有效塊，無效塊（即擦除失敗的塊）以及壞塊：

除了塊的狀態(tài)之外，塊的另一個(gè)重要參數(shù)是塊的擦除次數(shù)。NAND閃存的主要特性之一就是它不支持原地寫入（in-place update）。在寫入一個(gè)已經(jīng)存在的物理頁(yè)時(shí)，必須先擦除包含此頁(yè)的整個(gè)塊。這種特性也被稱為擦后寫（Erase Before W rite）。然而對(duì)于一個(gè)NAND閃存中的塊來說，可擦寫次數(shù)是有限的。如果擦寫次數(shù)超過硬件所能接受的上限，那么塊的工作就會(huì)不正常。由上，在Coq中定義塊為如下結(jié)構(gòu)：

其中，block-pages表示了塊內(nèi)的所有頁(yè)；blocknext-page是一個(gè)指向塊內(nèi)第一個(gè)空頁(yè)的位置的指針；block-erase-count記錄了當(dāng)前該塊的擦寫次數(shù)；block-state是塊的狀態(tài)記錄。

3.2.3 Plane構(gòu)成

Plane由一組塊構(gòu)成，每個(gè)Plane具有一個(gè)獨(dú)立的頁(yè)寄存器，因此多個(gè)Plane可以并行進(jìn)行讀寫操作。

頁(yè)寄存器是用來暫時(shí)存儲(chǔ)向plane內(nèi)部發(fā)送或從plane中取出的頁(yè)數(shù)據(jù)的。

3.2.4 邏輯單元

邏輯單元是NAND閃存中獨(dú)立執(zhí)行命令的最小單位，由若干個(gè)plane構(gòu)成，這些plane共享一個(gè)狀態(tài)寄存器、一個(gè)地址寄存器和一個(gè)命令寄存器。

在ONFI中，一個(gè)狀態(tài)寄存器由8位組成。由于篇幅有限、為增加易讀性，本文略去了一些繁瑣的硬

件規(guī)范，只模擬了Ready/Busy狀態(tài)位和Success/ Fail狀態(tài)位。本文的形式化方法可以很容易地?cái)U(kuò)展成完整的ONFINAND硬件規(guī)范。

在本文的Coq實(shí)現(xiàn)中，設(shè)定每個(gè)邏輯單元具有2個(gè)plane。LUN在Coq中的定義如下：

lun-status-RB表示Ready/Busy狀態(tài)位；lunstatus-SF表示Success/Fail狀態(tài)位；lun-cm d-reg表示命令寄存器；lun-addr-reg表示地址寄存器；lunintern-state標(biāo)識(shí)了lun所在的狀態(tài)。其中，Success/ Fail狀態(tài)位描述硬件操作是否成功。需要注意的是，按照大多數(shù)廠商提供的硬件規(guī)格和本文所遵從的ONFI規(guī)范，在真實(shí)的NAND閃存硬件操作的流程中，只有寫和擦除操作會(huì)失敗，讀操作不會(huì)失敗，只會(huì)讀到空數(shù)據(jù)。因此，Success/Fail位會(huì)真實(shí)地反映出諸如寫入非法地址、擦除非法地址等硬件操作失敗的情況。在本文模型中，可以通過讀狀態(tài)命令來從數(shù)據(jù)總線上得到狀態(tài)寄存器包含的內(nèi)容。

3.2.5 Target構(gòu)成

一個(gè)Target是由若干個(gè)邏輯單元（LUN）構(gòu)成的。如果是在一個(gè)具有多個(gè)Target的NAND閃存中，每一個(gè)Target會(huì)具有一個(gè)獨(dú)立的片選信號(hào)。本文只考慮具有一個(gè)邏輯單元的Target的NAND閃存。

3.2.6 設(shè)備

一個(gè)設(shè)備是由一個(gè)到多個(gè)Target組成的完整NAND閃存系統(tǒng)。在本文的例子中，每個(gè)設(shè)備只有一個(gè)Target。

4 NAND閃存設(shè)備的命令處理

NAND閃存設(shè)備操作如2.2節(jié)所述，是一種會(huì)經(jīng)過多個(gè)狀態(tài)，涉及一個(gè)或更多命令碼的接收，并且可能出現(xiàn)操作失敗的復(fù)雜邏輯。為了能夠真實(shí)地在硬件行為層面對(duì)NAND閃存進(jìn)行建模，在定義了所涉及的命令集合和寄存器的基礎(chǔ)上，本文詳細(xì)定義了發(fā)送命令、發(fā)送地址、等待設(shè)備就緒、數(shù)據(jù)輸入輸出的操作語(yǔ)義。

NAND閃存操作可被進(jìn)一步區(qū)分為基礎(chǔ)操作和高級(jí)操作2種?；A(chǔ)操作指每一種閃存設(shè)備都必須實(shí)現(xiàn)的操作，比如讀寫操作，沒有這些基礎(chǔ)操作NAND閃存就會(huì)無法工作；高級(jí)操作的實(shí)現(xiàn)要依賴廠商對(duì)于硬件的優(yōu)化設(shè)計(jì)，比如對(duì)于同一個(gè)LUN的多個(gè)p lane進(jìn)行寫入的命令，如果閃存設(shè)備的LUN僅有一個(gè)plane，就不能支持這一類高級(jí)操作。通常高級(jí)操作是用來提升閃存操作效率的，沒有這些高級(jí)操作，閃存依然能夠正常工作。為簡(jiǎn)化起見，只考慮基礎(chǔ)操作。

在真實(shí)的閃存時(shí)序操作中，一個(gè)基本的操作可能涉及多于一個(gè)的具體命令。本文所模擬的命令集合如表1所示。

表1 NAND閃存命令

在表1中，命令碼是指NAND閃存從總線上接收的16進(jìn)制命令代碼。這些命令碼分別對(duì)應(yīng)到不同的命令，用于在操作流程中控制和標(biāo)示下一個(gè)要進(jìn)行的步驟。這些命令碼的操作語(yǔ)義在Coq中描述。發(fā)送命令的操作語(yǔ)義在Coq中定義如下：

send-cmd的操作語(yǔ)義表示從一個(gè)設(shè)備狀態(tài)下，發(fā)送命令到設(shè)備之后，設(shè)備轉(zhuǎn)移到另一個(gè)狀態(tài)。輸入device是一個(gè)設(shè)備。cm d是設(shè)備從總線上接收的命令，根據(jù)不同的命令，省略部分的代碼執(zhí)行不同的操作和狀態(tài)轉(zhuǎn)移。最后send-cm d函數(shù)返回一個(gè)達(dá)到一個(gè)新狀態(tài)的設(shè)備device或者一個(gè)處于未定義狀態(tài)的設(shè)備device。未定義狀態(tài)描述和概括了一種情況：設(shè)備得到的輸入不是期待的輸入，比如一個(gè)已經(jīng)得到了讀取目標(biāo)頁(yè)地址的設(shè)備所期望的輸入是一個(gè)讀確認(rèn)命令，那么如果在這個(gè)時(shí)候發(fā)送一個(gè)寫開始命令給設(shè)備，就會(huì)造成一種未定義的結(jié)果。這個(gè)可能包含未定義狀態(tài)的返回值由以下Coq定義描述：

在send-cmd函數(shù)中，A這個(gè)類型變量就是device。因此當(dāng)設(shè)備所到達(dá)的狀態(tài)是一個(gè)合法的確定狀態(tài)時(shí)，send-cm d會(huì)返回一個(gè)Ok device；當(dāng)設(shè)備所到達(dá)的狀態(tài)是一個(gè)非法狀態(tài)的時(shí)候，會(huì)返回一個(gè)Unknow n。

大部分的NAND閃存操作都需要通過總線傳輸?shù)刂穪碇付ň唧w操作執(zhí)行的位置。發(fā)送地址的操作分為發(fā)送行列地址和僅發(fā)送行地址2種。這種區(qū)分來自于有些操作僅僅需要指明塊所在的位置而不需要指定頁(yè)和頁(yè)內(nèi)偏移。這2種發(fā)送地址的操作語(yǔ)義在Coq中的定義如下：

在這2個(gè)函數(shù)中，函數(shù)接收一個(gè)設(shè)備和一個(gè)地址作為輸入，根據(jù)當(dāng)前的設(shè)備狀態(tài)，進(jìn)行狀態(tài)轉(zhuǎn)移和操作，最后返回一個(gè)新的設(shè)備狀態(tài)或者一個(gè)未定義狀態(tài)。

在一部分NAND閃存操作中，會(huì)出現(xiàn)需要等待設(shè)備準(zhǔn)備好數(shù)據(jù)的情況，必須要等待狀態(tài)寄存器顯示設(shè)備是Ready的，方能進(jìn)行下一步子操作。這種等待設(shè)備就緒后進(jìn)行狀態(tài)轉(zhuǎn)移的操作語(yǔ)義在Coq中被定義如下：

這個(gè)操作語(yǔ)義的定義僅僅允許狀態(tài)寄存器顯示設(shè)備Ready時(shí)進(jìn)行下一步的狀態(tài)轉(zhuǎn)移。

輸出數(shù)據(jù)的操作語(yǔ)義在Coq中被定義如下：

5 NAND閃存設(shè)備的工作流程及性質(zhì)

本節(jié)將使用上一節(jié)定義的NAND閃存設(shè)備的命令來刻畫閃存的工作流程。由于篇幅所限，在這里只列舉讀操作、寫操作和擦除操作的流程和在Coq中的形式化定義。

5.1 讀操作

讀操作的目的是從NAND閃存中的某個(gè)頁(yè)內(nèi)讀出這個(gè)頁(yè)所保存的全部或部分?jǐn)?shù)據(jù)。讀操作的執(zhí)行流程如下：

（1）發(fā)送讀開始命令（00H）到設(shè)備；

（2）發(fā)送列地址和行地址到設(shè)備，設(shè)備找到對(duì)應(yīng)讀取起點(diǎn)；

（3）向設(shè)備發(fā)送一個(gè)讀確認(rèn)命令（30H），設(shè)備在接收到讀確認(rèn)命令之后會(huì)按照行地址和列地址讀出由列地址開始到頁(yè)末的所有數(shù)據(jù)到頁(yè)寄存器中，并設(shè)Ready/Busy標(biāo)志位為true；

（4）在等待設(shè)備讀取數(shù)據(jù)到頁(yè)寄存器就緒期間，設(shè)備并不向數(shù)據(jù)總線傳輸任何數(shù)據(jù)；

（5）當(dāng)設(shè)備就緒之后，開始通過數(shù)據(jù)總線向輸出端發(fā)送數(shù)據(jù)。

讀操作在Coq中的形式化定義如下：

5.2 寫操作

寫操作的目的是向NAND閃存中的某個(gè)頁(yè)寫入數(shù)據(jù)。寫操作在Coq中定義如下：

該定義與讀操作類似。

5.3 擦除操作

擦除操作被用來擦除某個(gè)塊的數(shù)據(jù)，該操作以塊為基本單位。擦除操作在Coq中的定義如下：

5.4 NAND閃存設(shè)備模型的性質(zhì)

本文中的形式化閃存模型滿足真實(shí)NAND閃存工作流程的常見的性質(zhì)，由于篇幅所限，僅列部分性質(zhì)如下：

性質(zhì)1 在執(zhí)行了正確的讀、寫或擦除操作后，設(shè)備一定會(huì)進(jìn)入空閑狀態(tài)。

性質(zhì)2 擦除或?qū)懖僮髡_執(zhí)行后，設(shè)備中的狀態(tài)寄存器R/B位為Ready，S/F位為Success。

性質(zhì)3 對(duì)設(shè)備中的某一塊進(jìn)行擦除后，該塊中的每一頁(yè)中的數(shù)據(jù)都為空（OxFF）、且塊擦寫次數(shù)加1。

性質(zhì)4 對(duì)某一塊進(jìn)行擦除或?qū)懭牒?，其他所有塊，其各狀態(tài)均與操作執(zhí)行前完全相同。

性質(zhì)5 當(dāng)給出的擦除地址超出尋址空間時(shí)，擦除失敗，狀態(tài)寄存器中S/F位為Fail，R/B位為Ready。

這些性質(zhì)均可在Coq中被證明。

6 結(jié)束語(yǔ)

NAND閃存硬件規(guī)格各異，內(nèi)部狀態(tài)轉(zhuǎn)換復(fù)雜，因此對(duì)于NAND閃存之上運(yùn)行的嵌入式軟件是否可靠進(jìn)行驗(yàn)證一直是一個(gè)難點(diǎn)。本文以O(shè)NFI規(guī)范所刻畫的一類典型NAND閃存為對(duì)象，對(duì)NAND閃存的真實(shí)層次結(jié)構(gòu)和操作中硬件層面的行為進(jìn)行了建模，能夠描述硬件操作是否成功，并已經(jīng)能夠得到證明其上驅(qū)動(dòng)命令的方法。本文的貢獻(xiàn)在于：

（1）本文根據(jù)ONFI進(jìn)行建模，不僅描述了帶有Plane的NAND閃存結(jié)構(gòu)，還描述了現(xiàn)實(shí)NAND閃存中存在的邏輯單元、Target、設(shè)備等結(jié)構(gòu)。

（2）該模型在聲明了讀、寫、擦除、讀ID、讀狀態(tài)和重置這幾個(gè)操作的基礎(chǔ)上，切實(shí)地描述了這些操作中所涉及的硬件層面的行為，比如命令碼的接收、地址的傳送、數(shù)據(jù)的輸入輸出、寄存器的控制和NAND閃存的狀態(tài)轉(zhuǎn)移等。這些描述均嚴(yán)格遵守真實(shí)的閃存操作流程。

（3）本文模型能夠反映硬件操作失敗或成功的狀態(tài)。這個(gè)狀態(tài)在模型中由狀態(tài)寄存器的Success/ Fail位進(jìn)行描述。

下一步將在該模型的基礎(chǔ)上，針對(duì)并行的NAND閃存高級(jí)操作進(jìn)行擴(kuò)展，證明更多的在此類NAND閃存上運(yùn)行的嵌入式軟件。

［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］ 李勝?gòu)V，張其善.閃存設(shè)備在嵌入式Linux系統(tǒng)中的應(yīng)用［J］.計(jì)算機(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?。跩］.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，F(xiàn)reitas 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

楊龍嬰，郭 宇.針對(duì)NAND閃存硬件的形式化建模［J］.計(jì)算機(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

國(guó)家自然科學(xué)基金青年基金資助項(xiàng)目（61202052，61103023）；國(guó)家自然科學(xué)基金海外及港澳學(xué)者合作研究基金資助項(xiàng)目（61229201）。

楊龍嬰（1988-），女，碩士研究生，主研方向：形式化驗(yàn)證，軟件安全；郭 宇，副教授。

2014-10-31

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