论文摘要
本论文是对高安全级别可信操作系统实现的综合分析。论文针对生产信息系统的安全需求,主要考虑达到GB17859中第四级—结构化保护级的操作系统面临的一些关键问题。本论文以国家的等级保护标准为主要依据,对强制访问控制模型、可信计算等高安全级别操作系统实现的重要理论问题做了深入讨论,提出了保密性和完整性结合的格访控模型、动态二维访问控制模型、基于Shannon信息论的BLP模型量化分析方法、可信传递的形式化模型以及可信封装等创新性的理论内容。并针对Linux系统,提出了透明的安全机制,以及对内核进行层次化结构改造的Linux系统高安全级别改造方案。基于格的多级访问控制模型(LBAC)模型是最常用的强制访问控制模型。论文针对LBAC模型中保密性和完整性的融合问题,以及LBAC模型中的下向信息流问题,引入信息清除操作,提出了对LBAC模型的改进方案,使得LBAC模型可以支持下向信息流,从而避免了传统LBAC模型中信息的严格单向限制,增加了LBAC模型的灵活性。在此基础上,论文给出了一个保密性和完整性相融合的DPAC模型,该模型融合经典的BLP模型和Biba模型,引入对实体的动态安全标识方法,并通过可信主体,实现了不同级别之间的安全信息交互,避免了保密性和完整性策略同时实施时,系统不同安全级别成为信息孤岛的问题。论文针对经典的保密模型—BLP模型,提出了一个基于shannon信息论的量化分析方法。这一量化分析方法把BLP模型的多级安全策略用对敏感信息的不确定度来表述,引入对敏感信息的条件熵,提出了安全门限的概念。并将BLP模型的安全需求用一组安全门限量化表示,给出了一个不依赖于无干扰隔离的多级安全策略表示方法。这一方法使得对BLP模型下向信息流安全性的分析成为可能。据此,论文对BLP模型的下向信息流保密性给出了一个判断定理并证明了该定理。这一定理描述了当系统敏感信息的安全门限存在冗余,且下向信息流带宽受限时,下向信息流可以从理论上证明其安全性。它给出了下向信息流安全的理论依据。论文围绕着可信元件的行为可预测性,引入软件工程的黑盒函数的概念,建立了一个新型的可信计算的形式化理论模型。这一模型提出了信任的形式化解释,体现了信任在行为可预测性方面的内涵,指出了TCG标准信任定义中所缺省的内容,并说明这些内容在分析安全操作系统时是不能省略的。同时,我们基于这一模型对可信传递行为给出了形式化的描述,定义了可信元件集合的有效性,并证明了关于可信元件集合有效性的两个定理。这两个定理给出了可信元件集合有效性的两个充分必要条件。论文在可信计算理论模型的基础上,引入净室软件工程中状态盒的概念,定义了可信子集,提出了可信封装的工程方法,并证明通过安全机制对元件初态和输入进行可信封装,即可在元件可信子集通过可信验证的情况下,保证元件的动态可信性。这一结论提出了一种低成本、可基于现有元件进行改造的可信元件实现方法。论文对proftpd程序的可信封装进行了研究,基于操作系统的安全机制,实现了对一个简单的ftp服务器需求的可信封装方法。这一实现表明可信封装技术是可行的。在高安全级别操作系统的工程实现上,本论文分为安全功能和安全保障两个方面,讨论了高安全级别操作系统的工程实现方法。在安全功能上,论文分析了操作系统安全机制上的一些流行观点,并根据生产信息系统上应用流程相对固定的特点,让安全策略独立于应用,提出了操作系统引用监视器的透明实现方案,从而使安全操作系统可以保持对应用的标准POSIX系统调用接口。另外,针对一些应用自身存在的安全问题,论文用信息流通道的观点观察系统调用,提出了通道信息变换操作和通道重定向操作,这两个操作可以在完全透明的情况下,解决应用中的一些具体安全问题,降低应用向高安全级别操作系统移植的门槛。在安全保障上,论文从程序结构化、数据结构化和连接结构化三个层面来讨论高安全级别操作系统结构化的实现,并针对Linux操作系统的程序结构化,提出了通过可信计算机制和内核层次化改造与调用检查来加强系统结构化的方法,并讨论了系统的隐通道问题。综上所述,本论文从强制访问控制模型和可信计算两个角度讨论高安全级别操作系统实现的理论问题,并针对Linux操作系统提出了高安全级别操作系统工程实现的方法。论文以强制访问控制的形式化模型以及可信计算的形式化理论为基础,内容涉及强制访问控制模型、保密性的量化分析、可信传递的形式化模型、应用的可信封装、操作系统的透明安全机制和安全保障机制等多个方面,在多处对传统理论有所突破,并针对多级强制访控模型的下向信息流、可信计算的形似化描述、安全操作系统与现有系统的兼容性、Linux操作系统的结构化改造等传统理论和工程难题提出了自己的解决思路。