Sound development of secure service-based systems

ABSTRACT

<i>Service-based software systems</i> are a useful concept recently developed to support the development of systems offering functions (the so-called <i>services</i>) which may be interrelated or may mutually depend on each other. Although appealing from a practical point of view, the development of service-based software for security-critical systems is, unfortunately, not well understood. Services may easily interact with each other in a way which may have unforeseen consequences on the various security properties provided. In this work, we propose a method for facilitating the development of security-critical service-based software systems using the computer-aided systems engineering tool A<sc>uto</sc>F<sc>ocus</sc> based on the formal method F<sc>ocus</sc>. We explain our method at the example of a service-based system from the automotive domain.

REFERENCES

• 1: Ross J. Anderson, Security Engineering: A Guide to Building Dependable Distributed Systems, John Wiley & Sons, Inc., New York, NY, 2001
• 2: Franco Arcieri , Fabio Fioravanti , Enrico Nardelli , Maurizio Talamo, A Layered IT Infrastructure for Secure Interoperability in Personal Data Registry Digital Government Services, Proceedings of the 14th International Workshop on Research Issues on Data Engineering: Web Services for E-Commerce and E-Government Applications (RIDE'04), p.95-102, March 28-29, 2004
• 3: Luciano Baresi , Reiko Heckel , Sebastian Thöne , Dániel Varró, Modeling and validation of service-oriented architectures: application vs. style, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 4: M. Broy. Modeling Services and Layered Architectures. In H. König, M. Heiner, and A. Wolisz, editors, Formal Techniques for Networked and Distributed Systems, volume 2767 of Lecture Notes in Computer Science, pages 48--61. springer, 2003.
• 5: M. Broy, F. Huber, and B. Schätz. AutoFocus -- Ein Werkzeugprototyp zur Entwicklung eingebetteter Systeme. Informatik Forschung und Entwicklung, 14(3):121--134, 1999.
• 6: Manfred Broy , Ketil Stølen, Specification and development of interactive systems: focus on streams, interfaces, and refinement, Springer-Verlag New York, Inc., Secaucus, NJ, 2001
• 7: G. Denker, L. Kagal, T. W. Finin, M. Paolucci, and K. P. Sycara. Security for DAML web services: Annotation and matchmaking. In International Semantic Web Conference, pages 335--350, 2003.
• 8: Martin Deubler , Johannes Grunbauer , Gerhard Popp , Guido Wimmel , Christian Salzmann, Tool Supported Development of Service-Based Systems, Proceedings of the 11th Asia-Pacific Software Engineering Conference (APSEC'04), p.99-108, November 30-December 03, 2004 [doi>10.1109/APSEC.2004.101]
• 9: Matthew B. Dwyer , George S. Avrunin , James C. Corbett, Patterns in property specifications for finite-state verification, Proceedings of the 21st international conference on Software engineering, p.411-420, May 16-22, 1999, Los Angeles, California, United States [doi>10.1145/302405.302672]
• 10: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 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 I.-Y. Song, S. Liddle, T. Ling, and P. Scheuermann, editors, 22nd International Conference on Conceptual Modeling (ER 2003), volume 2813 of LNCS, pages 263--276. Springer, 2003.
• 12: J. Grünbauer, H. Hollmann, J. Jürjens, and G. Wimmel. Modelling and verification of layered security protocols: A bank application. In Computer Safety, Reliability, and Security (SAFECOMP 2003), volume 2788 of LNCS, pages 116--129. Springer, 2003.
• 13: S. Molterer, A. Rausch, B. Schätz F. Hube , O. Slotosch, Tool Supported Specification and Simulation of Distributed Systems, Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems, p.155, April 20-21, 1998
• 14: ITU. ITU-TS Recommendation Z.120: Message Sequence Chart (MSC). ITU-TS, Geneva, 1996.
• 15: J. Jürjens. Secure Systems Development with UML. Springer, 2004.
• 16: Jan Jürjens , Guido Wimmel, Security Modelling for Electronic Commerce: The Common Electronic Purse Specifications, Proceedings of the IFIP Conference on Towards The E-Society: E-Commerce, E-Business, E-Government, p.489-506, October 03-05, 2001
• 17: Kees Leune , Willem-Jan van den Heuvel , Mike Papazoglou, Exploring a Multi-Faceted Framework for SoC: How to Develop Secure Web-Service Interactions?, Proceedings of the 14th International Workshop on Research Issues on Data Engineering: Web Services for E-Commerce and E-Government Applications (RIDE'04), p.56-61, March 28-29, 2004
• 18: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 19: MEWADIS Projekt Homepage. MEWADIS website at http://www4.in.tum.de/~mewadis. In German.
• 20: Open Services Gateway Inititative. OSGitexttrademark Service Platform Specification. Release 3, March 2003, http://www.osgi.org.
• 21: B. Orriëns, J. Yang, and M. P. Papazoglou. Model driven service composition. In M. E. Orlowska, S. Weerawarana, M. P. Papazoglou, and J. Yang, editors, First International Conference on Service-Oriented Computing (ICSOC 2003), volume 2910 of LNCS, pages 75--90, Trento, Italy, December 15--18 2003. Springer.
• 22: OSGi Alliance. OSGI World Congress 2003. http://2003.osgiworldcongress.com.
• 23: Jan Philipps , Oscar Slotosch, The Quest for Correct Systems: Model Checking of Diagrams and Datatypes, Proceedings of the Sixth Asia Pacific Software Engineering Conference, p.449, December 07-10, 1999
• 24: Halvard Skogsrud , Boualem Benatallah , Fabio Casati, Model-Driven Trust Negotiation for Web Services, IEEE Internet Computing, v.7 n.6, p.45-52, November 2003 [doi>10.1109/MIC.2003.1250583]
• 25: Oscar Slotosch, QUEST: Overview over the Project, Proceedings of the International Workshop on Current Trends in Applied Formal Method: Applied Formal Methods, p.346-350, October 07-09, 1998
• 26: Simon Thompson, The Haskell: The Craft of Functional Programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 27: Von Welch , Frank Siebenlist , Ian Foster , John Bresnahan , Karl Czajkowski , Jarek Gawor , Carl Kesselman , Sam Meder , Laura Pearlman , Steven Tuecke, Security for Grid Services, Proceedings of the 12th IEEE International Symposium on High Performance Distributed Computing (HPDC'03), p.48, June 22-24, 2003
• 28: Guido Wimmel , Jan Jürjens, Specification-Based Test Generation for Security-Critical Systems Using Mutations, Proceedings of the 4th International Conference on Formal Engineering Methods: Formal Methods and Software Engineering, p.471-482, October 21-25, 2002
• 29: Guido Wimmel , Alexander Wisspeintner, Extended description techniques for security engineering, Proceedings of the 16th international conference on Information security: Trusted information: the new decade challenge, June 11-13, 2001, Paris, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Computer-aided software engineering (CASE)

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
        D.2.11 Software Architectures
            Subjects: Domain-specific architectures

General Terms:
Design

Keywords:
UML, autofocus, automotive, model-based software engineering, security, service-based systems