Gesucht wird ein Hiwi für die Erweiterung und Pflege der Lehrstuhlarbeiten im Quis-Custodiet-Projekt mit Isabelle/HOL.
Software-Sicherheitsanalysen sind heute unverzichtbar. Aber: Quis Custodiet Ipsos Custodes? ("Wer bewacht die Wächter?", Juvenal, Satire 6) Die theoretischen Korrektheitsanforderungen an Sicherheitsanalysen sind seit langem bekannt, aber viele Verfahren werden ohne Korrektheitsbeweise publiziert, etliche nur mit einem manuellen. Maschinengeprüfte Korrektheitsbeweise gibt es nur für einige einfache Verfahren zur Software-Sicherheitsprüfung. Aus diesem Grund verwendet der Lehrstuhl wir den Theorembeweise Isabelle/HOL, um Programmiersprachen wie Java und C++ und entsprechende Analyseverfahren für diese zu formalisieren und zu verifizieren.
Durch den Einsatz eines Theorembeweisers, der jeden Beweisschritt auf seine Richtigkeit hin überprüft, wird sichergestellt, dass sich keine Fehler in die Beweise einschleichen können.
Im Rahmen der Tätigkeit können Sie sich folgende Kenntnisse erwerben:
- Verständnis in formalen Semantiken und Programmanalyseverfahren
- Beweis- und moderne Verifikationstechnik
- Umgang mit einem weitverbreiteten Theorembeweiser
- Übung im Modellieren, Formalisieren und Beweisen
Aufgabe:
- Einarbeitung in Isabelle/HOL
- Einarbeitung in den thematischen Kontext "Semantiken und Programmanalyse"
- Erweiterung und Überarbeitung der bestehenden Semantiken für C++ und Java um neue Features
- Eigenständige Formalisierung und Verifikation einfacher Softwaresicherheitsanalysen
Voraussetzungen
- Gute Kenntnisse in Logik und Deduktionssysteme
- Abstraktes Denkvermögen, Fähigkeit zum Umgang mit formalen Systemen
- Kenntnisse in funktionaler Programmierung (z.B. ML)
- Erfahrung mit Isabelle/HOL auf Isar-Ebene oder die Bereitschaft, sich diese anzueignen
- Kenntnisse in Programmiersprachen und Semantik sind wünschenswert, aber nicht zwingend nötig.
Schlüsselworte
Softwaresicherheit, Programmanalyse, Theorembeweiser, Verifikation Betreuer
| Ehemalige Mitarbeiter |
|---|
| Dipl.-Inform. Denis Lohner |