Symbolic reachability analysis for parameterized administrative role based access control

ABSTRACT

Role based access control (RBAC) is a widely used access control paradigm. In large organizations, the RBAC policy is managed by multiple administrators. An administrative role based access control (ARBAC) policy specifies how each administrator may change the RBAC policy. It is often difficult to fully understand the effect of an ARBAC policy by simple inspection, because sequences of changes by different administrators may interact in unexpected ways. ARBAC policy analysis algorithms can help by answering questions, such as user-role reachability, which asks whether a given user can be assigned to given roles by given administrators. Allowing roles and permissions to have parameters significantly enhances the scalability, flexibility, and expressiveness of ARBAC policies. This paper defines PARBAC, which extends the classic ARBAC97 model to support parameters, and presents an analysis algorithm for PARBAC. To the best of our knowledge, this is the first analysis algorithm specifically for parameterized ARBAC policies. We evaluate its efficiency by analyzing its parameterized complexity and benchmarking it on case studies and synthetic policies.

REFERENCES

• 1: Rajeev Alur , David L. Dill, A theory of timed automata, Theoretical Computer Science, v.126 n.2, p.183-235, April 25, 1994 [doi>10.1016/0304-3975(94)90010-8]
• 2: Tamarah Arons , Amir Pnueli , Sitvanit Ruah , Jiazhao Xu , Lenore D. Zuck, Parameterized Verification with Automatically Computed Inductive Assertions, Proceedings of the 13th International Conference on Computer Aided Verification, p.221-234, July 18-22, 2001
• 3: M. Y. Becker. Cassandra: Flexible Trust Management and its Application to Electronic Health Records. PhD thesis, University of Cambridge, Oct. 2005.
• 4: Bruno Blanchet , Andreas Podelski, Verification of cryptographic protocols: tagging enforces termination, Theoretical Computer Science, v.333 n.1-2, p.67-90, 1 March 2005 [doi>10.1016/j.tcs.2004.10.018]
• 5: Avrim L. Blum , Merrick L. Furst, Fast planning through planning graph analysis, Artificial Intelligence, v.90 n.1-2, p.281-300, Feb. 1997 [doi>10.1016/S0004-3702(96)00047-1]
• 6: E. M. Clarke , O. Grumberg , S. Jha, Verifying parameterized networks, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.726-750, Sept. 1997 [doi>10.1145/265943.265960]
• 7: Rod G. Downey , Michael R. Fellows, Fixed-Parameter Tractability and Completeness I: Basic Results, SIAM Journal on Computing, v.24 n.4, p.873-921, Aug. 1995 [doi>10.1137/S0097539792228228]
• 8: E. Allen Emerson , Kedar S. Namjoshi, Reasoning about rings, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-94, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199468]
• 9: E. Allen Emerson , Vineet Kahlon, Reducing Model Checking of the Many to the Few, Proceedings of the 17th International Conference on Automated Deduction, p.236-254, June 17-20, 2000
• 10: Mark Evered , Serge Bögeholz, A case study in access control requirements for a Health Information System, Proceedings of the second workshop on Australasian information security, Data Mining and Web Intelligence, and Software Internationalisation, p.53-61, January 01, 2004, Dunedin, New Zealand
• 11: Luigi Giuri , Pietro Iglio, Role templates for content-based access control, Proceedings of the second ACM workshop on Role-based access control, p.153-159, November 06-07, 1997, Fairfax, Virginia, United States [doi>10.1145/266741.266773]
• 12: 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, v.5 n.4, p.242-255, October 2008 [doi>10.1109/TDSC.2007.70225]
• 13: Ninghui Li , Ziqing Mao, Administration in role-based access control, Proceedings of the 2nd ACM symposium on Information, computer and communications security, March 20-22, 2007, Singapore [doi>10.1145/1229285.1229305]
• 14: Ninghui Li , Mahesh V. Tripunitara, Security analysis in role-based access control, ACM Transactions on Information and System Security (TISSEC), v.9 n.4, p.391-420, November 2006 [doi>10.1145/1187441.1187442]
• 15: Ravi Sandhu , Venkata Bhamidipati , Qamar Munawer, The ARBAC97 model for role-based administration of roles, ACM Transactions on Information and System Security (TISSEC), v.2 n.1, p.105-135, Feb. 1999 [doi>10.1145/300830.300839]
• 16: Ravi S. Sandhu , Edward J. Coyne , Hal L. Feinstein , Charles E. Youman, Role-Based Access Control Models, Computer, v.29 n.2, p.38-47, February 1996 [doi>10.1109/2.485845]
• 17: B. Sarna-Starosta and C. R. Ramakrishnan. Constraint-based model checking of data-independent systems. In 5th International Conference on Formal Engineering Methods (ICFEM), 2003.
• 18: Amit Sasturkar , Ping Yang , Scott D. Stoller , C. R. Ramakrishnan, Policy Analysis for Administrative Role Based Access Control, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.124-138, July 05-07, 2006 [doi>10.1109/CSFW.2006.22]
• 19: Scott D. Stoller , Ping Yang , C R. Ramakrishnan , Mikhail I. Gofman, Efficient policy analysis for administrative role based access control, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA [doi>10.1145/1315245.1315300]

INDEX TERMS

Primary Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

General Terms:
Security, Verification

Keywords:
parameterized administrative role based access control, security policy analysis