基于Isabelle/HOL的文件系統(tǒng)形式化設(shè)計與驗證

王文斌,錢振江,＊,靳勇,孫高飛,邢曉雙,蘇超,孫天琦

(1.蘇州大學(xué)計算機科學(xué)與技術(shù)學(xué)院,江蘇 蘇州 215000;2.常熟理工學(xué)院計算機科學(xué)與工程學(xué)院,江蘇 蘇州 215500)

0 引言

文件系統(tǒng)作為操作系統(tǒng)中負責(zé)數(shù)據(jù)持久化存儲的功能模塊,即使是一個微小[1-3]的錯誤,其造成的損失也將是巨大的,因為這可能導(dǎo)致關(guān)鍵的數(shù)據(jù)永久丟失。實現(xiàn)一個安全可信的文件系統(tǒng)一直是操作系統(tǒng)開發(fā)人員的目標(biāo),近年來眾多有關(guān)操作系統(tǒng)正確性方面的探索工作[4-6]已經(jīng)顯示出構(gòu)建一個安全可信的文件系統(tǒng)的可行性。

在操作系統(tǒng)的開發(fā)過程中,文件系統(tǒng)的安全性是指:文件系統(tǒng)在設(shè)計階段的設(shè)計符合預(yù)期的安全需求;文件系統(tǒng)的設(shè)計與實現(xiàn)是一致的;文件系統(tǒng)在開發(fā)過程中不存在各種語法錯誤等。在軟件開發(fā)過程中,常見的用于保障軟件安全性的方法有軟件測試和靜態(tài)分析。軟件測試對于軟件的安全性驗證是不完整的,靜態(tài)分析無法解決文件系統(tǒng)中的語義錯誤。因此,它們只能有效地滿足最后一項要求,而無法滿足文件系統(tǒng)安全性的前兩項要求。

基于嚴(yán)格數(shù)理邏輯的形式化方法一直是公認的用于保障操作系統(tǒng)安全性的方法。早期由于缺少像Isabelle/HOL和Coq這樣的輔助定理證明工具幫助完成文件系統(tǒng)形式化驗證的自動推理工作,致使對文件系統(tǒng)進行全面的形式化驗證是不現(xiàn)實的。另外,當(dāng)前有關(guān)文件系統(tǒng)的形式化驗證大多基于以Linux為代表的宏內(nèi)核架構(gòu)。宏內(nèi)核將所有的系統(tǒng)服務(wù)都集成到內(nèi)核中,導(dǎo)致在對文件系統(tǒng)進行形式化驗證時可信計算基(TCB)過大。自從微內(nèi)核架構(gòu)在開發(fā)Mach系統(tǒng)時被提出以來,其在安全方面的特性便得到研究人員的關(guān)注。微內(nèi)核架構(gòu)在內(nèi)核空間只提供進程調(diào)度、虛擬內(nèi)存等最核心的功能,將大多數(shù)的系統(tǒng)服務(wù)以模塊化的形式運行在用戶態(tài),以最大程度地降低內(nèi)核的代碼量。此特性可有效地降低形式化驗證過程的TCB規(guī)模。seL4[7]是第1個嘗試經(jīng)過完整形式化驗證的微內(nèi)核操作系統(tǒng)原型,但遺憾的是它并沒有對運行在用戶態(tài)的文件系統(tǒng)展開詳細的形式化驗證。

本文基于高階邏輯和自動機模型中的有限狀態(tài)機(FSA)理論,運用內(nèi)聯(lián)數(shù)據(jù)機制的微內(nèi)核架構(gòu)文件系統(tǒng),提出一種細粒度的形式化設(shè)計和驗證方法。通過抽象文件系統(tǒng)所涉及的工作對象和資源來構(gòu)建文件系統(tǒng)的狀態(tài),根據(jù)文件系統(tǒng)的功能需求與安全屬性給出相關(guān)系統(tǒng)調(diào)用的公理性語義,并將系統(tǒng)調(diào)用的公理性語義轉(zhuǎn)換成有限狀態(tài)自動機中的狀態(tài)轉(zhuǎn)移函數(shù),以狀態(tài)轉(zhuǎn)移函數(shù)所造成的文件系統(tǒng)狀態(tài)變化的合法性分析歸納出文件系統(tǒng)調(diào)用的功能正確性斷言,以此在Isabelle/HOL中完成對于文件系統(tǒng)的建模和形式化驗證。

1 相關(guān)工作

