Monitoring Hyperproperties
share
Hyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. HyperLTL extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express Hyperproperties. We investigate the runtime verification problem of HyperLTL formulas for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions may grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that deciding monitorability of HyperLTL formulas is PSPACE-complete for input models (1) and (3). Deciding monitorability is PSPACE-complete for alternation-free HyperLTL formulas in input model (2). For every input model, we provide practical monitoring algorithms. We also present various optimization techniques. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimized the number of traces that need to be stored. Finally, we provide an optimization that succinctly represents the stored traces by sharing common prefixes. We evaluate our optimizations, showing that this leads to much more scalable monitoring, in particular, significantly lower memory consumption.
READ FULL TEXT