Advertisement

Integrating a Model-Driven Approach and Formal Verification for the Development of Secure Service Applications

  • Marian Borek
  • Kuzman Katkalov
  • Nina Moebius
  • Wolfgang Reif
  • Gerhard Schellhorn
  • Kurt StenzelEmail author
Part of the Texts & Monographs in Symbolic Computation book series (TEXTSMONOGR)

Abstract

We present SecureMDD, a development method for secure service applications that integrates a model-driven approach with formal specification techniques using abstract state machines (ASMs), refinement to code and verification with the interactive theorem prover KIV. A larger case study is used to highlight various aspects of the method with a focus on services and their formal verification.

References

  1. 1.
    Alam, M.M., Breu, R., Breu, M.: Model driven security for web services (MDS4WS). In: 8th International Multitopic Conference, 2004. Proceedings of INMIC 2004, pp. 498–505. IEEE, Piscataway (2004)Google Scholar
  2. 2.
    Anderson, R.J., Needham, R.M.: Programming satan’s computer. In: Computer Science Today, vol. 1000, pp. 426–440. Springer, Heidelberg (1995)Google Scholar
  3. 3.
    Armando, A., Arsac, W., Avanesov, T., Barletta, M., Calvi, A., Cappai, A., Carbone, R., Chevalier, Y., Compagna, L., Cúellar, J., et al.: The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In: Proceedings of TACAS 2012 – Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 7214. Springer, Heidelberg (2012)Google Scholar
  4. 4.
    Baina, K., Benatallah, B., Casati, F., Toumani, F.: Model-driven web service development. In: Advanced Information Systems Engineering, pp. 527–543. Springer, Heidelberg (2004)Google Scholar
  5. 5.
    Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development with KIV. In: Fundamental Approaches to Software Engineering. Lecture Notes in Computer Science, vol. 1783. Springer, Heidelberg (2000)Google Scholar
  6. 6.
    Basin, D.A., Mödersheim, S., Viganò, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181–208 (2005)CrossRefGoogle Scholar
  7. 7.
    Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from UML models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15, 39–91 (2006)CrossRefGoogle Scholar
  8. 8.
    Bella, G.: Mechanising a protocol for smart cards. In: Proceedings of e-Smart 2001, International Conference on Research in Smart Cards. Lecture Notes in Computer Science, vol. 2140. Springer, Heidelberg (2001)Google Scholar
  9. 9.
    Bella, G., Massacci, F., Paulson, L.C.: Verifying the SET purchase protocols. J. Automat. Reas. 36(1–2), 5–37 (2006)zbMATHCrossRefGoogle Scholar
  10. 10.
    Blanchet, B.: Automatic verification of correspondences for security protocols. J. Comput. Secur. 17(4), 363–434 (2009)Google Scholar
  11. 11.
    Borek, M., Moebius, N., Stenzel, K., Reif, W.: Model-driven development of secure service applications. In: 2012 35th Annual IEEE Software Engineering Workshop (SEW), pp. 62–71. IEEE, Piscataway (2012)Google Scholar
  12. 12.
    Borek, M., Moebius, N., Stenzel, K., Reif, W.: Model checking of security-critical applications in a model driven approach. In: Software Engineering and Formal Methods. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Borek, M., Moebius, N., Stenzel, K., Reif, W.: Security requirements formalized with ocl in a model-driven approach. In: 2013 IEEE Model-Driven Requirements Engineering Workshop (MoDRE). IEEE, Piscataway (2013)Google Scholar
  14. 14.
    Börger, E., Sörensen, O.: BPMN core modeling concepts: inheritance-based execution semantics. In: Handbook of Conceptual Modeling. Theory, Practice, and Research Challenges, pp. 287–332. Springer, Heidelberg (2011)Google Scholar
  15. 15.
    Börger, E., Stärk, R.F.: Abstract State Machines—A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)zbMATHCrossRefGoogle Scholar
  16. 16.
    Börger, E., Thalheim, B.: Modeling workflows, interaction patterns, web services and business processes: the ASM-based approach. In: Proceedings of ABZ 2008. Lecture Notes in Computer Science, vol. 5238. Springer, Heidelberg (2008)Google Scholar
  17. 17.
    Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)CrossRefGoogle Scholar
  18. 18.
    Bushager, A., Zwolinski, M.: Modelling smart card security protocols in systemC TLM. In: IEEE/IFIP 8th International Conference on Embedded and Ubiquitous Computing, pp. 637–643. IEEE Computer Society, Piscataway (2010)Google Scholar
  19. 19.
    Deubler, M., Grünbauer, J., Jürjens, J., Wimmel, G.: Sound development of secure service-based systems. In: Proceedings of the 2nd International Conference on Service Oriented Computing, pp. 115–124. ACM, New York (2004)Google Scholar
  20. 20.
    Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.2. IETF Network Working Group. http://www.ietf.org/rfc/rfc5246.txt (2008)
  21. 21.
    Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of 22th IEEE Symposium on Foundations of Computer Science. IEEE, Piscataway (1981)Google Scholar
  22. 22.
    Foster, H., Gönczy, L., Koch, N., Mayer, P., Montangero, C., Varró, D.: UML extensions for service-oriented systems. In: Rigorous Software Engineering for Service-Oriented Systems, pp. 35–60. Springer, Heidelberg (2011)Google Scholar
  23. 23.
    Grandy, H., Stenzel, K., Reif, W.: Object-oriented verification kernels for secure Java applications. In: Aichering, B., Beckert, B. (eds.) SEFM 2005 – 3rd IEEE International Conference on Software Engineering and Formal Methods. IEEE, Piscataway (2005)Google Scholar
  24. 24.
    Gronmo, R., Skogan, D., Solheim, I., Oldevik, J.: Model-driven web services development. In: 2004 IEEE International Conference on e-Technology, e-Commerce and e-Service, 2004. EEE’04, pp. 42–45. IEEE, Piscataway (2004)Google Scholar
  25. 25.
    Grünbauer, J., Hollmann, H., Jürjens, J., Wimmel, G.: Modelling and verification of layered security protocols: a bank application. In: Proceedings of SAFECOMP 2003. Lecture Notes in Computer Science, vol. 2788. Springer, Heidelberg (2003)Google Scholar
  26. 26.
    Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying smart card applications: an ASM approach. In: International Conference on integrated Formal Methods (iFM) 2007. Lecture Notes in Computer Science, vol. 4591. Springer, Heidelberg (2007)Google Scholar
  27. 27.
    Huber, F., Molterer, S., Rausch, A., Schatz, B., Sihling, M., Slotosch, O.: Tool supported specification and simulation of distributed systems. In: Proceedings, International Symposium on Software Engineering for Parallel and Distributed Systems, 1998, pp. 155–164. IEEE, Piscataway (1998)Google Scholar
  28. 28.
    Java Card 2.2.2 Application Programming Interfaces: http://www.oracle.com/technetwork/java/\\javacard/specs-138637.html (2006)
  29. 29.
    Jensen, J., Jaatun, M.G.: Security in model driven development: a survey. In: Sixth International Conference on Availability, Reliability and Security, ARES 2011. Lecture Notes in Computer Science, pp. 704–709. Springer, Heidelberg (2011)Google Scholar
  30. 30.
    Jones, C., Woodcock, J. (eds.): Form. Asp. Comput. 20(1) (2008)Google Scholar
  31. 31.
    Jürjens, J.: Developing high-assurance secure systems with UML: a smartcard-based purchase protocol. In: IEEE International Symposium on High Assurance Systems Engineering. IEEE, Piscataway (2004)Google Scholar
  32. 32.
    Jürjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  33. 33.
    Kasal, K., Heurix, J., Neubauer, T.: Model-driven development meets security: an evaluation of current approaches. In: 44th Hawaii International Conference on System Sciences (HICSS), pp. 1–9. IEEE Computer Society, Piscataway (2011)Google Scholar
  34. 34.
    Katkalov, K., Moebius, N., Stenzel, K., Borek, M., Reif, W.: Model-driven testing of security protocols with secureMDD. In: Fifth IFIP International Conference on New Technologies, Mobility and Security (NTMS 2012). IEEE, Piscataway (2012)Google Scholar
  35. 35.
    Kroiss, C., Koch, N., Knapp, A.: UWE4JSF: a model-driven generation approach for web applications. In: 3rd Workshop on The Web and Requirements Engineering at ICWE 2012. Lecture Notes in Computer Science, vol. 5648, pp. 493–496. Springer, Heidelberg (2009)Google Scholar
  36. 36.
    Lopez Pimental, J.C., Monroy, R.: Formal support to security protocol development: a survey. Computacion y Sistemas 12(1), 89–108 (2008)Google Scholar
  37. 37.
    Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)Google Scholar
  38. 38.
    Mayer, P., Schroeder, A., Koch, N.: MDD4SOA: model-driven service orchestration. In: Proceedings of 12th IEEE International EDOC Conference (EDOC 2008). IEEE, Piscataway (2008)Google Scholar
  39. 39.
    Meadows, C.: The NRL protocol analyzer: an overview. J. Logic Program. 26(2), 113–131 (1996)zbMATHCrossRefGoogle Scholar
  40. 40.
    Memon, M., Hafner, M., Breu, R.: SECTISSIMO: a platform-independent framework for security services. In: Proceedings of the First International Modeling Security Workshop. CEUR Workshop Proceedings, vol. 413. http://ceur-ws.org/Vol-413/ (2008)
  41. 41.
    Mitra, N., Lafon, Y.: SOAP Version 1.2. W3C (2007)Google Scholar
  42. 42.
    Moebius, N., Stenzel, K., Reif, W.: Modeling security-critical applications with UML in the SecureMDD approach. Int. J. Adv. Softw. 1(1), 59–79 (2008)Google Scholar
  43. 43.
    Moebius, N., Stenzel, K., Grandy, H., Reif, W.: Model-driven code generation for secure smart card applications. In: 20th Australian Software Engineering Conference. IEEE, Piscataway (2009)Google Scholar
  44. 44.
    Moebius, N., Stenzel, K., Grandy, H., Reif, W.: SecureMDD: a model-driven development method for secure smart card applications. In: Workshop on Secure Software Engineering, SecSE, at ARES 2009. IEEE, Piscataway (2009)Google Scholar
  45. 45.
    Moebius, N., Stenzel, K., Reif, W.: Formal verification of application-specific security properties in a model-driven approach. In: Proceedings of ESSoS 2010 - International Symposium on Engineering Secure Software and Systems. Lecture Notes in Computer Science, vol. 5965. Springer, Heidelberg (2010)Google Scholar
  46. 46.
    Moebius, N., Stenzel, K., Borek, M., Reif, W.: Incremental development of large, secure smart card applications. In: Proceedings of the Workshop on Model-Driven Security. ACM, New York (2012)CrossRefGoogle Scholar
  47. 47.
    Mordani, R., Chinnici, R., Hadley, M.: The Java API for XML-Based Web Services (JAX-WS) 2.0. JCP (2006)Google Scholar
  48. 48.
    Murdoch, S.J., Drimer, S., Anderson, R., Bond, M.: Chip and PIN is broken. In: Proceedings of the 2010 IEEE Symposium on Security and Privacy, pp. 433–446. IEEE, Piscataway (2010)Google Scholar
  49. 49.
    Nadalin, A., Kaler, C., Hallam-Baker, P., Monzillo, R.: Web Services Security: SOAP Message Security 1.0. OASIS (2004)Google Scholar
  50. 50.
    Nadalin, A., Goodner, M., Gudgin, M., Barbir, A., Granqvist, H.: WS-SecurityPolicy 1.2. OASIS (2006)Google Scholar
  51. 51.
    Nakamura, Y., Tatsubori, M., Imamura, T., Ono, K.: Model-driven security based on a web services security architecture. In: IEEE International Conference on Services Computing, pp. 7–15. IEEE, Piscataway (2005)Google Scholar
  52. 52.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)zbMATHCrossRefGoogle Scholar
  53. 53.
    Object Management Group (OMG): Meta Object Facility (MOF) 2.0 Query/View/Transformation Specification, Version 1.1. http://www.omg.org/spec/QVT/1.1/ (2011)
  54. 54.
    Paulson, L.C.: The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 85–128 (1998)Google Scholar
  55. 55.
    Ray, M., Dispensa, S.: Renegotiating TLS. Technical Report, PhoneFactor Inc. (2009)Google Scholar
  56. 56.
    Schroeder, A., Mayer, P.: Verifying interaction protocol compliance of service orchestrations. In: Proceedings of the 6th International Conference on Service-Oriented Computing. Lecture Notes in Computer Science, vol. 5364. Springer, Heidelberg (2008)Google Scholar
  57. 57.
    Sheng, Q.Z., Benatallah, B.: Contextuml: a uml-based modeling language for model-driven development of context-aware web services. In: International Conference on Mobile Business, 2005. ICMB 2005, pp. 206–212. IEEE, Piscataway (2005)Google Scholar
  58. 58.
    Smith, S., Beaulieu, A., Greg Phillips, W.: Modeling and verifying security protocols using UML 2. In: International Systems Conference (SysCon), pp. 72–79. IEEE Computer Society, Piscataway (2011)Google Scholar
  59. 59.
    Stenzel, K., Moebius, N., Reif, W.: Formal verification of QVT transformations for code generation. In: 14th International Conference on Model Driven Engineering Languages and Systems, MODELS 2011. Lecture Notes in Computer Science, vol. 6981. Springer, Heidelberg (2011)Google Scholar
  60. 60.
    Woodcock, J.: First steps in the verified software grand challenge. IEEE Comput. 39(10), 57–64 (2006)CrossRefGoogle Scholar
  61. 61.

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Marian Borek
    • 1
  • Kuzman Katkalov
    • 1
  • Nina Moebius
    • 1
  • Wolfgang Reif
    • 1
  • Gerhard Schellhorn
    • 1
  • Kurt Stenzel
    • 1
    Email author
  1. 1.Institute for Software and Systems EngineeringAugsburg UniversityAugsburgGermany

Personalised recommendations