早期的文件系統(tǒng)形式化驗證需要進行大量的定理證明工作[8],因此研究人員選擇忽略底層實現(xiàn)細節(jié),在較高的抽象層次去實現(xiàn)對于文件系統(tǒng)的形式化建模。通過對實現(xiàn)文件系統(tǒng)的高級語言進行限制,在開發(fā)過程中只允許使用特定優(yōu)化過后的高級語言子集,可以在文件系統(tǒng)的設(shè)計規(guī)約與高級語言之間實現(xiàn)自動化鏈接,降低驗證的工作量。文獻[9-11]介紹的C語言的受限制子集Cogent、用于數(shù)據(jù)布局細化證明的DARFENT以及美國宇航局在太陽軌道衛(wèi)星系統(tǒng)的文件系統(tǒng)形式化驗證中所使用的Scala受限制子集都是基于這一思想。一方面,這樣的限制使得這些語言在開發(fā)時存在著功能受限的問題,如Cogent無法支持遞歸;另一方面,這些語言僅對其所實現(xiàn)的文件系統(tǒng)的設(shè)計規(guī)范與實現(xiàn)的一致性進行保證,而忽視了開發(fā)過程中所使用的語言組件的可信性驗證。雖然文獻[12]介紹的Cogent-C是針對后一種問題而提出的Cogent改良版本,其完成了文件系統(tǒng)開發(fā)過程中所使用的部分庫的驗證,但是仍然無法解決前一問題。

文獻[13]介紹了上海交通大學(xué)研究人員開發(fā)的并發(fā)關(guān)系邏輯輔助驗證(CRL-H)框架,并設(shè)計和驗證了第1個經(jīng)過形式化驗證的并發(fā)文件系統(tǒng)AutomFS。這是針對多核處理器與經(jīng)過驗證的并發(fā)式文件系統(tǒng),但它不支持持久化數(shù)據(jù),并且不考慮崩潰安全性。文獻[14]通過使用局部思想和偏序法構(gòu)建的CRL-T,將其用于驗證AutomFS的終止性的驗證框架, 成功地證明了并發(fā)性文件系統(tǒng)在公平調(diào)用情況下接口的終止性。

來自美國麻省理工學(xué)院(MIT)的計算機科學(xué)與人工智能實驗室(CSAIL)的研究人員主持了一系列關(guān)于文件系統(tǒng)形式化驗證項目,如表1所示。該項目組主要關(guān)注文件系統(tǒng)的崩潰安全與并發(fā)安全。文獻[15]介紹的FSCQ是CSAIL針對文件系統(tǒng)崩潰安全而展開的文件系統(tǒng)形式化驗證項目,它是使用Coq進行機器檢查證明的文件系統(tǒng)。

表1 文件系統(tǒng)形式化驗證項目Table 1 File system formal validation project

為克服FSCQ性能較差的缺點,文獻[16]介紹了后續(xù)的項目DFSCQ,在以不破壞FSCQ崩潰安全為前提的情況下,通過為功能體fsync和fdatafnc提供精確的規(guī)約,為FSCQ引入這兩種提高文件系統(tǒng)I/O速率的機制,進而開發(fā)出性能有所提高的文件系統(tǒng)DSFCQ。文獻[17]將加密文件系統(tǒng)與FSCQ文件系統(tǒng)相結(jié)合,設(shè)計了經(jīng)過形式化驗證的、使用加密原語保護磁盤文件安全的文件系統(tǒng)(IFSCQ)。文獻[18]設(shè)計了名為optimistic systems calls的機制,以較小的工作量在FSCQ上引入并發(fā)機制,進而構(gòu)建了并發(fā)性文件系統(tǒng)(CFSCQ)。針對并發(fā)文件系統(tǒng)機密性,文獻[19]提出DIESKSEC方法,并開發(fā)了SFSCQ文件系統(tǒng)。文獻[20]介紹了Perennial的形式化驗證框架,對文件系統(tǒng)的并發(fā)性崩潰安全展開進一步的驗證。文獻[21-23]引入更多技術(shù)規(guī)范構(gòu)建Perennial 2.0框架,并用其驗證使用Go語言實現(xiàn)的網(wǎng)絡(luò)文件系統(tǒng)服務(wù)器DaisyNFS,以及它的日志服務(wù)系統(tǒng)GoJournal。

CSAIL的研究人員針對文件系統(tǒng)的形式化驗證進行了諸多方向的探索和努力,他們的工作都是基于宏內(nèi)核操作系統(tǒng)而展開的,在一定程度上無法隔絕操作系統(tǒng)其他內(nèi)核模塊對于文件系統(tǒng)的影響,因此在形式化驗證過程中存在TCB過大的問題。

本文為一款用于網(wǎng)絡(luò)通信、安全可信微內(nèi)核操作系統(tǒng)(VSOS)[24]中的安全可信文件系統(tǒng)(VSFS)引入形式化的方法,探索在微內(nèi)核架構(gòu)下引入內(nèi)聯(lián)數(shù)據(jù)機制的可行性與實現(xiàn)的正確性。使用該方法在設(shè)計階段構(gòu)建VSFS的有限狀態(tài)機模型,抽象描述有關(guān)VSFS的系統(tǒng)狀態(tài)和可移植操作系統(tǒng)接口(POSIX)系統(tǒng)調(diào)用的功能語義,構(gòu)建VSOS的形式化模型,在Isabelle/HOL中完成該模型的細粒度驗證。

2 VSFS文件系統(tǒng)

本文從VSOS架構(gòu)、VSFS總體布局、內(nèi)聯(lián)數(shù)據(jù)機制等方面來介紹VSFS。對于VSOS架構(gòu)特性和內(nèi)核模塊匯編級形式化驗證工作,文獻[24]中已有詳細描述。本節(jié)重點介紹VSFS文件系統(tǒng)總體布局和適用于小文件場景的內(nèi)聯(lián)數(shù)據(jù)機制。

2.1 VSOS架構(gòu)

VSOS是用于網(wǎng)絡(luò)通信、安全可信的微內(nèi)核架構(gòu)操作系統(tǒng)。它在設(shè)計之初便致力于操作系統(tǒng)安全性,因此對內(nèi)核模塊進行了精心設(shè)計,最小化內(nèi)核的代碼量,其整體架構(gòu)如圖1所示。

圖1 VSOS整體架構(gòu)Fig.1 VSOS overall architecture

VSOS在邏輯上被劃分成4層:只提供中斷處理、進程調(diào)度等少量核心服務(wù)的內(nèi)核層;提供各硬件驅(qū)動服務(wù)的驅(qū)動層;VSFS文件系統(tǒng)所在的服務(wù)器層,這一層向上為應(yīng)用程序提供標(biāo)準(zhǔn)的系統(tǒng)調(diào)用,向下獲取驅(qū)動服務(wù)和內(nèi)核服務(wù);最上層為應(yīng)用程序?qū)?。在VSOS中內(nèi)核層和服務(wù)器層經(jīng)過形式化的驗證[25],確保在系統(tǒng)運行過程中不發(fā)生變化,因此被視為是安全可信的。高度個性化和具有極大自由度的驅(qū)動層和應(yīng)用程序?qū)?由于在運行時是動態(tài)加載的模塊,將被視為是不可信的。

服務(wù)器層和驅(qū)動層都將作為獨立的進程運行,它們之間只能通過進程間通信(IPC)來彼此間調(diào)用服務(wù)。如VSOS中提供的基礎(chǔ)原語SEND和RECEIVE。VSOS通過提供一個輕量化、固定長度的消息結(jié)構(gòu)來簡化消息的處理。VSFS運行在用戶模式,被劃分到服務(wù)器層。這將使得VSFS無法直接去獲取內(nèi)核中的特權(quán)服務(wù),比如I/O操作。基于“最小權(quán)限原則”的VSOS在內(nèi)核層設(shè)計了系統(tǒng)任務(wù)進程來專門處理VSFS通過IPC發(fā)出的內(nèi)核調(diào)用,避免VSFS直接獲取特權(quán)服務(wù)。

2.2 VSFS設(shè)計布局

VSFS在磁盤上設(shè)計布局如圖2所示。VSFS將block 0分配給Boot程序,負責(zé)程序的啟動和運行。隨后是磁盤上的元數(shù)據(jù)結(jié)構(gòu)區(qū)域,即超級塊、超級塊備份、索引節(jié)點位圖、塊位圖、索引節(jié)點樹以及一個日志區(qū)域。在圖2中它們的邏輯位置連續(xù),但其在磁盤上的物理塊位置不連續(xù)。超級塊與超級塊的備份并不會連續(xù)存儲,因為連續(xù)存儲會極大地增加兩者同時損壞的概率。VSFS將超級塊的備份與日志區(qū)域都部署于磁盤存儲位置的底部。日志、索引節(jié)點位圖、塊位圖以及索引節(jié)點表的具體位置會記錄在超級塊中。

圖2 VSFS文件系統(tǒng)的總體布局Fig.2 General layout of VSFS file system

VSFS會為每一個索引節(jié)點分配256 Byte的空間,但索引節(jié)點數(shù)據(jù)結(jié)構(gòu)只使用128 Byte,冗余的空間是為支持內(nèi)聯(lián)數(shù)據(jù)機制。

2.3 內(nèi)聯(lián)數(shù)據(jù)機制

基于提高處理體積較小文件效率、減少內(nèi)核源碼在運行時所占內(nèi)存空間的目的,本文為VSFS引入了內(nèi)聯(lián)數(shù)據(jù)機制。VSFS為每個索引節(jié)點分配256 Byte空間,但索引節(jié)點數(shù)據(jù)結(jié)構(gòu)所使用的空間大小為128 Byte。實際上索引節(jié)點數(shù)據(jù)結(jié)構(gòu)使用的128 Byte空間中仍有部分未被使用,而是被當(dāng)作擴展字段,為方便未來VSFS引進新的機制留有空間。內(nèi)聯(lián)數(shù)據(jù)機制會將不大于128 Byte的文件(后文將不大于128 Byte的文件稱為小文件)存放在未被索引節(jié)點數(shù)據(jù)結(jié)構(gòu)使用的128 Byte的索引節(jié)點空間中。

當(dāng)啟用內(nèi)聯(lián)數(shù)據(jù)機制時,系統(tǒng)會將較小的文件保存在索引節(jié)點的冗余空間中。在文件系統(tǒng)將文件從數(shù)據(jù)緩沖池中刷新回磁盤時,小文件若不采用內(nèi)聯(lián)數(shù)據(jù)機制,則磁盤需要尋找空閑數(shù)據(jù)塊來存放該文件的數(shù)據(jù)。由于在VSFS中數(shù)據(jù)塊缺省的大小為4 KB,在不使用內(nèi)聯(lián)數(shù)據(jù)機制、單獨存放小文件數(shù)據(jù)時,磁盤將會產(chǎn)生內(nèi)部碎片。因此,采用內(nèi)聯(lián)數(shù)據(jù)機制會極大地減少磁盤內(nèi)部碎片。

當(dāng)文件系統(tǒng)讀取小文件數(shù)據(jù)時,只需要遍歷目錄樹找到該文件的索引節(jié)點,即可查詢到該文件的數(shù)據(jù),而無須通過索引節(jié)點再次查詢數(shù)據(jù)所在位置。當(dāng)數(shù)據(jù)緩沖未命中時,將節(jié)省時間開銷。由于VSFS只需讀取一次磁盤便可將索引節(jié)點數(shù)據(jù)和文件數(shù)據(jù)讀入內(nèi)核空間的索引節(jié)點緩存。若不采用內(nèi)聯(lián)數(shù)據(jù)機制,則VSFS第1次讀磁盤會取出該文件的索引節(jié)點,再通過查詢索引節(jié)點中記錄的數(shù)據(jù)塊的存放位置從磁盤上讀取該文件數(shù)據(jù),如圖3所示。由于磁盤的讀取速度和內(nèi)存的讀取速度存在數(shù)量級的差異,因此在這種情況下節(jié)省了時間開銷。

圖3 內(nèi)聯(lián)數(shù)據(jù)機制讀取的對比Fig.3 Comparison of inline data mechanism read

磁盤的硬件機制保證了磁盤上不大于一個扇區(qū)大小(即512 Byte)的讀寫是原子性的,對于將索引節(jié)點數(shù)據(jù)結(jié)構(gòu)和文件數(shù)據(jù)存放在一起的小文件來說,這使得在不使用任何額外軟件機制輔助的前提下,即可保證對于小文件讀寫的原子性。

3 VSFS文件系統(tǒng)的有限狀態(tài)機模型

本節(jié)介紹基于高階邏輯和自動機模型為VSFS構(gòu)建形式化模型的過程,通過抽象VSFS文件系統(tǒng)相關(guān)的工作對象和資源來構(gòu)建文件系統(tǒng)的狀態(tài)。在此基礎(chǔ)上,根據(jù)VSFS的功能需求與安全屬性給出為上層應(yīng)用程序提供的系統(tǒng)調(diào)用的公理性語義,并將系統(tǒng)調(diào)用的公理性語義轉(zhuǎn)換成有限狀態(tài)自動機中的狀態(tài)轉(zhuǎn)移函數(shù),最后給出其在Isabelle/HOL中相應(yīng)的定義。

本文使用的自動機模型為確定性的有限狀態(tài)自動機。它的一般性定義為一個五元組,如式(1)所示:

M=(S,Φ,ξ,SI,SE)

(1)

其中:S、SI、SE分別表示系統(tǒng)的狀態(tài)集合、系統(tǒng)的初始狀態(tài)、系統(tǒng)的結(jié)束狀態(tài);Ф 是自動機可識別的字母表;ξ是狀態(tài)轉(zhuǎn)移函數(shù)。

3.1 狀態(tài)

VSFS提供服務(wù)的過程可以看作VSFS中狀態(tài)的轉(zhuǎn)變過程。在理論上,VSFS的狀態(tài)集合Svsfs是由VSFS中工作對象Xi,j所形成的笛卡兒積空間,如式(2)所示:

Svsfs=∏i,j

(2)

由于VSFS工作對象的取值有限,如索引節(jié)點數(shù)量,因此真實狀態(tài)集合S1是S的一個子集,即S1∈S。VSFS的系統(tǒng)狀態(tài)在Isabelle/HOL中的定義如算法1所示,其中,state是一個record數(shù)據(jù)類型。

