基于Isabelle/HOL的文件系统形式化设计与验证

作     者：王文斌 钱振江 靳勇 孙高飞 邢晓双 苏超 孙天琦 WANG Wenbin;QIAN Zhenjiang;JIN Yong;SUN Gaofei;XING Xiaoshuang;SU Chao;SUN Tianqi

作者机构：苏州大学计算机科学与技术学院江苏苏州215000 常熟理工学院计算机科学与工程学院江苏苏州215500 

出 版 物：《计算机工程》 (Computer Engineering)

年 卷 期：2024年第50卷第4期

页      面：277-285页

学科分类：081203[工学-计算机应用技术] 08[工学] 0835[工学-软件工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：江苏省自然科学基金面上项目(BK20191475) 常熟市社会发展项目(CS202204) 

主　　题：形式化验证 文件系统 定理证明 有限状态机 微内核 

摘      要：对于构建可信操作系统而言,文件系统设计和实现的正确性至关重要,即使是已经得到广泛运用的文件系统仍然有漏洞被检测出来。采用形式化方法对文件系统的设计和实现的正确性进行严格的验证是公认的可行方法。当前文件系统的形式化验证工作大多基于宏内核操作系统,而忽视了微内核操作系统架构下文件系统的验证。为此,提出一种微内核架构下采用内联数据机制的文件系统的形式化设计和验证方法。以高阶逻辑(HOL)和自动机模型为基础,将文件系统中的工作对象和系统资源抽象为系统对象来构建文件系统的工作状态,形式化地描述文件系统的相关系统调用的功能语义,将系统调用提供服务的过程抽象为系统工作状态发生跃迁的过程,并给出文件系统功能正确性和安全属性的断言。以实现的安全可信微内核操作系统(VSOS)中的安全可信文件系统(VSFS)为例,在设计阶段构建VSFS的有限状态机模型,并在Isabelle/HOL中抽象描述VSFS的可移植操作系统接口(POSIX)系统调用,分析和归纳出VSFS文件系统正确性断言,使用定理证明的方式来验证VSFS的正确性。实验结果表明,该方法在Isabella/HOL中完成VSFS有限状态机模型细粒度的形式化验证,满足预期的安全需求规范。