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

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

0 引言

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

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

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

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

1 相關工作

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

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

來自美國麻省理工學院(MIT)的計算機科學與人工智能實驗室(CSAIL)的研究人員主持了一系列關于文件系統(tǒng)形式化驗證項目,如表1所示。該項目組主要關注文件系統(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)相結合,設計了經過形式化驗證的、使用加密原語保護磁盤文件安全的文件系統(tǒng)(IFSCQ)。文獻[18]設計了名為optimistic systems calls的機制,以較小的工作量在FSCQ上引入并發(fā)機制,進而構建了并發(fā)性文件系統(tǒng)(CFSCQ)。針對并發(fā)文件系統(tǒng)機密性,文獻[19]提出DIESKSEC方法,并開發(fā)了SFSCQ文件系統(tǒng)。文獻[20]介紹了Perennial的形式化驗證框架,對文件系統(tǒng)的并發(fā)性崩潰安全展開進一步的驗證。文獻[21-23]引入更多技術規(guī)范構建Perennial 2.0框架,并用其驗證使用Go語言實現(xiàn)的網絡文件系統(tǒng)服務器DaisyNFS,以及它的日志服務系統(tǒng)GoJournal。

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

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

2 VSFS文件系統(tǒng)

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

2.1 VSOS架構

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

圖1 VSOS整體架構Fig.1 VSOS overall architecture

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

服務器層和驅動層都將作為獨立的進程運行,它們之間只能通過進程間通信(IPC)來彼此間調用服務。如VSOS中提供的基礎原語SEND和RECEIVE。VSOS通過提供一個輕量化、固定長度的消息結構來簡化消息的處理。VSFS運行在用戶模式,被劃分到服務器層。這將使得VSFS無法直接去獲取內核中的特權服務,比如I/O操作?；凇白钚嘞拊瓌t”的VSOS在內核層設計了系統(tǒng)任務進程來專門處理VSFS通過IPC發(fā)出的內核調用,避免VSFS直接獲取特權服務。

2.2 VSFS設計布局

VSFS在磁盤上設計布局如圖2所示。VSFS將block 0分配給Boot程序,負責程序的啟動和運行。隨后是磁盤上的元數(shù)據(jù)結構區(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ù)結構只使用128 Byte,冗余的空間是為支持內聯(lián)數(shù)據(jù)機制。

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

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

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

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

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

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

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

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

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

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

(1)

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

3.1 狀態(tài)

VSFS提供服務的過程可以看作VSFS中狀態(tài)的轉變過程。在理論上,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表示內存中超級塊的抽象,它存放有VSFS文件系統(tǒng)的有關信息,filps表示進程與被打開文件之間信息的抽象,文件描述符fd指向filp中被打開的文件,dentryCache表示目錄項在內存中的緩存抽象,由3個列表構成,分別為空閑目錄項對象的緩存與VSFS在初始化時將預分配部分的頁作為目錄項的緩存,正在被使用的目錄項對象,剛剛釋放的目錄項對象,類似于Linux中的最近最少使用(LRU)鏈表,inodeCache表示索引節(jié)點在內存中的抽象,其結構類似于dentryCache,bufferCache表示存放VSFS從磁盤讀取數(shù)據(jù)的抽象,在實現(xiàn)過程通過buffer_head來操作,buffer_head記錄各緩沖塊的詳細信息,fprocs表示進程與文件系統(tǒng)之間相關信息的抽象,messages表示進程之間IPC發(fā)送消息的抽象,disk表示VSFS磁盤的抽象,它是Isabelle/HOL對于VSFS中磁盤總體布局中各個數(shù)據(jù)結構的抽象,其在Isabelle/HOL中的定義如算法2所示。inodeTable記錄磁盤上所有索引節(jié)點的集合。需要注意的是,為支持內聯(lián)數(shù)據(jù)機制,索引節(jié)點由元數(shù)據(jù)和它所記錄的內聯(lián)數(shù)據(jù)兩部分所構成。內聯(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類型結構來抽象。這是一個為特里樹(trie)類型的抽象。葉子節(jié)點為普通的文件,樹節(jié)點的子節(jié)點表示的是一個目錄文件所包含的文件。每個樹上的節(jié)點有文件名NAME和文件相關信息及內容INOED_INFO兩個域。

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

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

(3)

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

3.2 Фvsfs字母表

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

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

(8)

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

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

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

ξvsfs:Svsfs*Φvsfs→Svsfs

(9)

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

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

{P}F{Q}

(10)

式(10)表示程序F在入口處與出口處各變量滿足的條件,即為狀態(tài)躍遷的前后狀態(tài),P和Q分別為前置條件與后置條件。當前置狀態(tài)合法時,功能正確的系統(tǒng)調用在運行結束后,后置狀態(tài)也應當合法。以初始化函數(shù)vsfs_init()為例進行講解。vsfs_init()所對應的事件為i,設在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í)行初始化服務之前系統(tǒng)處于何種狀態(tài),經初始化后都將滿足條件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個對應的緩存列表構成,初始化時將根節(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)最重要的提供讀寫服務的write()、read()系統(tǒng)調用為例,兩者實現(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)″

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

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

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

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

(12)

4 正確性證明

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

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

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

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

ffile=(Tf,ξf,ρf)

(13)

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

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

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

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

ξf=(getFileName,getDir,

isFile,isDir,updateDir)

(14)

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

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

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

(15)

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

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

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

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

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

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

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

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

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

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

有了不變式的定義,接下來給出VSFS中各系統(tǒng)調用的正確性斷言。如表4所示。表中給出了提供初始化服務的vsfs_init()斷言A1、提供讀取服務的vsfs_read()的斷言A2,以及真正實現(xiàn)讀取服務的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)調用的正確性斷言也通過類似的方法進行形式化證明。

5 結束語

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