Analysis of complex security and privacy policies (e.g., information flow) involves reasoning about multiple execution traces. This stems from the fact that an external observer may gain knowledge about the system through observing and comparing several executions. Monitoring of such policies is in particular challenging because most existing monitoring techniques are limited to the analysis of a single trace at run time. In this paper, we present a rewriting-based technique for runtime verification of the full alternation-free fragment of HyperLTL, a temporal logic for specification of hyperproperties. The distinguishing feature of our proposed technique is its space complexity, which is independent of the number of trace quantifiers in a given HyperLTL formula.
CITATION STYLE
Brett, N., Siddique, U., & Bonakdarpour, B. (2017). Rewriting-based runtime verification for alternation-free hyperLTL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10206 LNCS, pp. 77–93). Springer Verlag. https://doi.org/10.1007/978-3-662-54580-5_5
Mendeley helps you to discover research relevant for your work.