(2018) The Complexity of Monitoring Hyperproperties.
Abstract
—We study the runtime verification of hyperproperties, expressed in the temporal logic HyperLTL, as a means to inspect a system with respect to security polices. Runtime monitors for hyperproperties analyze trace logs that are organized by common prefixes in the form of a tree-shaped Kripke structure, or are organized both by common prefixes and by common suffixes in the form of an acyclic Kripke structure. Unlike runtime verification techniques for trace properties, where the monitor tracks the state of the specification but usually does not need to store traces, a monitor for hyperproperties repeatedly model checks the growing Kripke structure. This calls for a rigorous complexity analysis of the model checking problem over treeshaped and acyclic Kripke structures.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Uncontrolled Keywords: | computational complexity;formal verification;temporal logic;trees (mathematics);model checking problem;runtime monitors;tree-shaped Kripke structure;acyclic Kripke structure;runtime verification techniques;HyperLTL formula;hyperproperties;temporal logic HyperLTL;polynomial hierarchy;Complexity theory;Model checking;Monitoring;Runtime;Shape;Security;Protocols;Runtime-verification;Model-checking;Hyperproperties;HyperLTL |
| Conference: | CSF IEEE Computer Security Foundations Symposium (was CSFW) |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 23 Jun 2019 18:39 |
| Last Modified: | 15 Oct 2020 13:45 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/2931 |
Actions
Actions (login required)
 |
View Item |