论文部分内容阅读
隐蔽信息流检测是开发可信计算机系统中的关键问题,而状态空间爆炸是基于状态机模型检测隐蔽信息流的主要障碍。提出一种多安全级系统中基于主体安全级的二维抽象方法,在此基础上设计了广度优先的搜索空间划分方法,使得划分变量的选取范围更大,扩展了搜索空间划分的应用范围,克服了深度优先划分方法中划分变量难以选取的问题。实验数据表明,结合抽象和搜索空间划分的方法有效降低了模型的验证规模,因此有效缓解了状态空间爆炸问题。