Scalable automated symbolic analysis of administrative role-based access control policies by SMT solving¹

Issue title: STM'10

Guest editors: Gilles BartheGuest Editor, Jorge CuellarGuest Editor, Javier LopezGuest Editor and Alexander PretschnerGuest Editor

Article type: Research Article

Authors: Armando, Alessandro^{a; b} | Ranise, Silvio^{b; *}

Affiliations: [a] DIST, Università degli Studi di Genova, Genova, Italy | [b] Security and Trust Unit, FBK, Trento, Italy

Correspondence: [*] Corresponding author: Silvio Ranise, Povo-Via Sommarive, 18, I-38123 Italy. Tel.: +39 0461 314 192; Fax: +39 0461 302 040; E-mail: ranise@fbk.eu.

Note: [1] Preliminary versions of some parts of this paper appear in [2,3,5].

Abstract: 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.

Keywords: Decidability of the unbounded user–role reachability problem, automated analysis, infinite state model checking, automated theorem proving, satisfiability modulo theories

DOI: 10.3233/JCS-2012-0461

Journal: Journal of Computer Security, vol. 20, no. 4, pp. 309-352, 2012