Research On Methodology Of Formal Design And Verification For Security Operating System

The operating system as the basic software provides the support and service plat-form for the upper applications. The security of operating system is the important foundation in the scope of the information security. Moreover, the correctness of de-sign and implementation of the operating system is the basis of security of operating system. How to ensure the correctness of the system is the hot topic in the research field of information security. The academia pays close attention to the research on the methods of formal proving for the attributes of the operating system, such as correct-ness. This dissertation argues that, in order to ensure the security of the system, the developers should adopt the requirement analysis and system modeling to sum up the conditions of system security, and based on these criteria to design the functionality for the operating system, and propose the targeted design principles and solutions. Mean-while, the developers should confirm that there are no security vulnerabilities in the system design, and verify the consistency between the design and implementation.This dissertation aims to form the formal technology and methodology with easy modeling, strong expressiveness and convenient reasoning. In this dissertation, we s-tudy the effective theories of system design, and the methods of system implementation and verification, in order to provide the valuable theoretical basis.In this dissertation, from the aspect of formal design and verification of the op-erating system, we study the feasibility of formal methods in the system design and verification, and form a series of methods of formal design and verification, to the maximum extent to ensure the correctness and security of the system. The work con-sists of two parts:verification of design and requirement of system functionality, and correctness verification of system implementation. Specifically, the main contributions of the work are as follows:1) From the view of system design, we novelly propose an operating system objec-t semantics model (OSOSM) based on the high-order logic as the meta-logic. OSOSM adopts 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 the mapping from the set of operating system object vari-ables to the domain of discourse. OSOSM describes the semantics of system calls, and the security properties with the predicate formulae. We also elaborates on the formal methods of verifying that during execution the operating system maintains the security tactics and properties. Finally, we use the modules of the virtual memory management in the self-implemented and verified trusted oper-ating system (VTOS) as an example to illustrate the semantics correctness of OSOSM, and verify the consistency between the design and safety requirements with Isabelle/HOL theorem prover and show that VTOS has the expected secu-rity properties.2) With the OSOSM model, we formally model the design of the system, and il-lustrate the method of constructing OSOSM in the design progress of the micro-kernel of VTOS. From the perspective of functionality integrity and behavioral isolation, we analyze the security requirement of microkernel OS. With the high-order logic and temporal logic, we describe and define the security requirements rigorously. Meanwhile, we use the theorem prover Isabelle/HOL to verify the consistency between system design and security requirements, and show that V-TOS achieves the desired security.3) For verification of system functionalities in the level of assembly language, we propose an OS state automaton (OSSA) model as the link between the design and verification for VTOS assembly level. We describe the domain of discourse of OSSA by defining the legitimate states and state transition functions of OSSA, and also for the VTOS assembly level. We verify the correctness of functional modules to ensure the correctness of the VTOS assembly level.