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.
Recommendations
Cites work
- scientific article; zbMATH DE number 2102704 (Why is no real title available?)
- A new solution of Dijkstra's concurrent programming problem
- Algorithms for model checking HyperLTL and HyperCTL^*
- Constraint-based monitoring of hyperproperties
- From LTL and limit-deterministic Büchi automata to deterministic parity automata
- Model checking quantitative hyperproperties
- Monitoring hyperproperties
- On the menbership problem for functional and multivalued dependencies in relational databases
- Optimal enforcement of (timed) properties with uncontrollable events
- Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time
- Program Repair for Hyperproperties
- Runtime enforcement monitors: Composition, synthesis, and enforcement abilities
- Runtime enforcement of security policies on black box reactive programs
- Shield synthesis: runtime enforcement for reactive systems
- Synthesizing reactive systems from hyperproperties
- Unifying hyper and epistemic temporal logics
- Verifying hyperliveness
Cited in
(16)- Program Repair for Hyperproperties
- HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
- Decentralized LTL enforcement
- On bidirectional runtime enforcement
- Constraint-based monitoring of hyperproperties
- Rewriting-based runtime verification for alternation-free HyperLTL
- Monitoring hyperproperties
- On runtime enforcement via suppressions
- Runtime enforcement with reordering, healing, and suppression
- Compositional runtime enforcement revisited
- Explaining Hyperproperty Violations
- Gray-box monitoring of hyperproperties with an application to privacy
- Deciding hyperproperties combined with functional specifications
- Temporal team semantics revisited
- scientific article; zbMATH DE number 6851935 (Why is no real title available?)
- Gray-box monitoring of hyperproperties
This page was built for publication: Runtime enforcement of hyperproperties
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147207)
