- Suche

- Kontakt

SecureMDD - A Model-Driven Development Method for Secure Applications

Projektstart: 01.08.2008
Projektträger: Universität Augsburg
Projektverantwortung vor Ort: Nina Moebius

Zusammenfassung

The SecureMDD project is funded by Deutsche Forschungsgemeinschaft DFG

Beschreibung

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.

thumbs
A tour through several security-critical applications

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

CopyCard with symmetric encryption and generated GUI

CopyCard with two kinds of terminals (platform-independent model)

CopyCard with two kinds of terminals (platform-specific model)

Mondex electronic purse (with security proofs)

Bankingsystem (Debitcard) (with security proofs)

Age Verification

ePassport

E-Ticket (with ASLan++ specification)

GeldKarte

UpdateData (with security proofs)

The German Electronic Health Card (big, with security proofs)

 

The following publications describe different aspects of the SecureMDD approach:

 

  • Model-Driven Development of Secure Service Application
    Marian Borek, Nina Moebius, Kurt Stenzel and Wolfgang Reif
    Proceedings of the 35th IEEE Software Engineering Workshop 2012 (SEW-35), IEEE CS Press
  • SecureMDD: Transformation of a UML application model to a formal specification.
    Nina Moebius, Marian Borek, Kurt Stenzel, Wolfgang Reif.
    Technical Report 2012-10, Universität Augsburg, 2012
    Article available on the publication server of the University of Augsburg

  • Model-Driven Development of Secure Service Applications introduced by a Banking System Example.
    Marian Borek, Kurt Stenzel, Nina Moebius, Wolfgang Reif.
    Technical Report 2012-03, Universität Augsburg, 2012; PDF

  • 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

    KIV proofs for the example QVTO transformation in the paper that transforms a UML class diagram into Java classes with getters and setters.

  • 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.
    The UML models and links to formal proofs of the Mondex electronic purse

  • 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:
  • 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



-->