Lehre

 

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

• Secure Systems Development with UML (UB TU Dortmund: Signaturen L Sr 531 bis L Sr 531+4)

Zusätzliche Hinweise:

Hilfreiche Hinweise zum Vortrag sind zu finden in

• Merkblatt zur Gestaltung eines Seminarvortrages

• A Short Guide for Student Talks and Papers (.pdf)

• Research skills

• Hints for research students

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