Hauptseminar: Entwicklung sicherer Systeme

Moderne Wirtschaft und Gesellschaft beruhen auf Infrastrukturen für Kommunikation, Finanzdienstleistungen, Energieversorgung und Transport. Diese Infrastrukturen sind zunehmend abhängig von vernetzten Informationssystemen. Angriffe auf diese Systeme können das ökonomische oder sogar physikalische Wohlbehalten von Menschen und Organisationen bedrohen. Wegen der verbreiteten Vernetzung von Informationssystemen können Angriffe anonym und aus sicherer Entfernung geführt werden.

Die Entwicklung vertrauenswürdiger sicherheitskritischer Systeme ist schwierig. Es werden viele Systeme entworfen und realisiert, in denen im Nachhinein schwere Sicherheitslücken in Entwurf und Implementierung gefunden werden, die zum Teil schlagzeilenträchtiges Fehlverhalten oder Angriffe ermöglichen.

Zum Beispiel gelang es einem Hacker Team der U.S.-amerikanischen National Security Agency (NSA) in einer Uebung 1997 in Computer des U.S. Department of Defense und des Stromversorgungssystems der USA einzudringen, und u.a. die Verursachung einer Serie von Stromausfällen und Notrufausfällen in Washington, D.C. zu demonstrieren. Bei gegebener Terrorismusbedrohung erscheint dies als eine ernstzunehmende Gefahr.

Ziel des Seminars ist es, Grundlagen sicherer Systeme und Methoden des Software Engineering beim Entwurf sicherheitskritischer Systeme zu vermitteln.

Voraussetzungen

Inhaltlich: Das Seminar empfiehlt sich besonders für Studierende, die sich für die Anwendung mathematisch-formaler Verfahren auf reale Probleme, z.B. bei Systementwurf und -verifikation, interessieren.

Formal: Abgeschlossenes Vordiplom
 

Veranstalter

Das Seminar wird gemeinsam durchgeführt von der TUM und der Firma Giesecke & Devrient, einem der weltweit bedeutendsten Hersteller von Chipkartensystemen.

Veranstalter von Seiten der TUM sind:

• Prof. Manfred Broy
• Prof. Tobias Nipkow
• Jan Jürjens
• Gerhard Popp
• Katharina Spies
• Martin Strecker
• Guido Wimmel

Organisation

Vorbesprechung:

am Donnerstag, 31.1.2002, um 16:00 h in Raum 1546

Anmeldung:

in der Vorbesprechung (wer verhindert ist: bitte Nachricht an Jan Jürjens)

Seminartermin:

jeweils Donnerstags 14:15-15:45 h in Raum 1546

Erster Termin: 18.4.2002

Scheinerwerb:

Von den Teilnehmern wird erwartet:

• Ein Vortrag von 45-60 Min. inclusive Diskussion
• Eine schriftliche Ausarbeitung von ca. 15 Seiten
• Aktive Teilnahme an den Seminarvorträgen

Betreuung:

Siehe Themen.

Von G&D betreute Studenten wenden sich bei administrativen Fragen bitte an Martin Strecker

Fristen:

Bis eine Woche vor Vortrag: Absprache der endgültigen Fassung der Folien mit Betreuer

Bis 31.7.2002: Abgabe der endgültigen Fassung der schriftl. Ausarbeitung

Themen

1. 18.4.: Organisatorisches und Tips zur Vortragstechnik (vorgestellt von Katharina Spies, TUM)
2. 25.4.: Entwicklungsprozess und Konstruktion sicherer Systeme (betreut von Gerhard Popp, TUM; bearbeitet von Anton Matheis)
   (Vortrag, Ausarbeitung)
   Lit.:
   • Claudia Eckert: IT-Sicherheit: Konzepte, Verfahren, Protokolle (Kap. 4)
   • Monika Vetterling: Security Engineering nach den Common Criteria, Diplomarbeit, TUM 2001
   • Common Criteria - Gemeinsame Kriterien für die Prüfung und Bewertung der Sicherheit von Informationstechnik, Teil 1: Einführung und allgemeines Modell, Version 2.1
   • Ross Anderson: Security Engineering
3. 2.5.: Computersicherheit in der Praxis (betreut von Guido Wimmel, TUM; bearbeitet von Jun Chen)
   (Vortrag, Ausarbeitung)
   Lit.:
   • Claudia Eckert: IT-Sicherheit: Konzepte, Verfahren, Protokolle (Kap. 5,10)
   • Ross Anderson: Security Engineering (Kap. 4,7,8)
   • Pierangela Samarati, Access Control (Proceedings FOSAD Sommerschule)
