research-article

Mohawk: Abstraction-Refinement and Bound-Estimation for Verifying Access Control Policies

Authors:

Karthick Jayaraman,

Mahesh Tripunitara,

Steve ChapinAuthors Info & Claims

ACM Transactions on Information and System Security (TISSEC), Volume 15, Issue 4

Article No.: 18, Pages 1 - 28

https://doi.org/10.1145/2445566.2445570

Published: 01 April 2013 Publication History

Abstract

Verifying that access-control systems maintain desired security properties is recognized as an important problem in security. Enterprise access-control systems have grown to protect tens of thousands of resources, and there is a need for verification to scale commensurately. We present techniques for abstraction-refinement and bound-estimation for bounded model checkers to automatically find errors in Administrative Role-Based Access Control (ARBAC) security policies. ARBAC is the first and most comprehensive administrative scheme for Role-Based Access Control (RBAC) systems. In the abstraction-refinement portion of our approach, we identify and discard roles that are unlikely to be relevant to the verification question (the abstraction step). We then restore such abstracted roles incrementally (the refinement steps). In the bound-estimation portion of our approach, we lower the estimate of the diameter of the reachability graph from the worst-case by recognizing relationships between roles and state-change rules. Our techniques complement one another, and are used with conventional bounded model checking. Our approach is sound and complete: an error is found if and only if it exists. We have implemented our technique in an access-control policy analysis tool called Mohawk. We show empirically that Mohawk scales well to realistic policies, and provide a comparison with prior tools.

References

[1]

Ammann, P. and Sandhu, R. 1991. Safety analysis for the extended schematic protection model. In Proceedings of the IEEE Symposium on Security and Privacy. 87--97.

[2]

Aveksa. 2012. What is business-driven identity and access management? http://www.aveksa.com/ what-we-do/What-Is-Business-Driven-Identity-and-Access-Management.cfm.

[3]

Ball, T. and Rajamani, S. K. 2002. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’02). ACM, New York, 1--3.

Digital Library

[4]

Budd, T. A. 1983. Safety in grammatical protection systems. Int. J. Paral. Prog. 12, 6, 413--431.

[5]

Clarke, E., Biere, A., Raimi, R., and Zhu, Y. 2001. Bounded model checking using satisfiability solving. Form. Methods Syst. Des. 19, 1, 7--34.

Digital Library

[6]

Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2003. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 5, 752--794.

Digital Library

[7]

Clarke, E., Kroening, D., Ouaknine, J., and Strichman, O. 2005. Computational challenges in bounded model checking. Softw. Tools Tech. Trans. 7, 2, 174--183.

Digital Library

[8]

Clarke, E. M., Grumberg, O., and Peled, D. A. 1999. Model Checking. The MIT Press.

Digital Library

[9]

Crampton, J. and Loizou, G. 2003. Administrative scope: A foundation for role-based administrative models. ACM Trans. Inf. Syst. Secur. 6, 2, 201--231.

Digital Library

[10]

Ferraiolo, D. F., Kuhn, D. R., and Chandramouli, R. 2003. Role-Based Access Control. Artech House, Inc., Norwood, MA.

Digital Library

[11]

Ferrara, A. L., Madhusudan, P., and Parlato, G. 2012. Security analysis of access control through program verification. In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF’12). IEEE Computer Society, Cambridge, MA.

Digital Library

[12]

Fisler, K., Krishnamurthi, S., Meyerovich, L. A., and Tschantz, M. C. 2005. Verification and change-impact analysis of access-control policies. In Proceedings of the 27th International Conference on Software Engineering (ICSE’05). ACM, New York, 196--205.

Digital Library

[13]

Ganesh, V. and Dill, D. L. 2007. A decision procedure for bitvectors and arrays. In Proceedins of the 19th International Conference on Computer-Aided Verification. Lecture Notes in Computer Science, Springer, Berlin, 519--531.

Digital Library

[14]

Gofman, M. I., Luo, R., Solomon, A. C., Zhang, Y., Yang, P., and Stoller, S. D. 2009. Rbac-pat: A policy analysis tool for role based access control. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 5505, Springer-Verlag, 46--49.

Digital Library

[15]

Gofman, M. I., Luo, R., and Yang, P. 2010. User-role reachability analysis of evolving administrative role based access control. In Proceedings of the 15th European Conference on Research in Computer Security (ESORICS’10). Springer-Verlag, Berlin, 455--471.

Digital Library

[16]