算法1VSFS系統(tǒng)狀態(tài)在Isabelle/HOL中抽象

record state =

superBlocks :: SUPER_BLOCK_INFO

filps :: ″FILE list″

dentryCache :: ″D_cache″

inodeCache :: ″I_cache″

bufferCache :: ″B_cache″

fprocs :: ″FPROC list″

disk :: ″disk″

messages :: ″MESSAGE″

在算法1中,superBlocks表示內(nèi)存中超級塊的抽象,它存放有VSFS文件系統(tǒng)的有關(guān)信息,filps表示進程與被打開文件之間信息的抽象,文件描述符fd指向filp中被打開的文件,dentryCache表示目錄項在內(nèi)存中的緩存抽象,由3個列表構(gòu)成,分別為空閑目錄項對象的緩存與VSFS在初始化時將預(yù)分配部分的頁作為目錄項的緩存,正在被使用的目錄項對象,剛剛釋放的目錄項對象,類似于Linux中的最近最少使用(LRU)鏈表,inodeCache表示索引節(jié)點在內(nèi)存中的抽象,其結(jié)構(gòu)類似于dentryCache,bufferCache表示存放VSFS從磁盤讀取數(shù)據(jù)的抽象,在實現(xiàn)過程通過buffer_head來操作,buffer_head記錄各緩沖塊的詳細信息,fprocs表示進程與文件系統(tǒng)之間相關(guān)信息的抽象,messages表示進程之間IPC發(fā)送消息的抽象,disk表示VSFS磁盤的抽象,它是Isabelle/HOL對于VSFS中磁盤總體布局中各個數(shù)據(jù)結(jié)構(gòu)的抽象,其在Isabelle/HOL中的定義如算法2所示。inodeTable記錄磁盤上所有索引節(jié)點的集合。需要注意的是,為支持內(nèi)聯(lián)數(shù)據(jù)機制,索引節(jié)點由元數(shù)據(jù)和它所記錄的內(nèi)聯(lián)數(shù)據(jù)兩部分所構(gòu)成。內(nèi)聯(lián)數(shù)據(jù)機制必須滿足2.3節(jié)的要求才會被使用。

算法2磁盤在Isabelle/HOL中的抽象

record disk =

superBlocks :: D_SUPER_BLOCK

superBlockbk :: D_SUPER_BLOCK

Imap :: ″int list″

Bmap :: ″int list″

inodeTable :: ″D_INODE list″

files :: ″(NAME,INODE_INFO)file″

在算法2中,superBlocks表示磁盤的超級塊信息,superBlockbk表示超級塊在磁盤的備份,Imap表示索引節(jié)點空閑位圖,Bmap表示磁盤塊空閑位圖, inodeTable表示磁盤的索引節(jié)點表,files表示磁盤文件是由目錄樹組織的,通過使用file類型結(jié)構(gòu)來抽象。這是一個為特里樹(trie)類型的抽象。葉子節(jié)點為普通的文件,樹節(jié)點的子節(jié)點表示的是一個目錄文件所包含的文件。每個樹上的節(jié)點有文件名NAME和文件相關(guān)信息及內(nèi)容INOED_INFO兩個域。

至此,給出VSFS的狀態(tài)集合Svsfs定義,如式(3)所示:

Svsfs=S0∪S1∪…∪Sn-1∪Sn

(3)

其中:S0表示VSFS初始化之前的合法狀態(tài)集合,即式(4),vsfs_disk()表示磁盤檢測函數(shù);S1表示經(jīng)過初始化后能夠執(zhí)行各種系統(tǒng)調(diào)用的狀態(tài)的集合,即式(5);Sn表示執(zhí)行完成各個系統(tǒng)調(diào)用后,可以接收下次消息請求的狀態(tài)集合,即式(6);Sread、Swrite分別表示VSFS準(zhǔn)備提供讀寫服務(wù)時的狀態(tài)集合;S2～Sn-1分別表示VSFS在執(zhí)行各個請求之前的狀態(tài)集合。以read請求為例,設(shè)執(zhí)行讀取服務(wù)的狀態(tài)集合為Sread,即式(7)。

?s∈S0.vsfs_disk(s)

(4)

?s∈S1.?s′∈S0.disks=disks′

(5)

?s′∈Sn.((?s′∈Sread.s=vsfs_reads′)∪

(?s′∈Swrite.s=vsfs_writes′)∪…)

(6)

?s∈Sread.m_type(messages)=READ

(7)

初始狀態(tài)S1∈S0,即表示VSFS的初始狀態(tài)應(yīng)當(dāng)通過合法的磁盤檢查;終止?fàn)顟B(tài)SE=S1∪Sn,即VSFS的終止?fàn)顟B(tài)為執(zhí)行完系統(tǒng)調(diào)用后各種狀態(tài)的并集。

