Stale-safe security properties for group-based secure information sharing

ABSTRACT

Attribute staleness arises due to the physical distribution of authorization information, decision and enforcement points. This is a fundamental problem in virtually any secure distributed system in which the management and representation of authorization state are not globally synchronized. This problem is so intrinsic, it is inevitable that access decision will be based on attribute values that are stale. While it may not be practical to eliminate staleness, we can limit unsafe access decisions made based on stale subject and object attributes. In this paper, we propose and formally specify four stale-safe security properties of varying strength which limit such incorrect access decisions. We use Linear Temporal Logic (LTL) to formalize these properties making them suitable to be verified, for example, using model checking. We show how these properties can be applied in the specific context of group-based Secure Information Sharing (g-SIS) as defined in this paper. We specify the authorization decision/enforcement points of the g-SIS system as a Finite State Machine (FSM) and show how this FSM can be modified so as to satisfy one of the stale-safe properties.

REFERENCES

• 1: TCG specification architecture overview. http://www.trustedcomputinggroup.org.
• 2: Arosha K. Bandara , Emil C. Lupu , Alessandra Russo, Using Event Calculus to Formalise Policy Specification and Analysis, Proceedings of the 4th IEEE International Workshop on Policies for Distributed Systems and Networks, p.26, June 04-06, 2003
• 3: Kathi Fisler , Shriram Krishnamurthi , Leo A. Meyerovich , Michael Carl Tschantz, Verification and change-impact analysis of access-control policies, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062502]
• 4: David P. Gilliam , John D. Powell , Matt Bishop, Application of Lightweight Formal Methods to Software Security, Proceedings of the 14th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprise, p.160-165, June 13-15, 2005 [doi>10.1109/WETICE.2005.19]
• 5: J. Goguen and J. Meseguer. Security policies and security models. IEEE Symposium on Security and Privacy, 12, 1982.
• 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: S. Jha , T. Reps, Model checking SPKI/SDSI, Journal of Computer Security, v.12 n.3,4, p.317-353, May 2004
• 8: R. Krishnan, J. Niu, R. Sandhu, and W. Winsborough. Stale-safe security properties for group--based secure information sharing. Technical report CS-TR-2008--012, Department of Computer Science, University of Texas, San Antonio, 2008.
• 9: Ram Krishnan , Ravi Sandhu , Kumar Ranganathan, PEI models towards scalable, usable and high-assurance information sharing, Proceedings of the 12th ACM symposium on Access control models and technologies, June 20-22, 2007, Sophia Antipolis, France [doi>10.1145/1266840.1266863]
• 10: Adam J. Lee , Kazuhiro Minami , Marianne Winslett, Lightweight cnsistency enforcement schemes for distributed proofs with hidden subtrees, Proceedings of the 12th ACM symposium on Access control models and technologies, June 20-22, 2007, Sophia Antipolis, France [doi>10.1145/1266840.1266856]
• 11: Adam J. Lee , Marianne Winslett, Safety and consistency in policy-based authorization systems, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180422]
• 12: Zohar Manna , Amir Pnueli, The temporal logic of reactive and concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1992
• 13: Michael J. May , Carl A. Gunter , Insup Lee, Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies, Proceedings of the 19th IEEE workshop on Computer Security Foundations, p.85-97, July 05-07, 2006 [doi>10.1109/CSFW.2006.24]
• 14: Sandro Rafaeli , David Hutchison, A survey of key management for secure group communication, ACM Computing Surveys (CSUR), v.35 n.3, p.309-329, September 2003 [doi>10.1145/937503.937506]
• 15: Ravi S. Sandhu, Lattice-Based Access Control Models, Computer, v.26 n.11, p.9-19, November 1993 [doi>10.1109/2.241422]
• 16: Andreas Schaad , Volkmar Lotz , Karsten Sohr, A model-checking approach to analysing organisational controls in a loan origination process, Proceedings of the eleventh ACM symposium on Access control models and technologies, June 07-09, 2006, Lake Tahoe, California, USA [doi>10.1145/1133058.1133079]
• 17: A. P. Sistla and M. Zhou. Analysis of dynamic policies. In Proceedings of Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, pages 233--262, 2006.
• 18: N. Zhang, M. Ryan, and D. P. Guelev. Evaluating access control policies through model checking. In Proceedings of the 8th Information Security Conference, volume 3650 of LNCS, pages 446--460. Springer-Verlag, 2005.

INDEX TERMS

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

Additional Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)
          Subjects: Unauthorized access (e.g., hacking, phreaking)

General Terms:
Security

Keywords:
information sharing, security properties, stale attributes