Cargando…
Monitoring hyperproperties
Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. [Formula: see text] ext...
Autores principales: | , , , |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer US
2019
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6853877/ https://www.ncbi.nlm.nih.gov/pubmed/31806925 http://dx.doi.org/10.1007/s10703-019-00334-z |
_version_ | 1783470119356203008 |
---|---|
author | Finkbeiner, Bernd Hahn, Christopher Stenger, Marvin Tentrup, Leander |
author_facet | Finkbeiner, Bernd Hahn, Christopher Stenger, Marvin Tentrup, Leander |
author_sort | Finkbeiner, Bernd |
collection | PubMed |
description | Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. [Formula: see text] extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express hyperproperties. We investigate the runtime verification problem of [Formula: see text] formulas for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions is a-priori unbounded and may in fact grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that the existence of a bound in the parallel and bounded sequential models leads to a different notion of monitorability than in the unbounded sequential model. We show that deciding the monitoriability problem for alternation-free HyperLTL is [Formula: see text] -complete while the problem is undecidable in general. For every input model, we provide monitoring algorithms along with run-time and storage optimizations. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimizes the number of traces that need to be stored. We evaluate our optimizations, showing that this leads to a more scalable monitoring and, in particular, a significantly lower memory consumption. |
format | Online Article Text |
id | pubmed-6853877 |
institution | National Center for Biotechnology Information |
language | English |
publishDate | 2019 |
publisher | Springer US |
record_format | MEDLINE/PubMed |
spelling | pubmed-68538772019-12-03 Monitoring hyperproperties Finkbeiner, Bernd Hahn, Christopher Stenger, Marvin Tentrup, Leander Form Methods Syst Des Article Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. [Formula: see text] extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express hyperproperties. We investigate the runtime verification problem of [Formula: see text] formulas for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions is a-priori unbounded and may in fact grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that the existence of a bound in the parallel and bounded sequential models leads to a different notion of monitorability than in the unbounded sequential model. We show that deciding the monitoriability problem for alternation-free HyperLTL is [Formula: see text] -complete while the problem is undecidable in general. For every input model, we provide monitoring algorithms along with run-time and storage optimizations. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimizes the number of traces that need to be stored. We evaluate our optimizations, showing that this leads to a more scalable monitoring and, in particular, a significantly lower memory consumption. Springer US 2019-06-25 2019 /pmc/articles/PMC6853877/ /pubmed/31806925 http://dx.doi.org/10.1007/s10703-019-00334-z Text en © The Author(s) 2019 Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made. |
spellingShingle | Article Finkbeiner, Bernd Hahn, Christopher Stenger, Marvin Tentrup, Leander Monitoring hyperproperties |
title | Monitoring hyperproperties |
title_full | Monitoring hyperproperties |
title_fullStr | Monitoring hyperproperties |
title_full_unstemmed | Monitoring hyperproperties |
title_short | Monitoring hyperproperties |
title_sort | monitoring hyperproperties |
topic | Article |
url | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC6853877/ https://www.ncbi.nlm.nih.gov/pubmed/31806925 http://dx.doi.org/10.1007/s10703-019-00334-z |
work_keys_str_mv | AT finkbeinerbernd monitoringhyperproperties AT hahnchristopher monitoringhyperproperties AT stengermarvin monitoringhyperproperties AT tentrupleander monitoringhyperproperties |