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...

Descripción completa

Detalles Bibliográficos
Autores principales: Finkbeiner, Bernd, Hahn, Christopher, Stenger, Marvin, Tentrup, Leander
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