Synthesis from Hyperproperties

In this talk, I will give an overview on the reactive synthesis problem for hyperproperties. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical examples are information-flow policies like noninterference, which stipulates that sensitive data must not leak into the public domain. Synthesis from hyperproperties subsumes many classical variations of reactive synthesis, such as synthesis under incomplete information, and the synthesis of distributed synthesis. A particularly interesting application is the compositional synthesis of distributed systems, where the information-flow assumptions between the different components are captured as hyperproperties. In general, synthesis from hyperproperties is undecidable. We will discuss a semi-decision procedure that constructs implementations up to a given bound, and a practical method that uses standard synthesis to find a permissive overapproximation of the implementation, and then refines the approximation until the hyperproperty is satisfied.