Graham, G. S. and Denning, P. J. 1972. Protection --- Principles and practice. In Proceedings of the AFIPS Spring Joint Computer Conference. Vol. 40, AFIPS Press, 417--429.

Digital Library

[17]

Harrison, M. A. and Ruzzo, W. L. 1978. Monotonic protection systems. In Proceedings of the Conference on Foundations of Secure Computation. 461--471.

[18]

Harrison, M. A., Ruzzo, W. L., and Ullman, J. D. 1975. On protection in operating systems. In Proceedings of the 5th ACM Symposium on Operating Systems Principles (SOSP’75). ACM, New York, 14--24.

Digital Library

[19]

Hu, H. and Ahn, G. 2008. Enabling verification and conformance testing for access control model. In Proceedings of the 13th ACM Symposium on Access Control Models and Technologies (SAC’08). ACM, New York, 195--204.

Digital Library

[20]

Hu, V. C., Kuhn, D. R., and Xie, T. 2008. Property verification for generic access control models. In Proceedings of the 2008 IEEE/IFIP International Conference on Embedded and Ubiquitous Computing. IEEE Computer Society, Los Alamitos, CA, 243--250.

Digital Library

[21]

Hughes, G. and Bultan, T. 2008. Automated verification of access control policies using a sat solver. Int. J. Softw. Tools Technol. Transf. 10, 6, 503--520.

Digital Library

[22]

Jayaramam, K. 2012. Mohawk -- Automatic Verification of Access-Control Policies. http://code.google.com/p/mohawk/.

[23]

Jayaraman, K., Ganesh, V., Tripunitara, M., Rinard, M., and Chapin, S. 2011. Automatic error finding in access-control policies. In Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS’11). ACM, New York, 163--174.

Digital Library

[24]

Jayaraman, K., Ganesh, V., Tripunitara, M., Rinard, M. C., and Chapin, S. J. 2012. Real-world case studies of using ARBAC to enforce separation-of-duty constraints. http://kjayaram.mysite.syr.edu/mohawk/casestudy.pdf.

[25]

Jha, S. and Reps, T. W. 2004. Model Checking SPKI/SDSI. J. Comput. Sec. 12, 3--4, 317--353.

Digital Library

[26]

Jha, S., Schwoon, S., Wang, H., and Reps, T. 2006. Weighted Pushdown Systems and Trust-Management Systems. In Proceedings of TACAS. Springer-Verlag, Berlin.

Digital Library

[27]

Jha, S., Li, N., Tripunitara, M., Wang, Q., and Winsborough, W. 2008. Towards formal verification of role-based access control policies. IEEE Trans. Dependable Secur. Comput. 5, 4, 242--255.

Digital Library

[28]

Jones, A. K., Lipton, R. J., and Snyder, L. 1976. A linear time algorithm for deciding security. In Proceedings of the 17th Annual Symposium on Foundations of Computer Science (SFCS’76). IEEE Computer Society, Washington, DC, 33--41.

Digital Library

[29]

Kern, A. 2002. Advanced features for enterprise-wide role-based access control. In Proceedings of the 18th Annual Computer Security Applications Conference (ACSAC’02). IEEE Computer Society, Washington, DC, 333.

Digital Library

[30]

Kolovski, V., Hendler, J., and Parsia, B. 2007. Analyzing web access control policies. In Proceedings of the 16th International Conference on World Wide Web (WWW’07). ACM, New York, 677--686.

Digital Library

[31]

Kroening, D. 2006. Computing over-approximations with bounded model checking. Electron. Notes Theor. Comput. Sci. 144, 79--92.

Digital Library

[32]

Li, N. and Tripunitara, M. V. 2004. Security analysis in role-based access control. In Proceedings of the 9th ACM Symposium on Access Control Models and Technologies (SACMAT’04). ACM, New York, 126--135.

Digital Library

[33]

Li, N. and Tripunitara, M. V. 2006. Security analysis in role-based access control. ACM Trans. Inf. Syst. Secur. 9, 4, 391--420.

Digital Library

[34]

Li, N., Mitchell, J. C., and Winsborough, W. H. 2005. Beyond proof-of-compliance: Security analysis in trust management. J. ACM 52, 3, 474--514.

Digital Library

[35]

Martin, E. and Xie, T. 2007. A fault model and mutation testing of access control policies. In Proceedings of the 16th International Conference on World Wide Web (WWW’07). ACM, New York, 667--676.

Digital Library

