基于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

中图分类号:

TP391

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

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

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

参考文献

[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存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43(1):79-85. LI Q, ZHU X R, GUO J. Formal verification framework for AUTOSAR OS storage protection mechanism[J]. Computer Engineering, 2017, 43(1):79-85.(in Chinese)
[6] 石剑君, 计卫星, 石峰. 操作系统内核并发错误检测研究进展[J]. 软件学报, 2021, 32(7):2016-2038. SHI J J, JI W X, SHI F. Recent progress of concurrency bug detection in operating system kernels[J]. Journal of Software, 2021, 32(7):2016-2038.(in Chinese)
[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闪存硬件的形式化建模[J]. 计算机工程, 2015, 41(11):94-99. YANG L Y, GUO Y. Formal modeling for NAND flash hardware[J]. Computer Engineering, 2015, 41(11):94-99.(in Chinese)
[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[J]. 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] 邹沫, 谢昊彤, 魏卓然, 等. 基于锁耦合遍历算法的文件系统终止性验证[J]. 软件学报, 2022, 33(8):2980-2994. ZOU M, XIE H T, WEI Z R, et al. Verification of termination for file system based on lock coupling traversal[J]. Journal of Software, 2022, 33(8):2980-2994.(in Chinese)
[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[J]. IEEE Transactions on Intelligent Transportation Systems, 2023, 24(12):15459-15467.
[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[J]. Digital Communications and Networks, 2023, 9(5):1070-1079.

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

选择包含的内容