【作者】 季庆光；

【导师】 卿斯汉；

【作者基本信息】 中国科学院研究生院（软件研究所） ， 计算机应用技术， 2004， 博士

【摘要】 本文主要研究开发高安全等级的操作系统所必需的安全策略形式模型，为此我们从形式设计方法的探讨入手，确定模型设计的基本原则及组织结构，然后根据确定的组织结构逐步展开设计，提出支持多策略的形式框架、实现机密性策略的可动态调节安全级范围的多级安全模型DMLR_MLS(本文把它与DAC模型合在一起形成DBLP模型)、基于DTE技术实现完整性保护的形式模型DTE_IPM及基于权能、角色及DTE的特权控制模型PCM_RBPC。之后，分析整个模型可能存在的隐通道，提出分析模型的设计。最后，结合Linux内核，初步探讨模型的解释。 在这篇学位论文里，提出了八条模型设计的基本原则。构建了三位一体的模型开发模式：形式架构、策略规范语言及分量策略模型。分析了区分实现模型与分析模型的必要性。形式框架支持推理多策略的策略等价，策略冲突及策略协作，在多方面优于目前文献中的形式框架。DBLP模型作为可用于系统设计的形式模型，它在多方面改进了现有文献中的工作，使模型更实用。对于DTE_IPM模型，就我们所知，使用DTE技术构筑一个完整的完整性保护形式模型，是本文第一次进行了这样的尝试，该模型在控制恶意信息流方面有自己特殊的不变量。特权控制是在操作系统中实现安全的关键环节，模型PCM_RBPC通过三层结构，即：管理层、功能层及执行层，有效地实现了极小特权原理，从而成功地控制了特权，这个模型在五个方面有创新。提出了一个模型层次结构，并给出了在这个模型层次结构下系统安全的定义，获得安全的分解定理。给出了抽象安全策略的新定义，并用无干扰理论重新进行了解释。提出了多对象管理器与多安全服务器并存的实现体系。更多还原

【Abstract】 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.更多还原