[36]

Motwani, R., Panigrahy, R., Saraswat, V., and Ventkatasubramanian, S. 2000. On the decidability of accessibility problems (extended abstract). In Proceedings of the 32nd Annual ACM Symposium on Theory of Computing (STOC’09). ACM, New York, 306--315.

Digital Library

[37]

NuSMV. 2012. http://nusmv.irst.itc.it/.

[38]

Rao, P., Lin, D., and Bertino, E. 2007. XACML function annotations. In Proceedings of the 8th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY’07). IEEE Computer Society, Washington, DC, 178--182.

Digital Library

[39]

SailPoint. 2012. Policy enforcement. http://www.sailpoint.com/products/identity-iq/compliance-manager/policy-enforcement.php.

[40]

Saltzer, J. H. and Schroeder, M. D. 1975. The protection of information in computer systems. Proc. IEEE.

[41]

Sandhu, R., Bhamidipati, V., and Munawer, Q. 1999. The ARBAC97 model for role-based administration of roles. ACM Trans. Inf. Syst. Secur. 2, 1, 105--135.

Digital Library

[42]

Sandhu, R. S. 1992. The typed access matrix model. In Proceedings of the IEEE Symposium on Research in Security and Privacy. 122--136.

Digital Library

[43]

Sandhu, R. S., Coyne, E. J., Feinstein, H. L., and Youman, C. E. 1996. Role-based access control models. IEEE Computer 29, 2, 38--47.

Digital Library

[44]

Sasturkar, A., Yang, P., Stoller, S. D., and Ramakrishnan, C. 2006. Policy analysis for administrative role based access control. In Proceedings of the 19th Computer Security Foundations Workshop. IEEE Computer Society Press.

Digital Library

[45]

Sasturkar, A., Yang, P., Stoller, S. D., and Ramakrishnan, C. 2011. Policy analysis for administrative role-based access control. Theoret. Comput. Sci. 412, 44, 6208--6234.

Digital Library

[46]

Schaad, A., Moffett, J., and Jacob, J. 2001. The role-based access control system of a European bank: A case study and discussion. In Proceedings of the 6th ACM Symposium on Access Control Models and Technologies. ACM, New York, 3--9.

Digital Library

[47]

Sohr, K., Drouineaud, M., Ahn, G.-J., and Gogolla, M. 2008. Analyzing and managing role-based access control policies. IEEE Trans. Knowl. Data Eng. 20, 924--939.

Digital Library

[48]

Solworth, J. A. and Sloan, R. H. 2004. A layered design of discretionary access controls with decidable safety properties. In Proceedings of the IEEE Symposium on Security and Privacy, 56.

[49]

Soshi, M. 2000. Safety analysis of the dynamic-typed access matrix model. In Proceedings of the Computer Security (ESORICS 2000). Lecture Notes in Computer Science, Springer, Berlin, 106--121.

Digital Library

[50]

Stoller, S. D., Yang, P., Ramakrishnan, C. R., and Gofman, M. I. 2007. Efficient policy analysis for administrative role based access control. In Proceedings of the 14th ACM Conference on Computer and Communications Security (CCS’07). ACM, New York, 445--455.

Digital Library

[51]

Zhang, N., Ryan, M., and Guelev, D. P. 2008. Synthesising verified access control systems through model checking. J. Comput. Secur. 16, 1, 1--61.

Digital Library

[52]

Zhao, C., Heilili, N., Liu, S., and Lin, Z. 2005. Representation and reasoning on RBAC: A description logic approach. In Proceedings of the 2nd International Colloquium on Theoretical Aspects of Computing (ICTAC’05), (Hanoi, Vietnam, October 17--21, 2005). Lecture Notes in Computer Science, Springer, 381--393.

Digital Library

Cited By

Kuprešanin MSubotić PRegazzoni FFournaris A(2023)Ambit: Verification of Azure RBACProceedings of the 2023 on Cloud Computing Security Workshop10.1145/3605763.3625242(31-40)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1145/3605763.3625242
Cimorelli Belfiore RFerrara ARanise SCarbone RTakabi D(2023)Security Analysis of Access Control Policies for Smart HomesProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593842(99-106)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593842
Dubrovenski VChen EXu D(2023)SMT-Based Verification of NGAC Policies2023 IEEE 47th Annual Computers, Software, and Applications Conference (COMPSAC)10.1109/COMPSAC57700.2023.00115(860-869)Online publication date: Jun-2023
https://doi.org/10.1109/COMPSAC57700.2023.00115
Show More Cited By

