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

Security analysis of information flow policy on model checking

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

Decentralized information flow control（ DIFC ） is an effective method for enhancing security of systems, but its fle- xibility also increases the complexity of policy analysis and management. Security analysis of policy decides whether all the reachable states of the system keep some security property, and validates whether the policies satisfy the security requirements consistently and completely. Based on Kripke structure and computation tree logic, this paper proposed security analysis prob- lem for DIFC （SAP-DIFC） formally. It verified three information flow goals, like information flow allow/forbidden and author- ization management. It proposed two policy Verification methods, branch and bound method, and model checking. The experi- mental results show that the algorithms effectively verify whether the DIFC system satisfies the security requirements, and im- prove the usability of DIFC.