Efficient monitoring of hyperproperties using prefix trees

\(\text {RVHyper}\)¹ is written in C++. We use spot [18] for building the deterministic monitor automata and the Buddy BDD library for handling symbolic constraints. We use the \(\text {HyperLTL}\) satisfiability solver \(\text {EAHyper}\) [19, 22] to determine whether the input formula is reflexive, symmetric, or transitive. Depending on those results, we omit redundant tuples in the monitoring algorithm.

For the online algorithm, we use standard techniques for building LTL monitoring automata and use this to instantiate this monitor by the traces as specified by the \(\text {HyperLTL}\) formula. Let \(\text {AP}\) be a set of atomic propositions and \({\mathcal {V}}= \{\pi _1, \ldots , \pi _n\}\) a set of trace variables. A deterministic monitor template \(\mathcal {M}= (\Sigma , Q, \delta , q_0, F)\) is a tuple of a finite alphabet \(\Sigma = 2^{(\text {AP}\times {\mathcal {V}})}\), a non-empty set of states Q, a partial transition function \(\delta : Q \times \Sigma \hookrightarrow Q\), a designated initial state \(q_0 \in Q\), and a set of accepting states \(F \subseteq Q\). The instantiated automaton runs in parallel over traces in \((2^\text {AP})^*\), and thus, we define a run with respect to a n-ary tuple \(N \in ((2^\text {AP})^*)^n\) of finite traces. A run of N is a sequence of states \(q_0 q_1 \cdots q_m \in Q^*\), where m is the length of the smallest trace in N, starting in the initial state \(q_0\) such that for all i with \(0 \le i < m\), it holds thatA tuple N is accepted if there is a run on \(\mathcal {M}\) that ends in an accepting state. For LTL, such a deterministic monitor can be constructed in doubly exponential time in the size of the formula [13, 39].

The algorithm for monitoring \(\text {HyperLTL}\) formulas when traces are given sequentially to the monitor is presented as Algorithm 1. After building the deterministic monitoring automaton \(\mathcal {M}_\varphi \), the algorithm accepts new traces and afterward 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.

In the example execution in Example 2, we have seen that the algorithm had to do more work than necessary to monitor observational determinism. For example, a tuple (t, t) for some trace t cannot violate observational determinism as the traces are equal. Further, from the pairs \((t,t')\) and \((t',t)\) for some traces t and \(t'\), we only need to check one of them as a violation in one of them implies the violation in the other pair. We can automatically check for such conditions and, thus, omit unnecessary work.

\(\text {RVHyper}\) implements the specification analysis with the HyperLTL satisfiability solver EAHyper [19, 22]. The specification analysis is a preprocessing step that analyzes the HyperLTL formula under consideration. EAHyper can detect whether a formula is (1) symmetric, i.e., we halve the number of instantiated monitors, (2) transitive, i.e., we reduce the number of instantiated monitors to two, or (3) reflexive, i.e., we can omit the self-comparison of traces.

Symmetry is particularly interesting since many information flow policies satisfy this property. Consider, for example, observational determinism: \( \forall \pi \mathpunct {.}\forall \pi '\mathpunct {.}(o_\pi = o_{\pi '}) {\mathcal {W}}(i_\pi \ne i_{\pi '})\). \(\text {RVHyper}\) detects symmetry by translating this formula to a formula that is unsatisfiable if there exists no set of traces for which every trace pair violates the symmetry condition: \( \exists \pi \mathpunct {.}\exists \pi '\mathpunct {.}\big ((o_\pi = o_{\pi '}) {\mathcal {W}}(i_\pi \ne i_{\pi '})\big ) \nleftrightarrow \big ((o_\pi = o_{\pi '}) {\mathcal {W}}(i_\pi \ne i_{\pi '})\big ) \). If the resulting formula turns out to be unsatisfiable, \(\text {RVHyper}\) omits the symmetric instantiations of the monitor automaton.

While symmetric HyperLTL formulas allow us to prune half of the monitor instances, transitivity of a HyperLTL formula has an even larger impact on the required memory. Equality, i.e., \(\forall \pi . \forall \pi ' \mathpunct {.}\square (a_\pi \leftrightarrow a_{\pi '})\), for example, is transitive and symmetric and allows us to reduce the number of monitor instances to one, since we can check equality against any reference trace.

Lastly, if a formula is reflexive, \(\text {RVHyper}\) omits the composition of a trace with itself during the monitoring process. For example, equality and observational determinism have reflexive HyperLTL formulas.

This is efficiently implemented in \(\text {RVHyper}\) (cf. Algorithm 2) and is guaranteed to catch all redundant traces. In our experiments [23, 24], we made the observation that traces often share the same prefixes, leading to a lot of redundant monitor automaton instantiations, repetitive computations, and duplicated information when those traces get stored.

