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 Brett | 1 | 8 | 0.44 |
Umair Siddique | 2 | 63 | 12.26 |
Borzoo Bonakdarpour | 3 | 490 | 45.02 |