Review of Formal Specification and Verification for Operating Systems

Operating Systems (OSs), which form a critical infrastructure in the information age, are widely used in core fields such as medical care, industries, and the military. Their reliability and security directly determine the operational stability of these key fields, while vulnerabilities can lead to serious consequences, including system crashes and data leakage. Hence, the construction of a systematic security assurance system would be of great theoretical and engineering value. This paper systematically reviews the research achievements in this field over the past decade based on the framework of ″formal specification—formal verification—engineering implementation″ and analyzes technical paths and practical applications. With regard to formal specification level, it clarifies the differences between model specifications that describe system functions based on mathematical structures, such as transition systems, and property specifications that define safety and liveness requirements based on Linear Temporal Logic (LTL). This analysis focuses on two key aspects: functional correctness and security attributes. Functional correctness covers task management scheduling, memory allocation and recycling, exception interrupt handling, inter-task communication, and file system read—write consistency, while security attributes focus on the BLP and BIBA models for access control, multidomain isolation in separation kernels, and noninterference and nonleakage theories of information flow. For formal verification, three core methods are considered: deductive proof, which verifies program consistency by relying on Hoare's logic; model checking, which verifies temporal properties based on LTL and Computation Tree Logic (CTL); and standardized process of property verification. Taking the seL4 microkernel, which is the first to achieve functional correctness and information flow non-interference through machine proof, as a case study, this discussion reveals the transformation from theory to engineering. With regard to engineering applications, the achievements in Controller Area Network (CAN) bus communication verification within the automotive field and robustness detection of intercomponent communication in the Android system of smartphones are summarized. This systematic review aims to establish a foundation for future research in related fields, provide dataset support for large language models, and provide a reference for the engineering implementation of these technologies.