Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving
Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving
复制标题
通过 SMT 解决方案对基于管理角色的访问控制策略进行可扩展的自动符号分析
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
Silvio Ranise
中科院分区：
文献类型：
--
作者：
A. Armando;Silvio Ranise
基于角色的访问控制ARBAC是管理访问控制策略的最广泛的框架之一。已经提出了几种自动分析技术，以帮助维护理想的安全属性的ARBAC政策。可用的分析技术的主要限制之一是，用户的集合是有界的。在本文中，我们提出了一个象征性的框架，以克服这一限制。我们设计了一种自动化分析技术，可以处理有界和无界数量的用户通过适应最近的方法，使用一阶逻辑和SMT求解技术的无限状态系统的符号模型检查。广泛的实验评估证实了所提出的技术的可扩展性。
Administrative Role Based Access Control ARBAC is one of the most widespread framework for the management of access-control policies. Several automated analysis techniques have been proposed to help maintaining desirable security properties of ARBAC policies. One of the main limitation of available analysis techniques is that the set of users is bounded. In this paper, we propose a symbolic framework to overcome this limitation. We design an automated analysis technique that can handle both a bounded and an unbounded number of users by adapting recent methods for the symbolic model checking of infinite state systems that use first-order logic and SMT solving techniques. An extensive experimental evaluation confirms the scalability of the proposed technique.