OSOSM:Operating System Object Semantics Model and Formal Verification

The complexity of the operating system makes its security problems become increasingly prominent. Many research works verify the correctness of the existing operating systems using formal methods, and they mainly focus on verifying the implementation of functions on code level with programming formal logic. In this paper, from the view of system design, we recently propose an operating system object semantics model (OSOSM) based on the higher order logic and type theory. OSOSM adopts a hierarchical structure, including essential effectiveness layer, implementation layer, and optimization layer. OSOSM abstracts the execution subjects and resources as objects of the operating system, and establishes the domain of the discourse for the operating system. We denote the state of the operating system by mapping from the set of operating system object variables to the domain of discourse. OSOSM describes the semantics of system calls, and the security properties with the predicate formulae. This paper also elaborates on the formal methods of verifying that during execution the operating system maintains the security tactics and properties. Finally, we use the self-implemented and the verified trusted operating system (VTOS) as an example to illustrate the semantics correctness of OSOSM, and verify the consistency between the design and safety requirements with Isabelle theorem prover and show that VTOS has the expected security properties.