The detection of covert information flow is a key problem in developing secure systems.State space explosion is the main obstacle to the detection of covert information flow identification through the state machine model.This paper proposed a two-dimensional abstract method for the subject in multi-level security system.Thereafter,it proposed a verification space divi-sion method based on breadth first searching strategy.Compared with the known similar algorithms,this method enlarged the division variables candidates and thereby easier to be implemented in practice.Experiment data shows that the combination of multi-dimensional abstract and verification space division method effectively reduces the scale of verification model,and miti-gates the state space explosion problem.%隐蔽信息流检测是开发可信计算机系统中的关键问题，而状态空间爆炸是基于状态机模型检测隐蔽信息流的主要障碍。提出一种多安全级系统中基于主体安全级的二维抽象方法，在此基础上设计了广度优先的搜索空间划分方法，使得划分变量的选取范围更大，扩展了搜索空间划分的应用范围，克服了深度优先划分方法中划分变量难以选取的问题。实验数据表明，结合抽象和搜索空间划分的方法有效降低了模型的验证规模，因此有效缓解了状态空间爆炸问题。
展开▼
