Abstract
Developing security-critical systems is difficult, and there are many well-known examples of vulnerabilities exploited in practice. In fact, there has recently been a lot of work on methods, techniques, and tools to improve this situation already at the system specification and design. However, security-critical systems are increasingly long-living and undergo evolution throughout their lifetime. Therefore, a secure software development approach that supports maintaining the needed levels of security even through later software evolution is highly desirable. In this chapter, we recall the UMLsec approach to model-based security and discuss on tools and techniques to model and verify evolution of UMLsec models.
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.
References
Andries, M., Engels, G., Habel, A., Hoffmann, B., Kreowski, H.-J., Kuske, S., Plump, D., Schürr, A., Taentzer, G.: Graph transformation for specification and programming. Science of Computer Programming 34(1), 1–54 (1999)
Bézivin, J., Büttner, F., Gogolla, M., Jouault, F., Kurtev, I., Lindow, A.: Model transformations? Transformation models! In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 440–453. Springer, Heidelberg (2006)
Chaki, S., Sharygina, N., Sinha, N.: Verification of evolving software (2004)
Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the Annual Symposium on Logic in Computer Science (LICS), pp. 353–362 (June 1989)
ISO 15408:2007 Common Criteria for Information Technology Security Evaluation, Version 3.1, Revision 2: Part 2; Security Functional Components, CCMB-2007-09-002 (September 2007)
Grünbauer, J., Hollmann, H., Jürjens, J., Wimmel, G.: Modelling and verification of layered security protocols: A bank application. In: Anderson, S., Felici, M., Littlewood, B. (eds.) SAFECOMP 2003. LNCS, vol. 2788, pp. 116–129. Springer, Heidelberg (2003)
Heckel, R.: Compositional verification of reactive systems specified by graph transformation. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 138–153. Springer, Heidelberg (1998)
Höhn, S., Jürjens, J.: Rubacon: automated support for model-based compliance engineering. In: Robby [26], pp. 875–878
Jürjens, J.: Formal Semantics for Interacting UML subsystems. In: Proceedings of the International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS). International Federation for Information Processing (IFIP), pp. 29–44. Kluwer Academic Publishers, Dordrecht (2002)
Jürjens, J.: Principles for Secure Systems Design. PhD thesis, Oxford University Computing Laboratory (2002)
Jürjens, J.: Model-based security engineering with UML. In: Aldini, A., Gorrieri, R., Martinelli, F. (eds.) FOSAD 2005. LNCS, vol. 3655, pp. 42–77. Springer, Heidelberg (2005)
Jürjens, J.: Code security analysis of a biometric authentication system using automated theorem provers. In: Proceedings of the Annual Computer Security Applications Conference (ACSAC), pp. 138–149. IEEE Computer Society, Los Alamitos (2005)
Jürjens, J.: Secure Systems Development with UML. Springer, Heidelberg (2005)
Jürjens, J.: Sound methods and effective tools for model-based security engineering with UML. In: Roman, G.-C., Griswold, W.G., Nuseibeh, B. (eds.) Proceedings of the International Conference on Software Engineering (ICSE), pp. 322–331. ACM Press, New York (2005)
Jürjens, J.: Verification of low-level crypto-protocol implementations using automated theorem proving. In: MEMOCODE, pp. 89–98. IEEE, Los Alamitos (2005)
Jürjens, J.: Security analysis of crypto-based Java programs using automated theorem provers. In: Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 167–176. IEEE Computer Society, Los Alamitos (2006)
Jürjens, J., Schreck, J., Bartmann, P.: Model-based security analysis for mobile communications. In: Robby [26], pp. 683–692
Jürjens, J., Shabalin, P.: Tools for secure systems development with UML. Intern. Journal on Software Tools for Technology Transfer 9(5-6), 527–544 (2007); Invited submission to the special issue for FASE 2004/05
Jürjens, J., Wimmel, G.: Formally testing fail-safety of electronic purse protocols. In: 16th International Conference on Automated Software Engineering (ASE 2001), pp. 408–411. IEEE Computer Society, Los Alamitos (2001)
Kolovos, D.S., Paige, R.F., Polack, F., Rose, L.M.: Update transformations in the small with the epsilon wizard language. Journal of Object Technology 6(9), 53–69 (2007)
Lehman, M.: Software’s future: Managing evolution. IEEE Software 15(1), 40–44 (1998)
Lipson, H.: Evolutionary systems design: Recognizing changes in security and survivability risks. Technical Report CMU/SEI-2006-TN-027, Carnegie Mellon Software Engineering Institute (September 2006)
Mantel, H.: On the composition of secure systems. In: Proceedings of the IEEE Symposium on Security and Privacy, Oakland, CA, USA, pp. 88–101. IEEE Computer Society, Los Alamitos (2002)
Petriu, D.C., Woodside, C.M., Petriu, D.B., Xu, J., Israr, T., Georg, G., France, R.B., Bieman, J.M., Houmb, S.H., Jürjens, J.: Performance analysis of security aspects in UML models. In: Cortellessa, V., Uchitel, S., Yankelevich, D. (eds.) WOSP, pp. 91–102. ACM, New York (2007)
Rensink, A., Schmidt, Á., Varró, D.: Model checking graph transformations: A comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 226–241. Springer, Heidelberg (2004)
Robby (ed.): 30th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, May 10-18. ACM, New York (2008)
Secure Change Project. Deliverable 4.2., http://www-jj.cs.tu-dortmund.de/jj/deliverable_4_2.pdf
UML Revision Task Force. OMG Unified Modeling Language: Specification. Object Management Group (OMG) (September 2001), http://www.omg.org/spec/UML/1.4/PDF/index.htm
UMLsec group. UMLsec Tool Suite (2001-2011), http://www.umlsec.de
Watson, B.: Non-functional analysis for UML models. In: Real-Time and Embedded Distributed Object Computing Workshop, Object Management Group (OMG), July 15-18 (2002)
Woodside, C.M., Petriu, D.C., Petriu, D.B., Xu, J., Israr, T.A., Georg, G., France, R.B., Bieman, J.M., Houmb, S.H., Jürjens, J.: Performance analysis of security aspects by weaving scenarios extracted from UML models. Journal of Systems and Software 82(1), 56–74 (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Jürjens, J., Ochoa, M., Schmidt, H., Marchal, L., Houmb, S.H., Islam, S. (2011). Modelling Secure Systems Evolution: Abstract and Concrete Change Specifications. In: Bernardo, M., Issarny, V. (eds) Formal Methods for Eternal Networked Software Systems. SFM 2011. Lecture Notes in Computer Science, vol 6659. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21455-4_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-21455-4_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21454-7
Online ISBN: 978-3-642-21455-4
eBook Packages: Computer ScienceComputer Science (R0)