HOME | IMPRESSUM | SITEMAP | KIT
Jetzt mit mehr Theorie

Desaster in der Software-Sicherheit: Können formale Methoden helfen? (SoSe 16)

Formale Methoden gegen Desaster in der Software-Sicherheit
Veranstaltungstyp: Proseminar
Veranstaltungsnr.:
Zielgruppe: Bachelor Informatik
Lehrstuhl: Anwendungsorientierte Formale Verifikation
Dozent(en):

Prof. B. Beckert (BB)
Thorsten Bormer (TB)
Sarah Grebing (SaG)
Simon Greiner (SG)
Mihai Herda (MH)
Michael Kirsten (MK)
Vladimir Klebanov (VK)
Mattias Ulbrich (MU)
Alexander Weigl (AW)

SWS-Anzahl: 2
ECTS: 3
Semester: Sommersemester 2016
Raum: Gebäude 50.34, SR t.b.a.
Termine: 20.04.2016, 13-14 Uhr in SR 131, Auftaktveranstaltung
02.06.2016, 13:00 - 15:00 Uhr in SR 010 (Gebäude 50.34), Zwischenvorträge
18.07.2016, 13:45 - 17:00 Uhr in SR 010 (Gebäude 50.34), Hauptvorträge
20.07.2016, 12:45 - 16:00 Uhr in SR 010 (Gebäude 50.34), Hauptvorträge
21.07.2016, 12:45 - 16:00 Uhr in SR 010 (Gebäude 50.34), Hauptvorträge
Anmeldung: Persönlich oder per E-Mail bei Frau Meinhart, Raum 223, simone.meinhart@kit.edu
Platzvergabe: Reihenfolge nach Eingang der Anmeldung
Alle Plätze vergeben (08.04.2016)
Neue Anmeldungen kommen auf die Warteliste.

Thema

An unserem Lehrstuhl werden formale Methoden für ein weites Spektrum an Problemen in der Softwaresicherheit und -entwicklung erforscht. Soft- und Hardware stehen seit dem ersten Computerwurm von 1988 unter vielfältigen Angriffen. Daneben übernehmen Computer immer mehr und komplexere Überwachungs- und Kontrollaufgaben in unserer Gesellschaft, für die ein inkorrektes Verhalten Gefahren für Leib und Leben bedeutet. In diesem Proseminar werden formale Methoden vorgestellt, die praxisnahe Probleme vermeiden, optimieren oder verhindern.

Aufgabenstellung

Für jeden Vortrag sind von dem Studenten die folgenden Aufgabenpunkte zu erledigen:
  • Verstehen des Stoffes.
  • Auswahl der Themen, die in dem Vortrag präsentiert werden sollen.
  • Entscheidung, wie die Themen präsentiert werden sollen.
  • Erstellung der Folien für die Präsentation und gegebenfalls anderer Materialien.
  • Der Vortrag selbst.

Folien

Folien der Auftaktveranstaltung

Themen

  1. Verifikation von probabilistischen Sicherheitsprotokollen (AW)
    [1] -- [2] --
    [3] Kwiatkowska, Norman and Parker:
    Modeling and Verification of Probabilistic Systems.
    In: Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
  2. Verifikation von medizinischen Richtlinien mit Model-Checking (AW)
    [1] -- [2]-- [3] -- [4]
  3. Informationsflussanalyse mit Programmabhängigkeitsgraphen am Beispiel JOANA (SG)
    [1]
  4. Formale Verifikation von Kryptographischen Protokollen am Beispiel ProVerif (SG)
    [1]-- [2]
  5. Ironclad Apps: End-to-End Security via Automated Full-System Verification (TB)
    [1]
  6. Are We There Yet? Determining the Adequacy of Formalized Requirements and Test Suites (TB)
    [1]
  7. Neue Trends in der Autoaktiven Verifikation (SaG)
    [1] -- [2] -- [3] -- [4] -- [5]
  8. Exploit-Generation für Informationsflusseigenschaften (MH)
    [1]
  9. Automatisches Finden von Exploits mittels Fuzzing und Symbolic Execution (oder: wie man $ 750 000 gewinnt) (MK)
    [1] “Driller: Augmenting Fuzzing Through Selective Symbolic Execution”
    (N. Stephens et Al., 2016)
    [2] “32C3 Talk: A Dozen Years of Shellphish - From DEFCON to the DARPA Cyber Grand Challenge”
    (A. Bianchi und J. Corbetta und A. Dutcher, 2015)
  10. Judgement Aggregation (BB)
  11. Fehler in Hardware vermeiden durch Äquivalenzbeweise (MU)
    Sequential Equivalence Checking Based on Structural Similarities [vanEijk2001]
    "Hardware Verification using ANSI-C Programs as a Reference" [ClarkeKroening2003]
    "FDIV Floating Point Flaw Pentium Processor" [Intel 2004]
  12. Angriffe auf die IT-Sicherheit bei elektronischen Wahlen (BB+MK)
    [1] "Ukraine: Cyberwar’s Hottest Front", The Wall Street Journal
    (M. Coker and P. Sonne, 2015)
    [2] "The New South Wales iVote System: Security Failures and Verification Flaws in a Live Online Election"
    (J. A. Halderman and V. Teague, 2015)