Abstract: The attribute-based access control has bean used more and more widely, because it controls users and process to access system resources more accurate. However, it is necessary to ensure the correctness of policy, which can prevent illegal access to system resources. So an effective method must be developed to verify policies. In this paper, a method based on model checking is put forward, which can be used to check the coverage and completeness of rules. The main idea is to regard rule set and its variation as models, and then describe the properties with modal logic formulas. It uses model checking algorithm to check the logic formulas on models, which can help discover the fault of the model and deletion of rules. At the same time it analyzes the completeness of properties. Finally, it will call model checking algorithm again to verify fixed properties on fixed models. The case study shows that the coverage checking can find wrong rules effectively and the completeness checking can identify the integrity of rules. Since methods are based on model checking, they have some advantages of model checking such as automation, easy operation, reliable result et al.

Key words: attribute based access control, model checking, coverage verification, completeness verification

摘要： 基于属性的访问控制策略以更精确的粒度控制着用户或进程对系统资源的访问，因此获得了越来越广泛的应用。然而必须保证所制定策略的正确性，才能防止对系统资源的非法访问，因此必须研制出一种有效的方法来验证策略的正确性。基于模型检测技术提出了一种访问控制策略的覆盖性与完整性验证方法。主要思想是将覆盖性与完整性验证归约为模型检测问题。将规则集与其变异分别视为模型，以模态逻辑公式描述其性质。调用模型检测算法，分别在模型及其变异模型上检测性质，生成反例报告以确定模型故障点和模型规则缺失点，同时分析性质本身的完善性，最终以完善后的模型和性质再次调用模型检测算法来完成覆盖性与完整性验证。实例分析结果表明覆盖性验证能够有效发现错误的规则，完整性验证能够有效识别验证规则的完备性。方法依托于模型检测工具完成，具有自动化程度高、易操作、测试结果可靠的特点。

关键词: 基于属性的访问控制, 模型检测, 覆盖性验证, 完整性验证