多安全等级信息系统的跨域行为安全性研究

目前可信计算已经成为世界信息领域的新潮流，对构建多安全等级信息系统有着重大指导意义。根据我国信息系统等级保护政策的要求，可信计算系统应满足跨域信息交互设计需求。然而，国内外对于可信计算体系安全性研究刚刚起步，对跨域需求缺乏足够的理论支持，这将严重制约我国信息系统等级安全保护工作的实施。.本课题将以可信计算平台为对象，研究多安全等级信息系统的跨域行为安全性问题。通过对可信计算平台不同部件间的信息流动与相互影响的刻画，提出一种面向可信特征属性与实现功能统一的系统行为描述方法；建立基于谓词抽象的具有安全属性的系统行为约简技术；同时构造基于可信跨域属性的信息流无干扰理论扩展模型，并探索模型的应用研究。基于以上研究，将初步建立可信计算平台体系安全性分析的理论，并建立实验系统。这将丰富和发展可信计算安全理论、推动我国等级保护工作的实施。.本项目组在该领域已经具有较好的研究基础，可以圆满完成项目研究。

当前，云计算、物联网、移动互联网等多种计算模式的迅猛发展推动了世界范围内网络信息系统的进一步建设高潮。同时，由于其巨大的商业与应用价值，这类系统的信息安全问题成为了学术领域与工业界关注的热点。可信计算作为一种工业界所能接受的安全基础技术，成为当前构建多安全等级网络信息系统、建立可信计算环境的重要技术途径。但是当前可信计算问题缺乏有效的理论支撑，以可信计算为技术核心的多级安全问题在信息安全共享上一直存在瓶颈。为此，本课题以可信计算为研究基本对象，在三年的时间里，探索了多安全等级信息系统的跨域行为安全性问题。围绕可信计算平台系统的行为建模问题、多级系安全行为分析中信息流无干扰语义理论模型扩展问题、以无干扰语义为核心的多级系统安全策略应用问题、以及相关实验系统的研制等4个主要研究方向，在行为建模方面，我们提出了一种可信计算平台信任链行为建模方法，验证了现有可信平台信任链的一类安全缺陷；设计了一个基于谓词抽象的可信系统复杂行为约简算法，与已知同类工作相比有较好的压缩比提升；在形式化方法方面，提出了一种基于Hoare逻辑的面向并行程序设计的无干扰语义模型，为并行程序的无干扰属性验证提供一种较为简便的验证方法；为了解决从抽象模型到安全策略的鸿沟问题，我们选取了一种符合无干扰语义的非集中式分布式控制策略(DIFC)为对象，发现了一个其在标签配置不合理所导致的隐蔽通道问题，并给出了相应的隐通道检测算法；发现了Flume系统文件系统的安全性问题，并给出了相应系统安全增强设计；除探讨理论模型外，我们还研究了代码层面的多级可信问题，提出了一种基于复杂网络的软件缺陷定位方法；针对可信系统功能冗余带来的安全问题，给出了一种代码级冗余定位方法；给出了一种可信环境下多级安全性指标评估方法，可有效针对安全性功能指标与非功能指标进行成分分析；在实验系统构造方面，我们结合UEFI技术与虚拟化技术，设计并实现了一个可信环境系统行为安全性分析数据采集实验系统；基于虚拟化系统，设计了一个基于DIFC的行为监控实验系统。通过以上研究，初步形成了一套从行为建模到安全性分析方法，从安全策略设计到安全系统分析设计，从抽象模型安全到代码级安全评估的研究体系。我们的研究工作基本达到了最初课题立项的设计目标，并在无干扰语义策略的实际应用方面建立了较为实际的应用系统。这将丰富和发展可信计算理论研究，推动我国信息安全建设。