Runtime Enforcement of Hyperproperties

TL;DR

This paper explores runtime enforcement mechanisms for hyperproperties, focusing on two trace input models, and provides algorithms, undecidability results, and experimental validation for enforcing specifications expressed in HyperLTL.

Contribution

It introduces sound and transparent enforcement mechanisms for hyperproperties in parallel and sequential models, including algorithms and undecidability results.

Findings

Enforcement in the parallel model is based on parity games.

Enforcement in the sequential model is generally undecidable.

Prototype implementation demonstrates practical feasibility.

Abstract

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.