Formal Design and Verification of File System Based on Isabelle/HOL
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.
万方数据
维普
