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

doi:10.19678/j.issn.1000-3428.0067091

摘要/Abstract

摘要：

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

关键词: 形式化验证, 文件系统, 定理证明, 有限状态机, 微内核

Abstract:

To construct a trusted operating system, the correctness of file system design and implementation is essential. Even file systems that are widely used can have bugs. Using formal methods to verify the correctness of file system design and implementation is feasible. Most of the current formal verification research conducted on file systems are based on macro-kernel operating systems, whereas the verification of file systems under a micro-kernel operating system architecture is lacking. Accordingly, in this study, a formal design and verification method for a file system using an inline data mechanism with a micro-kernel architecture is proposed. Based on the Higher-Order Logic(HOL) and automaton models, the working state of the file system is constructed by abstracting the working objects and system resources in the file system into system objects, and the functional semantics of the related system calls of the file system are formally described. The process of invoking and providing the service is abstracted as the process of transitioning the system working state, and asserting the correctness of the file system function and security attributes is given. Using the implemented microkernel Verified Secure Operating System(VSOS) file system called Verified Secure File System(VSFS) as an example, the finite state machine model of VSFS is built in the design stage, Portable Operating System Interface of UNIX(POSIX) system of the VSFS is abstractly described in the Isabelle/HOL call, correctness assertion of the VSFS file system is analyzed and summarized, and a theorem proof is used to verify the correctness of VSFS. The experimental results depict that the proposed method can complete the fine-grained formal verification of the VSFS finite-state machine model in Isabella/HOL and meet the expected security requirements.

Key words: formal verification, file system, theorem proof, finite-state machine, microkernel

王文斌, 钱振江, 靳勇, 孙高飞, 邢晓双, 苏超, 孙天琦. 基于Isabelle/HOL的文件系统形式化设计与验证[J]. 计算机工程, 2024, 50(4): 277-285.

Wenbin WANG, Zhenjiang QIAN, Yong JIN, Gaofei SUN, Xiaoshuang XING, Chao SU, Tianqi SUN. Formal Design and Verification of File System Based on Isabelle/HOL[J]. Computer Engineering, 2024, 50(4): 277-285.

http://www.ecice06.com/CN/Y2024/V50/I4/277

图/表 8

图1 VSOS整体架构

Fig.1 VSOS overall architecture

图2 VSFS文件系统的总体布局

Fig.2 General layout of VSFS file system

图3 内联数据机制读取的对比

Fig.3 Comparison of inline data mechanism read

图4 属性P5在Isabelle/HOL中的证明过程

Fig.4 The proof process of attribute P5 in Isabelle/HOL

参考文献 25

1	ETHI U, PAN H, LU S, et al. Cancellation in systems: an empirical study of task cancellation patterns and failures[C]//Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. Carlsbad, USA: USENIX Association, 2022: 127-141.
2	OU X, YUAN J, SHILANE P, et al. The dilemma between deduplication and locality: can both be achieved?[C]//Proceedings of the 18th USENIX Conference on File and Storage Technologies. Santa Clara, USA: USENIX Association, 2021: 171-185.
3	PITCHUMANI R, KEE Y S. Hybrid data reliability for emerging key-value storage devices[C]//Proceedings of the 18th USENIX Conference on File and Storage Technologies. New York, USA: ACM Press, 2020: 309-322.
4	SONG Y, CHO M, KIM D, et al. CompCertM: CompCert with C-assembly linking and lightweight modular verification[C]//Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, USA: ACM Press, 2019: 1-23.
5	李青, 朱晓冉, 郭建. AUTOSAR OS存储保护机制的形式化验证框架. 计算机工程, 2017, 43(1): 79- 85. URL
	LI Q, ZHU X R, GUO J. Formal verification framework for AUTOSAR OS storage protection mechanism. Computer Engineering, 2017, 43(1): 79- 85. URL
6	石剑君, 计卫星, 石峰. 操作系统内核并发错误检测研究进展. 软件学报, 2021, 32(7): 2016- 2038. URL
	SHI J J, JI W X, SHI F. Recent progress of concurrency bug detection in operating system kernels. Journal of Software, 2021, 32(7): 2016- 2038. URL
7	KLEIN G, ELPHINSTONE K, HEISER G, et al. seL4: formal verification of an OS kernel[C]//Proceedings of the 22nd ACM SIGOPS Symposium on Operating systems Principles. New York, USA: ACM Press, 2009: 207-220.
8	杨龙婴, 郭宇. 针对NAND闪存硬件的形式化建模. 计算机工程, 2015, 41(11): 94- 99. URL
	YANG L Y, GUO Y. Formal modeling for NAND flash hardware. Computer Engineering, 2015, 41(11): 94- 99. URL
9	AMANI S, HIXON A, CHEN Z L, et al. Cogent: verifying high-assurance file system implementations[C]//Proceedings of the 21st International Conference on Architectural Support for Programming Languages and Operating Systems. New York, USA: ACM Press, 2016: 175-188.
10	CHEN Z L, LAFONT A, O'CONNOR L, et al. Dargent: a silver bullet for verified data layout refinement. Proceedings of the ACM on Programming Languages, 2023, 7(1): 47.
11	HAMZA J, FELIX S, KUNCAK V, et al. From verified scala to STIX file system embedded code using stainless[C]//Proceedings of the 14th International NASA Formal Methods Symposium. Pasadena, USA: [s. n. ], 2022: 393-410.
12	CHEUNG L, O'CONNOR L, RIZKALLAH C. Overcoming restraint: composing verification of foreign functions with cogent[C]//Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, USA: ACM Press, 2022: 13-26.
13	ZOU M, DING H R, DU D, et al. Using concurrent relational logic with helpers for verifying the AtomFS file system[C]//Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York, USA: ACM Press, 2019: 259-274.
14	邹沫, 谢昊彤, 魏卓然, 等. 基于锁耦合遍历算法的文件系统终止性验证. 软件学报, 2022, 33(8): 2980- 2994. URL
	ZOU M, XIE H T, WEI Z R, et al. Verification of termination for file system based on lock coupling traversal. Journal of Software, 2022, 33(8): 2980- 2994. URL
