Monitoring hyperproperties

Abstract

We investigate the runtime verification problem of hyperproperties, such as non-interference and observational determinism, given as formulas of the temporal logic HyperLTL. HyperLTL extends linear-time temporal logic (LTL) with trace quantifiers and trace variables. We show that deciding whether a HyperLTL formula is monitorable is PSPACE-complete. For monitorable specifications, we present an efficient monitoring approach. As hyperproperties relate multiple computation traces with each other, it is necessary to store previously seen traces, and to relate new traces to the traces seen so far. If done naively, this causes the monitor to become slower and slower, before it inevitably runs out of memory. In this paper, we present techniques that reduce the set of traces that new traces must be compared against to a minimal subset. Additionally, we exploit properties of specifications such as reflexivity, symmetry, and transitivity, to reduce the number of comparisons. We show that this leads to much more scalable monitoring with, in particular, significantly lower memory consumption.