Timed constraint programming: a declarative approach to usage control

ABSTRACT

This paper focuses on policy languages for (role-based) access control [14, 32], especially in their modern incarnations in the form of trust-management systems [9] and usage control [30, 31]. Any (declarative) approach to access control and trust management has to address the following issues:

• Explicit denial, inheritance, and overriding, and
• History-sensitive access control

.Our main contribution is a policy algebra, in the timed concurrent constraint programming paradigm, that uses a form of default constraint programming to address the first issue, and reactive computing to address the second issue.The policy algebra is declarative --- programs can be viewed as imposing temporal constraints on the evolution of the system --- and supports equational reasoning. The validity of equations is established by coinductive proofs based on an operational semantics.The design of the policy algebra supports reasoning about policies by a systematic combination of constraint reasoning and model checking techniques based on linear time temporal-logic. Our framework permits us to perform security analysis with dynamic state-dependent restrictions.

REFERENCES

• 1: M. Abadi and C. Fournet. Access control based on execution history. In Proc. Network and Distributed System Security Symp., 2003.
• 2: M. Backes, M. Dürmuth, and R. Steinwandt. An algebra for composing enterprise privacy policies. In P. Samarati, D. Gollmann, and R. Molva, editors, ESORICS, volume 3193 of Lecture Notes in Computer Science, pages 33--52. Springer, 2004.
• 3: L. Badger , D. F. Sterne , D. L. Sherman , K. M. Walker , S. A. Haghighat, Practical Domain and Type Enforcement for UNIX, Proceedings of the 1995 IEEE Symposium on Security and Privacy, p.66, May 08-10, 1995
• 4: Steve Barker , Michael Leuschel , Mauricio Varea, Efficient and flexible access control via logic program specialisation, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.190-199, August 24-25, 2004, Verona, Italy [doi>10.1145/1014007.1014026]
• 5: Steve Barker , Peter J. Stuckey, Flexible access control policy specification with constraint logic programming, ACM Transactions on Information and System Security (TISSEC), v.6 n.4, p.501-546, November 2003 [doi>10.1145/950191.950194]
• 6: Adam Barth , John C. Mitchell , Justin Rosenstein, Conflict and combination in privacy policy languages, Proceedings of the 2004 ACM workshop on Privacy in the electronic society, October 28-28, 2004, Washington DC, USA [doi>10.1145/1029179.1029195]
• 7: G. Berry. Real-time programming: General purpose or special-purpose languages. In G. Ritter, editor, Information Processing 89, pages 11--17. Elsevier Science Publishers B.V. (North Holland), 1989.
• 8: 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]
• 9: Matt Blaze , Joan Feigenbaum , Jack Lacy, Decentralized Trust Management, Proceedings of the 1996 IEEE Symposium on Security and Privacy, p.164, May 06-08, 1996
• 10: W. E. Boebert and R. Y. Kain. A practical alternative to hierarchical integrity policies. In Proceedings of the Eighth National Computer Security Conference, 1985.
• 11: Piero Bonatti , Sabrina De Capitani di Vimercati , Pierangela Samarati, An algebra for composing access control policies, ACM Transactions on Information and System Security (TISSEC), v.5 n.1, p.1-35, February 2002 [doi>10.1145/504909.504910]
• 12: D. Brewer and M. Nash. The Chinese Wall security policy. In Proceedings of 1989 IEEE Symposium on Security and Privacy, pages 206--214. IEEE Computer Society Press, 1989.
• 13: A. Chander, D. Dean, and J. C. Mitchell. Reconstructing trust management. Journal of Computer Security, 12(1):131--164, 2004.
• 14: 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]
• 15: Nicolas Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, Norwell, MA, 1992
• 16: J. Y. Halpern and V. Weissman. Using first-order logic to reason about policies. In CSFW '03: Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'03), pages 118--130. IEEE Computer Society, 2003.
• 17: Joseph Y. Halpern , Vicky Weissman, A Formal Foundation for XrML, Proceedings of the 17th IEEE Computer Security Foundations Workshop (CSFW'04), p.251, June 28-30, 2004 [doi>10.1109/CSFW.2004.2]
• 18: D. Harel , A. Pnueli, On the development of reactive systems, Logics and models of concurrent systems, Springer-Verlag New York, Inc., New York, NY, 1989
• 19: P. V. Hentenryck, V. A. Saraswat, and Y. Deville. Constraint processing in cc(fd). Technical report, Computer Science Department, Brown University, 1992.
• 20: J. Jaffar and M. J. Maher. Constraint logic programming: A survey. J. Log. Program., 19/20:503--581, 1994.
• 21: Sushil Jajodia , Pierangela Samarati , Maria Luisa Sapino , V. S. Subrahmanian, Flexible support for multiple access control policies, ACM Transactions on Database Systems (TODS), v.26 n.2, p.214-260, June 2001 [doi>10.1145/383891.383894]
• 22: Ninghui Li , Benjamin N. Grosof , Joan Feigenbaum, Delegation logic: A logic-based approach to distributed authorization, ACM Transactions on Information and System Security (TISSEC), v.6 n.1, p.128-171, February 2003 [doi>10.1145/605434.605438]
• 23: Ninghui Li , John C. Mitchell, DATALOG with Constraints: A Foundation for Trust Management Languages, Proceedings of the 5th International Symposium on Practical Aspects of Declarative Languages, p.58-73, January 13-14, 2003
• 24: Ninghui Li , John C. Mitchell , William H. Winsborough, Design of a Role-Based Trust-Management Framework, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.114, May 12-15, 2002
• 25: Ninghui Li , William H. Winsborough , John C. Mitchell, Beyond Proof-of-Compliance: Safety and Availability Analysis in Trust Management, Proceedings of the 2003 IEEE Symposium on Security and Privacy, p.123, May 11-14, 2003
• 26: P. A. Loscocco and S. D. Smalley. Meeting critical security objectives with Security-Enhanced Linux. In Proceedings of the 2001 Ottawa Linux Symposium, 2001.
• 27: P. A. Loscocco, S. D. Smalley, P. A. Muckelbauer, R. C. Taylor, S. J. Turner, and J. F. Farrell. The inevitability of failure: The flawed assumption of security in modern computing environments. In Proceedings of the 21st National Information Systems Security Conference, pages 303--314, 1998.
• 28: Michael McDougall , Rajeev Alur , Carl A. Gunter, A model-based approach to integrating security policies for embedded devices, Proceedings of the 4th ACM international conference on Embedded software, September 27-29, 2004, Pisa, Italy [doi>10.1145/1017753.1017789]
• 29: Mogens Nielsen , Catuscia Palamidessi , Frank D. Valencia, Temporal concurrent constraint programming: denotation, logic and applications, Nordic Journal of Computing, v.9 n.2, p.145-188, Summer 2002
• 30: Jaehong Park , Ravi S. Sandhu, Usage control: a unified framework for next generation access control, 2003
• 31: Jaehong Park , Ravi Sandhu, The UCON_ABC usage control model, ACM Transactions on Information and System Security (TISSEC), v.7 n.1, p.128-174, February 2004 [doi>10.1145/984334.984339]
• 32: 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]
• 33: V. A. Saraswat. The Category of Constraint Systems is Cartesian-closed. In Proc. 7th IEEE Symp. on Logic in Computer Science, Santa Cruz, 1992.
• 34: Vijay Saraswat , Radha Jagadeesan , Vineet Gupta, Timed default concurrent constraint programming, Journal of Symbolic Computation, v.22 n.5-6, p.475-520, Nov./Dec. 1996 [doi>10.1006/jsco.1996.0064]
• 35: V. A. Saraswat, R. Jagadeesan, and V. Gupta. jcc: Integrating timed default concurrent constraint programming into Java. In F. Moura-Pires and S. Abreu, editors, EPIA, volume 2902 of Lecture Notes in Computer Science, pages 156--170. Springer, 2003.
• 36: Vijay A. Saraswat , Martin Rinard , Prakash Panangaden, The semantic foundations of concurrent constraint programming, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.333-352, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99627]
• 37: François Siewe , Antonio Cau , Hussein Zedan, A compositional framework for access control policies enforcement, Proceedings of the 2003 ACM workshop on Formal methods in security engineering, p.32-42, October 30, 2003, Washington, D.C. [doi>10.1145/1035429.1035433]
• 38: Emin Gün Sirer , Ke Wang, An access control language for web services, Proceedings of the seventh ACM symposium on Access control models and technologies, June 03-04, 2002, Monterey, California, USA [doi>10.1145/507711.507715]
• 39: Michael M. Swift , Anne Hopkins , Peter Brundrett , Cliff Van Dyke , Praerit Garg , Shannon Chan , Mario Goertzel , Gregory Jensenworth, Improving the granularity of access control for Windows 2000, ACM Transactions on Information and System Security (TISSEC), v.5 n.4, p.398-437, November 2002 [doi>10.1145/581271.581273]
• 40: V. N. Venkatakrishnan , Ram Peri , R. Sekar, Empowering mobile code using expressive security policies, Proceedings of the 2002 workshop on New security paradigms, September 23-26, 2002, Virginia Beach, Virginia [doi>10.1145/844102.844113]
• 41: Lingyu Wang , Duminda Wijesekera , Sushil Jajodia, A logic-based framework for attribute based access control, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA [doi>10.1145/1029133.1029140]
• 42: Duminda Wijesekera , Sushil Jajodia, Policy algebras for access control the predicate case, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586134]
• 43: Duminda Wijesekera , Sushil Jajodia, A propositional policy algebra for access control, ACM Transactions on Information and System Security (TISSEC), v.6 n.2, p.286-325, May 2003 [doi>10.1145/762476.762481]
• 44: Xinwen Zhang , Jaehong Park , Francesco Parisi-Presicce , Ravi Sandhu, A logical specification for usage control, 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.990038]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Constraint and logic languages

General Terms:
Languages, Security, Verification

Keywords:
constraints, reactive systems, role-based access control, trust management, usage control