Research On Xen Security Model Design And Formal Verification

Cloud computing will face more threate,higher requirements is put forward to the cloud computing security.As the basic service platform of cloud computing,the security of virtualization system determines that of cloud computing,and the development of high security level virtualization system can improve the security of cloud computing.Based on the requirements of GB17859 structured protection level,this paper selects Xen as the development object,and constructs the security protection framework through demand analysis.Based on the framework,this paper puts forward the security strategy,builds the security model on the basis of the security policy,formally proves the consistency of the safety model and the security model,and develop high security level security model of Xen.Specific work is as follows.1.According to the requirements of GB17859 structure protection level,this paper develops the security framework of Xen.The security framework takes GB/T18336 for engineering standards as a template,adds the GB17859 for engineering practice and the cloud computing security industry standard.The security framework achieves the unity of oriented safety standards and oriented engineering practice,and achieves the unity of abstract standards and specific standards.2.Based on the function requirements of Xen security framework,a virtualized hybrid multi-policy security model(SV_HMPMD)combining RBAC,DTE and BLP is proposed.The model protects Xen's confidentiality and integrity,implements the privilege management of Dom0,uses a tab-based BLP and changes the security label value to a secure tag range,which improves the availability of the security model,and the use of interdomain isolation ensures the anti-jamming of the system.So the model has a high practical value.3.Based on the security assurance requirements of the Xen security framework,this paper formally verifies the consistency of security model and security requirements.Based on the type theory of high-order logic,a hierarchical semantic model based on state automata is proposed.The semantic model describes the constituent elements and the state transitions of the security model,and reduces the difficulty of describing the mixed multi-strategy model by hierarchical description.In the process of proof,this paper combines the automatic proof and semi-automatic proof,and outputs the structured theorem proving result that is easy to understand,and realizes automated proof and improves the readability of the proof process at the same time.4.To verify that the design of Xen security architecture and security requirements is consistent,this paper proposes a subject behavior semantic model based on the type description in set theory.The semantic model uses sequential logic in high order logic to formally describe the security architecture and security requirements,and verifies the consistency of the security architecture and safety requirements with the Isabelle / HOL theorem at the functional level.