论文研究基于模型检测的信息流策略安全性分析.pdf

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