Open Access

Nina Moebius

• Chipkartenanwendungen gewinnen weltweit zunehmend an Bedeutung. Immer mehr Menschen nutzen elektronische Geldbörsen und es gibt kaum noch eine Metropole, die keinen elektronischen Fahrausweis für ihren Nahverkehr anbietet. Viele Firmen setzen bei ihren Schließsystemen auf Transponderlösungen als Zugangskontrolle und in Deutschland steht aktuell die Einführung der elektronischen Gesundheitskarte an. All diesen Chipkartenanwendungen ist gemein, dass sowohl das Ausnutzen von Sicherheitslücken als auch deren Behebung erhebliche finanzielle Schäden bei den Betreibern verursachen und deren Ruf nachhaltig beschädigen können. Gleichzeitig gilt für viele Anwendungen, dass die Akzeptanz durch die Nutzer ganz entscheidend dadurch beeinflusst wird, wie sicher ihre teils hochsensiblen, persönlichen Daten in den Systemen sind. Die Praxis zeigt, dass Sicherheit in diesem Umfeld ein großes Problem darstellt. Immer wieder werden Sicherheitslücken in Anwendungen entdeckt, die zu dem Zeitpunkt bereitsChipkartenanwendungen gewinnen weltweit zunehmend an Bedeutung. Immer mehr Menschen nutzen elektronische Geldbörsen und es gibt kaum noch eine Metropole, die keinen elektronischen Fahrausweis für ihren Nahverkehr anbietet. Viele Firmen setzen bei ihren Schließsystemen auf Transponderlösungen als Zugangskontrolle und in Deutschland steht aktuell die Einführung der elektronischen Gesundheitskarte an. All diesen Chipkartenanwendungen ist gemein, dass sowohl das Ausnutzen von Sicherheitslücken als auch deren Behebung erhebliche finanzielle Schäden bei den Betreibern verursachen und deren Ruf nachhaltig beschädigen können. Gleichzeitig gilt für viele Anwendungen, dass die Akzeptanz durch die Nutzer ganz entscheidend dadurch beeinflusst wird, wie sicher ihre teils hochsensiblen, persönlichen Daten in den Systemen sind. Die Praxis zeigt, dass Sicherheit in diesem Umfeld ein großes Problem darstellt. Immer wieder werden Sicherheitslücken in Anwendungen entdeckt, die zu dem Zeitpunkt bereits jahrelang im Einsatz waren. Die Behebung dieser Fehler gestaltet sich aufgrund der vielen Chipkarten, die an die Nutzer einer Anwendung ausgegeben wurden, sowie der relativ hohen Zahl an Kartenlesegeräten oft schwierig und ist sehr kostspielig. Was bei der Entwicklung dieser Art von Anwendungen bisher fehlt ist ein Softwareentwicklungsansatz, der die Sicherheit der Anwendung als integralen Bestandteil begreift und diesen Aspekt durchgehend in den Ansatz einbettet. Die Entwickler von Chipkartenanwendungen setzen teilweise bereits formale Methoden ein, um Sicherheitseigenschaften nachzuweisen. Dennoch fehlt bislang ein Konzept, das die Sicherheitsanforderungen der zu entwickelnden Systeme vom Entwurf bis zur Implementierung durchgängig berücksichtigt und mit dem gleichzeitig Garantien für die Sicherheit gegeben werden können. Diese Arbeit stellt einen modellgetriebenen Softwareentwicklungsansatz vor, in dem die beiden oben genannten Aspekte umgesetzt werden. Der Ansatz umfasst den Entwurf der zu entwickelnden Anwendung mit UML und die vollautomatische Generierung von lauffähigem Quellcode aus dem UML-Anwendungsmodell. Einzigartig ist, dass neben dem eigentlichen Quellcode auch ein formales, abstraktes Modell der Anwendung generiert wird. Dieses kann automatisch in ein interaktives Verifikationswerkzeug eingelesen und es kann dann ein formaler Beweis der Sicherheit der Anwendung geführt werden. Auf diese Weise wird garantiert, dass die Anwendung kritische Eigenschaften erfüllt. Der Quellcode und das formale Modell werden so generiert, dass sich die auf formaler Ebene bewiesenen Sicherheitseigenschaften auf den generierten Code übertragen. Die Eigenschaften gelten somit auch für den Quellcode der Anwendung. Der gesamte Ansatz ist werkzeugunterstützt und wurde anhand mehrerer, teils sehr großer, Fallstudien evaluiert.…