Information flow property preserving transformation of UML interaction diagrams

ABSTRACT

We present an approach for secure information flow property preserving refinement and transformation of UML inspired interaction diagrams.The approach is formally underpinned by trace-semantics.The semantics is sufficiently expressive to distinguish underspecification from explicit nondeterminism. A running example is used to introduce the approach and to demonstrate that it is of practical value.

REFERENCES

• 1: H. Abie, D. B. Aredo, T. Kristoffersen, S. Mazaher, and T. Raguin. Integrating a security requirement language with UML.In UML 2004 - The Unified Modelling Language: Modelling Languages and Applications volume 3273 of Lecture Notes in Computer Science pages 350--364. Springer, 2004.
• 2: K. Alghathbar and D. Wijesekera. Consistent and complete access control policies in use cases. In UML 2003 - The Unified Modeling Language, Modeling Languages and Applications, 6th International Conference volume 2863 of Lecture Notes in Computer Science pages 373--387. Springer, 2003.
• 3: B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters 21(4):181--185, 1985.
• 4: David Basin , Jürgen Doser , Torsten Lodderstedt, Model driven security for process-oriented systems, Proceedings of the eighth ACM symposium on Access control models and technologies, June 02-03, 2003, Como, Italy [doi>10.1145/775412.775425]
• 5: A. Bossi, R. Focardi, C. Piazza, and S. Rossi. Refinement operators and information .ow security. In 1st International Conference on Software Engineering and Formal Methods (SEFM 2003)pages 44--53. IEEE Computer Society Press, 2003.
• 6: R. Breu, M. Hafner, B. Weber, and A. Novak. Model driven security for inter-organizational work flows in e-government.In E-Government: Towards Electronic Democracy, International Conference, TCGOV 2005 volume 3416 of Lecture Notes in Computer Science pages 122--133. Springer, 2005.
• 7: Carol C. Burt , Barrett R. Bryant , Rajeev R. Raje , Andrew Olson , Mikhail Auguston, Model Driven Security: Unification of Authorization Models for Fine-Grain Access Control, Proceedings of the 7th International Conference on Enterprise Distributed Object Computing, p.159, September 16-19, 2003
• 8: Thuong Doan , Steven Demurjian , T. C. Ting , Andreas Ketterl, MAC and UML for secure software design, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA [doi>10.1145/1029133.1029144]
• 9: Pete Epstein , Ravi Sandhu, Towards a UML based approach to role engineering, Proceedings of the fourth ACM workshop on Role-based access control, p.135-143, October 28-29, 1999, Fairfax, Virginia, United States [doi>10.1145/319171.319184]
• 10: E. Fernández-Medina and M. Piattini. Extending OCL for secure database development.In UML 2004-The Unified Modelling Language: Modelling Languages and Applications. 7th International Conference volume 3273 of Lecture Notes in Computer Science pages 380--394.Springer, 2004.
• 11: P. Giorgini, F. Massacci,and J. Mylopoulos. Requirement engineering meets security:a case study on modelling secure electronic transactions by VISA and mastercard.In Conceptual Modeling - ER 2003, 22nd International Conference on Conceptual Modeling volume 2813 of Lecture Notes in Computer Science pages 263--276. Springer, 2003.
• 12: O. M. Group. OMG Unified Modeling Language Specification v.1.5. Version 1.5.OMG Document formal/03-03-01, 2003.
• 13: O. M. Group. UML 2.0 Superstructure Specification. OMG Adopted Sepci .cation ptc/03-08-02, 2003.
• 14: O. Haugen, K. E. Husa, R. K. Runde,and K. Stolen. Why timed sequence diagrams require three-event semantics. Research Report 309,Department of Informatics,University of Oslo, 2004.
• 15: O. Haugen, K. E. Husa, R. K. Runde,and K. Stolen. STAIRS towards formal design with sequence diagrams. Journal of Software and Systems Modeling 4(4):355--367, 2005.
• 16: O. Haugen and K. Stolen. STAIRS .steps to analyse interactions with re .nement semantics. In Sixth International Conference on UML (UML'2003) Lecture Notes in Computer Science,pages 388--402. Springer, 2003.
• 17: Maritta Heisel , Andreas Pfitzmann , Thomas Santen, Confidentiality-Preserving Refinement, Proceedings of the 14th IEEE Workshop on Computer Security Foundations, p.295, June 11-13, 2001
• 18: R. Heldal and F. Hultin. Bridging model-based and language-based security.In Computer Security -ESORICS 2003, 8th European Symposium on Research in Computer Security volume 2808 of Lecture Notes in Computer Science pages 235--252. Springer, 2003.
• 19: C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica 1:271--281, 1972.
• 20: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 21: J. Jacob. On the derivation of secure components. In Security and Privacy pages 242--247. IEEE Computer Society Press, 1989.
• 22: J. Jürjens. Secure systems development with UML Springer, 2005.
• 23: Manuel Koch , Francesco Parisi-Presicce, Formal access control analysis in the software development process, Proceedings of the 2003 ACM workshop on Formal methods in security engineering, p.67-76, October 30, 2003, Washington, D.C. [doi>10.1145/1035429.1035437]
• 24: Torsten Lodderstedt , David A. Basin , Jürgen Doser, SecureUML: A UML-Based Modeling Language for Model-Driven Security, Proceedings of the 5th International Conference on The Unified Modeling Language, p.426-441, September 30-October 04, 2002
• 25: Heiko Mantel, Possibilistic Definitions of Security - An Assembly Kit, Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), p.185, July 03-05, 2000
• 26: Heiko Mantel, Preserving Information Flow Properties under Refinement, Proceedings of the 2001 IEEE Symposium on Security and Privacy, p.78, May 14-16, 2001
• 27: O. M. G. A. B. ORMSC. Model Driven Architecture (MDA). Document number ormsc/2001-07-01, 2001.
• 28: A. Poniszewska-Maranda, G. Goncalves, and F. Hemery. Representation of extended RBAC model using UML language.In SOFSEM 2005: Theory and Practice of Computer Science, 31st Conference on Current Trends in Theory and Practice of Computer Science volume 3381 of Lecture Notes in Computer Science pages 413--417.Springer, 2005.
• 29: Indrakshi Ray , Na Li , Robert France , Dae-Kyoo Kim, Using uml to visualize role-based access control constraints, 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.990054]
• 30: A. W. Roscoe, CSP and determinism in security modelling, Proceedings of the 1995 IEEE Symposium on Security and Privacy, p.114, May 08-10, 1995
• 31: F. Seehusen and K. Stolen. Information flow property preserving transformation of UML interaction diagrams. Technical report STF90 A06030,SINTEF ICT, 2006.
• 32: J. L. Vivas, J. A. Montenegro, and J. Lopez. Towards a business process-driven framework for security engineering with the UML. In Information Security, 6th International Conference, ISC 2003 volume 2851 of Lecture Notes in Computer Science pages 381--395. Springer, 2003.

INDEX TERMS

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

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

General Terms:
Design, Languages, Security

Keywords:
UML, information flow security, model driven architecture, refinement, transformation