Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation

Vorlesungsbegleitendes Forschungspraktikum
im Sommersemester 2021

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich, Michael Kirsten

Typ:	Praktikum
Zielgruppe:	Master Informatik
Umfang:	5 Leistungspunkte (3 Praktikum + 2 Schlüsselqualifikation)
Ort:	online
Veranstaltungs-Nr.:	2400281

Zur Seite der Vorlesung

Inhalt

In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistpungspunkten (LP) (davon zwei Schlüsselqualifikation (SQ)) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Die Bearbeitung aktueller Forschungsthemen erfordert hierbei ein größeres Maß an Eigeninitiative als dies bei im Vorhinein festgelegten Praktika der Fall ist. Die Fortschritte werden dabei regelmäßig mit einem bzw. einer betreuenden Mitarbeitenden der Forschungsgruppe diskutiert.

Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Teilnehmer:innen innerhalb der ersten Woche bewerben können (die Plätze sind begrenzt!). Das Forschungspraktikum basiert thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten. Die praktische Forschungsaktivität ist Teil einer (größeren) Forschungsaktivität der Forschungsgruppe und trägt zu deren Erfolg bei.

Beispiele für solche Forschungsaktivitäten sind etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation (u.ä.). Am Ende des Semesters werden die Ergebnisse des Forschungspraktikums auf drei bis fünf Seiten dokumentiert, sowie zum letzten Vorlesungstermin im Rahmen eines Kolloquiums in jeweils etwa 10 bis 15 Minuten präsentiert und in einer anschließenden Fragerunde diskutiert.

Qualifikationsziele

Einen Forschungsansatz und die eigene Forschungs(teil-)aufgabe verstehen, begründen, bewerten und einordnen können
Aus der Aufgabenbeschreibung konkrete Arbeitsschritte entwickeln können
In dem Forschungsbereich des Projekts wissenschaftlich arbeiten können
Die für das Projekt relevanten inhaltlichen Grundlagen kennen, einsetzen und die Relevanz für die Fragestellung bewerten können
Forschungsergebnisse dokumentieren, zusammenfassen und präsentieren, sowie diskutieren können

Methodische Begleitveranstaltungen

Neben der Forschungsarbeit umfasst das Praktikum auch die folgenden mit der Projektarbeit verzahnten methodischen Veranstaltungen im Rahmen von zwei Leistungspunkten (LP), die im Rahmen des Forschungspraktikums als Schlüsselqualifikationsleistungen zu besuchen sind:

Literaturrechereche und Zitieren (2,0 Stunden)
Projektmanagementworkshop (7,0 Stunden)
Präsentationsworkshop (8,0 Stunden)
Erkenntnistheorie (1,5 Stunden)
Wissenschaftstheorie (1,5 Stunden)
Workshop zum Aufstellen einer Forschungsfrage (3,0 Stunden)
Schreiben von Forschungsanträgen (1,5 Stunden)
Experimentaldesign (1,5 Stunden)

Die Workshops zu Projektmanagement und Präsentationen finden in Kooperation mit dem House of Competence (HoC) statt. Alle Veranstaltungen sind gezielt auf Forschungsprojekte im Bereich der Informatik ausgerichtet. Die Termine der Veranstaltungen werden zu Vorlesungsbeginn bekanntgegeben.

Themen

Die Themen werden zu Beginn der Vorlesung vorgestellt. Zudem sind wir offen für Themenvorschläge, die im Zusammenhang zur Vorlesung bzw. zur Forschung unserer Forschungsgruppe stehen. Beispiele hierfür sind Forschungsaktivitäten wie etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation ausgewählter formaler Methoden (u.ä.). An dieser Stelle werden wir vor Beginn der Vorlesung eine Auswahl geplanter Themen auflisten. Bei Fragen hierzu können Sie sich bereits im Vorfeld bei den genannten Ansprechpersonen melden. Gern gesehen sind auch Initiativanfragen zu Themengebieten unserer Forschungsgruppe.

