The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - October-December (2008 vol.5)
pp: 242-255
ABSTRACT
Specifying and managing access control policies is a challenging problem. We propose to develop formal verification techniques for access control policies to improve the current state of the art of policy specification and management. In this paper, we formalize classes of security analysis problems in the context of Role-Based Access Control. We show that in general these problems are PSPACE-complete. We also study the factors that contribute to the computational complexity by considering a lattice of various subcases of the problem with different restrictions. We show that several subcases remain PSPACE-complete, several further restricted subcases are NP-complete, and identify two subcases that are solvable in polynomial time. We also discuss our experiences and findings from experimentations that use existing formal method tools, such as model checking and logic programming, for addressing these problems.
INDEX TERMS
Access controls, Security and Protection, Complexity of proof procedures
CITATION
Somesh Jha, Ninghui Li, Mahesh Tripunitara, Qihua Wang, William Winsborough, "Towards Formal Verification of Role-Based Access Control Policies", IEEE Transactions on Dependable and Secure Computing, vol.5, no. 4, pp. 242-255, October-December 2008, doi:10.1109/TDSC.2007.70225
REFERENCES
[1] P. Ammann and R.S. Sandhu, “Safety Analysis for the Extended Schematic Protection Model,” Proc. IEEE Symp. Security and Privacy (S&P '91), pp. 87-97, May 1991.
[2] P. Ammann and R.S. Sandhu, “Implementing Transaction Control Expressions by Checking for Absence of Access Rights,” Proc. Eighth Ann. Computer Security Applications Conf. (ACSAC '92), Dec. 1992.
[3] American National Standard for Information Technology - Role Based Access Control, ANSI INCITS 359-2004, Am. Nat'l Standards Inst., Feb. 2004.
[4] R. Awischus, “Role-Based Access Control with the Security Administration Manager (SAM),” Proc. Second ACM Workshop Role-Based Access Control Table of Contents (RBAC '97), pp. 61-68, 1997.
[5] T. Budd, “Safety in Grammatical Protection Systems,” Int'l J. Computer and Information Sciences, vol. 12, no. 6, pp. 413-430, 1983.
[6] W. Chen and D.S. Warren, “Tabled Evaluation with Delaying forGeneral Logic Programs,” J. ACM, vol. 43, no. 1, pp. 20-74, Jan. 1996.
[7] E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking. MITPress, 2000.
[8] J. Crampton, “Authorizations and Antichains,” PhD dissertation, Univ. of London, U.K., 2002.
[9] J. Crampton and G. Loizou, “Administrative Scope: A Foundation for Role-Based Administrative Models,” ACM Trans. Information and System Security, vol. 6, no. 2, pp. 201-231, May 2003.
[10] W.F. Dowling and J.H. Gallier, “Linear-Time Algorithms for Testing the Satisfiability of Propositional Horn Formulae,” J. Logic Programming, vol. 1, no. 3, pp. 267-284, 1984.
[11] D.F. Ferraiolo, J.A. Cuigini, and D.R. Kuhn, “Role-Based Access Control (RBAC): Features and Motivations,” Proc. 11th Ann. Computer Security Applications Conf. (ACSAC '95), Dec. 1995.
[12] D.F. Ferraiolo and D.R. Kuhn, “Role-Based Access Control,” Proc. 15th Nat'l Information Systems Security Conf., 1992.
[13] D.F. Ferraiolo, R.S. Sandhu, S. Gavrila, D.R. Kuhn, and R. Chandramouli, “Proposed NIST Standard for Role-Based Access Control,” ACM Trans. Information and Systems Security, vol. 4, no. 3, pp. 224-274, Aug. 2001.
[14] M.R. Garey and D.J. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman and Co., 1979.
[15] T.X.R. Group, The XSB Programming System, http:/xsb.sourceforge.net/, 2008.
[16] M.A. Harrison and W.L. Ruzzo, “Monotonic Protection Systems,” Foundations of Secure Computation, R.A. DeMillo, D.P. Dobkin, A.K.Jones, and R.J. Lipton, eds., Academic Press, pp. 461-471, 1978.
[17] M.A. Harrison, W.L. Ruzzo, and J.D. Ullman, “Protection inOperating Systems,” Comm. ACM, vol. 19, no. 8, pp. 461-471, Aug. 1976.
[18] S. Jha, O. Sheyner, and J.M. Wing, “Two Formal Analysis of Attack Graphs,” Proc. 15th IEEE Computer Security Foundations Workshop (CSFW '02), June 2002.
[19] A.K. Jones, R.J. Lipton, and L. Snyder, “A Linear Time Algorithm for Deciding Security,” Proc. 17th Ann. IEEE Symp. Foundations of Computer Science (FOCS '76), pp. 33-41, Oct. 1976.
[20] G. Karjoth, “The Authorization Model of Tivoli Policy Director,” Proc. 17th Ann. Computer Security Applications Conf. (ACSAC '01), pp. 319-328, Dec. 2001.
[21] A. Kern, “Advanced Features for Enterprise-Wide Role-Based Access Control,” Proc. 18th Ann. Computer Security Applications Conf. (ACSAC '02), pp. 333-343, Dec. 2002.
[22] M. Koch, L.V. Mancini, and F. Parisi-Presicce, “Decidability of Safety in Graph-Based Models for Access Control,” Proc. Seventh European Symp. Research in Computer Security (ESORICS '02), pp.229-243, Oct. 2002.
[23] M. Koch, L.V. Mancini, and F. Parisi-Presicce, “A Graph-Based Formalism for RBAC,” ACM Trans. Information and System Security, vol. 5, no. 3, pp. 332-365, Aug. 2002.
[24] N. Li, J.C. Mitchell, and W.H. Winsborough, “Design of a Role-Based Trust Management Framework,” Proc. IEEE Symp. Security and Privacy (S&P '02), pp. 114-130, May 2002.
[25] N. Li, J.C. Mitchell, and W.H. Winsborough, “Beyond Proof-of-Compliance: Security Analysis in Trust Management,” J. ACM, vol. 52, no. 3, pp. 474-514, A preliminary version appeared in Proc. 2003 IEEE Symp. Security and Privacy (S&P), May 2005.
[26] N. Li and M.V. Tripunitara, “Security Analysis in Role-Based Access Control,” Proc. Ninth ACM Symp. Access Control Models and Technologies (SACMAT '04), pp. 126-135, June 2004.
[27] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. Springer, 1992.
[28] Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety. Springer, 1995.
[29] D. McPherson, Role-Based Access Control for Multi-Tier Applications Using Authorization Manager, http://www.microsoft. com/technet/prodtechnol/ windowsserver2003/technologies/management athmanwp.mspx, 2008.
[30] R. Motwani, R. Panigrahy, V.A. Saraswat, and S. Ventkatasubramanian, “On the Decidability of Accessibility Problems,” Proc. 32nd Ann. ACM Symp. Theory of Computing (STOC '00), extended abstract, pp. 306-315, May 2000.
[31] Q. Munawer and R.S. Sandhu, “Simulation of the Augmented Typed Access Matrix Model (ATAM) Using Roles,” Proc. ACM Int'l Conf. Information and Security (INFOSECU), 1999.
[32] NuSMV: A New Symbolic Model Checker, http://afrodite.itc.it:1024 nusmv/, 2008.
[33] X. Ou, S. Govindavajhala, and A.W. Appel, “MulVAL: A Logic-Based Network Security Analyzer,” Proc. 14th Usenix Security Symp., Aug. 2005.
[34] C.H. Papadimitriou, Computational Complexity. Addison-Wesley-Longman, 1994.
[35] R.S. Sandhu, “The Schematic Protection Model: Its Definition and Analysis for Acyclic Attenuating Systems,” J. ACM, vol. 35, no. 2, pp. 404-432, 1988.
[36] R.S. Sandhu, “The Typed Access Matrix Model,” Proc. IEEE Symp. Security and Privacy (S&P), pp. 122-136, May 1992.
[37] R.S. Sandhu and V. Bhamidipati, “Role-Based Administration of User-Role Assignment: The URA97 Model and Its Oracle Implementation,” J. Computer Security, vol. 7, 1999.
[38] R.S. Sandhu, V. Bhamidipati, and Q. Munawer, “The ARBAC97 Model for Role-Based Administration of Roles,” ACM Trans.Information and Systems Security, vol. 2, no. 1, pp. 105-135, Feb. 1999.
[39] R.S. Sandhu, E.J. Coyne, H.L. Feinstein, and C.E. Youman, “Role-Based Access Control Models,” Computer, vol. 29, no. 2, pp. 38-47, Feb. 1996.
[40] A. Schaad, J. Moffett, and J. Jacob, “The Role-Based Access ControlSystem of a European Bank: A Case Study and Discussion,” Proc. Sixth ACM Symp. Access Control Models and Technologies (SACMAT '01), pp. 3-9, 2001.
[41] O. Sheyner, J.W. Haines, S. Jha, R. Lippmann, and J.M. Wing, “Automated Generation and Analysis of Attack Graphs,” Proc. IEEE Symp. Security and Privacy (S&P), 2002.
[42] J.A. Solworth and R.H. Sloan, “A Layered Design of Discretionary Access Controls with Decidable Safety Properties,” Proc. IEEE Symp. Security and Privacy (S&P), May 2004.
[43] M. Soshi, “Safety Analysis of the Dynamic-Typed Access Matrix Model,” Proc. Sixth European Symp. Research in Computer Security (ESORICS '00), pp. 106-121, Oct. 2000.
[44] A. Sasturkar, P. Yang, S. Stoller, and C. Ramakrishnan, “Policy Analysis for Administrative Role-Based Access Control,” Proc. 19th Computer Security Foundations Workshop (CSFW '06), July 2006.
21 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool