  We study the reactive synthesis problem for hyperproperties given as formulas
of the temporal logic HyperLTL. Hyperproperties generalize trace properties,
i.e., sets of traces, to sets of sets of traces. Typical examples are
information-flow policies like noninterference, which stipulate that no
sensitive data must leak into the public domain. Such properties cannot be
expressed in standard linear or branching-time temporal logics like LTL, CTL,
or CTL$^*$. We show that, while the synthesis problem is undecidable for full
HyperLTL, it remains decidable for the $\exists^*$, $\exists^*\forall^1$, and
the $\mathit{linear}\;\forall^*$ fragments. Beyond these fragments, the
synthesis problem immediately becomes undecidable. For universal HyperLTL, we
present a semi-decision procedure that constructs implementations and
counterexamples up to a given bound. We report encouraging experimental results
obtained with a prototype implementation on example specifications with
hyperproperties like symmetric responses, secrecy, and information-flow.
