CISPA
Browse
cispa_all_3661.pdf (356.5 kB)

Runtime Enforcement of Hyperproperties

Download (356.5 kB)
Version 2 2023-12-11, 20:14
Version 1 2023-11-29, 18:18
conference contribution
posted on 2023-12-11, 20:14 authored by Norine CoenenNorine Coenen, Bernd FinkbeinerBernd Finkbeiner, Christopher Hahn, Jana Hofmann, Yannick Schillo
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.

History

Preferred Citation

Norine Coenen, Bernd Finkbeiner, Christopher Hahn, Jana Hofmann and Yannick Schillo. Runtime Enforcement of Hyperproperties. In: International Symposium on Automated Technology for Verification and Analysis (ATVA). 2021.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

International Symposium on Automated Technology for Verification and Analysis (ATVA)

Legacy Posted Date

2022-05-06

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3661, title = "Runtime Enforcement of Hyperproperties", author = "Coenen, Norine and Finkbeiner, Bernd and Hahn, Christopher and Hofmann, Jana and Schillo, Yannick", booktitle="{International Symposium on Automated Technology for Verification and Analysis (ATVA)}", year="2021", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC