Mohawk: Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies
Mohawk: Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies
复制标题
Mohawk：用于验证访问控制策略的抽象细化和界限估计
DOI：
10.1145/2445566.2445570
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
S. Chapin
中科院分区：
文献类型：
--
作者：
Karthick Jayaraman;Mahesh V. Tripunitara;Vijay Ganesh;M. Rinard;S. Chapin
验证访问控制系统是否保持所需的安全属性被认为是安全领域的一个重要问题。企业访问控制系统已经发展到可以保护数以万计的资源，并且需要进行相应的扩展验证。我们提出了有界模型检查器的抽象细化和边界估计技术，以自动查找基于管理角色的访问控制（ARBAC）安全策略中的错误。 ARBAC 是第一个也是最全面的基于角色的访问控制 (RBAC) 系统的管理方案。在我们方法的抽象细化部分中，我们识别并丢弃不太可能与验证问题相关的角色（抽象步骤）。然后，我们逐步恢复这些抽象角色（细化步骤）。在我们方法的边界估计部分，我们通过识别角色和状态更改规则之间的关系，降低了最坏情况下可达性图直径的估计。我们的技术相互补充，并与传统的有界模型检查一起使用。我们的方法是健全和完整的：当且仅当错误存在时才发现错误。我们已经在名为 Mohawk 的访问控制策略分析工具中实施了我们的技术。我们凭经验证明莫霍克可以很好地适应现实政策，并与之前的工具进行比较。
Verifying that access-control systems maintain desired security properties is recognized as an important problem in security. Enterprise access-control systems have grown to protect tens of thousands of resources, and there is a need for verification to scale commensurately. We present techniques for abstraction-refinement and bound-estimation for bounded model checkers to automatically find errors in Administrative Role-Based Access Control (ARBAC) security policies. ARBAC is the first and most comprehensive administrative scheme for Role-Based Access Control (RBAC) systems. In the abstraction-refinement portion of our approach, we identify and discard roles that are unlikely to be relevant to the verification question (the abstraction step). We then restore such abstracted roles incrementally (the refinement steps). In the bound-estimation portion of our approach, we lower the estimate of the diameter of the reachability graph from the worst-case by recognizing relationships between roles and state-change rules. Our techniques complement one another, and are used with conventional bounded model checking. Our approach is sound and complete: an error is found if and only if it exists. We have implemented our technique in an access-control policy analysis tool called Mohawk. We show empirically that Mohawk scales well to realistic policies, and provide a comparison with prior tools.