Monitoring hyperproperties

Hyperproperties [13] generalize trace properties in that they not only check the correctness of individual traces, but can also relate multiple computation traces to each other. This is needed, for example, to express information flow security policies like the requirement that the system behavior appears to be deterministic, i.e., independent of certain secrets, to an external observer. Monitoring hyperproperties is difficult, because it is no longer possible to analyze traces in isolation: a violation of a hyperproperty in general involves a set of traces, not just a single execution. We present monitoring algorithms for hyperproperties given in the temporal logic HyperLTL [12], which extends linear-time temporal logic (LTL) with trace variables and trace quantifiers in order to refer to multiple traces at a time. For example, the HyperLTL formula \(\forall \pi . \exists \pi '.~ \Box dummyInput_{\pi '} \wedge ~ lowOut_\pi = lowOut_{\pi '}\) expresses noninference [28] by stating that for all traces \(\pi \), there exists a trace \(\pi '\), such that the observable outputs are the same on both traces even when the high security input of \(\pi '\) being replaced by a dummy input. For example, in a messaging app, we might replace the address book, which we want to keep secret, with an empty address book.

A first, and absolutely fundamental, question to be answered is in what form the input, which now consists of more than one execution trace, should be presented to the monitor. Should the traces be presented all at once or one at a time? Is the number of traces known in advance? Obviously, the choice of the input representation has significant impact both on the principal monitoriability of a hyperproperty and on the actual monitoring algorithm. We study three basic input models for monitoring hyperproperties. (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.

Parallel model. The assumption that the number of incoming traces is fixed before the actual monitoring process starts is a straight-forward extension of the classic runtime verification problem for LTL, where only a single trace is observed. We distinguish online monitoring, where the traces become available one position at a time from left to right, from offline monitoring where the positions of the traces can be accessed in any order. Figure 1 illustrates the two types of algorithms. The parallel model is known from techniques like secure-multi-execution [15], where several system executions are generated by providing different high-security inputs. We present an online and an offline monitoring algorithm for hyperproperties expressed in \(\text {HyperLTL}\). The online algorithm is based on standard techniques for building monitoring automata from LTL formulas. Such a monitor automaton is then instantiated for multiple traces as specified by the HyperLTL formula. The offline algorithm is based on constructing an alternating automaton and then proceeding through the automaton in a bottom-up fashion, similar to the classic construction for LTL [23].

Sequential model. The sequential models are useful when multiple sessions of a system under observation have to be monitored one after the other in an online fashion. The disadvantage of the unbounded sequential model is that many interesting hyperproperties, in particular most hyperproperties with quantifier alternations, are not monitorable in this model. It is therefore often useful to define a stop condition in the form of a bound on the number of traces that need to be handled during the monitoring process. Figure 2 sketches the monitoring algorithm for the unbounded and bounded cases.

A naive monitoring approach for the sequential models would be to simply store all traces seen so far. However, this would create two problems: a memory problem, because the needed memory grows with the number of traces observed by the monitor, and a runtime problem, because one needs to relate every newly observed trace against the growing set of stored traces.

There are hyperproperties where this effect cannot be avoided. An example is the hyperproperty with two atomic propositions p and q, where any pair of traces that agree on their p labeling must also agree on their q labeling. Clearly, for every p labeling seen so far, we must also store the corresponding q labeling. In practice, however, it is often possible to greatly simplify the monitoring. Consider, for example, the hyperproperty that states that all traces have the same q labeling (independently of the p labeling). In HyperLTL, this property is specified as the formula \( \forall \pi .\forall \pi '.\Box (q_\pi {\leftrightarrow } q_{\pi '})\). The naive approach would store all traces seen so far, and thus requires, in the worst case, \(O(t \cdot n)\) memory after n traces of length t. A new trace would be compared against every stored trace twice, once as \(\pi \) and once as \(\pi '\), resulting in an \(O(t \cdot n)\) running time for each new trace. Obviously, however, in this example it is sufficient to store the first trace, and compare all further incoming traces against this reference. The required memory is thus, in fact, constant in the number of traces. A further observation is that the specification is symmetric in \(\pi \) and \(\pi '\). Hence, a single comparison suffices.

