VTOS: A Finite State Machine Model of OS and Formalized Verification of Its Microkernel

ABSTRACT. Operating system is a huge software with complicated functionality. The correctness of even single module cannot be proved through software test. Project seL4 has proved the correctness of each function of a microkernel operating system. The correctness of each single function of an operating system cannot prove its integrity and other security property. In this paper we proposed a OS model of finite state machine (OSMFSM). We design our VTOS(Verified Trusted Operating System), which is a microkernel operating system and aimed at being formally verified and trusted, according to this model. We define the state of the OSMFSM through the global objects in VTOS, and the transition function of the OSMFSM as a piecewise defined function through the functions in VTOS. Through establishing a domain for VTOS with the help of OSMFSM and another domain, which is isomorphic to the former, in Isabelle/HOL, we prove the correctness of some functions in the microkernel of VTOS formally. With the help of the concept of the invariability of the FSM, we propose a method of describing and proving the integrity of an OS.