3.2 Фvsfs字母表

Фvsfs是VSFS抽象模型可以識別的字母表,它由VSFS的系統(tǒng)調(diào)用所構(gòu)成,其定義如式(8)所示:

Φvsfs={i,do_r,r,…}

(8)

其中:i表示初始過程;do_r表示VSFS提供給上層應(yīng)用程序所使用的系統(tǒng)調(diào)用接口;r表示VSFS 提供實際讀取服務(wù)的事件。其他提供給上層服務(wù)的系統(tǒng)調(diào)用接口與實際提供服務(wù)的事件也以do_x、x的形式來表示,x為提供給應(yīng)用程序?qū)拥南到y(tǒng)調(diào)用。

3.3 狀態(tài)轉(zhuǎn)移函數(shù)ξvsfs

根據(jù)有限狀態(tài)自動機的定義,VSFS的狀態(tài)轉(zhuǎn)移函數(shù)ξvsfs的定義如式(9)所示:

ξvsfs:Svsfs*Φvsfs→Svsfs

(9)

ξvsfs表示當(dāng)VSFS系統(tǒng)狀態(tài)處于s(s∈Svsfs)時,發(fā)生事件e(e∈Фvsfs),狀態(tài)轉(zhuǎn)移函數(shù)Δ(Δ∈ξvsfs)將會通過修改抽象模型中的工作對象,使得VSFS系統(tǒng)狀態(tài)轉(zhuǎn)變?yōu)閟′ (s′∈Svsfs)。

狀態(tài)轉(zhuǎn)移函數(shù)由VSFS文件系統(tǒng)為用戶應(yīng)用層提供的系統(tǒng)調(diào)用抽象而來?；贖oare邏輯三元組來構(gòu)建這些函數(shù)的公理語義,如式(10)所示:

{P}F{Q}

(10)

式(10)表示程序F在入口處與出口處各變量滿足的條件,即為狀態(tài)躍遷的前后狀態(tài),P和Q分別為前置條件與后置條件。當(dāng)前置狀態(tài)合法時,功能正確的系統(tǒng)調(diào)用在運行結(jié)束后,后置狀態(tài)也應(yīng)當(dāng)合法。以初始化函數(shù)vsfs_init()為例進行講解。vsfs_init()所對應(yīng)的事件為i,設(shè)在VSFS初始化前的狀態(tài)為s0,初始化后的狀態(tài)為s′。vsfs_init(s0,i) =s′表示系統(tǒng)啟動后可以正確初始化并達到統(tǒng)一狀態(tài)。vsfs_init()公理語義如式(11)所示:

{tt}vsfs_init{R(s,s′)}

(11)

其中:tt為永真謂詞,表示VSFS處于任何狀態(tài)。式(11)表示無論執(zhí)行初始化服務(wù)之前系統(tǒng)處于何種狀態(tài),經(jīng)初始化后都將滿足條件R。R(s,s′)的定義如算法3所示。

算法3后置條件R(s,s′)

(s′.superBlocks= s.disk.superBlocks)∧

