Design And Application Research Of Secure Operating System Hybrid Multiple Policy Model

Security policy model is the foundation of a secure operating system, whether the resulting mechanisms have correctly enforced the security policies depends on the precise of the security definitions in the models. Hybrid Multi-Policy Model is the security policy model that organically integrates multiple single security policy models. It can fullfill the requirements of multiple security goals. Focusing on the formal security policy model, required by the high-level secure operating system, this paper researches some classical single policy models, implemented in current popular operating systems, and some typical hybrid multi-policy models, attracted by domestic and oversea researchers. Based on these pre-works, combining the concrete access control requirements of GB/T 20272-2006, it completes three jobs, which are:Firstly, one type of hybrid multi-policy model SOS_HMPM, abbr. for secure operating system hybrid multi-policy model, is designed. This model solves the confidentiality and integrity of the system and privilege controlled objects. It integrates three kinds of security policy model, including BLP, DTE and RBAC. On the basis of informal description, the model's formal design is completed, using the status machine theory as the computing model, and its characteristics and comparison with SELinux are also given.Secondly, a formal specification and validation method based on Isabelle/HOL for SOS_HMPM is proposed. It gives a construction method to formally specify the security status, constants and operation rules of SOS_HMPM, and definitudes the principle and steps to formally validate the model's inner consitency. Then, we use this method to formally specify and validate the confidential access control of SOS_HMPM.Thirdly, the application of the model in SELinux is discussed. We suggest an extended SELinux architecture as the basic platform for the realization of SOS_HMPM, discuss the implementing method of the model, and design the process of the system access control and the umpirage of security policy. At last, we show the application of the model in SELinux by means of several core policy configuration samples and its ability to fulfill the security requimreents.