Sommersemester 2012
Seminar Formale Methoden für Software-Sicherheit
| Typ: | Seminar | ||
|---|---|---|---|
| Semester: | SS 2012 | ||
| Zeit: | Blockveranstaltung am Semesterende |
||
| Dozierende: |
Prof. Dr. Bernhard Beckert
|
||
| SWS: | 2 | ||
| LVNr.: | 24841 | ||
| Hinweis: | Weiterführendes Seminar für Diplom- oder Master-Studierende |
||
Details zur Veranstaltung
Software-basierte Systeme sind aus unserem Alltag nicht mehr wegzudenken. Sie halten Einzug in nahezu alle Bereiche unseres Lebens. Allerdings bleibt die Qualität der Software trotz ihrer wachsenden Bedeutung nur allzu oft auf der Strecke.
Neben der Anforderung nach korrekter Implementation funktionaler Eigenschaften durch die Software spielt die Informationssicherheit als Qualitätsmerkmal eine zentrale Rolle. Eine Möglichkeit, fehlerfreie Software zu entwickeln, oder zumindest die Qualität der Software deutlich zu erhöhen, ist die Anwendung formaler Methoden.
In diesem Seminar wird eine Auswahl an aktuellen Ergebnissen aus der Forschung vorgestellt, die sich mit dem Thema Software Security befassen, wie etwa der Nachweis von Informationsflusseigenschaften mit Hilfe der Programmverifikation.
Die Seminarteilnehmer bereiten unter Anleitung durch einen Betreuer einen Vortrag zu einem dieser Forschungsergebnisse vor. Ziel ist, dass der Vortragende selbst sich ein gründliches Verständnis des Themas erarbeitet und dem Auditorium in der Kürze der zur Verfügung stehenden Zeit die wesentlichen Informationen und Einsichten vermittelt.
Organisatorisches
Die Veranstaltung richtet sich an Studierende im Master- bzw. fortgeschrittenen Diplom-Studium. Kenntnisse aus den Vorlesungen "Formale Systeme" und "Softwaretechnik" werden als bekannt vorausgesetzt. Die Prüfungsleistung besteht aus einem 45-minütigen Vortrag und einer schriftlichen Ausarbeitung. Vorträge und Ausarbeitungen können in deutsch oder englisch erstellt werden.
Eine Vorbesprechung der Themen findet am Mittwoch, 25. April von 13:15-14:00 Uhr im SR 236 statt. Bitte melden Sie sich zu dieser Vorbesprechung mit Hilfe des unten stehenden Formulars bis Sonntag, 22. April an. Für weitere organisatorische Fragen wenden Sie sich bitte an Thorsten Bormer.
Seminarthemen
- The KeY Approach for the Cryptographic Verification of JAVA Programs
- Eliminating covert flows with minimum typings
- Epistemic Temporal Logic for Information Flow Security
- A temporal logic characterisation of observational determinism
- Observational determinism for concurrent program security
- Quantifying Information Leaks in Software
Online-Anmeldung zur Vorbesprechung
Material
Tips für gute Seminarvorträge
LaTeX-Vorlagen
Die Erstellung der Ausarbeitung erfolgt verpflichtend in LaTeX unter Benutzung der IEEE-Transactions-Vorlage. Sie ist in den gängigen LaTeX-Distributionen enthalten (TeX Live: IEEEtran, MiKTeX: ieeetran). Zum Benutzen beginnen Sie Ihr Dokument mit "\documentclass[a4paper]{IEEEtran}".