基于多维抽象和搜索空间划分的隐蔽信息流检测方法

摘要

隐蔽信息流检测是开发高等级安全系统必须解决的关键问题，也是证明系统可信性的重要组成部分。隐蔽信息流存在的根本原因是，系统的安全模型不能与安全策略完全一致，从而导致涉密信息的外泄。目前，在已知的隐蔽信息流检测方法中，较为常用的是基于状态机与模型检测工具相结合的方法，但是状态空间爆炸是此类方法面临的主要问题。
　　针对模型状态空间爆炸问题，本文提出结合二维抽象和广度优先搜索空间划分的方法来缓解该问题。其中二维抽象方法以多安全级系统中主体的密级和类别集合为依据，分别对主体进行抽象操作，从而约减模型的状态空间，并拓展了搜索空间划分方法的应用范围。
　　本文的主要工作包括以下几点:(1)在多安全级系统中，提出了一种基于主体安全级的二维抽象方法，该方法分别以安全级中的密级和类别集合作为抽象参数，对原始模型中的主体进行分类划分，然后取两个划分的交叉划分，将交叉划分中的每一个集合元素作为一个抽象主体集合，达到约减状态空间的目的;(2)设计了一种广度优先的搜索空间划分方法，在已有方法的基础上，通过改变划分参数的定义形式，使得划分变量的选取更具可操作性，同时拓展了搜索空间划分的应用范围;(3)在理论分析的基础上，设计了实验模型，并验证了结合二维抽象和搜索空间划分方法在缓解模型状态空间爆炸问题上的有效性。

目录

声明

摘要

第一章 绪论

1．1 研究背景和意义

1．2 国内外研究现状

1．3 论文的主要工作及创新

1．4 论文的组织结构

第二章 抽象和搜索空间划分的相关理论概述

2．1 抽象

2．1．1 抽象理论

2．1．2 抽象方法

2．1．3 抽象方法对比

2．2 搜索空间划分

2．2．1 线性时态逻辑LTL

2．2．2 搜索空间的划分理论

2．3 可行性分析

2．4 本章小结

第三章 基于二维抽象的隐蔽信息流检测方法

3．1 二维抽象方法

3．1．1 安全级的数学模型

3．1．2 抽象方法

3．1．3 关于主体抽象的讨论

3．2 广度优先搜索空间划分

3．2．1 理论依据

3．2．2 工作原理

3．3 隐蔽信息流检测方法

3．4 本章小结

第四章 基于抽象和搜索空间划分的实验设计与实现

4．1 隐通道

4．2 实验体系结构

4．2．1 实验流程

4．2．2 整体模型设计

4．3 抽象与划分模块的设计与实现

4．3．1 抽象模块

4．3．2 划分模块

4．4 本章小结

第五章 实验结果与分析

5．1 可达状态与状态迁移

5．2 固定客体数实验对比

5．2．1 抽象结果对比

5．2．2 划分结果对比

5．3 固定主体数实验对比

5．3．1 抽象结果对比

5．3．2 划分结果对比

5．4 抽象对比实验

5．5 本章小结

第六章 总结与展望

6．1 工作总结

6．2 研究展望

参考文献

致谢

在读期间发表的论文