Thorsten Koch ist seit 2014 wissenschaftlicher Mitarbeiter in der Abteilung Sichere IoT-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 IEM 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 hinaus 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.