Static verification of security requirements in role based CSCW systems

ABSTRACT

In this paper, we present static verification of security requirements for CSCW systems using finite-state techniques, i.e., model checking. The coordination and security constraints of CSCW systems are specified using a role based collaboration model. The verification ensures completeness and consistency of the specification given global requirements. We have developed several verification models to check security properties, such as task-flow constraints, information flow or confidentiality, and assignment of administrative privileges. The primary contribution of this paper is a methodology for verification of security requirements during designing collaboration systems.

REFERENCES

• 1: Jean Bacon , Ken Moody , Walt Yao, A model of OASIS role-based access control and its support for active security, ACM Transactions on Information and System Security (TISSEC), v.5 n.4, p.492-540, November 2002 [doi>10.1145/581271.581276]
• 2: Elisa Bertino , Elena Ferrari , Vijayalakshmi Atluri, A flexible model supporting the specification and enforcement of role-based authorization in workflow management systems, Proceedings of the second ACM workshop on Role-based access control, p.1-12, November 06-07, 1997, Fairfax, Virginia, United States [doi>10.1145/266741.266746]
• 3: Roy H. Campbell , A. Nico Habermann, The specification of process synchronization by path expressions, Operating Systems, Proceedings of an International Symposium, p.89-102, April 23-25, 1974
• 4: S. Castano, P. Samarati, and C. Villa. Verifying System Security Using Petri Nets. In Security Technology, 1993. Security Technology, Proceedings. Institute of Electrical and Electronics Engineers 1993 International Carnahan Conference on, pages 244--250, Oct 1993.
• 5: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 6: Dorothy Elizabeth Rob Denning, Cryptography and Data Security, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1982
• 7: Rik Eshuis , Roel Wieringa, Verification support for workflow design with UML activity graphs, Proceedings of the 24th International Conference on Software Engineering, May 19-25, 2002, Orlando, Florida [doi>10.1145/581339.581362]
• 8: S. Foley and J. Jacob. Specifying Security for Computer Supported Collaborative Computing. Journal of Computer Security, 3(4):233--253, 1995.
• 9: 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]
• 10: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 11: Trent Jaeger , Jonathon E. Tidswell, Practical safety in flexible access control models, ACM Transactions on Information and System Security (TISSEC), v.4 n.2, p.158-190, May 2001 [doi>10.1145/501963.501966]
• 12: W. Janssen, R. Mateescu, S. Mauw, and J. Springintveld. Verifying Business Processes using Spin. In Proc. of 4th International SPIN Workshop, 1998.
• 13: Emil Lupu , Morris Sloman, Reconciling role based management and role based access control, Proceedings of the second ACM workshop on Role-based access control, p.135-141, November 06-07, 1997, Fairfax, Virginia, United States [doi>10.1145/266741.266770]
• 14: Paolo Maggi , Riccardo Sisto, Using SPIN to Verify Security Properties of Cryptographic Protocols, Proceedings of the 9th International SPIN Workshop on Model Checking of Software, p.187-204, April 11-13, 2002
• 15: P. Muth, D. Wodtke, J. Weissenfels, G. Weikum, and A. Kotz~Dittrich. Enterprise-wide Workflow Management based on State and Activity Charts, Workflow Management Systems and Interoperability in: A. Dogac, L. Kalinichenko, T. Ozsu, A. Sheth (Eds.):. Springer Verlag, 1998.
• 16: Andrew C. Myers , Barbara Liskov, A decentralized model for information flow control, Proceedings of the sixteenth ACM symposium on Operating systems principles, p.129-142, October 05-08, 1997, Saint Malo, France
• 17: Matunda Nyanchama , Sylvia Osborn, The role graph model and conflict of interest, ACM Transactions on Information and System Security (TISSEC), v.2 n.1, p.3-33, Feb. 1999 [doi>10.1145/300830.300832]
• 18: Sylvia L. Osborn, Information flow analysis of an RBAC system, Proceedings of the seventh ACM symposium on Access control models and technologies, June 03-04, 2002, Monterey, California, USA [doi>10.1145/507711.507738]
• 19: P. Roberts and J.-P. Verjus. Towards Autonomous Descriptions of Synchronization Modules. In Proc. of IFIP Congress, pages 981--986, 1977.
• 20: P. Ryan , J. McLean , J. Millen , V. Gligor, Non-Interference: Who Needs It?, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.237, June 11-13, 2001
• 21: Ravi S. Sandhu, The Typed Access Matrix Model, Proceedings of the 1992 IEEE Symposium on Security and Privacy, p.122, May 04-06, 1992
• 22: 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]
• 23: L. Snyder. Formal Models of Capability-Based Protection Systems. IEEE Transactions on Computers, C-30(3):172--181, March 1981.
• 24: Roshan K. Thomas, Team-based access control (TMAC): a primitive for applying role-based access controls in collaborative environments, Proceedings of the second ACM workshop on Role-based access control, p.13-19, November 06-07, 1997, Fairfax, Virginia, United States [doi>10.1145/266741.266748]
• 25: R. K. Thomas and R. S. Sandhu. Conceptual Foundations for a Model of Task-based Authorizations. In IEEE Computer Security Foundations Workshop, pages 66--79, 1994.
• 26: Anand R. Tripathi , Tanvir Ahmed , Richa Kumar, Specification of Secure Distributed Collaboration Systems, Proceedings of the The Sixth International Symposium on Autonomous Decentralized Systems (ISADS'03), p.149, April 09-11, 2003
• 27: Anand R. Tripathi , Tanvir Ahmed , Richa Kumar , Shremattie Jaman, Design of a Policy-Driven Middleware for Secure Distributed Collaboration, Proceedings of the 22 nd International Conference on Distributed Computing Systems (ICDCS'02), p.393, July 02-05, 2002
• 28: A. Zakinthinos , E. S. Lee, A general theory of security properties, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.94, May 04-07, 1997

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:
Design, Management, Security, Verification

Keywords:
finite-state based model checking, methodology for access control policy design, role based access control, security policy specification