论文部分内容阅读
形式化开发安全保证技术是高安全等级操作系统的关键技术难点，国内尚未见相关研究成果，论文围绕高安全等级操作系统开发的整个生命周期，研究了安全策略模型和顶层规范的形式规范和形式验证技术及系统实现。取得以下几个方面的成果：第一，提出一种通用的状态机安全策略模型的形式规范构造方法。该方法基于Isabelle/HOL语言，对多种安全策略模型通用，且充分考虑了与功能规范的对应性分析的可行性。分析了方法的原理，并给出了SBLP模型的规范和验证实例；第二，提出一种形式化顶层规范的构造方法，并给出实施了SBLP模型的SecLinux文件系统的FTLS实例。首次形式化描述了与POSIX1003.le兼容的ACL机制，并考虑了强制访问控制机制中客体间的信息流控制；第三，提出一种求精证明方法用于FSPM和FTLS之间的对应性分析。该方法包括一套基于Isabelle/HOL的求精规则，和一个引入了中间层的层次化求精方法。该方法大大降低了求精证明的难度。第四，针对支持动态多策略的需求，分析了当前几种典型安全体系结构在策略重用、策略共存方面的问题。提出一个新型的安全体系结构ELSM，引入模型组合器作为主模块实施模块堆栈管理和模块决策管理。策略决策基于访问控制空间形式规范方法，满足通用性。第五，给出了基于ELSM的FTLS的SecLinux文件系统实现实例。该系统基于Linux资源，为主流操作系统实现高安全等级提供了有意义的参考。第六，提出了一种支持多策略的基于微内核的安全体系结构，并基于此开发和验证一个微内核安全操作系统SecL4。该体系结构模块性强、结构清晰，解决了代码实现层难以形式化的难题。体系结构中的TPM保证了系统的引导和安全组件引入系统的可信性。