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