Study On Formalization Design For High-Level Secure Operating System

This thesis focuses on studying security policy formal model, which is indispensable for developing high level secure operating system. For this, based on analyzing formalized design method, principles and architecture for designing formal model are proposed, then according to them, the model is designed hierarchically. First, a formal framework for supporting multipolicy is presented. Second, some component models are constructed, including dynamically mediated security level rang multilevel security model DMLR-MLS, which is used to implement confidentiality policy, and renamed as DBLP model after it is combined with DAC model, based-DTE integrity protection security model DTE-IPM, and privilege control model PCM-RBPC based on capability mechanism, role mechanism and DTE privilege mechanism. Third, an analysis model aiming at finding out potential covert channel existing in implementation model is proposed. At last, model interpretation is discussed elementarily based on Linux kernel.In this work, eight principles are set out to direct model design. The model development mode with three components: formal framework, model specification language and component models, is figured out. The detailed analysis shows that it is necessary to distinguish implementation model from analysis model. The resulted formal framework reasoning about policy equivalence, policy conflict and policy cooperation has more advantages over ones described in literature. As a model that can be used to develop practical system, DBLP model has been designed based on some researches improving those works described in literature relevant to confidentiality policy models. To our knowledge, DTE-IPM is the first trying to build a whole integrity policy modelbased on DTE. It presents some new invariants, used to prevent malicious information flow from jeopardizing system, different from ones in some literatures. As key ingredient implementing secure operating system, effective privilege control is needed, and captured successfully by our model PCM-RBPC by means of the implementation of the least privilege principle with three layers structure, i.e., administration layer, functionality layer and execution layer; five original findings have been used to design this model. A model hierarchy is proposed, and system security under this model hierarchy is defined, and the unwinding theorem of system security is proved. The security policy is abstractly redefined, and made a new interpretation in noninterference theory. An implementation architecture consisted of multiple object managers and multiple security servers is described.