Index Terms

Recommendations

Mohawk+T: Efficient Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) Policies
SACMAT '15: Proceedings of the 20th ACM Symposium on Access Control Models and Technologies

Safety analysis is recognized as a fundamental problem in access control. It has been studied for various access control schemes in the literature. Recent work has proposed an administrative model for Temporal Role-Based Access Control (TRBAC) policies ...
PBDM: a flexible delegation model in RBAC
SACMAT '03: Proceedings of the eighth ACM symposium on Access control models and technologies

Role-based access control (RBAC) is recognized as an efficient access control model for large organizations. Most organizations have some business rules related to access control policy. Delegation of authority is among these rules. RBDM0 and RDM2000 ...
A flexible role-based delegation model using characteristics of permissions
DEXA'05: Proceedings of the 16th international conference on Database and Expert Systems Applications

Role-Based Access Control(RBAC) has recently received considerable attention as a promising alternative to traditional discretionary and mandatory access controls.[7] RBAC ensures that only authorized users are given access to protected data or ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Information and System Security

ACM Transactions on Information and System Security Volume 15, Issue 4

April 2013

117 pages

ISSN:1094-9224

EISSN:1557-7406

DOI:10.1145/2445566

Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 2013

Accepted: 01 January 2013

Revised: 01 October 2012

Received: 01 April 2012

Published in TISSEC Volume 15, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
455
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Kuprešanin MSubotić PRegazzoni FFournaris A(2023)Ambit: Verification of Azure RBACProceedings of the 2023 on Cloud Computing Security Workshop10.1145/3605763.3625242(31-40)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1145/3605763.3625242
Cimorelli Belfiore RFerrara ARanise SCarbone RTakabi D(2023)Security Analysis of Access Control Policies for Smart HomesProceedings of the 28th ACM Symposium on Access Control Models and Technologies10.1145/3589608.3593842(99-106)Online publication date: 24-May-2023
https://dl.acm.org/doi/10.1145/3589608.3593842
Dubrovenski VChen EXu D(2023)SMT-Based Verification of NGAC Policies2023 IEEE 47th Annual Computers, Software, and Applications Conference (COMPSAC)10.1109/COMPSAC57700.2023.00115(860-869)Online publication date: Jun-2023
https://doi.org/10.1109/COMPSAC57700.2023.00115
Gadouche HFarah ZTari A(2020)A Valid and Correct-by-Construction Formal Specification of RBACInternational Journal of Information Security and Privacy10.4018/IJISP.202004010314:2(41-61)Online publication date: 1-Apr-2020
https://doi.org/10.4018/IJISP.2020040103
Gadouche HFarah ZTari A(2020)A correct-by-construction model for attribute-based access controlCluster Computing10.1007/s10586-019-02976-423:3(1517-1528)Online publication date: 1-Sep-2020
https://dl.acm.org/doi/10.1007/s10586-019-02976-4
Shahen JNiu JTripunitara M(2019)Cree: a Performant Tool for Safety Analysis of Administrative Temporal Role-Based Access Control (ATRBAC) PoliciesIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2019.2949410(1-1)Online publication date: 2019
https://doi.org/10.1109/TDSC.2019.2949410
Dinh KTruong A(2019)Automated Security Analysis of Authorization Policies with Contextual InformationTransactions on Large-Scale Data- and Knowledge-Centered Systems XLI10.1007/978-3-662-58808-6_5(107-139)Online publication date: 7-Feb-2019
https://doi.org/10.1007/978-3-662-58808-6_5
Hohenstein UZillner SBiesdorf A(2019)Architectural Considerations for a Data Access Marketplace Based upon API ManagementData Management Technologies and Applications10.1007/978-3-030-26636-3_5(91-115)Online publication date: 20-Jul-2019
https://doi.org/10.1007/978-3-030-26636-3_5
Rajkumar PSandhu R(2018)Safety Decidability for Pre-Authorization Usage Control with Identifier Attribute DomainsIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2018.2839745(1-1)Online publication date: 2018
https://doi.org/10.1109/TDSC.2018.2839745
Gadouche HFarah ZTari A(2018)A Correct-by-Construction Model for Attribute-Based Access ControlModel and Data Engineering10.1007/978-3-030-00856-7_15(233-247)Online publication date: 13-Sep-2018
https://doi.org/10.1007/978-3-030-00856-7_15
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents