Abstract:As a fundamental component of a software system, the kernel of an operating system plays a crucial role in constructing a highly trusted software system. However, in practical verification, there are still many difficulties in invariant definition of global properties, and formal description and verification of complex data structure programs in the kernel of an operating system. Given the global properties satisfied by the kernel of an operating system, this study defines these properties at the code level on a function-by-function basis through global invariants and conducts formal verification in different functions to prove that each function conforms to the global properties of the operating system kernel. To formalize the complex data structure programs frequently adopted in the kernel of an operating system, the study proposes a method employing nested shape graph logic by extending the shape graph theory and provides a correctness proof for this method. Finally, it verifies the code related to task creation and scheduling, and message queue creation and operation in the operating system kernel.