Nachweis von Sicherheitseigenschaften

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

• Prof. Tobias Nipkow
• Martin Strecker

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:

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

Themen

Allgemein

• Einige Themen sind noch zu vergeben, und manche Themen können von zwei Vortragenden gemeinsam bearbeitet werden - bitte nachfragen.
• In einigen Vorträgen soll eine von der Firma Gemplus zur Verfügung gestellte und mit unterschiedlichen Systemen bearbeitete Fallstudie behandelt werden.

Themen

1. JavaCard: Hardware-nahe Aspekte / Betriebsystem etc. (bearbeitet von Tao Zhuang: Ausarbeitung / Vortrag)
   Lit.:
   • Chen: JavaCard Technology for SmartCards. Addison-Wesley 2000. Kap. 2-5
   • Lanet et al.: Checking Secure Interactions of Smart Card Applets (Beschreibung der Gemplus-Fallstudie)
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.:
   • Einführung: Huth/Ryan: Logic in Computer Science. Modelling and reasoning about systems. Cambridge University Press, 2000
   • SMV-System
   • Artikel Verification of control flow based security properties (Proc. IEEE Symposium on Security and Privacy, 1999) von Jensen et al., Zusatzinformation von Diss von Thorn
4. Sichere Interaktion von Smartcard-Applets (bearbeitet von Clovis Yemou: Ausarbeitung / Vortrag)
   Lit.:
   • Gemplus-Fallstudie mit SMV
   • insbesondere: Checking Secure Interactions of Smart Card Applets von P. Bieber et al.
5. SDL (bearbeitet von Patrice Kwemo)
   Lit.:
   • Belina; Hogrefe; Sarma: SDL with applications, Prentice Hall/Hanser 1991
   • Dissertation von Ursula Hinkel
   • Gemplus-Fallstudie in SDL
6. mu-Kalkül (bearbeitet von Michael Wahler: Ausarbeitung / Vortrag)
   Lit.:
   • Compositional Specification and Verification of Control Flow Based Security Properties of Multi-Application Programs Papier von Barthe/ Gurov/ Huisman
   • Einführung zum Model-Checking im mu-Kalkül: Kap. 7 in E. M. Clarke and Orna Grumberg and Doron Peled: Model Checking
   • Die Dissertation von A. Kick beschreibt verschieden Verfahren zum Model-Checking
   • Einführung: Artikel Modal logics and mu-calculi: an introduction von Bradfield und Stirling (Handbook of Process Algebra, Elsevier 2001)
   • Zusätzlich zum mu-Kalkül: Kap. aus Diss von Biere
   • Zusätzlich Kapitel aus Artikel von Stirling
   • System Mucke
7. Abstrakte Interpretation (bearbeitet von Bernhard Liebl: Ausarbeitung / Vortrag)
   Lit.:
   • Einführung: Wilhelm / Maurer: Übersetzerbau oder Muchnik: Advanced Compiler Design. Morgan Kaufmann 1997
   • Artikel Assertion-Based Debugging of Imperative Programs by Abstract Interpretation von Bourdoncle
   • Überblick: Sammlung von Cousot, insbesondere ein Einführungsartikel
   • Vertiefung: Marktoberdorf-Papier von Cousot
   • Lesbarer Artikel zum Thema "Interval Analysis of C-Variables using Abstract Interpretation" von Andreas Ermedahl
8. Bytecode-Verifikation (bearbeitet von Christian Pacher Ausarbeitung / Vortrag)
   Lit.:
   • Lindholm / Yellin: JVM Specification
   • Xavier Leroy: Gut lesbarer Übersichtsartikel zu Bytecodeverifikation
   • Klein/Nipkow: Verified Bytecode Verifiers und Verified Lightweight Bytecode Verification
9. Verifikation mit Unterstützung von Theorembeweisern (bearbeitet von Jens Wilke Ausarbeitung / Vortrag)
   Lit.:
   • Das Extended Static Checking Projekt
   • David L. Detlefs and K. Rustan M. Leino and Greg Nelson and James B. Saxe: Extended Static Checking (ursprünglich für Modula 3)
   • von den selben Autoren: Extended Static Checking for Java

Zusätzliche Hinweise

• 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

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.