Entwicklung eines STPA-Verifiers als Eclipse-Plug-in für die Verifikation von Software-Sicherheitsanforderungen

Abstract

Um die Sicherheit in kritischen Softwaresystemen zu gewährleisten ist immer häufiger eine Verifikation der Software in einem Systemkontext notwendig. Hierfür ist in den letzten Jahren die Verifikation von Softwaresystemen durch Model Checking, bedingt durch die wachsende Anzahl an dafür zur Verfügung stehenden Werkzeugen, eine bewährte Methode geworden. Diese Arbeit stellt auf Grundlage des in STPA SwISS [AWL15] vorgestellten Konzeptes eine Software zur automatisierten Ausführung von LTL und CTL Model Checking mit den Werkzeugen Spin und NuSMV bietet. Dabei können die Sicherheitsanforderungen sowohl manuell eingegeben werden, als auch aus einer STPA Analyse importiert werden. Das Ergebnis dieser Arbeit soll ein Ansatz zur Kombination einer Gefahrenanalyse auf Systemebene und einer Verifikation dieses Systems auf Implementierungsebene sein. Zu diesem Zweck wird der STPA Verifier zur automatisierten Verifikation von Sicherheitsanforderungen und Dokumentation der Ergebnisse vorgestellt.

To verify the safety on a critical softwaresystem includes more and more often the task of verifying Software in the context of the system. In the last years verifying software by using formal model checking has become a more and more popular method due to the increasing number of available tool support. This work presents a Software based on the concepts of the STPA SwISS approach [AWL15] that provides a graphical user interface for performing automated LTL and CTL model checking using the Spin or the NuSMV model checker. The safety properties can be derived either manually or by importing the results of a STPA hazard analysis. The result of this work are supposed to be an approach to combine a hazard analysis on system level and a Softwareverification on implementation level. To provide this the STPA Verifier for verfying safety constraints and creating a verification report is presented.