Towards formal security analysis of GTRBAC using timed automata

ABSTRACT

An access control system is often viewed as a state transition system. Given a set of access control policies, a general safety requirement in such a system is to determine whether a desirable property is satisfied in all the reachable states. Such an analysis calls for formal verification. While formal analysis on traditional RBAC has been done to some extent, the extensions of RBAC lack such an analysis. In this paper, we propose a formal technique to perform security analysis on the Generalized Temporal RBAC (GTRBAC) model which can be used to express a wide range of temporal constraints on different RBAC components like role, user and permission. In the proposed approach, at first the GTRBAC system is mapped to a state transition system built using timed automata. Characteristics of each role, user and permission are captured with the help of timed automata. A single global clock is used to express the various temporal constraints supported in a GTRBAC model. Next, a set of safety and liveness properties is specified using computation tree logic (CTL). Model checking based formal verification is then done to verify the properties against the model to determine if the system is secure with respect to a given set of access control policies. Both time and space analysis has been done for studying the performance of the approach under different configurations.

REFERENCES

• 1: Elisa Bertino , Piero Andrea Bonatti , Elena Ferrari, TRBAC: A temporal role-based access control model, ACM Transactions on Information and System Security (TISSEC), v.4 n.3, p.191-233, August 2001 [doi>10.1145/501978.501979]
• 2: Vijayalakshmi Atluri , Avigdor Gal, An authorization model for temporal and derived data: securing information portals, ACM Transactions on Information and System Security (TISSEC), v.5 n.1, p.62-94, February 2002 [doi>10.1145/504909.504912]
• 3: I. Ray and M. Toahchoodee. A spatio temporal role based access control model. In 21st Annual IFIP WG 11.3 Working Conference on Data and Applications Security, pages 211--226, Jul 2007.
• 4: S. Aich, S. Sural, and A. K. Majumdar. STARBAC: Spatiotemporal role based access control. In Information Security Conference, LNCS, Springer-Verlag, pages 1567--1582, November 2007.
• 5: James B. D. Joshi , Elisa Bertino , Usman Latif , Arif Ghafoor, A Generalized Temporal Role-Based Access Control Model, IEEE Transactions on Knowledge and Data Engineering, v.17 n.1, p.4-23, January 2005 [doi>10.1109/TKDE.2005.1]
• 6: Michael A. Harrison , Walter L. Ruzzo , Jeffrey D. Ullman, Protection in operating systems, Communications of the ACM, v.19 n.8, p.461-471, Aug. 1976 [doi>10.1145/360303.360333]
• 7: A. K. Jones , R. J. Lipton , L. Snyder, A Linear time algorithm for deciding security, Proceedings of the 17th Annual Symposium on Foundations of Computer Science, p.33-41, October 25-27, 1976
• 8: Ravinderpal Singh Sandhu, The schematic protection model: its definition and analysis for acyclic attenuating schemes, Journal of the ACM (JACM), v.35 n.2, p.404-432, April 1988 [doi>10.1145/42282.42286]
• 9: Manuel Koch , Luigi V. Mancini , Francesco Parisi-Presicce, Decidability of Safety in Graph-Based Models for Access Control, Proceedings of the 7th European Symposium on Research in Computer Security, p.229-243, October 14-16, 2002
• 10: Tanvir Ahmed , Anand R. Tripathi, Static verification of security requirements in role based CSCW systems, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy [doi>10.1145/775412.775438]
• 11: 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]
• 12: 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]
• 13: Yue Zhang , James B. D. Joshi, UAQ: a framework for user authorization query processing in RBAC extended with hybrid hierarchy and constraints, Proceedings of the 13th ACM symposium on Access control models and technologies, June 11-13, 2008, Estes Park, CO, USA [doi>10.1145/1377836.1377850]
• 14: 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]
• 15: James B. D. Joshi , Elisa Bertino , Arif Ghafoor, An Analysis of Expressiveness and Design Issues for the Generalized Temporal Role-Based Access Control Model, IEEE Transactions on Dependable and Secure Computing, v.2 n.2, p.157-175, April 2005 [doi>10.1109/TDSC.2005.18]
• 16: Basit Shafiq , Ammar Masood , James Joshi , Arif Ghafoor, A Role-Based Access Control Policy Verification Framework for Real-Time Systems, Proceedings of the 10th IEEE International Workshop on Object-Oriented Real-Time Dependable Systems, p.13-20, February 02-04, 2005 [doi>10.1109/WORDS.2005.11]
• 17: R. Alur, C. Courcoubetis, and D. L. Dill. Model checking for real time systems. In 5th Symposium on Logic in Computer Science, pages 414--425, 1990.
• 18: A. Furfaro and L. Nigro. Temporal verification of communicating real time state machines using Uppaal. In IEEE International Conference on Industrial Technology, pages 399--404, 2003.
• 19: Samrat Mondal , Shamik Sural, Security Analysis of Temporal-RBAC Using Timed Automata, Proceedings of the 2008 The Fourth International Conference on Information Assurance and Security, p.37-40, September 08-10, 2008 [doi>10.1109/IAS.2008.10]
• 20: Samrat Mondal , Shamik Sural, A Verification Framework for Temporal RBAC with Role Hierarchy (Short Paper), Proceedings of the 4th International Conference on Information Systems Security, December 16-20, 2008, Hyderabad, India [doi>10.1007/978-3-540-89862-7_11]
• 21: 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]
• 22: Christel Baier , Joost-Pieter Katoen, Principles of Model Checking (Representation and Mind Series), The MIT Press, 2008
• 23: F. Laroussinie, N. Markey, and Ph. Schnoebelen. Model checking timed automata with one or two clocks. In 15th International Conference on Concurrency Theory, pages 387--401, 2004.
• 24: G. Behrmann, A. David, and K. G. Larsen. A tutorial on UPPAAL. In 4th International School on Formal Methods for the Design of Computer, Communication and Software Systems, pages 200--236, 2004.

INDEX TERMS

Primary Classification:
  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.0 General
          Subjects: Security, integrity, and protection**

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

General Terms:
Algorithms, Performance, Security, Verification

Keywords:
GTRBAC, ctl, model checking, security analysis, timed automata