Ausgewählte Themen des Modellbasierten Sicherheits-Engineerings
Block-Seminar (2 SWS)
Seminar
Master:
Schwerpunkt (A) Software, Sicherheit und
Verifikation
Diplom:
Schwerpunkte 1 (Software-Konstruktion) und 5 (Sicherheit und
Verifikation)
Seminartermine:
-
Vorbesprechung: Montag, 10.10.2011, 13.00, OH14 Raum 305.
Themenvergabe; Tipps und Organisatorisches; Fragen zu den Vorträgen; etc. (ANWESENHEITSPFLICHT !)
Folien (inkl. weitere Hinweise !)
-
Blockseminar-Termin: Mi 15. - Fr 17.02.2012 (!!! GEÄNDERT !!!), Raum OH14/304
Zeitplan der Vorträge des Blockseminars
Datum |
Zeit |
Vortragender |
Thema |
Mi 15.02.12 |
13:00 |
Marco Pfahlberg |
Einführung in UMLsec |
Mi 15.02.12 |
14:00 |
Lars Ostwald |
UML-Maschinen und ihre Semantik |
Mi 15.02.12 |
15:00 |
Lukas Lerche |
Grundlagen des expliziten Model Checkings |
Mi 15.02.12 |
16:00 |
Aike J Sommer |
Model Checking mit LTL |
Do 16.02.12 |
13:00 |
Viktor Mucha |
Modellbasiertes Return On Security Investment |
Do 16.02.12 |
14:00 |
Stefan Plaga |
Event-basierte Modellierung von Geschäftsprozessen |
Do 16.02.12 |
15:00 |
Julia Werdelmann |
Homomorphe Verschlüsselung |
Fr 17.02.12 |
13:00 |
Christoph Kröger |
Sicherheitslücken in Cloud Computing Umgebungen |
Fr 17.02.12 |
14:00 |
Sylwia Melnarowicz |
Grundbegriffe der Ontologie |
Fr 17.02.12 |
15:00 |
Dmytro Galytskyy |
Ontologien für Sicherheit und Compliance in Clouds |
Fr 17.02.12 |
16:00 |
Wei Cai |
tba |
Von den TeilnehmerInnen wird erwartet:
- Ein Vortrag von mindestens 45 Minuten. (Richtwert: 60 Min., inklusive Diskussion)
- Eine schriftliche Ausarbeitung von ca. 15 Seiten
- Aktive Teilnahme an den Seminarvorträgen
- Weitere Informationen siehe hier: Folien (inkl. weitere Hinweise
!)
Überblick:
Entwicklung und Pflege vertrauenswürdiger,
sicherheitskritischer Systeme sind große Herausforderungen. Es werden viele softwareintensive Systeme entworfen,
realisiert und eingesetzt, die gravierende Sicherheitslücken aufweisen. Wir wissen das aus eigener Erfahrung und aus
Schlagzeilen über spektakuläres Fehlverhalten von Systemen bzw. über erfolgreiche Angriffe auf sie. Die Gründe dafür
sind vielfältig. Manchmal fehlt den Entwicklern das notwendige Sicherheitsbewußtsein, oft fehlen die notwendigen
Kenntnisse über die Entwicklungsprozesse, -methoden, -verfahren und -werkzeuge oder sie werden nicht eingesetzt, weil
man sich den vermeintlich zu großen Zeit- und Kostenaufwand beim derzeitigen Konkurrenzdruck nicht leisten zu können
glaubt. Beim Engineering oder Reengineering sicherheitskritischer Softwaresysteme stellen sich u.a. folgende Fragen:
- Welche Methoden gibt es für ein umfassendes Risikomanagement, mit denen Experten aus den Geschäftsprozessen und
Arbeitsabläufen eine vollständige Analyse der Sicherheitsrisiken durchführen und Vorschläge zu ihrer angemessenen
Behandlung ableiten können?
- Welche Methoden gibt es für das Engineering bzw. Reengineering sicherheitskritischer Systeme, für die Auswahl
eines geeigneten Entwicklungsprozesses und geeigneter Werkzeuge sowie zur Qualitätssicherung?
- Welche Werkzeuge gibt es, die z.B. die Geschäftsprozessmodelle, UML-Systemspezifikationen, Software-Quelltexte
und Konfigurationsdateien automatisch auf Sicherheit analysieren können?
- Kann man z.B. mit UML oder CASE-Werkzeugen wie AutoFocus Sicherheitsanforderungen einfach und intuitiv
spezifizieren? Und gibt es Werkzeuge für Simulation, Konsistenzprüfung, Codegenerierung, Verifikation und Test der
Sicherheitsaspekte?
- Sind die erstellten Modelle als Dokumentation für die Zertifizierung nach relevanten Standards brauchbar?
Zielsetzung:
Das Seminar untersucht Antworten auf diese Fragen. Die
Teilnehmenden werden die Anforderungen an sicherheitskritische Systeme und die Bedrohungsarten verstehen. Sie erhalten
einen Überblick über die vorhandenen Techniken zur Vermeidung von Sicherheitsrisiken und Abwehr von Bedrohungen. Sie
werden die Besonderheiten beim Management sicherheitsrelevanter Softwareprojekte, den Nutzen von
Sicherheitsaufwendungen und die einschlägigen Normen und Verordnungen kennen. Schließlich werden sie sich intensiv mit
modellbasierten Techniken zur Entwicklung sicherheitskritischer Systeme sowie zur Analyse und zum Reengineering
existierender Software beschäftigt haben, die damit gewonnenen Praxiserfahrungen einschätzen können, und einen
Überblick über vorhandene Werkzeuge und deren Leistungsfähigkeit haben.
Mögliche Themen:
Werden beim Vorbereitungstreffen vorgestellt.
Beispiele für mögliche Themen sind:
- Sicherheitslücken in Cloud Computing Umgebungen
Auslagerungen von Prozessen und Diensten in Cloud Computing Umgebungen bietet nicht nur den Benutzern Möglichkeiten
z.B. zur Kostenreduktion sondern auch Angreifern neue Angriffsvektoren z.B. die Möglichkeit durch Angriffe auf die
Virtualisierung oder die Interfaces der Cloud unberechtigten Zugang zu erhalten. Der Vortrag soll eine Übersicht über
bereits bekannte Angriffe auf Cloud Computing Umgebungen geben und dabei einzelne Angriffe detailliert vorstellen.
Vorgestellt werden könnten z.B. cross-VM side-channel attacks, die dem Angreifer unberechtigten Zugriff auf
Informationen anderer Cloud Computing Benutzer ermöglichen, oder XML Signature Element Wrapping attacks, die den
Angreifer unberechtigt Befehle ausführen lassen.
Literatur: [RTSS09], [GJLS09], [ESA-02]
Ansprechpartner: Sebastian Pape
- Homomorphe Verschlüsselung
Die Auslagerung von Prozessen und Berechnungen in Cloud Computing Umgebungen birgt insbesondere in Hinsicht auf
Datenschutz und Compliance zahlreiche Risiken. Eine Möglichkeit diesen Risiken entgegenzuwirken ist die
Verschlüsselung von Daten in der Cloud Computing Umgebung. Wählt man ein homomorphes Verschlüsselungsverfahren, so
können in der Cloud trotz der Verschlüsselung noch hinreichend sinnvolle Berechnungen ausgeführt werden. Der Vortrag
soll homomorphe Verschlüsselung anhand des "ring learning with errors" (Ring LWE) Problems vorstellen und derzeitige
Einsatzmöglichkeiten sowie Probleme beim Einsatz homomorpher Verschlüsselung aufzeigen.
Literatur: [O10], [LPR10], [LNV11]
Ansprechpartner: Sebastian Pape
- UML-Maschinen und formale Sicherheit
Für die formale Prüfung von Sicherheit werden häufig formale Modelle genutzt. Für UMLsec ist das formale Modell durch
UML-Maschinen gegeben. Dieser auf State-Maschinen aufbauende Formalismus kann genutzt werden, um UMLsec eine Semantik
zu geben. Gleichzeitig eignen sich diese Maschinen einen Angreifer zu modellieren. Die auf den Maschinen definierten
Verfeinerungsbegriffe können anschließend genutzt werden, um Bedrohungen des UMLsec-Modells zu analysieren.
Dieses Thema soll zwischen zwei oder drei Teilnehmern aufgeteilt werden. Eine Kooperation, um die Vorträge
aufeinander abzustimmen, wird erwartet. Eine natürliche Trennung ist gegeben durch die formalen Grundlagen der
UML-Maschinen bzw. der aus ihnen zusammengesetzten Systeme und der Nutzung der Verfeinerung, um die Abwesenheit
bestimmter Angriffsprobleme zu zeigen.
Literatur: Jürjens, J. Umlsec: Extending uml for secure systems development. UML 2002 —The Unified Modeling Language
(2002).
Ansprechpartner:
Dr. Thomas P. Ruhroth
- Grundlagen des expliziten Model Checking
An viele der heute verwendeten Computersysteme werden Sicherheitsanforderungen gestellt, die allein mit testbasierten
Verfahren nicht sichergestellt werden können. Model Checking bietet die Möglichkeit, für ein gegebenes System
geforderte Eigenschaften formal nachzuweisen.
Ziel des Vortrags ist die Darstellung des grundsätzlichen Vorgehens beim Model Checking, einschließlich der möglichen
Formalismen (insbesondere Kripke-Strukturen), und praktische Grenzen der Anwendbarkeit. Weiterhin soll mit CTL eine
der für die Spezifikation genutzten Logiken vorgestellt werden.
Literatur: z.B. Clarke, Grumberg, Peled "Model Checking"
-
Model Checking mit LTL
Die "Linear temporal logic" (LTL) stellt neben CTL eine weitere Möglichkeit dar, Anforderungen an ein System zu
formalisieren. Diesen Formalismus vorzustellen ist Teil des Vortrags. Weiterhin sollen existierende
Optimierungsmethoden erklärt und in ihren Eigenschaften verglichen werden, die den praktischen Einsatz von Model
Checkern erleichtern bzw. teilweise erst möglich machen. Als Referenz kann hierbei das Programm "SPIN" dienen. SPIN
ist ein Model Checker mit Unterstützung für LTL.
Literatur: z.B.
- Stephan Kleuker "Formale Modelle der Softwareentwicklung"
- Gerard Holzmann "The SPIN model checker"
- Ontologien für Sicherheit und Compliance in Clouds
Cloud Computing hat sich zu einem echten Hype entwickelt. Gerade für kleinere und mittelständische Unternehmen ist es
sinnvoll, Prozesse in eine Cloud auszulagern statt selbst in teure IT-Ressourcen zu investieren. Bei der Verarbeitung
von vertraulichen Daten stellt sich jedoch zunehmend die Frage nach Sicherheitsanforderungen an die Cloud und
inwiefern Compliance-Regularien beachtet werden.
In der Literatur sind bereits erste Ontologien und Referenzmodelle für Sicherheitsanforderungen und
Compliance-Regularien vorgestellt worden. Im Vortrag soll grundlegend das Konzept von Ontologien und semantischen
Netzen am Beispiel von Cloud Computing und Sicherheit bzw. Compliance erläutert und die bestehenden Ontologien
diskutiert werden. (Das Thema kann ggf. auf zwei Teilnehmer ausgedehnt werden.)
Literatur: [GMT11], [MT11]
Ansprechpartner: Sven Wenzel
- Artefakt- und Event-basierte Modellierung von Geschäftsprozessen
Geschäftsprozesse werden i.d.R. entweder Ereignis-basiert oder Artefakt-basiert modelliert. In diesem Vortrag soll
eine Gegenüberstellung der beiden Ansätze erfolgen und eine mögliche Kombination beider diskutiert werden.(Das Thema
kann ggf. auf zwei Teilnehmer ausgedehnt werden.)
Literatur: A. Nigam, N.S. Caswell; Business artifacts: an approach to operational specification, IBM Sys.J. 42(3),
2003
Ansprechpartner: Sven Wenzel
- Einige weitere Themen: s. die Kick-off Folien.
Weitere Informationen und Material dazu gibt es auf Anfrage bzw. bei der Vorbesprechung.
Literatur:
Zusätzliche Hinweise:
Hilfreiche Hinweise zum Vortrag sind zu finden in
Feedback:
Wir haben großes Interesse an veranstaltungsbegleitendem
Feedback, um auf Änderungswünsche gleich (und nicht erst im nächsten Semester) eingehen zu können, beispielsweise per
email oder über folgendes
anonyme Kontaktformular.
Studentische Arbeiten, Hiwi-Verträge:
Im Zusammenhang mit den in der
Vorlesung behandelten Themen werden auch
studentische Arbeiten und
Hiwi-Verträge betreut bzw. vergeben.
Kontakt:
Jan Jürjens
Kontakt
Zum Profil von Prof. Dr. Jan
Jürjens