  An enforcement mechanism monitors a reactive system for undesired behavior at
runtime and corrects the system's output in case it violates the given
specification. In this paper, we study the enforcement problem for
hyperproperties, i.e., properties that relate multiple computation traces to
each other. We elaborate the notion of sound and transparent enforcement
mechanisms for hyperproperties in two trace input models: 1) the parallel trace
input model, where the number of traces is known a-priori and all traces are
produced and processed in parallel and 2) the sequential trace input model,
where traces are processed sequentially and no a-priori bound on the number of
traces is known. For both models, we study enforcement algorithms for
specifications given as formulas in universally quantified HyperLTL, a temporal
logic for hyperproperties. For the parallel model, we describe an enforcement
mechanism based on parity games. For the sequential model, we show that
enforcement is in general undecidable and present algorithms for reasonable
simplifications of the problem (partial guarantees or the restriction to safety
properties). Furthermore, we report on experimental results of our prototype
implementation for the parallel model.
