javaconference.com

Frau Nina Moebius, Universität Augsburg, http://www.informatik.uni-augsburg.de/lehrstuehle/swt/se/staff/nmoebius/

In diesem Vortrag soll eine Methodik vorgestellt werden, die die modellgetriebene Softwareentwicklung sicherheitskritischer Anwendungen und die formale Verifikation integriert. Auf diese Weise soll sichergestellt werden, dass der mittels MDA erzeugte, lauffähige Java Code sicher bzgl. der relevanten Sicherheitseigenschaften ist. Anwendung findet die Methodik bei Applikationen, die u.a. auf Smartcards (implementiert in JavaCard) basieren. Ein Beispiel hierfür ist das Bezahlsystem Mondex, das von Mastercard betrieben wird und Münzgeld ersetzen soll. Der Besitzer eine Mondexkarte kann diese verwenden, um in einem Shop hiermit zu bezahlen. Das System funktioniert so, dass der Shopbesitzer sowie der Kunde jeweils eine Mondexkarte besitzen und der zu zahlende Betrag von der Kundenkarte abgebucht und auf der Karte des Ladenbesitzers gutgeschrieben wird. Die zwei wichtigsten Sicherheitseigenschaften der Anwendung sind, dass kein Geld verloren gehen kann (z.B. durch vorzeitiges Herausziehen der Mondexkarte aus dem Kartenleser) sowie dass ein bösartiger Angreifer kein Geld auf einer Karte erzeugen kann. Um dies sicherzustellen basiert die Anwendung auf kryptographischen Protokollen, die kryptographische Primitive wie Verschlüsselung verwenden. Die zu entwickelnde Anwendung wird in einem ersten Schritt mit UML modelliert. Hierbei wird eine plattformunabhängige Sicht auf das zu entwickelnde System definiert. Aus diesem Modell wird dann im Anschluss automatisch ein plattformspezifisches Modell generiert. Die Transformation ergänzt das Ausgangsmodell um Informationen, die für die Generierung von JavaCard Code relevant sind. Zu beachten ist dabei beispielsweise die beschränkte Speicherkapazität auf Smartcards sowie die Behandlung von Zuweisungen von Datentypen (explizites Kopieren oder Sharing). Anhand dieses Modells wird im Anschluss JavaCard Code erzeugt. Ebenfalls aus dem plattformunabhängigen Modell wird, mithilfe eines entsprechenden plattformspezifischen Modells, eine formale Spezifikation der modellierten Anwendung generiert. Basierend auf dieser Spezifikation können Sicherheitseigenschaften wie das Nicht-Erzeugen von Geld auf der Mondexkarte formuliert und anschließend mittels eines interaktiven Beweissystems nachgewiesen werden. Ergebnis ist also lauffähiger JavaCard Code, der - da aus demselben UML Modell erzeugt - die formal bewiesenen Sicherheitseigenschaften erfüllt.