Institute of Information Security and Dependability (KASTEL) – Application-oriented Formal Verification
Institute of Information Security and Dependability (KASTEL) – Application-oriented Formal Verification
Home

Vorlesungsbegleitendes Forschungspraktikum
im Wintersemester 2020/21

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ück zur Seite der Vorlesung

Inhalt

Das Forschungspraktikum wird optional vorlesungsbegleitend zur Vorlesung Formale Systeme als Praktikum im Umfang von insgesamt 5 LP (davon 2 SQ) angeboten. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Zu Beginn der Vorlesung werden Themen vorgestellt, für die sich die Studierenden bewerben können. Dabei basieren diese thematisch auf in der gekoppelten Vorlesung vermittelten Inhalten bzw. verknüpfen die Vorlesunginhalte und mit der aktuellen Forschung des Lehrstuhls. Die praktische Forschungsaktivität ist Teil einer größeren Forschungsaktivität und trägt zu deren Erfolg bei.

Zum Ende der Vorlesung werden die Ergebnisse in einem etwa 15-minütigen Vortrag präsentiert und in einer anschließenden Fragerunde diskutiert. Am Ende des Semesters werden die Ergebnisse des Forschungspraktikums abschließend in einer schriftlichen Ausarbeitung von 3 bis 5 Seiten dokumentiert.

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 (parallel zu besuchenden) mit der Projektarbeit verzahnten methodischen Veranstaltungen im Rahmen von zwei Leistungspunkten (Schlüsselqualifikation):

  • 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 stehen. Beispiele hierfür sind Forschungsaktivitäten wie etwa die Entwicklung eines Prototypen oder die Durchführung einer Evaluation (u.ä.). Im Folgenden finden Sie bereits eine Auflistung der vorläufig geplanten Themen. Bei Fragen hierzu können Sie sich bereits im Vorfeld bei den genannten Ansprechpersonen melden.

  • Verifikation von MPI-Programmen mit Session Types

    Ein neue Funktionalität in Frama-C – einem Werkzeug zur deduktiven Verifikation von C-Programmen – ermöglicht die Verifikation von parallelen C-Programmen, die das sogenannte Message Passing Interface (MPI) verwenden. Die Erweiterung basiert auf einem Typsystem, das Eigenschaften wie session fidelity, deadlock freedom und resource-leak freedom garantiert.

    In diesem Forschungspraktikum evaluieren Sie das Tool anhand verschiedener praktischer Beispiele und entwickeln bei Bedarf auch Weitere.

    Das Projekt beinhaltet dabei die Einarbeitung in Session Types, Durchführung formaler Verifikation mit Frama-C und Why3, sowie Gestaltung, Durchführung und Interpretation von Experimenten.

    Betreuung: Lionel Blatter

  • 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

  • Relationale Verifikation höherer Ordnung mit HyperMC

    Wie verifiziert man Programmeigenschaften bezüglich vier Ausführungen? Eine interessante Eigenschaft die auf vier Programmausführungen definiert ist, ist die Überprüfung von Regressionen beim "Leaken" von Geheimnissen. In diesem Projekt evaluieren Sie hierzu HyperMC, einen Model-Checker für HyperLTL.

    Das Projekt beinhaltet die Einarbeitung in HyperMC, die Formalisierung der Leakage-Regression für reaktive Programme, sowie die Gestaltung, Durchführung und Interpretation der Experimente.

    Betreuung: Mattias Ulbrich

  • Evaluierung der Modellierung von finalen Feldern

    Eine neue Behandlung von finalen Feldern für KeY (Werkzeug zur Java-Programmverifikation) ist aktuell in der Integrationsphase. In diesem Projekt evaluieren Sie diese Behandlung zum einen auf Korrektheit sowie zum anderen auf den Performancevorteil.

    Das Projekt beinhaltet die Einarbeitung in KeY und dessen Java-Semantik, sowie die Gestaltung, Durchführung und Interpretation von Experimenten für die unterschiedlichen Evaluierungsziele.

    Betreuung: Mattias Ulbrich

  • 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

  • Automatisches Finden von Wahlmanipulationen mit Bounded Model Checking

    Die strategische Manipulation eines Wahlverfahrens ist das unwahre Abstimmen, um das Wahlergebnis zum eigenen Vorteil zu beeinflussen. Hierzu gibt es grundsätzliche Ergebnisse, dass jedes nicht-diktatorische Wahlverfahren dafür anfällig ist, jedoch lassen sich manche Wahlverfahren einfacher manipulieren als andere. Traditionell wird diese Fragestellung komplexitätstheoretisch untersucht, in neueren Arbeiten aber auch konkret quantifiziert.

    Das Projekt beinhaltet die Einarbeitung in obige Fragestellung, die Formalisierung einer solcher Quantifizierung für einfache Scoring-Wahlverfahren (z. B. relative Mehrheitswahl, Borda, ...) und die Entwicklung und Evaluation von Experimenten für den Bounded Model Checker CBMC, um solche Manipulationen automatisch zu generieren.

    Betreuung: Michael Kirsten

Ansprechperson

Bei Fragen rund um das Thema Forschungspraktikum (hier oder bei anderen Vorlesungen) können Sie sich bei Michael Kirsten melden.