论文部分内容阅读
在安全系统中，惟一重要的接口是能够进入安全周界的外部接口，可信进程明显运行于安全周界之内且是安全内核的扩展。所以，可信进程与内核之间的接口不比内核各部分之间的接口更特别，需要一种安全策略始终实施于安全周界。但可信进程缺乏像BLP模型一样具有通用指导性的形式化模型，基于TCSEC B2级以上安全功能需求，以及CC标准EAL5以上评估保证级的形式化需求，提供一个通用的可信进程安全策略和模型，可为系统开发者和评估者规范和验证可信进程的安全性提供参考。在解决以上问题上，本文取得了六个方面的成果：第一，在系统和深入地分析可信进程的本质及其行为特性的基础上，通过找出通用的四种可信进程行为的共同特点和安全需求，首次提出了一种基于RBAC、DTE、POSIX权能机制和无干扰理论相结合的设计思想，并制定出控制可信进程行为的通用安全策略，为建立通用的可信进程安全模型奠定了基础。第二，通过对现有安全系统中权能遗传算法的分析，提出了一种多策略适应的POSIX权能遗传算法。该算法可以支持安全操作系统对可信进程行为实现不同的特权控制需求，并保证最小特权原则的有效实施。第三，在深入研究建立形式化安全策略模型的目的、要求和方法的基础上，借助数学的形式语言，给出了一个完整的、形式化的可信进程安全策略模型。本模型的提出，对于形式化规范和验证可信进程的行为，为今后对TCSEC B2级以上高安全等级操作系统的设计和评估奠定了一定的基础。第四，在深入分析和对比目前可用于高安全等级操作系统中的形式化分析方法和证明工具的基础之上，提出了用Isabelle语言对可信进程模型属性和规则进行形式化规范的方法，总结出基于Isabelle系统证明模型规范内部一致性和正确性的实用方法。第五，基于符合GB17859-1999第四级(TCSEC B2级)、自主开发的结构化保护级安全操作系统(安胜OS v4.0)的特权控制目标，提出了本模型在该系统中进行实现的有效方法。第六，对可信进程实现涉及的其他几个关键技术问题，包括可信路径机制、审计机制和可信功能的设计和实现等都做了有益的研究和探讨，给出了在高安全等级操作系统环境中进行实施的大致方案和原则。