In this article, we present a monitoring approach for hyperproperties in the unbounded model that reduces the set of traces that new traces must be compared against to a minimal subset. Our approach comes with a strong correctness guarantee: our monitor produces the same verdict as a naive monitor that would store all traces and, additionally, we keep a sufficient set of traces to always provide an actually observed witness for the monitoring verdict. Our monitoring algorithm thus delivers a result that is equally informative as the naive solution. We introduce two analysis techniques: The trace analysis reduces the stored set of traces to a minimum, thus minimizing the required memory. The specification analysis, which is applicable in the parallel model as well, identifies symmetry, transitivity, and reflexivity in the specification, in order to reduce the algorithmic workload that needs to be carried out on the stored traces.

Trace analysis As an example for a system where information flow control is of outstanding importance for the intended operation, we consider a conference management system. There are a number of confidentiality properties that such a system should satisfy, like “The final decision of the program committee remains secret until the notification”. We want to focus on important hyperproperties of interest beyond confidentiality, like the property that no paper submission is lost or delayed. Informally, one formulation of this property is “A paper submission is immediately visible for every program committee member”. More formally, this property relates pairs of traces, one belonging to an author and one belonging to a program committee member. We assume this separation is indicated by a proposition pc that is either disabled or enabled in the first component of those traces. Further propositions in our example are the proposition s, denoting that a paper has been submitted, and v denoting that the paper is visible.

