Algorithms for reasoning about information flow and knowledge in distributed systems

Abstract

This thesis shows how reasoning about information flow and knowledge, two core hyperproperties in the security and verification of distributed systems, can guide the design of correct-by-construction synthesis algorithms. Traditionally, these notions appear only as system requirements: security constrains information flow, and agents act based on what they know. By reinterpreting them as principles for algorithm design, we develop fundamentally new compositional synthesis methods. For distributed synthesis, whose goal is to automatically build component implementations that jointly satisfy a specification, we introduce explicit assumptions about the necessary information flow between components. These assumptions enable a decomposition into subproblems whose local solutions compose into a globally correct system. For controller synthesis, where the synthesized controller has to correctly govern a plant, we introduce prophecies: declarative statements of what a controller must know about a plant’s implementation. Prophecies allow us to construct a universal controller that is correct for all plants and can later be specialized to a concrete plant. Finally, we take first steps toward handling common knowledge, the shared agreement among agents, by lifting existing temporal hyperlogics to express second-order hyperproperties. We also present a monitoring algorithm that checks, during execution, whether a distributed system satisfies a second-order hyperproperty.

Diese Arbeit zeigt, wie die Analyse von Informationsfluss und Wissen, zwei zentrale Hypereigenschaften in der Sicherheit und Verifikation verteilter Systeme, die Entwicklung von korrekt-durch-Konstruktion Synthesealgorithmen positiv beeinflussen kann. Traditionell treten diese Begriffe nur als Systemanforderungen auf: Sicherheit beschränkt den Informationsfluss, und Agenten handeln basierend auf dem, was sie wissen. Indem wir sie als Entwurfsprinzipien für das Algorithmendesign neu interpretieren, entwickeln wir grundlegend neue Methoden für die kompositionelle Synthese. Für die verteilte Synthese, deren Ziel es ist, automatisch mehrere Implementierungen zu erzeugen, die gemeinsam eine Spezifikation erfüllen, führen wir explizite Annahmen über den notwendigen Informationsfluss zwischen Komponenten ein. Diese Annahmen ermöglichen eine Zerlegung in Teilprobleme, deren lokale Lösungen zu einem global korrekten System zusammengesetzt werden können. Für die Controllersynthese, bei der der synthetisierte Controller eine Strecke korrekt steuern muss, führen wir Prophezeiungen ein: deklarative Aussagen darüber, was ein Controller über die Implementierung einer Strecke wissen muss. Prophezeiungen erlauben es uns, einen universellen Controller zu konstruieren, der für jede Strecke korrekt ist und später auf eine konkrete Strecke spezialisiert werden kann. Abschließend unternehmen wir erste Schritte zur Behandlung von Allgemeinwissen, dem geteilten Wissen der Agenten, indem wir bestehende temporale Hyperlogiken so erweitern, dass sie Hypereigenschaften zweiter Stufe ausdrücken können. Zudem präsentieren wir einen Monitoring-Algorithmus, der zur Laufzeit überprüft, ob ein verteiltes System eine Hypereigenschaft zweiter Stufe erfüllt.