4. 16.5.: Beschreibungstechniken für sichere Systeme (betreut von Jan Jürjens, TUM; bearbeitet von Willy Chen)
   (Vortrag, Ausarbeitung)
   Lit.:
   • Jan Jürjens: Developing secure systems with UMLsec (VIS'01) (lokaler Zugang)
   • Jan Jürjens: Secure Java development with UMLsec (INETSEC'01) (lokaler Zugang)
   • Jan Jürjens, Guido Wimmel: Security modelling for electronic commerce (I3E'01)
5. 23.5.: Typsysteme für Informationsfluß (betreut von Martin Strecker, TUM; bearbeitet von Franz Strasser)
   (Vortrag, Ausarbeitung)
   Lit.:
   • Dennis Volpano, Geoffrey Smith and Cynthia Irvine: A Sound Type System for Secure Flow Analysis
6. 6.6.: Kryptographische Verfahren (betreut von Gerhard Popp, TUM; bearbeitet von Sabine Blechinger)
   (Vortrag, Ausarbeitung)
   Lit.:
   • Claudia Eckert: IT-Sicherheit: Konzepte, Verfahren, Protokolle (Kap. 6,7,8)
   • Alfred J. Menezes, Paul C. van Oorschot and Scott A. Vanstone: Handbook of Applied Cryptography
7. 13.6.: Protokollanalyse mit Isabelle entfällt!
   Lit.:
   • Larry Paulson: The inductive approach to verifying cryptographic protocols
   • siehe generell: Verifying Security Protocols Using Isabelle
8. 20.6.: Anwendungsbeispiel: Smartcard-basierte elektronische Geldbörsen (betreut von Guido Wimmel, TUM; bearbeitet von Michael Dyrna)
   (Vortrag, Ausarbeitung)
   Lit.:
   • Rankl/Effing: Handbuch der Chipkarten (Kap. 12)
   • Common Electronic Purse Specifications (CEPS) und PalME-Projekthomepage
   • Intersector Electronic Purse and Purchase Device Protection Profile
9. 4.7.: Symmetrische und asymmetrische Authentisierungs- und Key Management Protokolle für Chipkarten (betreut von Herrn Stutenbäumer, G&D; bearbeitet von Martin Schlaffer)
   (Vortrag, Ausarbeitung)
   Lit.: Verschiedene Normen und Spezifikationen (vom Betreuer bereitgestellt), u.a.
   • SC 27 Normen, Auszug DIN Vornorm V66291-1
   • Auszug HPC Specification ESIGN -K Specification, Auszug STARCOS S PK 2.3,
10. 11.7.: Elektronische Signaturverfahren gemäß der EU Direktive (betreut von Herrn Vogel, G&D; bearbeitet von Wei Yu)
    in Raum 1565 !
    (Vortrag, Ausarbeitung)
    Lit.:
    • EU Direktive, Deutsches Signaturgesetz / Verordnung, Österreichisches Signaturgesetz
    • ESIGN Dokumente, Algorithmenkataloge (deutsch, europäisch)
11. 18.7.: Aufstellung der Historie mit kurzer Beschreibung aller bekannt gewordenen Angriffe auf Chipkarten seit 1990 (betreut von Herrn Rankl, G&D; bearbeitet von Axel Heider)
    (Vortrag, Ausarbeitung)
    Lit.: wird vom Betreuer bereitgestellt

Zusätzliche Hinweise

Vortragsfolien und schriftliche Ausarbeitung sollen als PDF-Dokumente vorliegen, die plattformunabhängig gelesen werden können. PDF kann aus diversen Microsoft-Produkten exportiert oder auch direkt aus LaTeX generiert werden, wie im folgenden beschrieben:

• Verwendung von LaTeX für die schriftl. Ausarbeitung:
• Beispieldateien
zur Erzeugung von Artikeln mit latex oder pdflatex.
• Verwendung von LaTeX für Vorträge:
• Beispieldateien
zur Erzeugung von Folien mit latex oder pdflatex.
• Wer glaubt, auf die (weitgehend verzichtbaren) Powerpoint-Effekte nicht verzichten zu können, sollte sich PPower installieren.
• Es empfiehlt sich, LaTeX-Dateien mit Emacs oder XEmacs zu schreiben (Syntax-Highlighting, Compilierung direkt aus dem Editor heraus ...). Zu weiterer Unterstützung die Datei tex-site.el z.B. in das Verzeichnis ~/emacs/ schieben und die Zeile (load-file "~/emacs/tex-site.el") in der Datei .emacs einfügen.
• Weiteres zu TeX findet sich bei Dante

• Im Rahmen des Projektes Fairpay beschäftigen wir uns mit der Sicherheit elektronischer Bezahlsysteme (s.a. unsere Projektseite). In diesem Zusammenhang werden auch Praktika und Diplomarbeiten betreut.
• In dem Projekt Verificard beschäftigen wir uns mit der Sprachformalisierung von JavaCard und Formalisierungen von Sicherheitseigenschaften in dem System Isabelle. Siehe hierzu Praktika und Diplomarbeiten