Given a set of finite traces T, i.e., finite sequences over sets of atomic propositions, we can verify that the property holds by checking for every pair of traces \((t,t') \in T \times T\) with \(pc \notin t[0]\) and \(pc \in t'[0]\) that \(s \in t[i]\) implies \(v \in t'[i+1]\) for every \(i \ge 0\). When T satisfies the property, \(T \cup \{t^*\}\), where \(t^*\) is a new trace, amounts to checking new pairs \((t^*,t)\) and \((t,t^*)\) for \(t \in T\). This, however, leads to an increasing size of T and thereby to an increased number of checks: the monitoring problem inevitably becomes costlier over time. To circumvent this, we present a method that keeps the set of traces minimal with respect to the underlying property. When monitoring hyperproperties, traces may pose requirements on future traces. The core idea of our approach is to characterize traces that pose strictly stronger requirements on future traces than others. In this case, the traces with the weaker requirements can be safely discarded. As an example, consider the following set of traces

A satisfying PC trace would be \(\{pc\}\{v\}\{v\}\{v\}\emptyset \) as there are author traces with paper submissions at time step 0, 1, and 2. For checking our property, one can safely discard trace A.2 as it poses no more requirements than trace A.3. We say that trace A.3 dominates trace A.2. We show that, given a property in the temporal logic \(\text {HyperLTL}\), we can automatically reduce trace sets to be minimal with respect to this dominance. On relevant and more complex information flow properties, this reduces the memory consumption dramatically.

Specification analysis Our specification analysis technique allows us to reduce the number of monitor instantiations in order to detect violation or satisfaction of a given \(\text {HyperLTL}\) formula. We use the decision procedure for the satisfiability problem of \(\text {HyperLTL}\) [18] to check whether or not a universally quantified \(\text {HyperLTL}\) formula is symmetric, transitive, or reflexive. If a hyperproperty is symmetric, then we can omit every symmetric monitor, thus, performing only half of the language membership tests. A canonical example for a symmetric \(\text {HyperLTL}\) formula is \(\forall \pi . \forall \pi '.\; (O_\pi = O_{\pi '}) {\mathcal {W}}(I_\pi \ne I_{\pi '}),\) a variant of observational determinism [27, 31, 38]. Symmetry is especially interesting, since many information flow policies have this property. If a hyperproperty is transitive, then we can omit every, except for one, monitor, since we can check every incoming trace against any reference trace. One example for a transitive \(\text {HyperLTL}\) formula is equality \(\forall \pi . \forall \pi ' .\Box (a_\pi \leftrightarrow a_{\pi '}).\) If a hyperproperty is reflexive, then we can omit the monitor where every trace variable i same trace. For example, both hyperproperties above are reflexive.

Structure of this article The remainder of this article is structured as follows. Section 2 introduces the syntax and semantics of \(\text {HyperLTL}\) and the notion of monitorable \(\text {HyperLTL}\) formula in all three input models. We furthermore present algorithms for checking whether a \(\text {HyperLTL}\) formula is monitorable or not. In Sect. 3, we give a finite trace semantics for \(\text {HyperLTL}\). For the parallel input model, we present an offline and an online monitoring algorithm for arbitrary \(\text {HyperLTL}\) formulas. In Sect. 4, we present online algorithms for (universal) \(\text {HyperLTL}\) formulas in the (unbounded) sequential model. We then tackle the aforementioned memory explosion by formally introducing the trace analysis and hyperproperty analysis sketched above. We report on our implementation RVHyper and experimental results in Sect. 5, before concluding in Sect. 6.

This is a revised and extended version of a paper that appeared at RV 2017 [20]. Our contributions and extensions compared to [20] are (1) the study of the above mentioned different runtime verification models for hyperproperties, (2) an online and offline, using backwards trace traversal, algorithm for the parallel model, and (3) an extended evaluation of an improved version of RVHyper.

Related work The temporal logic \(\text {HyperLTL}\) was introduced to model check security properties of reactive systems [12, 22]. For one of its predecessors, \(\text {SecLTL}\) [16], there has been a proposal for a white box monitoring approach [17] based on alternating automata. The problem of monitoring \(\text {HyperLTL}\) has been considered before [1, 9]. Agrawal and Bonakdarpour [1] were the first to study the monitoring problem of HyperLTL for the sequential model. They focused on k-safety hyperproperties [13], where a hyperproperty \(\varphi \) is k-safety, if for each set of traces violating \(\varphi \) a bad set of prefixes of those traces can be given with at most k elements. In their paper Agrawal and Bonakdarpour show that HyperLTL formulas with at most k universal quantifiers can express a rich subset of k-safety hyperproperties. Following this observation they defined the notion of monitorability for HyperLTL based on the definitions for LTL monitorability by Pnueli and Zaks [30]. The concept of a monitorability formalizes the intuitive idea of being able to detect acceptance or violation of a property by only observing a system at runtime. So the monitorable HyperLTL formulas are those for which it is either possible to find a witness, a set of finite prefixes, of acceptance or violation, respectively. They gave a syntactic characterization of monitorable \(\text {HyperLTL}\) formulas, which we extend in this work. The monitoring algorithm they propose is based on a progression logic expressing trace inter-dependencies and the composition of \(\hbox {LTL}_3\) monitor automata in a Petri net whose special sink states represent verdicts for sub-formulas. Incoming traces get evaluated for each \(\hbox {LTL}_3\) monitor in the Petri net and the progression logic keeps track of seen events for monitoring future traces. In subsequent work, a constraint based approach has been proposed [9]. By analyzing HyperLTL formulas syntactically, they identify propositions of interest and store corresponding constraints. Like with our monitoring algorithm, they do not have access to the implementation (black box), but in contrast to our work, they do not provide witnessing traces as a monitor verdict.

In [7], the authors study the complexity of monitoring hyperproperties. They show that the form and size of the input, as well as the formula have a significant impact on the feasibility of the monitoring process. They differentiate between several input forms and study their complexity: a set of linear traces, tree-shaped Kripke structures, and acyclic Kripke structures. For acyclic structures and alternation-free HyperLTL formulas, the problems complexity gets as low as NC. In [8], the authors discuss examples where static analysis can be combined with runtime verification techniques to monitor HyperLTL formulas beyond the alternation-free fragment. They discuss the challenges in monitoring formulas beyond this fragment and lay the foundations towards a general method.

The need to store traces during runtime is not unique to hyperproperties. There has been, for example, work on verifying parametric trace properties [10] which takes each event in the parametric trace and distributes it to its corresponding trace slices. This slicing is, unlike our trace analysis, independent of the specification. This technique motivated the work on Quantified Event Automata [4] that can evaluate quantifiers over parameters. They cannot, however, express general hyperproperties as they cannot relate different parametric traces.

For certain information flow policies, like non-interference and some extensions, dynamic enforcement mechanisms have been proposed. Techniques for the enforcement of information flow policies include tracking dependencies at the hardware level [34], language-based monitors [2, 3, 6, 32, 36], and abstraction-based dependency tracking [11, 24, 25]. Secure multi-execution [15] is a technique that can enforce non-interference by executing a program multiple times in different security levels. To enforce non-interference, the inputs are replaced by default values whenever a program tries to read from a higher security level.

As hyperproperties relate multiple executions to each other, a monitor for hyperproperties has to consider sets of traces instead of solely processing a single execution in isolation. In this section, we elaborate on the runtime verification problem of \(\text {HyperLTL}\). In the first subsection, we present \(\text {HyperLTL}\), which is a temporal logic for expressing hyperproperties. In the second subsection, we define the notion of monitorable \(\text {HyperLTL}\) specifications for three different input models: the unbounded input model, the bounded model, and the parallel model.

We start by giving necessary notation. Given a finite or infinite set A, we denote the powerset of a A by \({\mathcal {P}}(A)\) and define \({\mathcal {P}}^*(A)\) to be the set of all finite subsets of A. Note that \({\mathcal {P}}(A) = {\mathcal {P}}^*(A)\) if A is finite. For some \(b > 0\) and infinite set A, we use the notation \({\mathcal {P}}^b(A)\) and \({\mathcal {P}}^{\le b}(A)\) to denote all subsets of A of cardinality b and \(\le b\), respectively. Let \(\text {AP}\) be a finite set of atomic propositions and let \(\varSigma = {\mathcal {P}}(\text {AP})\) be the corresponding finite alphabet. A finite (infinite) trace is a finite (infinite) sequence over \(\varSigma \). We denote the concatenation of a finite trace \(u \in \varSigma ^*\) and a finite or infinite trace \(v \in \varSigma ^* \cup \varSigma ^\omega \) by uv and write \(u \preceq v\) if u is a prefix of v. Further, we lift the prefix operator to sets of traces, i.e., \(U \preceq V\) if, and only if, \(\forall u \in U .\exists v \in V .u \preceq v\) where \(U \subseteq \varSigma ^*\) and \(V \subseteq \varSigma ^* \cup \varSigma ^\omega \). Let t be a (infinite) trace and let \(i,j \in {\mathbb {N}}\) be natural numbers with \(j \ge i\). t[i] denotes the i-th element of t. Therefore, t[0] is the starting element of the trace. t[i, j] is the sequence \(t[i] t[i+1] \ldots t[j-1] t[j]\). Lastly, \(t[i,\infty ]\) denotes the infinite suffix of t starting at position i.

Whereas the previous section was concerned with the question whether a HyperLTL formula is monitorable, we now focus our attention towards monitoring algorithms. As a prerequisite, we recap the semantics of HyperLTL for finite traces [9], which is itself based on the finite trace semantics of LTL [26]. Afterwards, we discuss the monitoring algorithms for the parallel model, where the set of traces is fixed and the traces are processed in parallel, either online in a forward fashion, or offline in a backwards fashion. Figure 1 gives a visual representation how the algorithms process the traces.

After discussing monitoring algorithms for the parallel model in the previous section, we now focus our attention to the case where traces are given sequentially to the monitor. This setting is of interest as it can, for example, detect information flow violations after multiple executions of a program. We also focus on universal HyperLTL formulas, as formulas with alternations are in general not monitorable in this setting (see Sect. 2.2).

The algorithm for monitoring \(\text {HyperLTL}\) formulas in the unbounded sequential model is presented in Fig. 6. After building the deterministic monitoring automaton \({\mathcal {M}}_\varphi \), the algorithm accepts new traces and afterwards proceeds with the pace of the incoming stream. We have a variable S that maps tuples of traces to states of the deterministic monitor. Whenever the current trace t progresses, we progress every tuple \((t_1,\ldots ,t_n)\) that contains t with one of the following outcomes:When a new trace t starts, only new tuples are considered for S, that are tuples \(\mathbf {t} \in (T \cup \{t\})^n\) containing the new trace t.

Given a HyperLTL formula with n different quantifiers, the algorithm requires \({\mathcal {O}}({|T|}^n)\) space during runtime. This results in a space consumption of \({\mathcal {O}}( 2^{2^{|\varphi |}} + {|T|}^n )\). For m traces of length t, the algorithm requires \({\mathcal {O}}(m^n)\) time for each iteration, resulting in an overall time complexity of \({\mathcal {O}}( 2^{2^{|\varphi |}} + t \cdot m^n )\).

The correctness arguments for the parallel model translate to the sequential model: since we solely consider \(\forall ^n\) HyperLTL formulas, it is sufficient, by the finite trace semantics of HyperLTL, to check every combination of trace tuples \((t_1, \ldots , t_n)\) and immediately report a violation if the automaton cannot progress or stops in a non-accepting state.

Bounded model In the bounded model, we have an upper bound m on the number of traces. Thus, we can update the algorithm presented in Fig. 6 to evaluate an arbitrary quantifier prefix similar to the algorithms in Figs. 4 and 5. However, in general, we lose the ability to detect violations and satisfactions during monitoring as we have to reach the bound m to be able to compute a verdict.

A benefit to the monitoring algorithm presented in this section is that it is able to return a witness for violation. As a negative consequence, we have to remember each and every trace seen so far. This is, in general, unavoidable, as shown by the following hyperproperty: “every new trace has to be different than the one before”. However, it turns out that in many cases hyperproperties satisfy certain properties that allows us to prune a majority of traces during the monitoring process. We discuss these cases in the following.

We report on experimental results of our implementation RVHyper [21], where traces are given sequentially to the monitor, to detect violations after multiple executions of a program. RVHyper is written in C++. It uses spot for building the deterministic monitor automata and the Buddy BDD library for handling symbolic constraints. We use the \(\text {HyperLTL}\) satisfiability solver EAHyper [18, 19] to determine whether the input formula is reflexive, symmetric, or transitive.

In our experiments, we show that (1) the specification analysis is a cheap preprocessing step that reduces the amount of comparisons corresponding to the factor determined in the analysis, (2) the trace analysis has a small overhead during runtime and is effective when applicable, and (3) both optimizations can be used in combination and their impact is orthogonal.

Specification analysis We checked variations of observational determinism, quantitative non-interference [22], equality, a Hamming-distance of 2, and our conference management example for symmetry, transitivity, and reflexivity. The results are depicted in Table 1. The specification analysis comes with low costs (every check was done in under a second), but with a high reward in terms of constructed monitor instances. Figure 9 shows the runtime during the monitoring of a Hamming-distance preserving encoder: analyzing the specification beforehand halves the algorithmic workload by omitting symmetric monitor instantiations.

Trace analysis For evaluating our trace analysis, we use a scalable, bounded variation of observational determinism: \(\forall \pi .\forall \pi '.\Box _{<n} (I_\pi = I_{\pi '}) \rightarrow \Box _{< n +c} (O_\pi = O_{\pi '})\), where \(\Box _{<n} \varphi \) is syntactic sugar that \(\varphi \) has to hold until the \((n-1)\)-th position of the incoming traces. Figure 8 shows a family of plots for this benchmark class, where c is fixed to three. We randomly generated a set of \(10^5\) traces. The blue (dashed) line depicts the number of traces that need to be stored, the red (dotted) line the number of traces that violated the property, and the green (solid) line depicts the pruned traces. When increasing the requirements on the system, i.e., decreasing n, we prune the majority of incoming traces with our trace analysis techniques.

Optimizations in combination We furthermore considered our optimizations in combination. As a first benchmark we monitored whether an encoder preserves a Hamming-distance of 2, which can be encoded as a universally quantified HyperLTL formula [12]: . In Fig. 9 we compare the naive monitoring approach to the monitor using specification analysis and trace analysis, as well as a combination thereof. We randomly built traces of length 50. In each position of the trace, the corresponding bit had a 1% chance to be flipped. Applying our techniques results in a tremendous speed up of the monitoring algorithm.

For our second benchmark, we evaluate what effect the similarity of the incoming traces have on our optimizations. For this setup, we considered a black box combinatorial circuit, guarded by a multiplexer that selects between the two input vectors \(\mathbf {i}\) and \(\mathbf {i}'\) and an inverse multiplexer that forwards the output of the black box either towards \(\mathbf {o}\) or \(\mathbf {o}'\). The circuit is depicted in Fig. 10. We monitored whether there is a semantic dependency between the in- and outputs, i.e., \(\forall \pi _1 \forall \pi _2 .(\mathbf {o}_{\pi _1} = \mathbf {o}_{\pi _2}) {\mathcal {W}}(\overline{\mathbf {i}}_{\pi _1} \ne \overline{\mathbf {i}}_{\pi _2})\), where \({\mathcal {W}}\) is the weak version of the until operator, i.e., \(\varphi {\mathcal {W}}\psi :=\Box \varphi \vee \varphi {\mathcal {U}}\psi \). Intuitively, the formula asserts that for every two pairs of execution traces \((\pi _1,\pi _2)\) the value of \(\mathbf {o}\) has to be the same until there is a difference between \(\pi _1\) and \(\pi _2\) in the input vector \(\overline{\mathbf {i}}\), i.e., the inputs on which \(\mathbf {o}\) may depend. For our experimental evaluation we generated each time 1000 traces of length 30 and varying trace similarity. Specifically the traces of a single configuration were derived by flipping the input bits of a reference input trace with a certain probability after which we simulated the mux circuit on the altered input.

Figure 11 shows the total runtime of our monitoring approach with the different optimizations and a combination thereof. Note that both axes are log-scaled. Also note that the x-axis is chosen such that from left to right the trace similarity decreases, that is, there are only few unique traces in the left most configuration up to almost only different traces in the right most one. From the plot we can derive several interesting characteristics of our optimizations that we discuss in the following. As observed in our previous experiments, the specification analysis, if applicable as in this case, is a valuable optimization consistently reducing the runtime and does so also when combined with the trace analysis. As expected the runtime is halved by exploiting symmetry and reflexivity in the formula. From the plot we can also infer that the trace analysis is effective in a context with a majority of redundant traces. For such a highly redundant setup the trace analysis reduces the overall runtime of the monitoring algorithm by several magnitudes. With a decrease of similarity and redundancy in the traces the positive effect of the trace analysis steadily decreases up until the overhead of the trace analysis itself gets noticeable. The decrease in runtime for configurations without trace analysis, which comes with reduced traces similarity, is explained by the fact that the more the input of the monitored traces is different the earlier trace tuples can get pruned as they satisfy the specification and thereby reduce the computational burden of the algorithm. This is also the reason why the configurations with trace analysis show decreasing runtime behavior again as soon as the aforementioned effects dominate the runtime characteristics of the monitoring approach.

In this article, we considered the problem of monitoring hyperproperties in the temporal logic \(\text {HyperLTL}\). We studied the question whether a \(\text {HyperLTL}\) formula is monitorable in three different input models, where the traces are either given in parallel or sequentially, and, when given sequentially, may either grow beyond any bound or be limited by a fixed bound. For each input model, we have presented automata-based monitoring algorithms for \(\text {HyperLTL}\).

We presented two optimizations tackling different problems in monitoring hyperproperties: The trace analysis minimizes the needed memory, by minimizing the stored set of traces and the specification analysis reduces the algorithmic workload by reducing the number of comparisons between a newly observed trace and the previously stored traces.

We have evaluated our tool implementation RVHyper on several benchmarks. We showed that the optimizations contribute significantly towards the practical monitoring of hyperproperties. Furthermore, we provided a use case on detecting spurious dependencies in hardware designs using RVHyper and compared it against a previous prototype implementation.