Title
Rewriting-Based Runtime Verification for Alternation-Free HyperLTL.
Abstract
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.
Year
DOI
Venue
2017
10.1007/978-3-662-54580-5_5
TACAS
Field
DocType
Volume
Information flow (information theory),Programming language,Computer science,Theoretical computer science,Runtime verification,Rewriting,Temporal logic,Security policy,Observer (quantum physics),Boolean expression,Alternation (linguistics)
Conference
10206
ISSN
Citations 
PageRank 
0302-9743
8
0.44
References 
Authors
20
3
Name
Order
Citations
PageRank
Noel Brett180.44
Umair Siddique26312.26
Borzoo Bonakdarpour349045.02