面向不同信任域网络安全隔离交换的访问控制策略形式化技术研究

不同信任域网络安全隔离交换技术在电子政务等行业有着广泛的应用需求，但是对于其安全机制的理论研究远远不能达到用户期望，已严重制约了其实际应用和部署。本课题指出，该技术虽然采用了独特的信息交换方式，但是其本质上仍然属于一种网络访问控制技术，其安全性主要取决于所能实现的访问控制策略。因此，课题系统地研究了其访问控制策略的建模、描述，分析和验证的形式化技术。针对不同信任域网络安全隔离交换系统的特定应用需求和安全特征，课题首先采用RBAC模型对其访问控制机制进行抽象建模，然后设计实现了基于CIM-SPL的RBAC访问控制策略描述语言，进而提出支持多约束条件的策略代数来分析访问控制策略的合成，最后发展建立了形式化验证方法对其RBAC策略安全性分析问题进行建模求解。课题成果将对该类技术的安全性评估、设计开发和应用部署提供关键的理论支持和实际指导，并对促进我国高安全等级网络信息化建设具有直接的应用价值。

本项目针对不同信任域网络安全隔离系统的特定应用需求和安全特征，系统地研究了其访问控制策略的形式化技术。项目重点围绕访问控制机制和策略的形式化建模与描述，系统实现机制，跨域访问控制策略合成以及策略系统安全性分析与验证等四个方面展开工作，全部达到了项目预订目标并进行了扩展性研究。. 项目首先将网络强制访问控制技术与网络安全隔离技术相结合，对跨信任域隔离交换的访问控制机制进行建模，提出了基于BLP的网络访问控制模型N-BLP。在此基础上，对DMTF国际标准化组织提出的分布式网络管理策略语言CIM-SPL进行了扩展，提出并实现了基于CIM-SPL的RBAC策略语言，并开发了一个基于CIM-SPL的RBAC访问控制系统框架。. 项目将上述建模理论及策略描述成果应用到系统的设计开发中。采用基于策略的访问控制思想，对原网络安全隔离交换系统的访问控制机制进行了形式化设计，突破了多项实现关键技术。为进一步提高网络访问控制系统的安全性，项目系统地研究了由于网络隐蔽信道带来的信息泄露问题，提高了访问控制机制的安全性。相关成果已在网络安全隔离与信息交换系统样机中得到实现。该系统已在电子政务网络中得到应用推广。. 在跨域访问控制策略合成及冲突解决方面，针对多域间基于角色的访问控制（RBAC）策略合成问题，提出了基于权限的RBAC策略合成方法；针对多域间RBAC策略合成冲突问题，提出了基于角色映射的策略冲突检测与解决方法。针对多域间基于ABAC的访问控制策略合成问题，提出了一种基于二进制序列集合的策略合成代数，显著提高了合成效率，具有良好的实际应用前景。. 针对跨域信息交换访问控制策略合成结果的复杂性，引入了树图、语义基和多级网格等数据可视化分析技术，提出了多种对不同信任域网络访问控制策略合成结果分析方法，有效地提高对多域策略合成的管理能力。在RBAC系统动态安全性验证方面。项目定义了角色继承关系和用户角色分配关系的安全性分析问题(RRA-SAP)和(URA-SAP)，采用模型检测等形式化技术对多域访问控制策略的安全性进行了自动化分析验证。. 通过本项目研究工作，已发表国内外学术论文15篇，培养硕士研究生（毕业）10人。获得国家发明专利4项，申请发明专利3项。基于部分研究成果开发的系统样机于获得国家保密局涉密信息系统产品检测证书，并已推广应用。