The trace analysis, as it is based on a language inclusion check of the entire traces, cannot handle partial redundancy, for example, in the case that traces have redundant prefix requirements. This leaves room for optimization, which we address by implementing a trie data structure for managing the storage of incoming traces.

Tries, also known as prefix trees, are a tree data structure, which can represent a set of words over an alphabet in a compact manner. The root of a trie is identified with the empty word \(\epsilon \); additionally, each node can have several child nodes, each of which corresponds to a unique letter getting appended to the representing word of the parent node. So the set of words of a trie is identified with the set of words the leaf nodes represent.

Instead of \(((\tau ,a),\tau ') \in \longrightarrow \), we will write \(\tau \overset{a}{\longrightarrow } \tau '\) in the following. For a trie to be of valid form, we restrict \(\longrightarrow \) such that, \(\forall \tau ,\tau ' \in \mathcal {T}. |\{\tau \overset{a}{\longrightarrow } \tau '| a \in \Sigma \}| \le 1\).

In our case, the alphabet would be the set of propositions used in the specification, and the word built by the trie represents the traces. Instead of storing each trace individually, we store all of them in one trie structure, branching only in case of deviation. This means equal prefixes only have to be stored once. Besides the obvious benefits for memory, we also can make use of the maintained trie data structure to improve the runtime of our monitoring algorithms. As traces with same prefixes end up corresponding to the same path in the trie, we only have to instantiate the monitor automaton as much as the trie contains branches.

We depict a trie-based offline monitoring algorithm in Fig. 3. For the sake of readability, we assume that there are as many traces as universal quantifiers that we progress through all traces in parallel, and that all traces have the same length. This is merely a simplification in the presentation, and one can build the trie in a sequential fashion for online monitoring by a slight modification of the presented algorithm.

Without using tries, our monitoring algorithm was based on instantiating the deterministic monitor template \(\mathcal {M}_\varphi \) with tuples of traces. Now, we instantiate \(\mathcal {M}_\varphi \) with tuples of tries. Initially, we only have to create the single instance having the root of our trie.

The trie-based algorithm has much in common with its previously discussed trace-based counterpart. Initially, we have to build the deterministic monitor automaton \(\mathcal {M}_\varphi = (\Sigma _{\mathcal {V}}, Q, q_0, \delta , F)\). We instantiate the monitor with a fresh trie root \(\tau _0\). A mapping from trie instantiations to a state in \(\mathcal {M}_\varphi \) \(S: \mathcal {T}^n \rightarrow Q\) stores the current state of every active branch of the trie, stored in the set I. For each of the incoming traces, we provide an entry in a tuple of tries \({\tau }\), and each entry gets initialized to \(\tau _0\). During the run of our algorithm, these entries are updated such that they always correspond to the word built by the traces up to this point. For as long as there are traces left, which have not yet ended, and we have not yet detected a violation, we will proceed updating the entries in \(\mathbf {i}\) as follows. Having entry \(\tau \) and the correspond trace sequence proceeds with a, if \(\exists \tau ' \in \mathcal {T}. \tau \overset{a}{\longrightarrow } \tau '\), we update the entry to \(\tau '\); otherwise, we create such a child node of \(\tau \) (add_child in line 8). Creating a new node in the trie always occurs when the prefix of the incoming trace starts to differ from already seen prefixes. After having moved one step in our traces sequences, we have to reflect this step in our trie structure, in order for the trie-instantiated automata to correctly monitor the new propositions. As a trie node can branch to multiple child nodes, each monitor instantiation is replaced by the set of instantiations, where all possible child combinations of the different assigned tries are existent (update of I in line 11). Afterward, we update S in the same way as in Algorithm 2; thus, we omit algorithmic details here. If a violation is detected here, that is, there is no transition in the monitor corresponding to \(\mathbf {i}\), we will return the corresponding counterexample as a tuple of traces, as those can get reconstructed by stepping upwards in the tries of \(\mathbf {i}\). If the traces end, we check if every open branch \(\mathbf {i} \in I\) is in an accepting state.

We monitored whether an encoder preserves a Hamming distance of 2. We randomly built traces of length 50. In each position of the trace, the corresponding bit had a 1% chance to be flipped. The specification can be encoded as the following \(\text {HyperLTL}\) formula [26]:The right plot of Fig. 2 shows the results of our experiments. We compared the naive monitoring approach to different combinations of \(\text {RVHyper}\)’s optimizations. The specification analysis returns in under one second with the result that the formula is symmetric and reflexive. Hence, as expected, this preprocessing step has a major impact on the running time of the monitoring process as more than half of the, in general necessary, monitor instantiations can be omitted. A combination of the specification and trace analysis performs nearly equally well as naively storing the traces in our trie data structure. Combining the trie data structure with the specification analysis performs best and results in a tremendous speedup compared to the naive approach.

Non-interference [33] is an important information flow policy demanding that an observer of a system cannot infer any high security input of a system by observing only low security input and output. Formally, we specify that all low security outputs \(\mathbf {o}^{\mathrm{low}}\) have to be equal on all system executions as long as the low security inputs \(\mathbf {i}^{\mathrm{low}}\) of those executions are the same: \(\forall \pi , \pi ' \mathpunct {.}({\mathbf {o}^{\mathrm{low}}_\pi } \leftrightarrow {\mathbf {o}^{\mathrm{low}}_{\pi '}}) {\mathcal {W}} ({\mathbf {i}^{\mathrm{low}}_\pi } \nleftrightarrow {\mathbf {i}^{\mathrm{low}}_{\pi '}}).\) This class of benchmarks has previously been used to evaluate RVHyper [23]. We repeated the experiments, to show that using the trie data structure is a valid optimization. The results are depicted in Table 1. We chose a trace length of 50 and monitored non-interference on 2000 randomly generated traces, where we distinguish between an input range of 8 to 64 bits. The results show that the trie optimization has an enormous impact compared to a naive approach that solely relies on the specification analysis. As expected, the difference in runtime is especially high on experiments where traces collapse heavily in the trie data structure, i.e., producing almost no instances that must be considered during the monitoring process.

In this benchmark (introduced as a case study in [26]), we monitor whether a Verilog implementation of the Bakery protocol [31] from the VIS verification benchmark satisfies a symmetry property. Symmetry violations indicate that certain clients are privileged. The Bakery protocol is a classical protocol implementing mutual exclusion, working as follows: Every process that wishes to access a critical resource draws a ticket, which is consecutively numbered. The process with the smallest number may access the resource first. If two processes draw a ticket concurrently, i.e., obtaining the same number, the process with the smaller process ID may access the resource first. We monitored the following HyperLTL formula [26]:where \(\text {select}\) indicates the process ID that runs in the next step and \(\text {pause}\) indicates whether the step is stuttering. Each process i has a program counter \(\text {pc}(i)\) and when process i is selected, \(\text {pc}(i)\) is executed. \(\text {sym}(\text {select}_\pi ,\text {select}_{\pi '})\) states that process 0 is selected on trace \(\pi \) and process 1 is selected on trace \(\pi '\). Unsurprisingly, the implementation violates the specification, as it is provably impossible to implement a mutual exclusion protocol that is entirely symmetric [32]. Figure 3 shows the results of our experiment. In this benchmark, we can observe that the language inclusion check, on which the trace optimization is based on, produces an overhead during the monitoring. Since the traces differ a lot, the trace analysis cannot prune enough traces to be valuable. As there are only a few instances (in this case 4), the trie optimization outperforms the previous version of \(\text {RVHyper}\) massively on such a low instance count. The specification analysis, however, is always a valuable optimization.

While HyperLTL has been applied to a range of domains, including security and information flow properties, we focus in the following on a classical verification problem, the independence of signals in hardware designs. We demonstrate how \(\text {RVHyper}\) can automatically detect such dependencies from traces generated from hardware designs.

Input and output The input to \(\text {RVHyper}\) is a set of traces and a \(\text {HyperLTL}\) formula. For the following experiments, we generate a set of traces from the Verilog description of several example circuits by random simulation. If a set of traces violates the specification, \(\text {RVHyper}\) returns a counterexample.

Specification We consider the problem of detecting whether input signals influence output signals in hardware designs. We write \(\mathbf {i} \not \leadsto \mathbf {o}\) to denote that the inputs \(\mathbf {i}\) do not influence the outputs \(\mathbf {o}\). Formally, we specify this property as the following \(\text {HyperLTL}\) formula:where \(\overline{\mathbf {i}}\) denotes all inputs except \(\mathbf {i}\). 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.

Sample hardware designs We apply \(\text {RVHyper}\) to traces generated from the following hardware designs. Note that, since \(\text {RVHyper}\) observes traces and treats the system that generates the traces as a black box, the performance of \(\text {RVHyper}\) does not depend on the size of the circuit.

Results The results of multiple random simulations are given in Table 2. Even the previous version of \(\text {RVHyper}\) was able to scale up to thousands of input traces with millions of monitor instantiations. The novel implemented optimization of \(\text {RVHyper}\), i.e., storing the traces in a prefix tree data structure combined with our specification analysis, results in a remarkable speedup. Particularly interesting is the reduction in the number of instances in the counterexample. As there is only one input, the traces collapse in our trie data structure. For the two instances, where the property is satisfied (xor and mux), \(\text {RVHyper}\) has not found a violation for any of the runs. For instance, where the property is violated, \(\text {RVHyper}\) was able to find counterexamples.