Das Seminar wird ca. Mitte Januar 2020 stattfinden. Eine Vorbesprechnung
ist in der ersten Semesterwoche.
Die meisten der folgenden Themen geben ein wissenschaftliches
Papier an. Der Kerninhalt dieses Papiers soll im Vortrag
und der Ausarbeitung vorgestellt werden.
Die Anmeldung für ein Thema erfolgt ab sofort per email an schellhorn@isse.de. Sobald ein Thema vergeben ist,
werde ich es hier entsprechend markieren, und zurückmailen,
dass das Thema geklappt hat. Sie können mir auch mehrere Themen
mit Reihenfolge schicken, dann gebe ich Ihnen das erste davon
noch nicht vergebene.
Thema 3, 4,6 und 7 sind vergeben
Thema 1: Verifikation von Securityprotokollen mit Tamarin:
Tamarin ist ein Beweiser für die automatische Analyse von
Sicherheitsprotokollen. Tamarin erlaubt die Modellierung von
Angreiferfähigkeiten und die Spezifikation der Protokoll in einer
eigenen Sprache. Für ein fertiges Protokollmodell erlaubt Tamarin den
automatischen und den interaktiven Beweis von Eigenschaften des
Protokolls. Thema des Seminars ist ein Überblick über die Fähigkeiten
von Tamarin mit realen Beispielen.
Thema 2: Untersuchung von IoT-basierten Medizintechnikgeräten mit dem
Failures-Divergences Refinement Checker (FDR).
Medizintechnikgeräte werden in zunehmendem Maße vernetzt, sie
kommunizieren also mit der Außenwelt. Aus offensichtlichen Gründen ist
Kommunikationssicherheit für solche Geräte dann ein wichtiges
Thema. In dieser Seminararbeit soll es um die Modellierung eines
Authentifizierungsprotokolls für ein IoT-basiertes Medizintechnikgerät
in CSP gehen und welche Eigenschaften für dieses Protokollmodell
bewiesen wurden.
Thema 3 [VERGEBEN]: Security-Testing von emedded Devices
In Netzwerke integrierte embedded Devices entwickeln sich zu einem
wesentlichen Element unseres Lebens. Leider haben solche Geräte oft
schwerwiegende Sicherheitslücken, viele davon eher trivial als
komplex. Zur Verbesserung der Sicherheit dieser Geräte wird daher
versucht, solche Geräte mit automatisierten Testwerkzeugen zu
untersuchen. Thema dieser Seminararbeit ist, wie diese Testtechniken
funktionieren, was sie können und welche Einschränkungen
bzw. Herausforderungen es gibt.
Thema 4 [VERGEBEN]+5: Automatische Werkzeuge zur Programmverifikation
Die automatische Analyse von Programmen auf Fehler ist inzwischen
in der Industrie verbreitet (z.B. checkt Microsoft alle
Treiberimplementierungen automatisch auf Deadlocks)
und kann oft Bugs verhindern. In den beiden Themen sollen
open source Werkzeuge vorgestellt werden,
an konkreten C-Programmen ausprobiert und evaluiert werden.
Hintergrundliteratur findet sich auf den Web-Seiten.
Thema 6 [VERGEBEN]: Algorithmen für persistente Speicher
Derzeit sind eine Reihe von neuen Speichertechnologien
in Entwicklung, die für die Zukunft versprechen,
persistent Daten zu halten (wie Flash, ROM oder Festplatten),
aber beliebigen Zugriff zu erlauben und (nahezu) so effizient
wie RAM zu sein. 3D Xpoint ist ein erster Prototyp für
solche NVM's (non-volatile memories).
Die Architektur zukünftiger Rechner könnte
statt RAM und ROM nur noch NVM's verwenden,
der einzige flüchtige Speicher ist dann nur noch der Prozessorcache.
Neue Algorithmen sollten dann mit expliziten Flushes aus dem
Prozessorcache arbeiten, die dafür sorgen, dass die Daten im NVM
auch bei Stromausfall jederzeit einen konsistenten Zustand ergeben.
Der Vortrag soll ein Papier vorstellen, in dem eine
derartige Implementierung für Hashmaps vorgestellt wird.
Thema 7 [VERGEBEN]: Verifikation findet überraschende Bugs
Vor ein paar Jahren konnte durch Verifikation mit
dem interaktiven Beweiser KeY im Sortieralgorithmus
der Java-Library ein Bug gefunden werden.
Der Vortrag soll den Algorithmus vorstellen, den gefundenen Bug
und den anschließend gemachte Korrektur erklären, sowie
ein wenig auf die bei der formalen Verifikation
verwendeten Formeln und das Tool eingehen.
Voraussetzung für das Thema sind Grundkenntnisse
zum Hoare-Kalkül.
Thema 8: Effiziente Algorithmen für immutable Datenstrukturen.
Eine Standard-Datenstruktur zur effizienten Speicherung
von Mengen oder Maps (mit Komplexität O(1) für die
Operationen zum Einfügen, Löschen und Lookup)
sind Hashtabellen. Diese arbeiten destruktiv, d.h. das Einfügen
überschreibt die alte Tabelle. Seit einiger Zeit gibt es
nicht-destruktive ("immutable") Implementierungen von Maps,
bei denen das Einfügen/Löschen keinen Seiteneffekt auf die alte Tabelle
hat (eine neue Tabelle wird erzeugt), bei denen die Operationen
aber trotzdem O(1)-Komplexität haben.
Der Vortrag soll anschaulich erklären, wie diese,
basierend auf "hash array mapped trie"'s (HAMT) funktionieren.
Thema 9: Software Transactional Memory (STM) am Beispiel der ScalaTM
Software Transactional Memory ist eine Alternative zur
Verwendung von Locks, bei dem in einem Programm
um Code-Stücke "p", die atomar (als Transaktion) ablaufen
sollen, einfach ein "atomic { p }" geschrieben wird.
Eine korrekte, aber ineffiziente Implementierung wäre mit einem
globalen Lock/Unlock um den atomic block.
Tatsächliche Implementierungen lassen die Blöcke parallel laufen und
stellen effizient fest, wann sie Konflikte haben, weil sie
die gleichen Variablen schreiben,
ähnlich wie das bei Datenbank-Transaktionen der Fall ist
(sie erfüllen "ACI" ohne "D").
Der Vortrag soll das Konzept von STMs und seine
Implementierung ("SwissTM") anhand des Papiers erklären.
