Zuverlässigkeit von Software in sicherheitskritischen Systemen

Seminar (2 SWS, Di. 16-18 Uhr)
Sommersemester 2005

Lehrstuhl Programmiersprachen und Übersetzerkonstruktion
Lehrstuhl Echtzeitsysteme und Eingebettete Systeme

UnivIS

Weitere Angaben zum Seminar (UnivIS). Das Seminar findet jeweils am Dienstag von 16-18 Uhr im Seminarraum 715 (CAP4, Hochhaus, 7. OG) statt.

Dozenten

Wolfgang Goerigk
Reinhard v. Hanxleden

Termine und annotierte Vorträge

Datum/Uhrzeit Ort Vortragender Thema Betreuer
Ausarbeitung *
Mo. 7.2.2005 13:30 CAP4/R715 W. Goerigk /  R. v. Hanxleden
Vorbesprechung

Di.
12.4.2005
16:15
CAP4/R715 W. Goerigk /  R. v. Hanxleden Vergabe der Vortragstermine

Di.
7.6.2005
16:15
CAP4/R715 Dennis Peters Temporal-Safety Proofs for Systems Code wg
[H] [P] [A] [S]
Di.
14.6.2005
16:15 CAP4/R715 Arne Schipper
CCured: Type-Safe Retrofitting of Legacy Software wg
[H] [P] [A]
Di. 21.6.2005 16:15 CAP4/R715 Sven Grünewald Error Sensitivity of the Linux Kernel rvh
[H] [P] [A]
Di. 28.6.2005 16:15 CAP4/R715 Malte Tiedje A Fault Tolerant Java Virtual Machine rvh
[H] [P] [A]
Di. 5.7.2005 16:15 CAP4/R715 Ken Bell Programming With Assertions wg
[H] [P] [A]
Di. 12.7.2005 16:15 CAP4/R715 Mohamed Ziad Albari A Taxonomy and Catalog of Runtime Software-Fault Monitoring Tools rvh
[H] [P] [A]

*) [H] Handout, [P] Präsentation, [A] Abstract, [S] Folien (ohne Animation)

Zielgruppe

Studierende im Hauptstudium beider Informatik-Studiengänge (Dipl.-Inf. und Dipl.-Ing.) sowie Studierende mit Nebenfach Informatik.

Inhalt

Das Thema der Zuverlässigkeit von Software, ihrer Sicherheit, Korrektheit, Robustheit, ist vielschichtig. Immer wieder treten Fehler auf, auch kritische, die auf gedanklich-logische Irrtümer in Spezifikation und Implementierung der die Systeme steuernden Software zurückzuführen sind. Compiler und Systemsoftware spielen ebenso eine Rolle wie die verwendeten Softwaretechniken und Programmiersprachen. Zur Vermeidung von Fehlern werden oft Einschränkungen an die verwendeten Sprachen festgelegt, um dynamische Fehlfunktionen (Speicherüberläufe, Speicherlecks u.ä.) zu verhindern, aber auch, um Analyse und Verifikation zu vereinfachen. Techniken der statischen Analyse von Programmen und Spezifikationen hinsichtlich der verschiedensten Fragestellungen finden Verwendung, mehr und mehr in Kombination mit maschinellen Beweissystemen und Model-Checkern. Neben Fehlervermeidung ist auch Fehlertoleranz (z.B. durch Redundanz, Mehrfachauslegung) für Software ein interessanter Ansatz, aber auch Techniken der Laufzeitprüfung, Beobachterprozesse, Monitoring, Konsistenzprüfung werden eingesetzt.

Mehr und mehr wird auch der Nachweis der Qualität von Software, die Garantie von Eigenschaften verlangt, z.B. bei der Zertifizierung sicherheitsrelevanter Systeme. In diesem Zusammenhang sind auch Bibliotheken, Werkzeuge, Compiler, Systemkomponenten, Fremdsoftware im weitesten Sinne von Bedeutung, für die Hersteller ebenfalls verantwortlich zeichnen. Die Beherrschung dieser komplexen Zusammenhänge ist nicht nur für Systeme relevant, von denen Gefahr für Leib und Leben von Menschen ausgeht, sondern auch bei wirtschaftlichem Gefahrenpotential softwarebasierter Systeme, z.B. im Bereich der Security.

