论文部分内容阅读
高等级安全操作系统的完整性保护比机密性保护要复杂得多,对它的研究工作远没有机密性保护进展得顺利。本文基于TESEC等国内外计算机信息系统评估标准的要求,从理论和实践两个方面对高等级安全操作系统完整性保护策略模型的设计、实现和分析进行了研究,取得了以下五个方面的主要成果:第一,通过综合地分析比较经典的各种完整性策略模型各自的优点和不足,指出了完整性保护策略模型的发展方向。对当前广泛应用的混合RBAC-DTE策略,首次揭露了当中的多角色管理问题,从角色特权和角色的访问许可权两种层面上结合角色所允许进入的域,提出一种角色粗划分粒度,域细划分粒度的解决方法,进一步地引入域的静态继承关系来提供角色获得访问许可权的另一种方式,不但解决不同域的进程共享访问控制权集,同时又使策略的代码尺寸得以有效控制,特别地,充分支持极小特权原则。第二,利用传统DTE模型的突出特征,即通过域限制进程的活动范围使得授权用户的不当修改行为得以有效控制,以及模型易于实现和应用等特点,结合Biba模型的明确完整性目标,在对Biba完整性两种角度解释的基础上,分别提出以DTE为基本的组成框架,不同Biba完整性解释为安全目标的两种DTE完整性保护形式模型。从策略目标分析和验证来看,这两种DTE完整性保护形式模型差别在于它们的实用性,但它们都为DTE系统的完整性策略配置、完整性策略分析和完整性保护验证提供了理论基础。第三,提供了所设计的DTE完整性保护形式模型内在一致性的非形式化证明过程。进一步地通过选用Isabelle/Isar形式化验证技术,以更为严谨的形式化方法成功地对DTE完整性保护形式模型进行描述并验证其内在一致性。第四,研究SELinux中DTE模型的实现技术,在达到结构化保护级的安胜OSv4.0系统上,结合Flask安全体系结构和LSM访问控制框架,从策略配置、数据结构、系统调用、应用层命令以及访问控制流程等方面真正地实现了DTE完整性保护形式模型。第五,在安全增强L4微内核(SecL4微内核)上实现了DTE完整性保护形式模型的工作基础上,提供SecL4微内核的DTLS,并有效论证了TCB的描述性顶层规范(DTLS)和模型的一致性。