(s′.dentryCache=(freeDentrylst=(FreeDentry #…#FreeDentry)∧(inuseDentrylst=[RootDentry])∧ (unuseDentrylst = []))) ∧

(s′.inodeCache = …)∧(s′.bufferCache = …)∧(s′.filps = Freefile #…# Freefilp) ∧

(s′.fprocs = []) ∧ (s′.disks = s.disks)

dentryCache、inodeCache、bufferCache由3個對應(yīng)的緩存列表構(gòu)成,初始化時將根節(jié)點的信息更新至緩存。inodeCache與bufferCache的語義類似于dentryCache的語義。根據(jù)vsfs_init()的公理語義,在Isabelle/HOL中給出它的形式化抽象,如算法4所示。

算法4vsfs_init()在Isabelle/HOL中的抽象

fun vsfs_init::″state ? state″

where

superBlocks:= sb_init (superBlock(disk s)),

filps:= init_filp_s (filp_s s),

dentryCache:= d_cache_init (dentry_cache s),

inodeCache:= i_cache_init (inode_cache s),

bufferCache:= b_cache_init (buffer_cache s),

fprocs:= init_fproc_list [] FPROC_NUM,

vsfs_init()的類型為″state?state″。在抽象過程中使用輔助函數(shù)來更加簡潔高效地表示。以sb_init()為例,它所需的參數(shù)為磁盤超級塊信息(superBlock(disks)),返回的對象被用于更新工作對象superBlocks,其他的輔助函數(shù)與此類似。這使得在后續(xù)驗證過程中,必須驗證輔助函數(shù)的正確性。

以文件系統(tǒng)最重要的提供讀寫服務(wù)的write()、read()系統(tǒng)調(diào)用為例,兩者實現(xiàn)函數(shù)分別為vsfs_write()、vsfs_read(),其在Isabelle/HOL中的抽象分別為算法5、算法6。

算法5vsfs_write()在Isabelle/HOL中的抽象

fun vsfs_write::″state ? state″

where

″vsfs_write s =

(if valid_fd s (m_fd(messages s))

then (if valid_write_len s

then (if write_free_block s

then (if write_free_buffer s

then (if inline_data s

then inline_write s

else plain_write s)

else s) else s) else s) else s)″

算法6vsfs_read()在Isabelle/HOL中的抽象

fun vsfs_read::″state ? state″

where

″vsfs_read s =

(if valid_fd s (m_fd(message_s s))

then (if m_len(message_s s) >0

then (if find_free_buffer s

then (if valid_pos s

then (if if_inline_data s

then inline_read s

else plain_read s )

else s) else s) else s) else s)″

讀寫服務(wù)的具體實現(xiàn)分為兩種:在讀寫文件時,會通過索引節(jié)點中的inline_type字段識別是否啟用內(nèi)聯(lián)數(shù)據(jù)機制,若啟用內(nèi)聯(lián)數(shù)據(jù)機制,則在讀取數(shù)據(jù)時會先檢索索引節(jié)點的后128 Byte空間;在寫入文件時,會先判斷新數(shù)據(jù)寫入是否導(dǎo)致文件大小超出內(nèi)聯(lián)數(shù)據(jù)機制的容量限制,若未超出則將數(shù)據(jù)寫至索引節(jié)點的后128 Byte空間,若超出則為其分配新數(shù)據(jù)塊,將數(shù)據(jù)復(fù)制到該數(shù)據(jù)塊,并修改相關(guān)標(biāo)識位。

VSFS文件系統(tǒng)為上層應(yīng)用程序提供的系統(tǒng)調(diào)用都有與之對應(yīng)的狀態(tài)轉(zhuǎn)換函數(shù),根據(jù)它的功能規(guī)范與安全需求建立與之對應(yīng)的公理語義,并在Isabelle/HOL中實現(xiàn)狀態(tài)轉(zhuǎn)移函數(shù)的抽象。

至此,以一個五元組來表示VSFS的有限狀態(tài)機模型Mvsfs,如式(12)所示:

Mvsfs=(Svsfs,Φvsfs,ξvsfs,SI,SE)

(12)

4 正確性證明

VSFS為上層用戶程序提供的服務(wù)是其提供的系統(tǒng)調(diào)用集合,因此為驗證VSFS的安全性與可信性,不僅要驗證在抽象系統(tǒng)調(diào)用時所使用的輔助函數(shù)功能正確性,還需歸納分析出VSFS有限狀態(tài)機模型中抽象化的狀態(tài)轉(zhuǎn)移函數(shù)正確性斷言。通過使用證明策略,在交互式定理輔助證明器Isabelle/HOL中完成對于輔助函數(shù)功能正確性和狀態(tài)轉(zhuǎn)移函數(shù)正確性的斷言驗證。

4.1 輔助函數(shù)的功能正確性

為更加細粒度地驗證文件系統(tǒng)的實現(xiàn)正確性,以及提高驗證工作的模塊化與簡潔性,本文使用了大量的輔助函數(shù)。針對VSFS的正確性,這些輔助函數(shù)的功能正確性同樣決定著整個模型的正確性。因此,對于這些輔助函數(shù)的功能正確性的驗證是必要的。

以磁盤上的文件抽象file為例,定義如式(13)所示:

ffile=(Tf,ξf,ρf)

(13)

Tf為文件目錄樹的抽象結(jié)構(gòu),它在Isabelle/HOL中的定義如算法7所示。

算法7Tf在Isabelle/HOL中的定義

datatype (′a,′v)File = FILE″ ′v option″ ″(′a * (′a,′v) File) list″

ξf為作用在Tf上的操作函數(shù),即為抽象系統(tǒng)調(diào)用過程中使用的輔助函數(shù),其定義如式(14)所示:

ξf=(getFileName,getDir,

isFile,isDir,updateDir)

(14)

這些函數(shù)的功能分別為返回文件名、返回目錄結(jié)構(gòu)、查詢指定文件是否存在并返回、指定目錄是否存在并返回、更新目錄結(jié)構(gòu)中的內(nèi)容。

ρf為ξf的安全屬性,其定義如式(15)所示:

ρf=(P1,P2,P3,P4,P5)

(15)

其中:P1、P2、P3、P4、P5分別為ρf中對應(yīng)函數(shù)的功能正確性的屬性。具體定義見表2。

表2 ρf中各屬性的具體定義Table 2 Specific definitions of each attributes in ρf

由于屬性P1、P2、P3的內(nèi)容并不復(fù)雜,根據(jù)它們各自所對應(yīng)的函數(shù)的定義,在Isabelle/HOL中使用自動證明策略“auto”完成證明。屬性P4與屬性P5的證明策略較為類似,以更為復(fù)雜的屬性P5為例進行講解。屬性P5所對應(yīng)的函數(shù)updateDir通過遞歸方式查找文件目錄樹來更新文件內(nèi)容,因此通過對變元as使用證明策略“induct_tac”進行啟發(fā)式歸納,獲得證明子目標(biāo)g1、g2,如表3所示。

表3 屬性P5證明過程中各子目標(biāo)Table 3 Each subgoal in the proof process of attribute P5

在Isabelle/HOL的幫助下使用證明策略“auto”可以將證明工作轉(zhuǎn)化為證明子目標(biāo)g3、g4、g5。最后使用證明策略“case_tac”對變元bs進行分類實例化,即可在證明策略“auto”的幫助下完成對于屬性P5的證明,在Isabelle/HOL中“No subgoals”表示完成證明。具體證明過程與結(jié)果如圖4所示。

圖4 屬性P5在Isabelle/HOL中的證明過程Fig.4 The proof process of attribute P5 in Isabelle/HOL

同理,其他系統(tǒng)調(diào)用的屬性也通過在Isabelle/ HOL中使用類似的證明策略來完成正確性證明。

4.2 狀態(tài)轉(zhuǎn)移函數(shù)的斷言

在分析歸納出狀態(tài)轉(zhuǎn)移函數(shù)斷言之前,需要先給出VSFS的不變式V(s)。不變式V(s)的具體含義是指磁盤上的數(shù)據(jù)需要與內(nèi)存上緩存的對應(yīng)數(shù)據(jù)保持一致性。假設(shè)VSFS在狀態(tài)s提供相應(yīng)的系統(tǒng)調(diào)用后,系統(tǒng)的狀態(tài)躍遷為s′′,該一致性條件仍然成立,即V(s′′)仍然成立。不變式是由磁盤格式的正確性屬性以及內(nèi)存上inode、dentry、buffer 3個對象的緩存鏈表的正確性屬性來決定的。它們在Isabelle/HOL中的抽象分別對應(yīng)vsfs_inode()、vsf_dentry()、vsfs_buffer()。

以最為復(fù)雜的磁盤格式的正確性屬性為例,其表示需要檢查磁盤上整體數(shù)據(jù)的正確性,如超級塊中魔數(shù)是否為指定值、第1塊可用的數(shù)據(jù)塊號是否合法、在初始化時超級塊中數(shù)據(jù)與超級塊備份數(shù)據(jù)是否一致等。此外,磁盤格式的正確性屬性對磁盤的文件組織關(guān)系也有所限制,如不同的文件所具有的數(shù)據(jù)塊號相異、處于不同目錄下文件的索引節(jié)點號相異、文件所持有的索引節(jié)點號與數(shù)據(jù)塊號分別在索引節(jié)點位圖和塊位圖中對應(yīng)數(shù)據(jù)位都已被置位等。

有了不變式的定義,接下來給出VSFS中各系統(tǒng)調(diào)用的正確性斷言。如表4所示。表中給出了提供初始化服務(wù)的vsfs_init()斷言A1、提供讀取服務(wù)的vsfs_read()的斷言A2,以及真正實現(xiàn)讀取服務(wù)的2個不同函數(shù)Plain_read()和Inline_read()的正確性斷言A3和A4。

表4 VSFS文件系統(tǒng)中部分正確性斷言的定義Table 4 Definition of partial correctness assertion in VSFS file system

如前所述,這些斷言在Isabelle/HOL的幫助下,通過使用證明策略完成正確性驗證。同理,其他系統(tǒng)調(diào)用的正確性斷言也通過類似的方法進行形式化證明。

5 結(jié)束語

本文基于高階邏輯和有限狀態(tài)機理論,提出一種細粒度的形式化方法對微內(nèi)核架構(gòu)操作系統(tǒng)的文件系統(tǒng)模塊進行設(shè)計和驗證,并為安全可信的微內(nèi)核操作系統(tǒng)VSOS設(shè)計和驗證了帶有內(nèi)聯(lián)數(shù)據(jù)機制的文件系統(tǒng)VSFS。在Isabelle/HOL中,通過定理證明的方法完成了對VSFS功能正確性驗證。下一步將對微內(nèi)核操作系統(tǒng)的文件系統(tǒng)的并發(fā)性進行研究,以提高文件系統(tǒng)在提供并發(fā)性數(shù)據(jù)服務(wù)時的可靠性和安全性。