Monitoring hyperproperties

Abstract

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. $\text{HyperLTL}$ extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express hyperproperties. We investigate the runtime verification problem of $\text{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 is a-priori unbounded and may in fact grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that the existence of a bound in the parallel and bounded sequential models leads to a different notion of monitorability than in the unbounded sequential model. We show that deciding the monitoriability problem for alternation-free HyperLTL is $\mathrm{PS}PACE$ -complete while the problem is undecidable in general. For every input model, we provide monitoring algorithms along with run-time and storage optimizations. 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 minimizes the number of traces that need to be stored. We evaluate our optimizations, showing that this leads to a more scalable monitoring and, in particular, a significantly lower memory consumption.

Keywords: Hyperproperties; Information-flow; Monitoring; Runtime verification.

Fig. 1

Monitor approaches for the parallel model: online in a forward fashion (left) and offline in a backwards fashion (right)

Fig. 2

Monitor approaches for the sequential models: an unbounded number of traces (left) and bounded number of traces (right) are processed sequentially

Fig. 3

Visualization of a monitor template corresponding to the formula given in Eq. 1. We use a symbolic representation of the transition function $\delta$

Fig. 4

Online algorithm for the parallel model, where ${◊}_i:=\wedge$ if the i-th quantifier in $\phi$ is a universal quantifier and $\vee$ otherwise

Fig. 5

Offline backwards algorithm for the parallel model, where ${◊}_i:=\wedge$ if the i-th quantifier in $\phi$ is a universal quantifier and $\vee$ otherwise

Fig. 6

Evaluation algorithm for monitoring ${\forall }^n$ HyperLTL formulas in the unbounded sequential model

Fig. 7

Storage Minimization Algorithm

Fig. 8

Absolute numbers of violations in red (dotted), number of instances stored in blue (dashed), number of instances pruned in green (solid) for ${10}^5$ randomly generated traces of length 100, 000. The y axis is scaled logarithmically

Fig. 9

Hamming-distance preserving encoder: runtime comparison of naive monitoring approach with different optimizations and a combination thereof

Fig. 10

mux circuit with black box

Fig. 11

Monitoring of black box circuits: runtime comparison of naive monitoring approach with different optimizations and a combination thereof