TY - GEN
T1 - Vac - Verifier of administrative role-based access control policies
AU - Ferrara, Anna Lisa
AU - Madhusudan, P.
AU - Nguyen, Truc L.
AU - Parlato, Gennaro
PY - 2014
Y1 - 2014
N2 - In this paper we present Vac, an automatic tool for verifying security properties of administrative Role-based Access Control (RBAC). RBAC has become an increasingly popular access control model, particularly suitable for large organizations, and it is implemented in several software. Automatic security analysis of administrative RBAC systems is recognized as an important problem, as an analysis tool can help designers check whether their policies meet expected security properties. Vac converts administrative RBAC policies to imperative programs that simulate the policies both precisely and abstractly and supports several automatic verification back-ends to analyze the resulting programs. In this paper, we describe the architecture of Vac and overview the analysis techniques that have been implemented in the tool. We also report on experiments with several benchmarks from the literature.
AB - In this paper we present Vac, an automatic tool for verifying security properties of administrative Role-based Access Control (RBAC). RBAC has become an increasingly popular access control model, particularly suitable for large organizations, and it is implemented in several software. Automatic security analysis of administrative RBAC systems is recognized as an important problem, as an analysis tool can help designers check whether their policies meet expected security properties. Vac converts administrative RBAC policies to imperative programs that simulate the policies both precisely and abstractly and supports several automatic verification back-ends to analyze the resulting programs. In this paper, we describe the architecture of Vac and overview the analysis techniques that have been implemented in the tool. We also report on experiments with several benchmarks from the literature.
UR - http://www.scopus.com/inward/record.url?scp=84904807144&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84904807144&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-08867-9_12
DO - 10.1007/978-3-319-08867-9_12
M3 - Conference contribution
AN - SCOPUS:84904807144
SN - 9783319088662
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 184
EP - 191
BT - Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings
PB - Springer
T2 - 26th International Conference on Computer Aided Verification, CAV 2014 - Held as Part of the Vienna Summer of Logic, VSL 2014
Y2 - 18 July 2014 through 22 July 2014
ER -