Abstract
The administration of access control policies is a task of paramount importance for distributed systems. A crucial analysis problem is to foresee if a set of administrators can give a user an access permission. We consider this analysis problem in the context of the Administrative Role-Based Access Control (ARBAC), one of the most widespread administrative models. Given the difficulty of taking into account the effect of all possible administrative actions, automated analysis techniques are needed. In this paper, we describe how a model checker can scale up to handle very large ARBAC policies while ensuring completeness. An extensive experimentation shows that an implementation of our techniques performs significantly better than Mohawk, a recently proposed tool that has become the reference for finding errors in ARBAC policies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alberti, F., Armando, A., Ranise, S.: ASASP: Automated Symbolic Analysis of Security Policies. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 26–33. Springer, Heidelberg (2011)
Alberti, F., Armando, A., Ranise, S.: Efficient Symbolic Automated Analysis of Administrative Role Based Access Control Policies. In: ASIACCS, ACM Pr. (2011)
Armando, A., Ranise, S.: Automated Symbolic Analysis of ARBAC-Policies. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) STM 2010. LNCS, vol. 6710, pp. 17–34. Springer, Heidelberg (2011)
Crampton, J.: Understanding and developing role-based administrative models. In: Proc. 12th CCS, pp. 158–167. ACM Press (2005)
Ferrara, A.L., Madhusudan, P., Parlato, G.: Security Analysis of Access Control Policies through Program Verification. In: CSF (2012)
Ghilardi, S., Ranise, S.: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis. In: LMCS, vol. 6(4) (2010)
Gofman, M.I., Luo, R., Solomon, A.C., Zhang, Y., Yang, P., Stoller, S.D.: Rbac-Pat: A policy analysis tool for role based access control. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 46–49. Springer, Heidelberg (2009)
Jayaraman, K., Ganesh, V., Tripunitara, M., Rinard, M., Chapin, S.: Automatic Error Finding for Access-Control Policies. In: CCS, ACM (2011)
Jha, S., Li, N., Tripunitara, M.V., Wang, Q., Winsborough, H.: Towards formal verification of role-based access control policies. IEEE TDSC 5(4), 242–255 (2008)
Li, N., Tripunitara, M.V.: Security analysis in role-based access control. ACM TISSEC 9(4), 391–420 (2006)
Sandhu, R., Coyne, E., Feinstein, H., Youmann, C.: Role-Based Access Control Models. IEEE Computer 2(29), 38–47 (1996)
Sasturkar, A., Yang, P., Stoller, S.D., Ramakrishnan, C.R.: Policy analysis for administrative role based access control. In: CSF. IEEE Press (July 2006)
Stoller, S.D., Yang, P., Ramakrishnan, C.R., Gofman, M.I.: Efficient policy analysis for administrative role based access control. In: CCS. ACM Press (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ranise, S., Truong, A., Armando, A. (2013). Boosting Model Checking to Analyse Large ARBAC Policies. In: Jøsang, A., Samarati, P., Petrocchi, M. (eds) Security and Trust Management. STM 2012. Lecture Notes in Computer Science, vol 7783. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38004-4_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-38004-4_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38003-7
Online ISBN: 978-3-642-38004-4
eBook Packages: Computer ScienceComputer Science (R0)