基于谓词抽象技术的访问控制策略安全性快速判定方法的研究

With customizable access conctrol system prevalent, dynamic configuration ability is required, which inevitably lead to dynamic access control policies and thereby may cause unknown secuity flaws. To fulfill dynamic adjustment, rapid safety determination method is necessary.The known method, which based on theorem prover requires manual induction and intervention, whereas model checking method faces the impact of states explosion, moreover both speed and efficiency of them are not practicable. Thereafter, based on predicate abstraction to deduct state space, we propose a rapid access control policy safety determination method, with the aid of model checking tool NuSMV, which converts safety analysis among original state machine model to an abstract model with less state. Based on that, orthogonal decompose access control policy to build a checking basis and refining the combination of test methods is introduced, by which makes the historical results of access control policy safety analysis reusable. Compared with the known methods, our method is expected to be faster, less manual intervention and competent to rapidly determine the safety of access control policies.

可定制访问系统的出现，要求提供对访问控制状态配置的可修改能力，这必然导致访问控制策略的动态调整进而影响其安全性。为满足这种动态调整的需求，对访问控制策略的安全性进行快速判定就变得非常必要。在目前使用的方法中，基于定理证明器的手段需要较多的人工干预和对证明方向的诱导，而基于模型检测的方法会面临状态空间爆炸的影响，在速度上和效率上均难以胜任。本项目针对模型检测方法中状态空间爆炸问题，提出一种谓词抽象来约简访问控制策略的状态空间，从而可在包含较少状态的抽象模型上分析安全性，并借助模型检测工具NuSMV进行抽象模型上安全属性的自动化验证。当抽象失效时，需要对抽象系统进行精化，因此进一步提出借助正交分解集合覆盖给定访问控制策略的组合精化检验方法，使得局部访问控制策略的安全性分析结果具有可复用性。该方法与传统方法相比，预期具有速度更快、自动化程度更高等优点，能够胜任访问控制策略安全性快速判定的要求。

可定制访问系统的出现，要求提供对访问控制状态配置的可修改能力，这必然导致访问控制策略的动态调整进而影响其安全性。为满足这种动态调整的需求，对访问控制策略的安全性进行快速判定就变得非常必要。在目前使用的方法中，基于定理证明器的手段需要较多的人工干预和对证明方向的诱导，而基于模型检测的方法会面临状态空间爆炸的影响，在速度上和效率上均难以胜任。本项目针对UCON模型及其模型检测方法中状态空间爆炸问题进行了系统的研究，分别研究了UCON访问控制模型的优化、UCON模型的形式化验证与测试、状态空间约简技术以及UCON模型的应用，取得了四个方面的突破：（1）提出一种基于RABC的UCON管理模型R-UCON：通过在UCON模型的基础上引入角色元素，并对权限进行划分，实现对权限的管理和委托以及对属性来源的管理；（2）提出一种基于PAT的使用控制模型的形式化规约与安全性分析方法：利用PAT的建模语言TCSP#建立了所有UCON核模型的规范，以及一般化UCON模型的规范机制，对复杂的使用会话场景，如并发、时间控制与非确定性也建立了一套规范机制。（3）提出一种基于多维度抽象和广度优先搜索空间划分的隐蔽信息流检测方法：基于多安全级系统中主体安全级的概念，引入了二维抽象的方法。该方法的优点在于，其抽象操作位于系统建模之前，可以使系统模型中的主体数得到有效约减之后再对系统建模，从而降低了对复杂模型的建模难度，且到达了抽象约减系统状态的目的；（4）提出一种克服状态空间爆炸的马尔可夫决策过程模型检测技术：围绕限界模型检测的三个核心问题，分别提出了有效的解决方案。这些方案不是传统限界模型检测技术的直接推广，而是一种全新的限界模型检测过程，特别是在终止判别标准的设计与限界模型检测算法方面，解决方案的思想完全异于传统限界检测技术。