基于Isabelle/HOL的文件系統形式化設計與驗證

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

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

0 引言

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

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

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

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

1 相關工作

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

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

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

表1 文件系統形式化驗證項目Table 1 File system formal validation project

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

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

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

2 VSFS文件系統

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

2.1 VSOS架構

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

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

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

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

2.2 VSFS設計布局

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

圖2 VSFS文件系統的總體布局Fig.2 General layout of VSFS file system

VSFS會為每一個索引節點分配256 Byte的空間,但索引節點數據結構只使用128 Byte,冗余的空間是為支持內聯數據機制。

2.3 內聯數據機制

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

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

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

圖3 內聯數據機制讀取的對比Fig.3 Comparison of inline data mechanism read

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

3 VSFS文件系統的有限狀態機模型

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

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

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

(1)

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

3.1 狀態

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

Svsfs=∏i,j

(2)

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

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

算法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表示索引節點空閑位圖,Bmap表示磁盤塊空閑位圖, inodeTable表示磁盤的索引節點表,files表示磁盤文件是由目錄樹組織的,通過使用file類型結構來抽象。這是一個為特里樹(trie)類型的抽象。葉子節點為普通的文件,樹節點的子節點表示的是一個目錄文件所包含的文件。每個樹上的節點有文件名NAME和文件相關信息及內容INOED_INFO兩個域。

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

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

(3)

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

初始狀態S1∈S0,即表示VSFS的初始狀態應當通過合法的磁盤檢查;終止狀態SE=S1∪Sn,即VSFS的終止狀態為執行完系統調用后各種狀態的并集。

3.2 Фvsfs字母表

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

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

(8)

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

3.3 狀態轉移函數ξvsfs

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

ξvsfs:Svsfs*Φvsfs→Svsfs

(9)

ξvsfs表示當VSFS系統狀態處于s(s∈Svsfs)時,發生事件e(e∈Фvsfs),狀態轉移函數Δ(Δ∈ξvsfs)將會通過修改抽象模型中的工作對象,使得VSFS系統狀態轉變為s′ (s′∈Svsfs)。

狀態轉移函數由VSFS文件系統為用戶應用層提供的系統調用抽象而來。基于Hoare邏輯三元組來構建這些函數的公理語義,如式(10)所示:

{P}F{Q}

(10)

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

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

(11)

其中:tt為永真謂詞,表示VSFS處于任何狀態。式(11)表示無論執行初始化服務之前系統處于何種狀態,經初始化后都將滿足條件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個對應的緩存列表構成,初始化時將根節點的信息更新至緩存。inodeCache與bufferCache的語義類似于dentryCache的語義。根據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″。在抽象過程中使用輔助函數來更加簡潔高效地表示。以sb_init()為例,它所需的參數為磁盤超級塊信息(superBlock(disks)),返回的對象被用于更新工作對象superBlocks,其他的輔助函數與此類似。這使得在后續驗證過程中,必須驗證輔助函數的正確性。

以文件系統最重要的提供讀寫服務的write()、read()系統調用為例,兩者實現函數分別為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)″

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

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

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

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

(12)

4 正確性證明

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

4.1 輔助函數的功能正確性

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

以磁盤上的文件抽象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上的操作函數,即為抽象系統調用過程中使用的輔助函數,其定義如式(14)所示:

ξf=(getFileName,getDir,

isFile,isDir,updateDir)

(14)

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

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

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

(15)

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

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

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

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

4.2 狀態轉移函數的斷言

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

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

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

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

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

5 結束語

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