Research On Verification Of Secure Operating System Based On Model Checking

As an important index of high-level operating system evaluation criterion,and the most effective proof of the security property of the operating system,formal verification of secure operating system has great significance and practical value.In the current stage,formal verification can be divided mainly into two classes:model checking and theory proving.This thesis focuses on some key issues of model checking,in each hierarchy of the formal verification framework of the secure operating system. The main work and innovations are listed as follows:Fist,to the problem that SELinux policy configuration is complicated and hard to analyze,a unified information flow analysis of SELinux policies is proposed,which is based on the techniques of model checking.It can be used to verify the coherence of the security requirement and the policy implementations.A labeled transition system is adopted to merge MLS policies and TE-RBAC policies into a unified description framework.A complete definition of information flow property of the policy configuration is given,including the information flow caused by type access rules, type transition rules and especially MLS constraint rules in SELinux policy configuration. Also,a new security requirement description language is designed to strip off the high-level security requirement description from the low-level policy implementation, which makes the requirement representation independent of the detail of policy language and extends the capability to explore unknown vulnerability.Secondly,a coherence verification of security model and requirement is proposed. In the use of the expression of UML class diagram and state machine diagram in the static and dynamic modeling,a new security model description method of UML is designed.The UMLized model is compiled to model checker's specification language after given the UML diagram's state machine semantics.Then the requirement,which is also translated to the model checker's input,can be checked accordingly against to the security model.This achievement makes it possible to verify the correctness of security model semi-automatically and reduces the high requirement of formal methods and the heavy work in the traditional security model verification.Finally,about optimization of test sets in the security verification,the concept of degenerate test set is proposed,considering not only the redundant state,but also the state transition.The generation algorithm is represented then.A discussion is made to determine the algorithm's effectiveness when test case fails for the first time. After that,an improved DTS generation algorithm is given,which can show the failure location accurately without affecting the efficiency of the algorithm.