In diesem Seminar werden wir uns mit aktuellen Forschungsarbeiten beschäftigen, Themenliste und Literatur siehe unten. Einige Vorträge sind fest vergeben, aber es stehen auch noch Themen zur Verfügung. Bitte melden Sie sich bei Interesse telefonisch oder per Email (wg, rvh).

Sonstiges

Hinweise zur Ausarbeitung, zum Seminarvortrag, und zur Benotung.

Durchsprache des Ausarbeitungsentwurfs:

Jeweils 14 Tage vor dem Vortrag (Dienstags), anschließend an das Seminar oder, falls das Seminar nicht stattfindet, um 16:00 Uhr, im Büro des Dozenten (Hochhaus, R713 bzw. R1117); falls ein anderer Termin gewünscht wird, bitte mit den Dozenten absprechen.
Der Ausarbeitungsentwurf sollte jeweils bis spätestens 2 Tage vor der Durchsprache eingereicht werden, per E-Mail an wg@informatik.uni-kiel.de (W. Goerigk) oder rvh@informatik.uni-kiel.de (R. v. Hanxleden).
Nach dem Seminar sollte eine PDF-Version des gehaltenen Vortrags, ggf. mit Korrekturen, geschickt werden.

Themenliste & Literatur

Hinweis: Die Papers sind nicht für den öffentlichen Zugriff bestimmt und können daher auch nur innerhalb des Institutsnetzes heruntergeladen werden.

  1. Programmanalyse, Laufzeitprüfung, Codeinstrumentierung und Verifikation

    1. David S. Rosenblum, A Practical Approach to Programming With Assertions, IEEE Transactions on Software Engineering, Vol. 21, No. 1; January 1995, pp. 19--31

    2. Arnaud Venet and Guillaume Brat, Precise and efficient static array bound checking for large embedded C programs, PLDI '04: Proceedings of the ACM SIGPLAN 2004 Conference on Programming language design and implementation, 2004, Washington DC, USA, ACM Press, pp. 231--242

    3. G. Necula, J. Condit, M. Harren, S. McPeak, and W. Weimer, CCured: Type-Safe Retrofitting of Legacy Software, ACM ToPLaS

    4. G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv: Deriving Specialized Program Analyses for Certifying Component-Client Conformance, Proceedings of the ACM SIGPLAN 2004 Conference on Programming language design and implementation PLDI 2002

    5. Symbolic Analysis Laboratory SAL (Shankar et al., SRI International)
      1. S. Bensalem et al.: An Overview of SAL, Langley Formal Methods Workshop LFM 2000
      2. N. Shankar: Symbolic Analysis of Transition Systems, Workshop on Abstract State Machines ASM 2000

    6. Thomas A. Henzinger, R. Jhala, R. Majumdar, G. Necula, G. Sutre, and W. Weimer: Temporal-Safety Proofs for Systems Code. International Conference on Computer Aided Verification CAV 2002

    7. ( J. Souyris: Proving Automatically the Absence of Runtime Errors. VMCAI 2005, Automatic Tools for Program Verification )

  2. Fehlererkennung und Fehlertoleranz

    1. Jeff Napper, Lorenzo Alvisi, Harrick Vin, A Fault-Tolerant Java Virtual Machine, 2003 International Conference on Dependable Systems and Networks (DSN'03), June 22 - 25, 2003, San Francisco, California, pp. 425--433

    2. Weining Gu, Zbigniew Kalbarczyk, Ravishankar K. Iyer, Error Sensitivity of the Linux Kernel Executing on PowerPC G4 and Pentium 4 Processors, 2004 International Conference on Dependable Systems and Networks (DSN'04), June 28 - July 01, 2004, Florence, Italy, pp. 887--896

    3. Nelly Delgado, Ann Quiroz Gates, Steve Roach, A Taxonomy and Catalog of Runtime Software-Fault Monitoring Tools, IEEE Transactions on Software Engineering. Published by the IEEE Computer Society Vol. 30, No. 12; December 2004, pp. 859--872

    4. S.S. Kulkarni, J. Rushby, and N. Shankar: A Case Study in Component Based Mechanical Verification of Fault-Tolerant Programs. 4th. Workshop on Self-Stabilization WSS99, Austin, Tx., 1999