| Safety-critical systems take an important role in social production and life, especially used in some areas for high reliability requirements. As the core component of the system, security kernel is very important to build a reliable operating system. Based on security kernel, separation kernel can solve the large and complex problems of security kernel in the design and validation process of a security kernel; it provides a multi-level security operation for system. How to provide separation mechanism to ensure that no unauthorized information interaction will happen between applications, as well as how to make related formal verification, has been one of the focused researches inter-nationally. There are three methods of formal verification, model checking, equivalence proving and theorem proving. This paper adopts the theorem proving approach. By means of design the framework of the operating system kernel, it then describes the features of the kernel, and finally proves its sepa-ration properties.First we construct a verified separation kernel, which meets the require-ments of separation properties that are described by the GWV theorem, which explicitly describes the operations that the separation kernel provides. The construction of such security policy lays the foundation of separation kernel verification. By analysing the formal specification of system allowed behaviour and pro-tected system, we can describe the isolated kernel framework of partition op-erating system. Based on above description and other necessary properties, we define the properties of memory, partition, system and isolation with the z/z++formal description language. The description of isolated kernel on abstract level is completed based on the previous descriptions.The last step is to transform the core components of separation kernel from z/z++to Coq, and describe the components of separation kernel of partition operating system with formal methods. The formalized proof of the separation properties of partition operating system is provided by Coq theorem proving tools. |
