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

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

项目编号： No.61300228

项目类型： 青年科学基金项目

立项/批准年度： 2014

项目学科： 自动化技术、计算机技术

项目作者： 刘志锋

作者单位： 江苏大学

项目金额： 23万元

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

中文关键词： 访问控制模型；状态空间爆炸；模型检测；抽象；形式化验证

英文摘要： 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.

英文关键词： access model；states explosion；model checking；abstraction；formal verification