Ableitung von Angriffen auf industrielle Kommunikationsprotokolle mittels Model Checking

Ansprechpatner:
Andreas Paul

Motivation

Zur Steuerung, Überwachung und Optimierung von Industrieanlagen werden seit geraumer Zeit SCADA-Systeme (supervisory control and data aquisition) eingesetzt. Während SCADA-Systeme früher ausschließlich aus proprietären Insellösungen bestanden, ist in den letzten Jahren ein starker Trend hin zu standardisierten und vollständig vernetzten Kommunikationsstrukturen erkennbar. Verbunden mit der zunehmenden Anbindung von SCADA-Systemen an öffentliche Netze steigt das Gefährdungspotential dieser Systeme durch Angriffe Dritter.Da existierende Sicherheitskonzepte den speziellen Anforderungen im industriellen Umfeld nicht gerecht werden, weisen hier eingesetzte Technologien im Allgemeinen fehlende Mechanismen zur Gewährleistung typischer IT-Schutzziele auf. Ein erster Schritt zur Entwicklung geeigneter Schutzmaßnahmen stellt die Identifizierung von Schwachstellen und konkreten Verwundbarkeiten der eingesetzten Kommunikationsprotokolle dar. Hierbei wird die Ableitung von Angriffsszenarien in einem aufwendigen und Fehleranfälligen Analyseprozess derzeit ausschließlich manuell vorgenommen.

Aufgabenbeschreibung

Im Rahmen dieser Abschlussarbeit soll mit Hilfe von Methoden des Model Checking die Ableitung von Angriffen auf industrielle Kommunikationsprotokolle automatisiert und am Beispiel des Protokolls PROFINET IO evaluiert werden. Hierzu ist ein geeignetes Verifikationsmodell in der entsprechenden Spezifikationssprache - unter Berücksichtigung der speziellen Gegebenheiten industrieller Kommunikationsprotokolle - zu entwickeln. Außerdem müssen entsprechende Kriterien zur Verifikation des Protokolls definiert werden. Durch Auswertung der Verifikationsergebnisse sind schließlich konkrete Angriffssequenzen auf das Protokoll PROFINET IO abzuleiten.

Zusammenfassung

  • Einarbeitung in das Model Checking (z.B. in den Model Checker SPIN und in die Spezifikationssprache PROMELA )
  • Einarbeitung in das Industrial Ethernet Protokoll PROFINET IO (Material wird vom Betreuer zur Verfügung gestellt!)
  • Entwicklung eines Verifikationsmodells für PROFINET IO
  • Formulierung geeigneter Verifikationskriterien in LTL/CTL
  • Auswertung der Verifikation + Angriffsableitung

Sonstige Informationen

Die hier vorgestellten Aufgaben entsprechen dem Umfang einer Bachelorarbeit. Der Umfang der Aufgaben kann ggf. an eine Masterarbeit angepasst werden.