(2021) Runtime Enforcement of Hyperproperties.
|
Text
CFHHS21.pdf Download (365kB) | Preview |
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Christopher Hahn |
| Date Deposited: | 06 May 2022 07:03 |
| Last Modified: | 06 May 2022 07:03 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3661 |
Actions
Actions (login required)
 |
View Item |