15	CHEN H G, ZIEGLER D, CHAJED T, et al. Using Crash Hoare logic for certifying the FSCQ file system[C]//Proceedings of the 25th Symposium on Operating Systems Principles. New York, USA: ACM Press, 2015: 18-37.
16	CHEN H G, CHAJED T, KONRADI A, et al. Verifying a high-performance crash-safe file system using a tree specification[C]//Proceedings of the 26th Symposium on Operating Systems Principles. New York, USA: ACM Press, 2017: 270-286.
17	ONG D W, MAMOURAS K, CHEN A. The design and implementation of a verified file system with end-to-end data integrity[EB/OL]. [2023-02-01]. http://arxiv.org/abs/2012.07917v1.
18	CHAJED T, CHLIPALA A, KAASHOEK M, et al. Extending a verified file system with concurrency[D]. Houston, USA: Rice University, 2017.
19	LERI A M, CHAJED T, CHLIPALA A, et al. [C]//Proceedings of the 13th USENIX Conference on Operating Systems Design and Implementation. New York, USA: USENIX Association, 2018: 323-338.
20	CHAJED T, TASSAROTTI J, KAASHOEK M F, et al. Verifying concurrent, crash-safe systems with Perennial[C]//Proceedings of the 27th ACM Symposium on Operating Systems Principles. New York, USA: ACM Press, 2019: 243-258.
21	CHAJED T, TASSAROTTI J, THENG M, et al. Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning[C]//Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. Carlsbad, USA: USENIX Association, 2022: 447-463.
22	HAJED T, TASSAROTTI J, THENG M, et al. GoJournal: a verified, concurrent, crash-safe journaling system[C]//Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation. Carlsbad, USA: USENIX Association, 2021: 423-439.
23	HAJED T. Verifying a concurrent, crash-safe file system with sequential reasoning[D]. Cambridge, USA: Massachusetts Institute of Technology, 2022.
24	QIAN Z J, ZHONG S, SUN G F, et al. A formal approach to design and security verification of operating systems for intelligent transportation systems based on object model. IEEE Transactions on Intelligent Transportation Systems, 2023, 24(12): 15459- 15467. doi: 10.1109/TITS.2022.3224385
25	QIAN Z J, XIA R, SUN G F, et al. A measurable refinement method of design and verification for micro-kernel operating systems in communication network. Digital Communications and Networks, 2023, 9(5): 1070- 1079.

[1]	黄保华, 郑慧颖, 屈锡, 陈宁江. 联盟链高效存储访问控制方案[J]. 计算机工程, 2023, 49(8): 37-45.
[2]	余进, 严华. 基于数据更新间隔的NAND闪存垃圾回收算法[J]. 计算机工程, 2022, 48(3): 54-59.
[3]	黄志清, 解鲁阳, 张严心, 尹泽明. 基于区块链的物联网数据服务信誉评估模型[J]. 计算机工程, 2022, 48(1): 33-42.
[4]	魏秀然, 王峰. 基于协调器与遗传算法的云存储数据复制策略[J]. 计算机工程, 2021, 47(8): 124-130,139.
[5]	夏锐, 钱振江, 刘苇. 一种基于Isabelle/HOL的安全通信协议验证方法[J]. 计算机工程, 2021, 47(1): 146-153.
[6]	欧阳恒一, 熊焰, 黄文超. 一种代币智能合约的形式化建模与验证方法[J]. 计算机工程, 2020, 46(10): 41-45,51.
[7]	钟建, 徐扬, 陈树伟, 何星星. 一阶逻辑中基于稳定度的项评估方法[J]. 计算机工程, 2019, 45(11): 183-190,197.
[8]	祁龙云, 吕小亮, 路红, 黄皓. 汇编级顺序语句块的自动形式化规约及其验证[J]. 计算机工程, 2019, 45(10): 64-69,77.
[9]	林荣峰, 施健, 朱晏庆, 沈怡颹, 周宇. 基于STP方法的SCADE模型形式化验证框架[J]. 计算机工程, 2019, 45(10): 70-77.
[10]	李堃,张雪松. STP安全通信协议设计与形式化验证[J]. 计算机工程, 2018, 44(12): 120-128.
[11]	高原,任升,顾文杰. 异构环境中HDFS数据块调度算法的设计与实现[J]. 计算机工程, 2017, 43(8): 82-89.
[12]	朱嘉舟,邵培南,陈景. 影像数据分布并行计算处理平台体系架构研究[J]. 计算机工程, 2017, 43(5): 60-66,74.
[13]	詹玲,方协云,李大平,万继光. 基于Ceph文件系统的元数据缓存备份[J]. 计算机工程, 2017, 43(4): 67-72,83.
[14]	阚文枭,黄秋兰,陈刚. 桌面网格环境下虚拟化技术的应用研究[J]. 计算机工程, 2017, 43(3): 11-17.
[15]	李青,朱晓冉,郭建. AUTOSAR OS存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43(1): 79-85.

选择文件类型/文献管理软件名称

选择包含的内容