SecureMDD - A Model-Driven Development Method for Secure Smart Card Applications

The SecureMDD project is funded by Deutsche Forschungsgemeinschaft DFG

SecureMDD facilitates the development of security-critical applications that are based on cryptographic protocols. The approach seamlessly integrates the generation of code and formal methods. Starting with a platform-independent UML model of a system under development, we generate executable Java(Card) code as well as a formal model from the UML model. Subsequent to this, the formal model is used to verify the security of the modeled system. Our goal is to prove that the generated code is correct w.r.t. the generated formal model in terms of formal refinement. The approach is tailored to the domain of security-critical systems, e.g. smart card applications.

The SecureMDD approach is based on our work and experience with the Go!Card project. The SecureMDD project is funded by Deutsche Forschungsgemeinschaft DFG since July 2008.

The slides of the SecSE talk give a short overview of the approach.

A short modeling tour of a simple CopyCard example and the generated Java Card code for the example. And the KIV proofs (uses xml/xsl).

Modeling the Mondex electronic purse

The following publications describe different aspects of the SecureMDD approach:

• Formal Verification of QVT Transformations for Code Generation.
  Nina Moebius, Kurt Stenzel, Wolfgang Reif.
  Proceedings of MODELS 2011 - 14th International Conference on Model Driven Engineering Languages and Systems; Springer LNCS 6981; Springer link
  
  
• Mondex: Engineering a Provable Secure Electronic Purse.
  D. Haneberg, N. Moebius, W. Reif, G. Schellhorn, and K. Stenzel.
  International Journal of Software and Informatics, 5(1):159-184, 2011. http://www.ijsi.org.
  
  
• Formal Verification of Application-Specific Security Properties in a Model-Driven Approach
  Nina Moebius, Kurt Stenzel, Wolfgang Reif
  Proceedings of ESSoS 2010 - International Symposium on Engineering Secure Software and Systems; Springer LNCS 5965; Springer link
  The example in the paper is based on CopyCard.
  
  
• Pitfalls in Formal Reasoning about Security Protocols
  Nina Moebius, Kurt Stenzel, Wolfgang Reif
  Proceedings of ARES 2010 - Fifth International Conference on Availability, Reliability and Security; IEEE Press 2010; Digital Object Identifier 10.1109/ARES.2010.36; IEEE Online.
  The paper describes two different models:
  • The insecure model with a meaningless security property and its proof.
  • The secure model with a meaningful security property and its proof.
  
  
• SecureMDD: A Model-Driven Development Method for Secure Smart Card Applications
  N. Moebius, K. Stenzel, H. Grandy, W. Reif
  ARES 2009 Workshop: Proceedings of the Third International Workshop on Secure Software Engineering (SecSE), IEEE Computer Society Press (2009)
  abstract; Digital Object Identifier 10.1109/ARES.2009.22; online available at IEEE Online.
  
  
• Generating Formal Specifications for Security-Critical Applications - A Model-Driven Approach
  N. Moebius, K. Stenzel, W. Reif
  ICSE 2009 Workshop: International Workshop on Software Engineering for Secure Systems (SESS'09), IEEE/ACM Digital Libary
  abstract ; Digital Object Identifier 10.1109/IWSESS.2009.5068461 online available at IEEE Online.
   
• Model-Driven Code Generation for Secure Smart Card Applications
  N. Moebius, K. Stenzel, H. Grandy, W. Reif
  Proceedings of the 20th Australian Software Engineering Conference , IEEE Computer Society Press (2009)
  abstract; Digital Object Identifier 10.1109/ASWEC.2009.15; online available at IEEE Online.
  The example in the paper is based on Mondex.
  
  
• Modeling Security-Critical Applications with UML in the SecureMDD Approach
  N. Moebius, W. Reif, K. Stenzel
  International Journal On Advances in Software (2008) vol 1 nr 1:59-79, IARIA
  abstract; online available at Iaria Journal On Advances in Software;
  The example in the paper is based on Mondex.
  
  
• A Modeling Framework for the Development of Provably Secure E-Commerce Applications
  Nina Moebius, Dominik Haneberg, Wolfgang Reif, Gerhard Schellhorn
  Proceedings of the International Conference on Software Engineering Advances 2007, IEEE Computer Society Press **** Best Paper Award ****
  abstract; online available at IEEE Online
   

All publications of our group also contain publications related to Go!Card and the Mondex case study.

Contacts

• Nina Moebius
• Dr. Kurt Stenzel
• Prof. Dr. Wolfgang Reif