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

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 den Studierenden 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)