ISSE

Search

SecureMDD


A Model-Driven Development Method for Secure Applications

Start date: 01.08.2008
Funded by: DFG (Deutsche Forschungsgemeinschaft)
Local scientists: Kuzman Katkalov
Wolfgang Reif
Publications: Publication list

Abstract

SecureMDD is a model-driven approach to develop secure applications.

Description

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 and web service applications.

The SecureMDD approach is based on our work and experience with the Go!Card project. The SecureMDD project was funded by the Deutsche Forschungsgemeinschaft DFG from 2008 to 2012.

Presentation

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

Case Studies

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 two kinds of terminals (platform-independent model)

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

Mondex electronic purse (with security proofs)

Banking System (with ATM withdrawal and online money transfer between different banks) (with security proofs)

Age Verification

ePassport

E-Ticket  (and interactive proofs - big)

E-Ticket (with ASLan++ specification and automatic abstractions)

E-Ticket (with ASLan++ specification and manual abstractions)

GeldKarte

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

 

Links: