Fraunhofer-Institut für Thorsten Koch promoviert zum Thema Security Protokolle
Am 7. Mai 2024 hat unser Kollege Thorsten Koch erfolgreich seine Promotion bei Professor Eric Bodden abgeschlossen. In seinem Dissertationsvorhaben entwickelte er einen Ansatz zur Spezifikation und Verifikation von Security Protokollen sowie deren Verwendung im szenario-basierten Requirements Engineering.
Thorsten Koch ist seit 2014 wissenschaftlicher Mitarbeiter in der Abteilung Sichere loT-Systeme des Fraunhofer IEM. In unterschiedlichen Forschungs- und Industrieprojekten legt er seinen Fokus auf das Thema Softwareentwicklung im Maschinen- und Anlagenbau. Hier konzentriert er sich insbesondere auf das Konzipieren und Durchführen von zielgruppengerechten Weiterbildungen zur Entwicklung sicherer Systeme. Das ganze Team des Fraunhofer lEM gratuliert herzlich zur
Promotion!
Zur Dissertation: Spezifikation und Verifikation von Security Protokollen sowie deren Verwendung im szenario-basierten Requirements Engineering
Security Protokolle spielen eine zentrale Rolle, um die Kommunikation von software-intensiven Systemen vor Cyberangriffen zu schützen. Die korrekte Spezifikation und Anwendung dieser Protokolle ist jedoch langwierig und fehleranfällig. Mit Hilfe des symbolischen Model-Checkings wird überprüft, ob die Spezifikation korrekt ist und das Protokoll die gewünschten Eigenschaften aufweist.
Allerdings reicht ein einzelner Model-Checker nicht aus, um das Protokoll vollständig zu verifizieren. Stattdessen müssen mehrere Model-Checker verwendet werden. Dies führt zu einer zeitaufwändigen und fehleranfälligen Modellierung desselben Protokolls in verschiedenen Eingabesprachen. Darüber ninaus adressieren die heutigen Ansätze zum Requirements Engineering entweder funktionale oder sicherheits-bezogene Anforderungen. Es ist daher schwer zu beurteilen, ob die spezifizierten Maßnahmen ausreichen, um das System abzusichern und ob die Maßnahmen zu Konflikten mit anderen funktionalen Anforderungen führen.
Ziel des Dissertationsvorhabens war ein modellbasierter Ansatz zur Spezifikation und Verifikation von Security Protokollen sowie deren Verwendung im szenario-basierten Requirements
Engineering. Auf Basis einer UML-konformen Modellierungssprache können Protokolle nun spezifiziert und automatisch in die Eingabesprache verschiedener Model-Checker überführt werden. Zudem können die spezifizierten Protokolle mit Hilfe eines template-basierten Ansatzes systematisch in eine Anforderungsspezifikation integriert werden