Jacobs

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.

Gefördert durch die Deutsche Forschungsgemeinschaft (DFG) -513487900

Fördergeber

Fördergeber

Deutsche Forschungsgemeinschaft

In diesem Projekt wollen wir Globale Synchronisationsprotokolle (GSPs) als ein neues Rechenmodell für nebenläufige Systeme mit einer parametrischen Anzahl von Komponenten einführen. Zusätzlich zu lokalen Updates einer Komponente unterstützen GSPs synchrone globale Updates des Systems, die mittels Bedingungen an den globalen Zustand des Systems beschränkt sein können. Mit dieser Kombination eignen sie sich zur Modellierung von Anwendungen, die auf globaler Synchronisation, z.B. mittels Consensus oder Leader Election, basieren - auf einem Abstraktionslevel der die interne Implementierung des Übereinstimmungsprotokolls verbirgt, aber seine Vor- und Nachbedingungen originalgetreu abbildet. Wir werden Bedingungen identifizieren, unter denen parametrierte Sicherheitsverifikation von GSPs entscheidbar bleibt, obwohl dieses Problem im Allgemeinen für die Kombination der in GSPs unterstützten Kommunikationsprimitive unentscheidbar ist. Eine vorläufige Version der GSPs unterstützt bereits globale Synchronisation und globale Transitionsbedingungen, und wir planen eine Erweiterung des Systemmodells um asynchrone Nachrichtenübermittlung sowie verschiedene Arten der Fehlerbehandlung, so dass die Entscheidbarkeit der parametrierten Verifikation erhalten bleibt. Weiterhin werden wir Bedingungen für kleine Cutoffs für die Sicherheitsverifikation identifizieren, d.h. kleine Schranken auf die Anzahl der Komponenten, die in Betracht gezogen werden müssen um parametrische Sicherheitsgarantien zu bestimmen. Basierend auf diesen Cutoffs werden wir auch einen Ansatz zur automatischen Synthese von GSPs entwickeln, die gegebene Eigenschaften per Konstruktion erfüllen. Zuletzt werden wir auch einen verfeinerungs-basierten Syntheseansatz für GSPs untersuchen, und seine Eigenschaften mit dem Cutoff-basierten Ansatz vergleichen.Unsere Erforschung entscheidbarer Fragmente von GSPs wird geleitet von Anwendungen in verschiedenen Bereichen, darunter Sensornetzwerke, Roboterschwärme und auf Blockchains basierende Anwendungen.

Fördergeber

Funding Body

Deutsche Forschungsgemeinschaft (DFG)