Information Flow Guided Synthesis with Unbounded Communication

TL;DR

This paper introduces a novel method for automatically constructing information flow assumptions in distributed systems, capable of handling unbounded communication scenarios, and presents a practical synthesis tool that outperforms previous methods.

Contribution

It presents the first approach to handle unbounded information flow requirements in distributed synthesis and offers a practical synthesis technique implemented in the FlowSy tool.

Findings

FlowSy outperforms previous approaches on benchmarks.

The method can analyze protocols with infinite message streams.

It enables synthesis of components from unbounded information flow specifications.

Abstract

Information flow guided synthesis is a compositional approach to the automated construction of distributed systems where the assumptions between the components are captured as information-flow requirements. Information-flow requirements are hyperproperties that ensure that if a component needs to act on certain information that is only available in other components, then this information will be passed to the component. We present a new method for the automatic construction of information flow assumptions from specifications given as temporal safety properties. The new method is the first approach to handle situations where the required amount of information is unbounded. For example, we can analyze communication protocols that transmit a stream of messages in a potentially infinite loop. We show that component implementations can then, in principle, be constructed from the information flow requirements using a synthesis tool for hyperproperties. We additionally present a more practical synthesis technique that constructs the components using efficient methods for standard synthesis from trace properties. We have implemented the technique in the prototype tool FlowSy, which outperforms previous approaches to distributed synthesis on several benchmarks.