Technische Universität München, Department of Computer Science, Programming Methods, Distributed Systems up: Lehre

Nachweis von Sicherheitseigenschaften

für JavaCard durch approximative Programmauswertung



 
  Inhalt
  Voraussetzungen
  Veranstalter
  Organisation
  Themen
  Zusätzliche Hinweise
  Weiterführende Veranstaltungen
 Inhalt

An sicherheitskritische Anwendungen, z.B. im Bereich Transportwesen, Medizintechnik, Versicherung und Banken, werden hohe Anforderungen hinsichtlich Zuverlässigkeit und Zugriffsschutz gestellt, die durch traditionelle Techniken nur unzureichend abgesichert werden können.

Aus Praktikabilitäts- und Kostengründen ist man hier an Verifikationsmethoden interessiert, die vollständig automatisch ablaufen, dabei jedoch die Einhaltung spezieller Sicherheitseigenschaften garantieren können (und sie, etwa im Gegensatz zu Tests, nicht nur nahelegen). Auf diese Weise läßt sich z.B. verhindern, daß bestimmte Ausnahmesituationen wie Speicher-Zugriffsverletzungen beim Programmablauf auftreten oder unerlaubterweise Informationen an Dritte weitergeleitet werden können.

Ein grundsätzlicher Ansatz besteht darin, den Nachweis von Eigenschaften von Programmen nicht durch Berechnung mit konkreten Werten zu führen, sondern durch symbolische Auswertung mit geeigneten Abstraktionen, z.B. Mengen von Werten oder Typen.

Das Seminar hat zum Ziel, einige Ausprägungen dieser Technik vorzustellen und deren Nutzen anhand von Fallstudien, besonders aus dem Chipkartenbereich, zu analysieren.

 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.

Vertrautheit mit Logik und Semantik von Programmiersprachen ist von Vorteil, aber keine unabdingbare Voraussetzung.

Formal: Abgeschlossenes Vordiplom
 
 Veranstalter

 Organisation
Vorbesprechung:
... hat bereits stattgefunden. Es sind noch einige Themen zu vergeben (s.u.) - bitte Martin Strecker fragen.
Zeit / Ort / Beginn:
Erster Termin am Donnerstag, 6.12., ab 14:00 h in Raum 1546
Zweiter Termin am Donnerstag, 24.1., ab 14:00 h in Raum 1546
Scheinerwerb:
Von den Teilnehmern wird erwartet:
Weitere Hinweise finden sich auf folgenden Folien

 Themen

Allgemein

Themen

  1. JavaCard: Hardware-nahe Aspekte / Betriebsystem etc. (bearbeitet von Tao Zhuang: Ausarbeitung / Vortrag)
    Lit.:
  2. JavaCard: Software (Applet firewall etc.) (bearbeitet von Jin Zhou: Ausarbeitung / Vortrag)
    Lit.: Chen: JavaCard Technology for SmartCards. Addison-Wesley 2000. Kap. 9
  3. Temporallogik Noch zu vergeben
    Lit.:
  4. Sichere Interaktion von Smartcard-Applets (bearbeitet von Clovis Yemou: Ausarbeitung / Vortrag)
    Lit.:
  5. SDL (bearbeitet von Patrice Kwemo)
    Lit.:
  6. mu-Kalkül (bearbeitet von Michael Wahler: Ausarbeitung / Vortrag)
    Lit.:
  7. Abstrakte Interpretation (bearbeitet von Bernhard Liebl: Ausarbeitung / Vortrag)
    Lit.:
  8. Bytecode-Verifikation (bearbeitet von Christian Pacher Ausarbeitung / Vortrag)
    Lit.:
  9. Verifikation mit Unterstützung von Theorembeweisern (bearbeitet von Jens Wilke Ausarbeitung / Vortrag)
    Lit.:

 Zusätzliche Hinweise

 Weiterführende Veranstaltungen

Unsere Arbeitsgruppe beschäftigt sich mit der Sprachformalisierung von JavaCard (siehe die Projekte Bali und Verificard). In diesem Bereich werden einige Praktika und Diplomarbeiten angeboten.


Martin Strecker
Last modified: Thu Jan 24 20:11:52 MET 2002