[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Security patterns modeling and formalization for pattern-based development of secure software systems

  • Original Paper
  • Published:
Innovations in Systems and Software Engineering Aims and scope Submit manuscript

Abstract

Pattern-based development of software systems has gained more attention recently by addressing new challenges such as security and dependability. However, there are still gaps in existing modeling languages and/or formalisms dedicated to modeling design patterns and the way how to reuse them in the automation of software development. The solution envisaged here is based on combining metamodeling techniques and formal methods to represent security patterns at two levels of abstraction to fostering reuse. The goal of the paper is to advance the state of the art in model and pattern-based security for software and systems engineering in three relevant areas: (1) develop a modeling language to support the definition of security patterns using metamodeling techniques; (2) provide a formal representation and its associated validation mechanisms for the verification of security properties; and (3) derive a set of guidelines for the modeling of security patterns within the integration of these two kinds of representations.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

Notes

  1. http://www.semcomdt.org.

  2. http://www.teresa-project.org/.

References

  1. Yoder J, Barcalow J (1998) Architectural patterns for enabling application security. In: Conference on pattern languages of programs (PLoP 1997)

  2. Schumacher M (2003) Security engineering with patterns—origins, theoretical models, and new applications, vol 2754 of Lecture notes in computer science. Springer http://www.springerlink.com/openurl.asp?genre=issue&issn=0302-9743&volume=2754

  3. Selic B (2003) The pragmatics of model-driven development. IEEE Softw 20(5):19–25

    Article  Google Scholar 

  4. Atkinson C, Kühne T (2003) Model-driven development: a metamodeling foundation. IEEE Softw 20(5):36–41

    Article  Google Scholar 

  5. Uzunov AV, Fernandez EB, Falkner K (2012) Securing distributed systems using patterns: a survey. J Comput Secur 31(5):681–703

    Article  Google Scholar 

  6. Hamid B, Geisel J, Ziani A, Bruel J, Perez J (2013) Model-driven engineering for trusted embedded systems based on security and dependability patterns. In: SDL Forum, pp 72–90

  7. The TLS protocol version 1.2, rfc5246 (2008)

  8. Hamid B, Gürgens S, Jouvray C, Desnos N (2011) Enforcing S&D pattern design in RCES with modeling and formal approaches. In: Whittle J (ed) ACM/IEEE international conference on model driven engineering languages and systems (MODELS), Wellington, 16/10/2011-21/10/2011, vol 6981, Springer, pp 319–333

  9. Giacomo VD et al (2008) Using security and dependability patterns for reaction processes. IEEE Computer Society, pp 315–319

  10. Yoshioka N, Washizaki H, Maruyama K (2008) A survey of security patterns. Prog Inform 5:35–47

    Article  Google Scholar 

  11. Daniels F (1997) The reliable hybrid pattern: a generalized software fault tolerant design pattern. In: Proceedings of pattern language of programs, pp 1–9

  12. Tichy M et al (2004) Design of self-managing dependable systems with uml and fault tolerance patterns, ACM, pp 05–109

  13. Maña A, Fernandez E, Ruiz J, Rudolph C (2013) Towards computer-oriented security patterns. In: The 20th international conference on pattern languages of programs PLoP13

  14. Guennec AL, Sunyé G, Jézéquel J-M (2000) Precise modeling of design patterns. In: Proceedings of the unified modeling language (UML 00), vol 1939, Springer, pp 482–496

  15. Kim D-K, France R, Ghosh S, Song E (2004) A uml-based meta-modeling language to specify design patterns. In: Proceedings of the Workshop on Software Model Engineering (WiSME) at UML 2003

  16. Gasparis AHEE, Nicholson J (2008) Lepus3: an object-oriented design description language. In: Stapleton G et al (eds) DIAGRAMS, LNAI 5223, pp 364–367

  17. Gamma E, Helm R, Johnson RE, Vlissides J (1995) Design patterns: elements of reusable object-oriented software. Addison-Wesley, Longman Publishing Co., Inc., Boston

    MATH  Google Scholar 

  18. Douglass BP (1998) Real-time UML: developing efficient objects for embedded systems. Addison-Wesley, Longman Publishing Co., Inc., Boston

    Google Scholar 

  19. Mapelsden JGD, Hosking J (2002) Design pattern modelling and instantiation using dpml. In: CRPIT ’02: Proceedings of the 40th international conference on tools Pacific, Australian Computer Society, Inc., pp 3–11

  20. Serrano D, Mana A, Sotirious A-D (2008) Towards precise and certified security patterns. In: Proceedings of 2nd international workshop on secure systems methodologies using patterns (Spattern 2008), IEEE Computer Society, pp 287–291

  21. Boussaidi GE, Mili H (2005) Representing and applying design patterns: what is the problem?. In: Proceedings of the ACM/IEEE 8th international conference on model driven engineering languages and systems (MODELS), Springer, pp 186–200

  22. Maña A, Damiani E, Gürgens S, Spanoudakis G (2014) Extensions to pattern formats for cyber physical systems. In: Proceedings of the 31st conference on pattern languages of programs (PLoP 14)

  23. Jürjens J (2002) Umlsec: extending uml for secure systems development. In: Proceedings of the 5th international conference on the unified modeling language, UML ’02, Springer-Verlag, London, UK, pp 412–425

  24. Lodderstedt T, Basin D, Doser J (2002) Secureuml: a uml-based modeling language for model-driven security. In: Proceedings of the 5th international conference on the unified modeling language, UML ’02, Springer-Verlag, London, UK, pp 426–441

  25. Hamid B, Radermacher A, Lanusse A, Jouvray C, Gérard S, Terrier F (2008) Designing fault-tolerant component based applications with a model driven approach. In: The IFIP workshop on software technologies for future embedded and ubiquitous systems (SEUS). Lecture notes in computer science, Springer, pp 9–20

  26. Basin D, Doser J, Lodderstedt T (2006) Model driven security: from UML models to access control infrastructures. ACM Trans Softw Eng Methodol (TOSEM) 15(1):39–91

    Article  Google Scholar 

  27. Basin D, Clavel M, Doser J, Egea M (2009) Automated analysis of security-design models. Inf Softw Technol 51:815–831

    Article  Google Scholar 

  28. Jensen J, Jaatun MG (2011) Security in model driven development: a survey. In: Proceedings of the 2011 6th international conference on availability, reliability and security. ARES ’11, IEEE Computer Society, pp 704–709

  29. Lucio L, Zhang Q, Nguyen PH, Amrani M, Klein J, Vangheluwe H, Traon YL (2014) Advances in model-driven security. Adv Comput 93:103–152

    Article  Google Scholar 

  30. McDonald J, Oualha N, Puccetti A, Hecker A, Planchon F (2013) Application of ebios for the risk assessment of ict use in electrical distribution sub-stations. In: PowerTech (POW- ERTECH), IEEE, pp 1–6

  31. Braber F, Hogganvik I, Lund MS, Stlen K, Vraalsen F (2007) Model-based security analysis in seven steps—a guided tour to the corasc method. BT Technol J 25(1):101–117

    Article  Google Scholar 

  32. Srivatanakul T, Clark JA, Polack F (2004) Effective security requirements analysis: Hazop and use cases, information security. Lect Notes Comput Sci 3225:416–427

    Article  Google Scholar 

  33. Schneier B Attack trees, modeling security threats. Dr. Dobbs J December 1999

  34. Rodano M, Giammarc K (2013) A formal method for evaluation of a modeled system architecture. Procedia Comput Sci 20:210–215

    Article  Google Scholar 

  35. Landwehr CE (1981) Formal models for computer security. ACM Comput Surv 13:247–278

    Article  Google Scholar 

  36. Devanbu P, Stubblebine S, Premkumar SS, Devanbu T (2000) Software engineering for security—a roadmap. In: Proceedings of the conference on the future of software engineering, ICSE ’00, ACM, pp 227–239

  37. Lee AJ, Boyer JP, Olson LE, Gunter CA (2006) Defeasible security policy composition for web services. In: Proceedings of the 4th ACM workshop on formal methods in security, ACM, pp 45–54

  38. Bruns G, Dantas DS, Huth M (2007) A simple and expressive semantic framework for policy composition in access control. In: Proceedings of the 2007 ACM workshop on formal methods in security engineering, ACM, pp 12–21

  39. Bruns G, Huth M (2011) Access control via belnap logic: intuitive, expressive, and analyzable policy composition. ACM Trans Inf Syst Secur (TISSEC) 14(1):1–27

    Article  Google Scholar 

  40. Burrows M, Abadi M, Needham R (1990) A logic of authentication. ACM Trans Comput Syst 8(1):18–36

    Article  MATH  Google Scholar 

  41. Paulson L (1996) Proving properties of security protocols by induction. Technical report 409, Computer Laboratory, University of Cambridge

  42. Lowe G (1995) An attack on the Needham-Schroeder public-key protocol. Inf Process Lett 56(3):131–133

    Article  MATH  Google Scholar 

  43. Roscoe B, Ryan P, Schneider S, Goldsmith M, Lowe G (2000) The modelling and analysis of security protocols. Addison Wesley, Boston

    Google Scholar 

  44. AVISPA The HLPSL tutorial. A beginner’s guide to modelling and analysing internet security protocols. http://www.avispa-project.org

  45. Chevalier Y, Compagna L, Cuellar J, Hankes DP, Mantovani J, Mdersheim S, Vigneron L (2004) A high level protocol specification language for industrial security-sensitive protocols. In: Workshop on specification and automated processing of security requirements (SAPS 2004)

  46. Gürgens S, Rudolph C Security analysis of (un-) fair non-repudiation protocols. In: Proceedings of Formal Aspects of Security, vol 2629, Springer 2003, pp 97–114

  47. Gürgens S, Rudolph C, Scheuermann D, Atts M, Plaga R (2007) Security evaluation of scenarios based on the TCG’s TPM specification. In: Biskup J, Lopez J (eds) Computer security—ESORICS 2007, vol 4734 of Lecture notes in computer science, Springer Verlag

  48. Fuchs A, Gürgens S, Apvrille L, Pedroza G (2010) D3.4.3—on-board architecture and protocols verification. Technical report. EVITA-Project

  49. Gürgens S, Ochsenschläger P, Rudolph C (2005) On a formal framework for security properties. Int Comput Stand Interface J (CSI). Special issue on formal methods, techniques and tools for secure and reliable applications 27(5):457–466

  50. Zdun U, Avgeriou P (2005) Modeling architectural patterns using architectural primitives. In: Proceedings of the 20th annual ACM SIGPLAN conference on object-oriented programming, systems, languages, and applications, OOPSLA ’05, ACM, New York, NY, USA, pp 133–146

  51. Ziani A, Hamid B, Trujillo S (2011) Towards a unified meta-model for resources-constrained embedded systems. In: 37th EUROMICRO conference on software engineering and advanced applications, IEEE, pp 485–492

  52. OMG, Omg (2008) A uml profile for marte: modeling and analysis of real-time embedded systems,beta 2. http://www.omgmarte.org/Documents/Specifications/08-06-09.pdf

  53. OMG, OCL 2.2 Specification (2010) http://www.omg.org/spec/OCL/2.2

  54. Avizienis A, Laprie J-C, Randell B, Landwehr C (2004) Basic concepts and taxonomy of dependable and secure computing. IEEE Trans Dependable Secure Comput 1:11–33

    Article  Google Scholar 

  55. Schumacher M, Fernandez-Buglioni E, Hybertson D, Buschmann F, Sommerlad P (2006) Security patterns: integrating security and systems engineering. John Wiley & Sons, Chichester

    Google Scholar 

  56. Fuchs A, Gürgens S, Rudolph C (2010) A formal notion of trust—enabling reasoning about security properties. In: Preceedings of 4th IFIP WG 11.1 international conference on trust management

  57. Fuchs A, Gürgens S, Lincke N, Weber D (2012) D5.2 & d5.4—application of formal validation to relevant examples & guidelines for platform dependent implementation v1. Technical report. TERESA-Project

  58. Gürgens S, Ochsenschläger P, Rudolph C (2003) Parameter confidentiality. In: Informatik 2003—Teiltagung Sicherheit, Gesellschaft für Informatik

  59. Gürgens S, Ochsenschläger P, Rudolph C (2002) Authenticity and provability—a formal framework. In: Infrastructure security conference InfraSec 2002, vol 2437 of Lecture notes in computer science. Springer Verlag, pp 227–245

  60. Gürgens S, Ochsenschläger P, Rudolph C (2005) Abstractions preserving parameter confidentiality. In: European symposium on research in computer security (ESORICS 2005), pp 418–437

  61. Fuchs A, Gürgens S (2011) D05.1 Formal models and model composition. Technical report. ASSERT4SOA Project

  62. Fuchs A, Gürgens S (2012) D5.1v2.5—formal validation approach. Technical report. TERESA-Project

  63. Fuchs A, Gürgens S, Rudolph C (2011) Formal notions of trust and confidentiality—enabling reasoning about system security. J Inf Process 19:274–291

    Google Scholar 

  64. Powel DB (2003) Real-time design patterns: robust scalable architecture for real-time systems. The Addison-Wesley object technology series. Addison-Wesley, Boston, San Francisco, Paris

  65. Compagna L, El Khoury P, Harjani R, Kloukinas C, Li K, Maña A, Muñoz A, Pujol G, Ruiz JF, Saidane A, Serrano D, Sinha SK, Spanoudakis G (2008) A5.D2.5—patterns and integration schemes languages. Technical report. SERENITY-Project

  66. OMG, OMG Unified Modeling Language (OMG UML) (2009) Superstructure. http://www.omg.org/spec/UML/2.2/Superstructure

  67. OMG, OCL 2.2 Specification (2010)

Download references

Author information

Authors and Affiliations

  1. IRIT, University of Toulosue, 118 Route de Narbonne, 31062, Toulouse Cedex 9, France

    B. Hamid

  2. Fraunhofer Institute for Secure Information Technology SIT 75, 64295, Darmstadt, Germany

    S. Gürgens & A. Fuchs

Authors
  1. B. Hamid
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. S. Gürgens
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. A. Fuchs
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to B. Hamid.

Appendix

Appendix

Example of establishing a secure TLS channel.

In the following, we present one possible and desired sequence of actions of a client C and server S that result, as we have shown in Sect. 6.4, in establishing a secure TLS channel. Note that the actions need not occur in exactly this order, other orders are possible to achieve the same result. Further, some of the actions may not be needed at all or may be implemented differently within particular implementations. Keys to be used for encryption for example may be passed from the calling application or may be accessible directly. Since our proof focuses on authenticity of the client we disregard all actions that are concerned with server authentication.

figure f

Proof of SeBB.3

Proof

Trivially, if for a specific sequence \(\omega \) of actions, all agents in \(\mathbb {P}{\setminus } who\) consider all values of par possible, then all agents in the smaller set \(\mathbb {P}{\setminus } (who \cup \{Q\})\) still consider all values of par possible, i.e. \(restricted \hbox {-}conf ({\mathcal {A}}(par),par,who,\{\omega \})\) implies \(restricted \hbox {-}conf ({\mathcal {A}}(par),par,who \cup \{Q\},\{\omega \})\). If \(\omega \) is continued by encrypting par with an RSA public key, then the security property provided by RSA encryption ensures that nobody but the owner of the public key can gain knowledge about the value of par, hence \(restricted \hbox {-}conf ({\mathcal {A}}(par),par,who \cup \{Q\},\{\omega a\})\) holds.

Proof of SeBB.4

Proof

Let \(\omega \in B\) and \(verifyMac(Q,key,m,mac(key,m)) \in alph(\omega )\). Then it follows that exists \(v \in \varPhi (\{s\},T),x,z \in \varSigma ^*\) with \(\omega = uvx\) and verifyMac(Q, key, m, mac(key,  \(m)) \in alph(v)\). Further, by the nature of the MAC algorithm, a MAC verification action is always preceded by a MAC generation action, hence genMac(R, key, m,  \(mac(key,m)) \in alph(\omega )\) for some \(R \in \mathbb {P}\). Since the MAC generation action in turn is preceded by the start action s of the phase class, it follows genMac(R, key, m, mac(key,  \(m)) \in alph(v)\). Further, since s is the only phase class start action in \(\omega \), there is no other word \(v'\) contained in \(\omega \) with \(verifyMac(Q,key,m,mac(key,m)) \in alph(v')\). Finally, the key key is confidential for P and Q during this phase class, thus \(R \in \{P,Q\}\), and since Q never itself generates a MAC before having verified it, it follows that P has done so and, therefore, the assertion.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Hamid, B., Gürgens, S. & Fuchs, A. Security patterns modeling and formalization for pattern-based development of secure software systems. Innovations Syst Softw Eng 12, 109–140 (2016). https://doi.org/10.1007/s11334-015-0259-1

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11334-015-0259-1

Keywords

Search

Navigation