基于模型检测的信息流策略安全性分析

• 作者: 杨政 殷红武 邵婧 陈左宁
• 来源期刊: 计算机应用研究
• 关键词: 策略安全性分析 分布式信息流控制 模型检测 计算树逻辑 Kripke 结构
• 年，卷（期）: 2016,（8）
• 所属期刊栏目: 信息安全技术
• 页码范围: 2429-2432
• 页数: 4页
• 分类号: TP309.2
• 语种: 中文
• DOI: 10.3969/j.issn.1001-3695.2016.08.042

摘要

分布式信息流控制是增强系统安全的一种有效方法，但其灵活性也增加了策略管理和分析的复杂性。策略的安全性分析判定系统的所有可达状态是否都能保持特定的安全属性，可以验证策略是否一致完备地满足安全需求。形式化定义了基于 Kripke 结构和计算树时序逻辑的信息流策略安全性分析问题，验证信息流允许、禁止和授权管理三类信息流安全目标，提出了分支限界和模型检测两种策略验证算法。实验结果表明，算法可有效验证分布式信息流控制系统是否满足特定安全需求，提高了分布式信息流控制的可用性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈左宁		40	174	7.0	12.0
3	邵婧		13	85	5.0	8.0
7	殷红武		19	28	4.0	4.0
8	杨政		3	3	1.0	1.0