基于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功能正确性验证。下一步将对微内核操作系统的文件系统的并发性进行研究,以提高文件系统在提供并发性数据服务时的可靠性和安全性。