Enabling verification and conformance testing for access control model

ABSTRACT

Verification and testing are the important step for software assurance. However, such crucial and yet challenging tasks have not been widely adopted in building access control systems. In this paper we propose a methodology to support automatic analysis and conformance testing for access control systems, integrating those features to Assurance Management Framework (AMF). Our methodology attempts to verify formal specifications of a role-based access control model and corresponding policies with selected security properties. Also, we systematically articulate testing cases from formal specifications and validate conformance to the system design and implementation using those cases. In addition, we demonstrate feasibility and effectiveness of our methodology using SAT and Alloy toolset.

REFERENCES

• 1: The ArgoUML Project. http://argouml.tigris.org.
• 2: American National Standards Institute Inc. Role Based Access Control, ANSI-INCITS 359--2004, 2004.
• 3: Gail-Joon Ahn , Hongxin Hu, Towards realizing a formal RBAC model in real systems, Proceedings of the 12th ACM symposium on Access control models and technologies, June 20-22, 2007, Sophia Antipolis, France [doi>10.1145/1266840.1266875]
• 4: Gail-Joon Ahn , Ravi Sandhu, Role-based authorization constraints specification, ACM Transactions on Information and System Security (TISSEC), v.3 n.4, p.207-226, Nov. 2000 [doi>10.1145/382912.382913]
• 5: 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
• 6: E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000.
• 7: 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]
• 8: J. Y. Halpern and V. Weissman. Using first-order logic to reason about policies. In 16th IEEE Computer Security Foundations Workshop (CSFW'03), pages 187--201. IEEE Computer Society, 2003.
• 9: Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002 [doi>10.1145/505145.505149]
• 10: Daniel Jackson , Ian Schechter , Hya Shlyahter, Alcoa: the alloy constraint analyzer, Proceedings of the 22nd international conference on Software engineering, p.730-733, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337616]
• 11: Trent Jaeger , Xiaolan Zhang , Antony Edwards, 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]
• 12: N. Li, J.-W. Byun, and E. Bertino. A critique of the ANSI standard on role based access control. Technical Report TR 2005-29, Purdue University, 2005.
• 13: Evan Martin , Tao Xie, A fault model and mutation testing of access control policies, Proceedings of the 16th international conference on World Wide Web, May 08-12, 2007, Banff, Alberta, Canada [doi>10.1145/1242572.1242663]
• 14: A. Masood, A. Ghafoor, and A. Mathur. Scalable and effective test generation for access control systems that employ RBAC policies that employ RBAC policies. SERC-TR-285, Purdue University, 2005.
• 15: D. G. Mitchell. A SAT Solver Primer. EATCS Bulletin (The Logic in Computer Science Column), Volume 85, February 2005, pages 112--133.
• 16: J. Robinson , Andrei Voronkov, Handbook of Automated Reasoning: Volume 1, MIT Press, Cambridge, MA, 2001
• 17: 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]
• 18: Yves Le Traon , Tejeddine Mouelhi , Benoit Baudry, Testing Security Policies: Going Beyond Functional Testing, Proceedings of the The 18th IEEE International Symposium on Software Reliability, p.93-102, November 05-09, 2007 [doi>10.1109/ISSRE.2007.29]
• 19: Jan Tretmans, A Formal Approach to Conformance Testing, Proceedings of the IFIP TC6/WG6.1 Sixth International Workshop on Protocol Test systems VI, p.257-276, September 28-30, 1993
• 20: Mark Utting , Bruno Legeard, Practical Model-Based Testing: A Tools Approach, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2006

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking; Validation

  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.5 Security and Protection (D.4.6, K.4.2)

General Terms:
Design, Languages, Security, Verification

Keywords:
SAT solver, access control, alloy, model-based testing, model-based verification