Opazität von Large-Scale Cyber-Physikalischen Systemen

• Antragsteller: Professor Dr. Majid Zamani
• Fachliche Zuordnung: Automatisierungstechnik, Mechatronik, Regelungssysteme, Intelligente Technische Systeme, Robotik
• Förderung: Förderung seit 2021
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 449086651

Im vergangenen Jahrzehnt war ein erhebliches Interesse an der algorithmischen Verifikation von a-priori korrekter Reglersynthese für cyber-physikalische Systeme (CPS) zu beobachten, bei denen Softwarekomponenten eng mit physikalischen Systemen interagieren. CPS führen in modernen Anwendungen immer öfter sicherheitskritische Aufgaben aus, bei denen sich ein Entwurfsfehler oder eine Sicherheitsschwachstelle katastrophal auswirken kann. Autonome Fahrzeuge, implantierbare medizinische Geräte und smarte vernetzte Gemeinschaften (Smart Cities) sind einige der oft genannten Beispiele, welche die Probleme der Privatssphäre und Sicherheitskritikalität von modernen CPS unterstreichen.Im vergangenen Jahrzehnt haben Sicherheitsbedenken beim Entwurf von CPS eine beachtliche Aufmerksamkeit erhalten, während die Sicherheitsanalyse eher ein Nebengedanke für spätere Entwicklungsschritte geblieben ist. Eine der wichtigen Sicherheitseigenschaften wird Opazität (Nicht-Transparenz) genannt. Grob gesagt ist Opazität eine Vertraulichkeits- oder Privatheitseigenschaft in der Sicherheitsanalyse, die charakterisiert ob externe Beobachter mit potentiell bösartigen Absichten (z.B.~Eindringlinge oder Angreifer) eine "geheime" Information über das System (z.B.~Verteidiger) erschließen können. Viele der CPS-Anwendungen sind sicherheitskritisch mit einer gewissen Verwundbarkeit gegenüber (Cyber-)Attacken, und Opazität kann bestimmte formale Garantien liefern für die plausible Abstreitbarkeit der "geheimen" Systemeigenschaft in der Gegenwart eines potentiell bösartigen Beobachters. Dieses Projekt zielt darauf ab, die Anwendbarkeit formaler Methoden zum Entwurf zuverlässiger und sicherer CPS zu vergrößern. Jüngere theoretische Fortschritte, zum Teil durch Mitglieder unseres Forschungsteams, lassen dieses Ziel erreichbar werden. Insbesondere schlagen wir algorithmische Ansätze vor, um Regler für CPS zu synthetisieren, die a-priori Sicherheit garantieren. Dabei nehmen wir an, dass die Sicherheitsanforderungen an das System durch Formeln der temporalen Logik (wie z.B.~lineare temporale Logik) beschrieben werden oder durch Automaten über unendlichen Zeichenketten. Dann konstruieren wir eine endliche Abstraktion des CPS, so dass Opazitätseigenschaften beim Übergang zur Abstraktion erhalten bleiben und ein a-priori sicherer Regler, der für die endliche Abstraktion entworfen wurde, verfeinert werden kann zu einem a-priori sicheren Regler für das ursprüngliche System. Um den Rechenaufwand, der sich bei endlichen Systemen ergibt, zu verringern, schlagen wir zudem kompositionelle Methoden vor zur formalen Verifikation oder zum Erzwingen von Opazität für hochdimensionale vernetzte CPS. Dabei machen wir uns als Hauptwerkzeug Zerlegungen in Teilsysteme zunutze, um den mit der Analyse oder dem Entwurf verbundenen Rechenaufwand zu bewältigen

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: China
• Partnerorganisation: National Natural Science Foundation of China
• Kooperationspartner: Professor Xiang Yin, Ph.D.