Ensuring spatio-temporal access control for real-world applications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Ensuring spatio-temporal access control for real-world applications

Full text

Pdf (400 KB)

Source

Symposium on Access Control Models and Technologies archive
Proceedings of the 14th ACM symposium on Access control models and technologies table of contents

Stresa, Italy

SESSION: Security analysis and verification table of contents

Pages 13-22

Year of Publication: 2009

ISBN:978-1-60558-537-6

Authors

Manachai Toahchoodee	Colorado State University, Fort Collins, CO, USA
Indrakshi Ray	Colorado State University, Fort Collins, CO, USA
Kyriakos Anastasakis	University of Birmingham, Edgbaston, United Kingdom
Geri Georg	Colorado State University, Fort Collins, CO, USA
Behzad Bordbar	University of Birmingham, Edgbaston, United Kingdom

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): n/a, Downloads (12 Months): n/a, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1542207.1542212 What is a DOI?

ABSTRACT

Traditional access control models, such as Role-Based Access Control (RBAC), do not take into account contextual information, such as location and time, for making access decisions. Consequently, they are inadequate for specifying the access control needs of many complex real-world applications, such as the Dengue Decision Support (DDS) that we discuss in this paper. We need to ensure that such applications are adequately protected using emerging access control models. This requires us to represent the application and its access control requirements in a formal specification language. We choose the Unified Modeling Language (UML) for this purpose, since UML is becoming the defacto specification language in the software industry. We need to analyze this formal specification to get assurance that the application is adequately protected. Manual analysis is error-prone and tedious. Thus, we need automated tools for verification of UML models. Towards this end, we propose that the UML models be converted to Alloy. Alloy is based on first-order logic, has a software infrastructure that supports automated analysis, and has been used for the verification of real-world applications. We show how to convert the UML models to Alloy and verify the resulting model using the Alloy Analyzer which has embedded SAT-solvers. The results from the Alloy Analyzer will help uncover the flaws in the specification and help us refine the application and its access control requirements.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	K. Anastasakis, B. Bordbar, G. Georg, and I. Ray. On Challenges of Model Transformation from UML to Alloy. Journal on Software & System Modeling, 2009. To appear.
	2	Kyriakos Anastasakis, Behzad Bordbar, Geri Georg, and Indrakshi Ray. UML2Alloy: A Challenging Model Transformation. In Proceedings of the ACM/IEEE 10th International Conference on Model Driven Engineering Languages and Systems, pages 436--450, Nashville, TN, USA, October 2007.
	3	Claudio A. Ardagna , Marco Cremonini , Ernesto Damiani , Sabrina De Capitani di Vimercati , Pierangela Samarati, Supporting location-based conditions in access control policies, Proceedings of the 2006 ACM Symposium on Information, computer and communications security, March 21-24, 2006, Taipei, Taiwan [doi>10.1145/1128817.1128850]
	4	Elisa Bertino , Piero Andrea Bonatti , Elena Ferrari, TRBAC: a temporal role-based access control model, Proceedings of the fifth ACM workshop on Role-based access control, p.21-30, July 26-28, 2000, Berlin, Germany [doi>10.1145/344287.344298]
	5	Elisa Bertino , Barbara Catania , Maria Luisa Damiani , Paolo Perlasca, GEO-RBAC: a spatially aware RBAC, Proceedings of the tenth ACM symposium on Access control models and technologies, June 01-03, 2005, Stockholm, Sweden [doi>10.1145/1063979.1063985]
	6	Behzad Bordbar and Kyriakos Anastasakis. MDA and Analysis of Web Applications. In Trends in Enterprise Application Architecture, volume 3888 of Lecture notes in Computer Science, pages 44--55, Trondheim, Norway, August 2005.
	7	Behzad Bordbar and Kyriakos Anastasakis. UML2ALLOY: A tool for lightweight modelling of discrete event systems. In Proceedings of the IADIS International Conference on Applied Computing, pages 209--216, Algarve, Portugal, February 2005.
	8	Suroop Mohan Chandran and James B. D. Joshi. LoT-RBAC: A Location and Time-Based RBAC Model. In Proceedings of the 6th International Conference on Web Information Systems Engineering, pages 361--375, New York, NY, USA, November 2005.
	9	Michael J. Covington , Prahlad Fogla , Zhiyuan Zhan , Mustaque Ahamad, A Context-Aware Security Architecture for Emerging Applications, Proceedings of the 18th Annual Computer Security Applications Conference, p.249, December 09-13, 2002
	10	Michael J. Covington , Wende Long , Srividhya Srinivasan , Anind K. Dev , Mustaque Ahamad , Gregory D. Abowd, Securing context-aware applications using environment roles, Proceedings of the sixth ACM symposium on Access control models and technologies, p.10-20, May 2001, Chantilly, Virginia, United States [doi>10.1145/373256.373258]
	11	David F. Ferraiolo , Ravi Sandhu , Serban Gavrila , D. Richard Kuhn , Ramaswamy Chandramouli, Proposed NIST standard for role-based access control, ACM Transactions on Information and System Security (TISSEC), v.4 n.3, p.224-274, August 2001 [doi>10.1145/501978.501980]
	12	Geri Georg , Indrakshi Ray , Kyriakos Anastasakis , Behzad Bordbar , Manachai Toahchoodee , Siv Hilde Houmb, An aspect-oriented methodology for designing secure applications, Information and Software Technology, v.51 n.5, p.846-864, May, 2009 [doi>10.1016/j.infsof.2008.05.004]
	13	Geri Georg , Jores Bieman , Robert B. France, Using Alloy and UML/OCL to Specify Run-Time Configuration Management: A Case Study, Workshop of the pUML-Group held together with the «UML»2001 on Practical UML-Based Rigorous Development Methods - Countering or Integrating the eXtremists, p.128-141, October 01, 2001
	14	Urs Hengartner , Peter Steenkiste, Implementing access control to people location information, Proceedings of the ninth ACM symposium on Access control models and technologies, June 02-04, 2004, Yorktown Heights, New York, USA [doi>10.1145/990036.990039]
	15	Hongxin Hu , GailJoon Ahn, Enabling verification and conformance testing for access control model, Proceedings of the 13th ACM symposium on Access control models and technologies, June 11-13, 2008, Estes Park, CO, USA [doi>10.1145/1377836.1377867]
	16	Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
	17	Daniel Jackson. Micromodels of Software: Lightweight Modelling and Analysis with Alloy. At http://alloy.mit.edu/alloy2website/reference-manual.pdf , 2002.
	18	Daniel Jackson. Alloy 3.0 reference manual. At http://alloy.mit.edu/reference-manual.pdf, 2004.
	19	Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
	20	Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
	21	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]
	22	Anneke G. Kleppe , Jos Warmer , Wim Bast, MDA Explained: The Model Driven Architecture: Practice and Promise, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
	23	Ulf Leonhardt and Jeff Magee. Security Consideration for a Distributed Location Service. Imperial College of Science, Technology and Medicine, London, UK, 1997.
	24	OMG. MOF Core v. 2.0. Document Id: formal/06-01-01. http://www.omg.org.
	25	OMG. OCL Version 2.0. Document id: formal/06-05-01. http://www.omg.org.
	26	OMG. UML: Superstructure. Version 2.0. Document id: formal/05-07--04. http://www.omg.org.
	27	OMG. Unified Modeling Language: Superstructure Version 2.1.2 Formal/07/11/02. At http://www.omg.org/docs/formal/07-11-02.pdf., 2002.
	28	Indrakshi Ray and Mahendra Kumar. Towards a Location-Based Mandatory Access Control Model. Computers & Security, 25(1), February 2006.
	29	Indrakshi Ray, Mahendra Kumar, and Lijun Yu. LRBAC: A Location-Aware Role-Based Access Control Model. In Proceedings of the 2nd International Conference on Information Systems Security, pages 147--161, Kolkata, India, December 2006.
	30	Indrakshi Ray , Na Li , Robert France , Dae-Kyoo Kim, Using uml to visualize role-based access control constraints, Proceedings of the ninth ACM symposium on Access control models and technologies, June 02-04, 2004, Yorktown Heights, New York, USA [doi>10.1145/990036.990054]
	31	Indrakshi Ray and Manachai Toahchoodee. A Spatio-temporal Role-Based Access Control Model. In Proceedings of the 21st Annual IFIP WG 11.3 Working Conference on Data and Applications Security, pages 211--226, Redondo Beach, CA, July 2007.
	32	Indrakshi Ray , Manachai Toahchoodee, A Spatio-temporal Access Control Model Supporting Delegation for Pervasive Computing Applications, Proceedings of the 5th international conference on Trust, Privacy and Security in Digital Business, September 04-05, 2008, Turin, Italy [doi>10.1007/978-3-540-85735-8_6]
	33	Mark Richters. A Precise Approach to Validating UML Models and OCL Constraints. PhD thesis, Universitaet Bremen, 2002. Logos Verlag, Berlin, BISS Monographs, No. 14.
	34	Geetanjali Sampemane , Prasad Naldurg , Roy H. Campbell, Access Control for Active Spaces, Proceedings of the 18th Annual Computer Security Applications Conference, p.343, December 09-13, 2002
	35	Arjmand Samuel, Arif Ghafoor, and Elisa Bertino. A Framework for Specification and Verification of Generalized Spatio-Temporal Role Based Access Control Model. Technical report, Purdue University, February 2007. CERIAS TR 2007-08.
	36	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]
	37	Andreas Schaad , Jonathan D. Moffett, A lightweight approach to specification and analysis of role-based access control extensions, Proceedings of the seventh ACM symposium on Access control models and technologies, June 03-04, 2002, Monterey, California, USA [doi>10.1145/507711.507714]
	38	Richard Simon , Mary Ellen Zurko, Separation of Duty in Role-based Environments, Proceedings of the 10th IEEE workshop on Computer Security Foundations, p.183, June 10-12, 1997
	39	Mana Taghdiri and Daniel Jackson. A lightweight formal analysis of a multicast key management scheme. In Formal Techniques for Networked and Distributed Systems - FORTE 2 003, volume 2767 of Lecture Notes in Computer Science, pages 240--256, 2003.
	40	Manachai Toahchoodee , Indrakshi Ray, On the Formal Analysis of a Spatio-temporal Role-Based Access Control Model, Proceeedings of the 22nd annual IFIP WG 11.3 working conference on Data and Applications Security, July 13-16, 2008, London, UK [doi>10.1007/978-3-540-70567-3_2]
	41	Manachai Toahchoodee and Indrakshi Ray. Using Alloy to Analyze a Spatio-Temporal Access Control Model Supporting Delegation. IET Information Security, 2009. To appear.
	42	Chunyang Yuan, Yeping He, Jianbo He, and Zhouyi Zhou. A Verifiable Formal Specification for RBAC Model with Constraints of Separation of Duty. In Proceedings of the 2nd SKLOIS Conference on Information Security and Cryptology, pages 196--210, Beijing, China, November 2006.
	43	John Zao, Hoetech Wee, Jonathan Chu, and Daniel Jackson. RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis. At http://alloy.mit.edu/publications.php, 2002.