Constraint-based monitoring of hyperproperties

DOI10.1007/978-3-030-17465-1_7MaRDI QIDQ6091406zbMATH OpenFDO

Authors Christopher Hahn, Marvin Stenger, Leander Tentrup

Publication date 24 November 2023

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1905.13517

zbMATH Keywords

constraint-based monitoringhyperpropertiesrewriting

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: Verifying hyperproperties at runtime is a challenging problem as hyperproperties, such as non-interference and observational determinism, relate multiple computation traces with each other. It is necessary to store previously seen traces, because every new incoming trace needs to be compatible with every run of the system observed so far. Furthermore, the new incoming trace poses requirements on future traces. In our monitoring approach, we focus on those requirements by rewriting a hyperproperty in the temporal logic HyperLTL to a Boolean constraint system. A hyperproperty is then violated by multiple runs of the system if the constraint system becomes unsatisfiable. We compare our implementation, which utilizes either BDDs or a SAT solver to store and evaluate constraints, to the automata-based monitoring tool RVHyper.

Recommendations

• Monitoring hyperproperties
• Monitorable hyperproperties of nonterminating systems
• Gray-box monitoring of hyperproperties
• Runtime enforcement of hyperproperties
• Rewriting-based runtime verification for alternation-free HyperLTL

Cited in

(10)

• Runtime enforcement of hyperproperties
• Monitoring hyperproperties with circuits
• Monitorable hyperproperties of nonterminating systems
• Conformance relations and hyperproperties for doping detection in time and space
• Monitoring of Real-Time Properties
• Explaining Hyperproperty Violations
• Gray-box monitoring of hyperproperties
• Centralized vs decentralized monitors for hyperproperties
• Centralized vs. decentralized monitors for hyperproperties
• Parameter synthesis for probabilistic hyperproperties

This page was built for publication: Constraint-based monitoring of hyperproperties

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6091406)