VTOS: Research on Methodology of 'Light-Weight' Formal Design and Verification for Microkernel OS

摘要

The correctness of the operating systems is difficult to be described with the quantitative methods, because of the complexity. Using the rigorous formal methods to verify the correctness of the operating systems is a recognized method. The existing projects of formal design and verification focus on the validation of code level. In this paper, we present a "light-weight" formal method of design and verification for OS. We propose an OS state automaton model (OSSA) as a link between the system design and verification, and describe the correctness specifications of the system based on this model. We implement the trusted operating system (verified trusted operating system, VTOS) as a prototype, to illustrate the method of consistency verification of system design and safety requirements with formalized theorem prover Isabelle/HOL. The result shows that this approach is feasible.