Abstract
The requirement for higher security and dependability of systems is continuously increasing even in domains not traditionally deeply involved in such issues. Yet, evolution of embedded systems towards devices connected via Internet, wireless communication or other interfaces requires a reconsideration of secure and trusted embedded systems engineering processes. In this paper, we propose an approach that associates model driven engineering (MDE) and formal validation to build security and dependability (S&D) patterns for trusted RCES applications. The contribution of this work is twofold. On the one hand, we use model-based techniques to capture a set of artifacts to encode S&D patterns. On the other hand, we introduce a set of artifacts for the formal validation of these patterns in order to guarantee their correctness. The formal validation in turn follows the the MDE process and thus links concrete validation results to the S&D requirements identified at higher levels of abstraction.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
AVISPA. The HLPSL Tutorial, A Beginner’s Guide to Modelling and Analysing Internet Security Protocols, http://www.avispa-project.org
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. ACM Transactions on Computer Systems 8, 18–36 (1990)
Daniels, F., Kim, K., Vouk, M.A.: The Reliable Hybrid Pattern: A Generalized Software Fault Tolerant Design Pattern, pp. 1–9 (1997)
Douglass, B.P.: Real-time UML: Developing Efficient Objects for Embedded Systems. Addison-Wesley, Reading (1998)
Fernandez, E.B., Yoshioka, N., Washizaki, H., Jürjens, J., VanHilst, M., Pernul, G.: Using security patterns to develop secure systems. In: Software Engineering for Secure Systems: Industrial and Research Perspectives. IGI Global (2010)
Fuchs, A., Gürgens, S., Rieke, R., Apvrille, L.: 1st Version Architecture and Protocols Verification and Attack Analysis. Technical Report D3.4.1, EVITA Project (2010)
Fuchs, A., Gürgens, S., Rudolph, C.: A Formal Notion of Trust – Enabling Reasoning about Security Properties. In: Nishigaki, M., Jøsang, A., Murayama, Y., Marsh, S. (eds.) IFIPTM 2010. IFIP Advances in Information and Communication Technology, vol. 321, pp. 200–215. Springer, Heidelberg (2010)
Gamma, E., Helm, R., Johnson, R.E., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading (1995)
Gasparis, E., Nicholson, J., Eden, A.H.: LePUS3: An Object-Oriented Design Description Language. In: Stapleton, G., Howse, J., Lee, J. (eds.) Diagrams 2008. LNCS (LNAI), vol. 5223, pp. 364–367. Springer, Heidelberg (2008)
Guennec, A.L., Sunyé, G., Jézéquel, J.-M.: Precise Modeling of Design Patterns, pp. 482–496. Springer, Heidelberg (2000)
Gürgens, S., Ochsenschläger, P., Rudolph, C.: Authenticity and provability - A formal framework. In: Davida, G.I., Frankel, Y., Rees, O. (eds.) InfraSec 2002. LNCS, vol. 2437, pp. 227–245. Springer, Heidelberg (2002)
Gürgens, S., Ochsenschläger, P., Rudolph, C.: Abstractions Preserving Parameter Confidentiality. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 418–437. Springer, Heidelberg (2005)
Gürgens, S., Ochsenschläger, P., Rudolph, C.: On a Formal Framework for Security Properties. International Computer Standards & Interface Journal (CSI), Special issue on formal methods, techniques and tools for secure and reliable applications 27(5), 457–466 (2005)
Gürgens, S., Rudolph, C.: Security Analysis of (Un-) Fair Non-repudiation Protocols. Formal aspects of computing 2629, 229–232 (2004)
Gürgens, S., Rudolph, C., Scheuermann, D., Atts, M., Plaga, R.: Security evaluation of scenarios based on the tCG’s TPM specification. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 438–453. Springer, Heidelberg (2007)
Hamid, B., Radermacher, A., Jouvray, C., Gérard, S., Terrier, F.: Designing fault-tolerant component based applications with a model driven approach. In: Brinkschulte, U., Givargis, T., Russo, S. (eds.) SEUS 2008. LNCS, vol. 5287, pp. 9–20. Springer, Heidelberg (2008)
Jürjens, J.: UMLsec: Extending UML for Secure Systems Development. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 412–425. Springer, Heidelberg (2002)
Kim, D.-K., France, R., Ghosh, S., Song, E.: A UML-based Meta-modeling Language to Specify Design Patterns, vol. 30, pp. 193–206 (2004)
Lodderstedt, T., Basin, D., Doser, J.: SecureUML: A UML-Based Modeling Language for Model-Driven Security. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 426–441. Springer, Heidelberg (2002)
Lowe, G.: An Attack on the Needham-Schroeder Public-Key Protocol. Information Processing Letters (1995)
Mapelsden, D., Hosking, J., Grundy, J.: Design Pattern Modelling and Instantiation Using DPML. In: CRPIT 2002: Proceedings of the Fortieth International Conference on Tools Pacific, pp. 3–11. Australian Computer Society, Inc. (2002)
Nhlabatsi, A., Bandara, A., Hayashi, S., Haley, C.B., Jürjens, J., Kaiya, H., Kubo, A., Laney, R., Mouratidis, H., Nuseibeh, B., Tahara, Y., Tun, T.T., Washizaki, H., Yoshioka, N., Yu, Y.: Security Patterns: Comparing Modeling Approaches. In: Software Engineering for Secure Systems: Industrial and Research Perspectives. IGI Global (2010)
OMG. OMG. A UML Profile for MARTE: Modeling and Analysis of Real-Time Embedded Systems,beta 2 (June 2008)
Paulson, L.C.: Proving Properties of Security Protocols by Induction. In: 10th Computer Security Foundations Workshop, pp. 70–83. IEEE Computer Society Press, Los Alamitos (1997)
Ravi, S., Raghunathan, A., Kocher, P., Hattangady, S.: Security in Embedded Systems: Design challenges. ACM Trans. Embed. Comput. Syst. 3(3), 461–491 (2004)
Roscoe, B., Ryan, P., Schneider, S., Goldsmith, M., Lowe, G.: The Modelling and Analysis of Security Protocols. Addison Wesley, Reading (2000)
Serrano, D., Maña, A., Sotirious, A.-D.: Towards Precise and Certified Security Patterns. In: Proceedings of 2nd International Workshop on Secure Systems Methodologies Using Patterns (Spattern 2008), pp. 287–291. IEEE Computer Society, Los Alamitos (2008)
Tichy, M., Schilling, D., Giese, H.: Design of Self-managing Dependable Systems with UML and Fault Tolerance Patterns, pp. 105–109. ACM, New York (2004)
Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drieslma, P., Mantovani, J., Mödersheim, S., Vigneron, L.: A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. In: Workshop on Specification and Automated Processing of Security Requirements, SAPS 2004 (2004)
Yoder, J., Barcalow, J.: Architectural Patterns for Enabling Application Security. In: Conference on Pattern Languages of Programs, PLoP 1997 (1998)
Yoshioka, N., Washizaki, H., Maruyama, K.: A survey of Security Patterns. Progress in Informatics (5), 35–47 (2008)
Zurawski, R.: Embedded Systems. In: Embedded Systems Handbook. CRC Press Inc., Boca Raton (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
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., Clark, T., Kühne, T. (eds) Model Driven Engineering Languages and Systems. MODELS 2011. Lecture Notes in Computer Science, vol 6981. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24485-8_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-24485-8_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24484-1
Online ISBN: 978-3-642-24485-8
eBook Packages: Computer ScienceComputer Science (R0)