Security & Trust


Automated Symbolic Analysis of Security Policies

ASASP is a tool for the automated safety analysis of administrative access control policies in (extensions of) the Role-Based Access Control (RBAC) model. The goal of the tool is to establish if untrusted users can get permissions to access sensitive resources. ASASP is capable of performing an analysis that is parametric in the number of users, i.e. it certifies safety with respect to a finite but unknown number of users. ASASP is also capable of taking into account attribute-based assignments of roles to users and temporal constraints on the RBAC policies.

Role-Based Access Control (RBAC) policies have been widely adopted by enterprise and complex organizations around the world. Because of their size and complexity, automated techniques for their security analysis are crucial for design and maintenance. In particular, the definition of administrative domains by means of attributes restrieved from user profiles makes the RBAC model easier to use in real scenarios but complicates the development of security analysis techniques, that should be able to modularly reason about a wide range of attribute domains. Another complication is the use of contextual information, such as time and location, in the expression of the authorization conditions of RBAC policies.

The prototype tool ASASP (short for Automated Symbolic Analysis of Security Policies) implements a symbolic backward reachability analysis to solve user-role reachability problems, i.e. it is capable of establishing if there exists a coalition of administrators capable of giving a certain set of priviliges to a certain (untrusted) user. ASASP uses the model checker MCMT to mechanize the backward reachability procedure and integrates several herustic to alleviate the state-space explosion problem while providing a flexibile framework to express various extensions of RBAC policies encompassing attributes and contextual information. Despite is flexibility, ASASP is competitive with other tools for the analysis of administrative RBAC policies such as Mohawk and VAC or the tool by Uzun et al. for the analysis of temporal RBAC policies. To the best of our knowledge, ASASP is the only tool capable of handling user-role assignments based on attributes.

Related Publications

  • Silvio Ranise, Tuan Anh Truong, Alessandro Armando
    Scalable and Precise Automated Analysis of Administrative Temporal Role-Based Access Control
    In: 18th ACM Symposium on Access Control Models and Technologies (SACMAT 2014) (DOI, news)
  • Silvio Ranise, Tuan Anh Truong
    Incremental Analysis of Evolving Administrative Role Based Access Control Policies
    In: 28th Annual IFIP WG 11.3 Working Conference on Data and Applications Security and Privacy (DBSec 2014) (DOI)
  • Alessandro Armando, Silvio Ranise
    Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving
    In: Journal of Computer Security (JCS), vol. 20, no. 4, pp. 309-352 (DOI)
  • Silvio Ranise, Tuan Anh Truong, Alessandro Armando
    Boosting Model Checking to Analyse Large ARBAC Policies
    In: 8th International Workshop on Security and Trust Management (STM 2012) (DOI)
  • Francesco Alberti, Alessandro Armando, Silvio Ranise
    Efficient Symbolic Automated Analysis of Administrative Attribute-based RBAC-Policies
    In: 6th ACM Symposium on Information, Computer and Communications Security (ASIACCS '11) (DOI)
  • Francesco Alberti, Alessandro Armando, Silvio Ranise
    ASASP: Automated Symbolic Analysis of Security Policies
    In: 23rd International Conference on Automated Deduction (CADE 2011) (DOI)
  • Alessandro Armando, Silvio Ranise
    Automated Symbolic Analysis of ARBAC Policies
    In: 6th International Workshop on Security and Trust Management (STM 2010) (DOI)