Relationale Verifikation von Algorithmenimplementierungen
Wenn im Rahmen von Programmierkursen Algorithmen implementiert werden sollen, ist es wichtig zu prüfen, ob die Abgaben sich auch strukturell an die Vorgaben der Aufgabe halten.

In diesem Projekt passen Sie relationale Verifikationsansätze so an, dass damit überprüfbar ist, ob sich eine Programmierlösung im Bereich der vorgesehenen Lösungen bewegt.

Beispiel: Eine Bubblesort-Implementierung ist im Ergebnis zwar ununterscheidbar von einer Quicksort-Implementierung, aber eben nicht der gleiche Algorithmus. Eine Quicksort-Implementierung, die ein anderes Pivot-Element wählt, dagegen schon.

Betreuung: Mattias Ulbrich
Verifikation des "Verifying Key Servers" HAGRID
Seit letztem Jahr ist HAGRID der neue Standard für PGP-Keyserver. Diese Neuentwicklung war notwendig, da der alte PGP-Keyserver aufgrund diverser Sicherheits- und Datenschutzvorfälle (CVE-2019-13050, GPRD), sowie Performanceproblemen nicht mehr tragfähig war.

Aber verwaltet HAGRID die Schlüssel auch korrekt? Ist es sicher?

HAGRID ist Gegenstand des diesjährigen Verifikationswettbewerbs "VerifyThis LongTerm Challenge".

In diesen Projekt wenden Sie das Verifikationswerkzeug KeY an, um die Korrektheit einer abstrahierten, auf den kritischen Kern fokussierten Java-Version von HAGRID zu beweisen. Hierzu gibt es bereits erste Untersuchungen – allerdings mit der vereinfachenden Annahme, dass die gespeicherten E-Mails und öffentlichen Schlüssel nur Integer (und bspw. keine Strings) sind.

An diese Untersuchung schließt sich dieses Projekt an: Wir wollen nun eine Version verifizieren, die mit Zeichenketten arbeitet. Neben der Verifikation kann dieses Projekt auch Erweiterungen der logischen Modellierung in KeY umfassen.

Betreuung: Mattias Ulbrich, Alexander Weigl
Evaluation der String-Theorie in SMT-Solvern
SMT-Solver unterstützen mittlerweile auch die Theorien von Zeichenketten und Sequenzen. In diesem Projekt evaluieren Sie die Eignung der Entscheidungstheorien für die Programmverifikation.

Das Projekt beinhaltet dabei die Einarbeitung in die Verwendung von SMT-Solvern und die String-Theorie, das Aufstellen und Beschreiben von Beispielen aus der Programmverifikation, sowie die Durchführung der Evaluation. Gegebenenfalls versuchen Sie hierbei, die genannten Fragestellungen zu optimieren.

Betreuung: Jonas Schiffl
Ermittlung von Spezifikationsabdeckungen mittels Slicing
Die Validität einer formalen Spezifikation ist eine klassische Fragestellung formaler Methoden. Diese besteht in der Übersetzungen einer "gemeinten", "gedachten" und "erwarteten" (d.h. insbesondere informellen) Spezifikation in eine formale Spezifikation.

In diesem Projekt gehen Sie diese Frage quantitativ an. Die Zielsetzung besteht darin, zu bestimmen, wie viele (bzw. welche) Programmbefehle überhaupt einen Einfluss auf die Spezifikation haben. Hierzu bauen Sie eine Pipeline aus den folgenden bestehenden Werkzeugen: (a) einer spezifikationsgetriebenen Generierung von Laufzeitbedingungen (sogenannten Runtime Assertions) sowie (b) einem Programm-Slicer.

Das Projekt beinhaltet die Einarbeitung in die obige Fragestellung, die Formalisierung des Problems, sowie der Konstruktion der Pipeline und deren anschließender Evaluierung.

Betreuung: Alexander Weigl, Mattias Ulbrich

Ansprechpartner