摘要
隐蔽信息流分析是开发高等级可信计算机系统必须面对的问题.以Petri网作为开发安全系统的形式化建模工具,给出Petri网中隐蔽信息流存在的判定条件.提出该条件成立的两种网结构,进而可以在语法层次上预先判断隐蔽信息流的存在性,并使由此类结构引起的隐蔽信息流在系统的设计阶段得以避免.开发了一种基于Petri网可达图的隐蔽信息流存在性判定算法,算法遵循无干扰方法的思想,但是避免了无干扰方法中等价状态的区分和展开定理的使用.另外,算法采用深度优先搜索的策略,避免了Petri网全局可达图的构造.对复杂的安全系统,分析了子系统的各种组合运算对隐蔽信息流存在性的影响,降低了大规模系统分析的复杂度.
The covert information flow analysis is a key problem in developing high secure systems. In this paper Petri net is used to model the dynamic behavior of the secure system. A condition characterizing the existence of the covert information flow in Petri net is proposed, and two kinds of net structures are proposed for judging the condition such that the covert information flow could be searched in the structure level. Based on the reachable graph of Petri nets, an algorithm for deciding the condition is proposed, and it follows the idea of noninterference. However, it avoids using the unwinding theorem and distinguishing the equivalent states. In addition, the algorithm is based on the depth first search strategy such that it avoids constructing the global reachable graph. For complex secure systems, we analyze how the composition operating of Petri nets influences the covert information flow such that the complexity of analyzing the large system is reduced.
出处
《计算机学报》
EI
CSCD
北大核心
2012年第8期1688-1699,共12页
Chinese Journal of Computers
基金
国家自然科学基金青年基金(61003288)
中德合作交流基金(6111130184)
江苏省自然科学基金(BK2010192)
教育部博士点基金(20093227110005)资助~~
关键词
隐蔽信息流
无干扰
PETRI网
组合
展开定理
covert information flow
noninterference
Petri net
composition
unwinding theorem
