Verification and change-impact analysis of access-control policies

ABSTRACT

Sensitive data are increasingly available on-line through the Web and other distributed protocols. This heightens the need to carefully control access to data. Control means not only preventing the leakage of data but also permitting access to necessary information. Indeed, the same datum is often treated differently depending on context.System designers create policies to express conditions on the access to data. To reduce source clutter and improve maintenance, developers increasingly use domain-specific, declarative languages to express these policies. In turn, administrators need to analyze policies relative to properties, and to understand the effect of policy changes even in the absence of properties.This paper presents Margrave, a software suite for analyzing role-based access-control policies. Margrave includes a verifier that analyzes policies written in the XACML language, translating them into a form of decision-diagram to answer queries. It also provides semantic differencing information between versions of policies. We have implemented these techniques and applied them to policies from a working software application.

REFERENCES

• 1: 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]
• 2: A. Anderson. Evaluating XACML as a policy language. Technical report, OASIS, Mar. 2003. Document identifier: wd-xacml-wspleval-03.
• 3: Michael Backes , Günter Karjoth , Walid Bagga , Matthias Schunter, Efficient comparison of enterprise privacy policies, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus [doi>10.1145/967900.967983]
• 4: R. Iris Bahar , Erica A. Frohm , Charles M. Gaona , Gary D. Hachtel , Enrico Macii , Abelardo Pardo , Fabio Somenzi, Algebraic decision diagrams and their applications, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.188-191, November 07-11, 1993, Santa Clara, California, United States
• 5: Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
• 6: D. D. Clark and D. R. Wilson. A comparison of commercial and military computer security policies. In IEEE Symposium of Security and Privacy, pages 184--194, 1987.
• 7: E. Clarke, M. Fujita, P. McGeer, J. Yang, and X. Zhao. Multi-terminal binary decision diagrams: An efficient data structure for matrix representation. In International Workshop on Logic Synthesis, 1993.
• 8: David F. Ferraiolo , D. Richard Kuhn , Ramaswamy Chandramouli, Role-Based Access Control, Artech House, Inc., Norwood, MA, 2003
• 9: Robert Bruce Findler , John Clements , Cormac Flanagan , Matthew Flatt , Shriram Krishnamurthi , Paul Steckler , Matthias Felleisen, DrScheme: a programming environment for Scheme, Journal of Functional Programming, v.12 n.2, p.159-182, March 2002 [doi>10.1017/S0956796801004208]
• 10: D. P. Guelev, M. D. Ryan, and P.-Y. Schobbens. Model-checking access control policies. In Information Security Conference, Lecture Notes in Computer Science. Springer-Verlag, Sept. 2004.
• 11: J. D. Guttman and A. L. Herzog. Rigorous automated network security management. International Journal of Information Security, Dec. 2004.
• 12: J. D. Guttman, A. L. Herzog, and J. D. Ramsdell. Verifying information flow goals in security-enhanced Linux. In Workshop on Issues in the Theory of Security, January 2004.
• 13: P. W. Hopkins. Enabling complex UI in Web applications with send/suspend/dispatch. In Scheme Workshop, 2003.
• 14: Susan Horwitz, Identifying the semantic and textual differences between two versions of a program, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.234-245, June 1990, White Plains, New York, United States
• 15: G. Hughes and T. Bultan. Automated verification of access control policies. Technical Report 2004-22, University of California, Santa Barbara, 2004.
• 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 , Somesh Jha , Craig A. Damon, Isomorph-free model enumeration: a new method for checking relational specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.2, p.302-343, March 1998 [doi>10.1145/276393.276396]
• 18: Trent Jaeger , Xiaolan Zhang , Fidel Cacheda, Policy management using access control spaces, ACM Transactions on Information and System Security (TISSEC), v.6 n.3, p.327-364, August 2003 [doi>10.1145/937527.937528]
• 19: N. I. Adams, IV , D. H. Bartley , G. Brooks , R. K. Dybvig , D. P. Friedman , R. Halstead , C. Hanson , C. T. Haynes , E. Kohlbecker , D. Oxley , K. M. Pitman , G. J. Rozas , G. L. Steele, Jr. , G. J. Sussman , M. Wand , H. Abelson, Revised5 report on the algorithmic language scheme, ACM SIGPLAN Notices, v.33 n.9, p.26-76, Sept. 1, 1998 [doi>10.1145/290229.290234]
• 20: M. Koch , L. V. Mancini , F. Parisi-Presicce, On the specification and evolution of access control policies, Proceedings of the sixth ACM symposium on Access control models and technologies, p.121-130, May 2001, Chantilly, Virginia, United States [doi>10.1145/373256.373280]
• 21: Grzegorz Kolaczek, Specification and Verification of Constraints in Role Based Access Control for Enterprise Security System, Proceedings of the Twelfth International Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises, p.190, June 09-11, 2003
• 22: S. Krishnamurthi. The Continue server. In Symposium on the Practical Aspects of Declarative Languages, January 2003.
• 23: F. Mayer. Tools and techniques for analyzing type enforcement policies in security enhanced Linux. In Annual Computer Security Applications Conference, Dec. 2003.
• 24: T. Moses. eXtensible Access Control Markup Language (XACML) version 1.0. Technical report, OASIS, Feb. 2003.
• 25: C. Powers and M. Schunter. Enterprise privacy authorization language (EPAL 1.2). W3C Member Submission, November 2003.
• 26: A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, 21(1):5--19, January 2003.
• 27: B. Sarna-Starosta and S. D. Stoller. Policy analysis for security-enhanced Linux. In Workshop on Issues in the Theory of Security, pages 1--12, April 2004.
• 28: Andreas Schaad , Jonathan Moffett , Jeremy Jacob, The role-based access control system of a European bank: a case study and discussion, Proceedings of the sixth ACM symposium on Access control models and technologies, p.3-9, May 2001, Chantilly, Virginia, United States [doi>10.1145/373256.373257]
• 29: 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]
• 30: F. Somenzi. CUDD: The CU decision diagram package. http://vlsi.colorado.edu/ fabio/CUDD/.
• 31: Nan Zhang , Mark Ryan , Dimitar P. Guelev, Synthesising verified access control systems in XACML, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA [doi>10.1145/1029133.1029141]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.7 Distribution, Maintenance, and Enhancement
          Subjects: Version control
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Specialized application languages
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

General Terms:
Algorithms, Languages, Security, Verification

Keywords:
XACML, access-control policies, change-impact analysis, decision diagram, verification