Weiterentwicklung Formaler Methoden zur Unterstützung des Designs neuer homogener verteilter Systeme und Technologien mit hybrider Resilienz

• Antragsteller: Privatdozent Dr.-Ing. Swen Jacobs
• Fachliche Zuordnung: Theoretische Informatik ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 513487900

Computersysteme in Banken und Versicherungsgesellschaften, aber auch in autonomen Fahrzeugen oder Satelliten sind vielversprechende Ziele für Cyberattacken und müssen geschützt werden um solchen Attacken zu widerstehen, oder um sie auszuhalten und dennoch sicher zu funktionieren. Leider gewinnen Angreifer mit zunehmender Komplexität dieser Systeme immer mehr Möglichkeiten, weshalb wir bei ihrer Verteidigung annehmen müssen, dass manche Attacken erfolgreich sein könnten. Glücklicherweise existieren bereits Resilienz-Techniken, wie etwa die dreifache Replikation des Computersystems mitsamt des Protokolls, um dann durch Abstimmung das korrekte Ergebnis zu bestimmen, auch wenn eine der Instanzen wegen einer erfolgreichen Cyberattacke ein fehlerhaftes Ergebnis liefert. Damit diese Techniken angewendet werden können, müssen sie aber auf die Struktur des Systems abgestimmt sein, insbesondere darauf wie die Komponenten des Systems miteinander interagieren. Die Resilienz-Techniken, die bisher entwickelt wurden, sind auf gewisse Formen der Interaktion eingeschränkt, und die Entwicklung neuer Techniken für aufwendigere Formen der Interaktion ist immer noch eine schwierige und fehleranfällige Aufgabe. Insbesondere können Tools, die die Entwicklung solcher Protokolle durch Korrektheitsprüfungen unterstützen, üblicherweise nur auf komplett fertiggestellte Protokolle angewandt werden, und ihre Anwendung benötigt darüber hinaus seltenes Expertenwissen. Im FM-CReST Projekt haben sich Forscher vom CISPA, Deutschland, und aus dem SnT der Universität Luxembourg zusammengeschlossen, um eine neue Klasse in hohem Maße automatisierter und leicht bedienbarer Tools zu entwickeln, die beim Design beweisbar korrekter Resilienz-Protokolle Unterstützung bieten. Um dies zu erreichen, setzen wir auf Co-Design von Protokollen mit komplexen Interaktionsformen, und basieren die Entwicklung unserer Tools auf den Beobachtungen während der Protokollentwicklung, mit dem Ziel ähnliche Aufgaben in Zukunft zu vereinfachen.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Luxemburg
• Kooperationspartner: Professor Dr.-Ing. Marcus Völp