Current page:
Seminar: Seminar zu Software- und Systems Engineering (Master) - Details

  • Detaillierte Informationen über die Veranstaltung werden angezeigt, wie z.B. die Veranstaltungsnummer, Zuordnungen, DozentInnen, TutorInnen etc. In den Detail-Informationen ist unter Aktionen das Eintragen in eine Veranstaltung möglich.

  • link-extern Further help
You are not logged in.

Seminar zu Software- und Systems Engineering (Master)

General information

Course number INF-0136
Semester WS 2019/20
Home institute Softwaretechnik
Courses type Seminar in category Teaching
Performance record Schriftliche Ausarbeitung (ca. 15 Seiten) und Vortrag (30 Minuten)
Hauptunterrichtssprache deutsch
ECTS points 4

Lecturers

Times

The course times are not decided yet.

Course location

unspecified

Fields of study

Comment/Description

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.

https://link.springer.com/chapter/10.1007/978-3-642-39799-8_48#
https://tamarin-prover.github.io/

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.

https://pdfs.semanticscholar.org/b46f/82a4951f520d5f1eac73c9ef251ff53c9ce8.pdf

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.

http://s3.eurecom.fr/docs/ndss18_muench.pdf


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 4 [VERGEBEN]: CMBC für C-Programme
https://www.cprover.org/cbmc/

Thema 5: CPAChecker für C-Programme
https://cpachecker.sosy-lab.org/


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.

https://dl.acm.org/citation.cfm?id=2803144

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.

https://link.springer.com/article/10.1007/s10817-017-9426-4

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.

https://lampwww.epfl.ch/papers/idealhashtrees.pdf

Ein Video-Vortrag zum Thema ist
https://vimeo.com/28760673

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.

Papier:
https://dl.acm.org/citation.cfm?id=1542494
ScalaSTM:
https://nbronson.github.io/scala-stm/

attendance

Current number of participants 5
expected number of participants 9