MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the $\exists^*\forall^*$ Fragment

TL;DR

MGHyper is a new tool that extends satisfiability checking for HyperLTL hyperproperties beyond the decidable fragment, enabling automatic verification, equivalence checking, and counterexample generation for complex hyperproperties.

Contribution

It introduces a semi-decision procedure for the full HyperLTL logic, surpassing previous limitations to the $orall^* herefore^*$ fragment, and provides practical verification capabilities.

Findings

Successfully checked complex hyperproperties beyond the $orall^* herefore^*$ fragment.

Demonstrated effectiveness on literature and randomly generated HyperLTL formulas.

Enabled automatic counterexample generation and property equivalence verification.

Abstract

Hyperproperties are properties that refer to multiple computation traces. This includes many information-flow security policies, such as observational determinism, (generalized) noninterference, and noninference, and other system properties like symmetry or Hamming distances between in error-resistant codes. We introduce MGHyper, a tool for automatic satisfiability checking and model generation for hyperproperties expressed in HyperLTL. Unlike previous satisfiability checkers, MGHyper is not limited to the decidable $\exists^* \forall^*$ fragment of HyperLTL, but provides a semi-decisionprocedure for the full logic. An important application of MGHyper is to automatically check equivalences between different hyperproperties (and different formalizations of the same hyperproperty) and to build counterexamples that disprove a certain claimed implication. We describe the semi-decisionprocedure implemented in MGHyper and report on experimental results obtained both with typical hyperproperties from the literature and with randomly generated HyperLTL formulas.

Tables

Table 1. Table 1: Random ∃ n ∀ m superscript 𝑛 superscript for-all 𝑚 \exists^{n}\forall^{m} formulas: instances solved (sol) in 120 120 120 s 𝑠 s and average time (avgt) in s 𝑠 s for 100 100 100 random formulas of size 60 60 60 with 15 15 15 atomic propositions.

avgt	sol	avgt	sol	avgt	sol	avgt	sol	avgt	sol	avgt	sol	avgt	sol	avgt	sol	avgt	sol	avgt	sol
${\exists }^1{\forall }^1$		${\exists }^1{\forall }^2$		${\exists }^1{\forall }^3$		${\exists }^1{\forall }^4$		${\exists }^1{\forall }^5$		${\exists }^1{\forall }^6$		${\exists }^1{\forall }^7$		${\exists }^1{\forall }^8$		${\exists }^1{\forall }^9$		${\exists }^1{\forall }^{10}$
0.472	96	0.599	95	1.371	96	1.537	96	1.322	96	1.587	96	0.529	92	2.823	96	3.166	94	2.303	97
${\exists }^2{\forall }^1$		${\exists }^2{\forall }^2$		${\exists }^2{\forall }^3$		${\exists }^2{\forall }^4$		${\exists }^2{\forall }^5$		${\exists }^2{\forall }^6$		${\exists }^2{\forall }^7$		${\exists }^2{\forall }^8$		${\exists }^2{\forall }^9$		${\exists }^2{\forall }^{10}$
6.772	80	2.743	85	2.698	93	6.319	94	4.233	97	4.107	92	3.162	87	2.906	94	4.847	92	2.131	96
${\exists }^3{\forall }^1$		${\exists }^3{\forall }^2$		${\exists }^3{\forall }^3$		${\exists }^3{\forall }^4$		${\exists }^3{\forall }^5$		${\exists }^3{\forall }^6$		${\exists }^3{\forall }^7$		${\exists }^3{\forall }^8$		${\exists }^3{\forall }^9$		${\exists }^3{\forall }^{10}$
5.533	79	9.921	81	5.836	82	4.851	88	7.589	82	3.852	82	9.975	82	5.222	79	6.328	77	5.044	83
${\exists }^4{\forall }^1$		${\exists }^4{\forall }^2$		${\exists }^4{\forall }^3$		${\exists }^4{\forall }^4$		${\exists }^4{\forall }^5$		${\exists }^4{\forall }^6$		${\exists }^4{\forall }^7$		${\exists }^4{\forall }^8$		${\exists }^4{\forall }^9$		${\exists }^4{\forall }^{10}$
10.316	75	8.669	80	5.631	83	3.722	83	5.843	73	5.62	81	10.074	79	6.955	76	8.037	85	5.938	79
${\exists }^5{\forall }^1$		${\exists }^5{\forall }^2$		${\exists }^5{\forall }^3$		${\exists }^5{\forall }^4$		${\exists }^5{\forall }^5$		${\exists }^5{\forall }^6$		${\exists }^5{\forall }^7$		${\exists }^5{\forall }^8$		${\exists }^5{\forall }^9$		${\exists }^5{\forall }^{10}$
5.431	71	5.009	80	2.812	69	8.514	81	4.501	76	6.255	83	1.574	76	3.616	76	5.85	79	7.486	80
${\exists }^6{\forall }^1$		${\exists }^6{\forall }^2$		${\exists }^6{\forall }^3$		${\exists }^6{\forall }^4$		${\exists }^6{\forall }^5$		${\exists }^6{\forall }^6$		${\exists }^6{\forall }^7$		${\exists }^6{\forall }^8$		${\exists }^6{\forall }^9$		${\exists }^6{\forall }^{10}$
3.53	78	4.378	74	3.503	71	3.057	76	4.354	71	4.513	81	3.492	79	4.836	79	6.289	80	6.0	74
${\exists }^7{\forall }^1$		${\exists }^7{\forall }^2$		${\exists }^7{\forall }^3$		${\exists }^7{\forall }^4$		${\exists }^7{\forall }^5$		${\exists }^7{\forall }^6$		${\exists }^7{\forall }^7$		${\exists }^7{\forall }^8$		${\exists }^7{\forall }^9$		${\exists }^7{\forall }^{10}$
4.33	74	3.173	70	1.789	72	7.187	69	4.99	78	5.584	74	4.783	77	7.558	75	7.744	74	6.043	78
${\exists }^8{\forall }^1$		${\exists }^8{\forall }^2$		${\exists }^8{\forall }^3$		${\exists }^8{\forall }^4$		${\exists }^8{\forall }^5$		${\exists }^8{\forall }^6$		${\exists }^8{\forall }^7$		${\exists }^8{\forall }^8$		${\exists }^8{\forall }^9$		${\exists }^8{\forall }^{10}$
5.681	81	4.617	79	6.803	74	5.563	75	6.219	80	5.999	74	3.013	73	2.041	72	6.146	75	3.997	75
${\exists }^9{\forall }^1$		${\exists }^9{\forall }^2$		${\exists }^9{\forall }^3$		${\exists }^9{\forall }^4$		${\exists }^9{\forall }^5$		${\exists }^9{\forall }^6$		${\exists }^9{\forall }^7$		${\exists }^9{\forall }^8$		${\exists }^9{\forall }^9$		${\exists }^9{\forall }^{10}$
3.509	77	2.514	72	5.659	68	1.345	78	4.379	72	3.914	73	3.422	71	1.784	66	6.903	72	5.142	77
${\exists }^{10}{\forall }^1$		${\exists }^{10}{\forall }^2$		${\exists }^{10}{\forall }^3$		${\exists }^{10}{\forall }^4$		${\exists }^{10}{\forall }^5$		${\exists }^{10}{\forall }^6$		${\exists }^{10}{\forall }^7$		${\exists }^{10}{\forall }^8$		${\exists }^{10}{\forall }^9$		${\exists }^{10}{\forall }^{10}$
3.986	81	4.553	70	5.777	70	4.791	75	8.284	75	1.534	72	4.338	71	4.18	76	5.512	65	4.529	75

Equations

$$\psi$$

$$\phi$$

$$\Pi {\models }_T\exists \pi .\psi$$

$$\Pi {\models }_T\forall \pi .\psi$$

$$\Pi {\models }_T{a}_{\pi }$$

$$\Pi {\models }_T\neg \psi$$

$$\Pi {\models }_T{\psi }_1\vee {\psi }_2$$

$$\displaystyle\Pi\models_{T}~{}\mbox{$\sf X$}\psi$$

$$\displaystyle\Pi\models_{T}~{}\psi_{1}\mbox{$\,{\sf U}\,$}\psi_{2}$$

$$\text{and for all}0\le j<i\text{we have}\Pi [j,\infty ]{\models }_T{\psi }_1$$

$$Prefix(\phi )=\exists {Traces}_T^k.Q_0{Traces}_{\overrightarrow{{\pi }_0}}^k.Q_1{Traces}_{\overrightarrow{{\pi }_1}}^k.\dots .Q_n{Traces}_{\overrightarrow{{\pi }_n}}^k.$$

$$P_{Q_{i}}:=\Bigg{[}\bigwedge_{\pi\in\vec{\pi_{i}}}\bigvee_{t_{i}\in T}\Bigg{[}\bigwedge_{\begin{subarray}{c}(a^{j}_{t_{i}},a^{j}_{\pi})\in\\ \mathit{Traces}^{k}_{t_{i}}\times\mathit{Traces}^{k}_{\pi}\end{subarray}}a^{j}_{t_{i}}\leftrightarrow a^{j}_{\pi}\Bigg{]}\Bigg{]}$$

$$Linking(\phi ):=P_{Q_0}^k{\circ }_{Q_0}{P}_{Q_1}^k{\circ }_{Q_1}\dots P_{Q_{n-1}}^k{\circ }_{Q_{n-1}}{P}_{Q_n}^k{\circ }_{Q_n},$$

$$\displaystyle\exists\mathit{Traces}^{0}_{T_{2}}\forall\mathit{Traces}^{0}_{\pi_{0}}\exists\mathit{Traces}^{0}_{\pi_{1}}\exists\mathit{Traces}^{0}_{\pi_{2}}.\left[\lor\begin{tabular}[]{c}$(a_{\pi_{0}}^{0}\leftrightarrow a_{t_{0}}^{0}\land b_{\pi_{0}}^{0}\leftrightarrow b_{t_{0}}^{0})$\\ $(a_{\pi_{0}}^{0}\leftrightarrow a_{t_{1}}^{0}\land b_{\pi_{0}}^{0}\leftrightarrow b_{t_{1}}^{0})$\\ \end{tabular}\right]$$

$$\displaystyle\rightarrow\left(\left[\land\begin{tabular}[]{r c r}$\Big{(}\lor$&\begin{tabular}[]{c}$[a_{\pi_{1}}^{0}\leftrightarrow a_{t_{0}}^{0}\land b_{\pi_{1}}^{0}\leftrightarrow b_{t_{0}}^{0}]$\\ $[a_{\pi_{1}}^{0}\leftrightarrow a_{t_{1}}^{0}\land b_{\pi_{1}}^{0}\leftrightarrow b_{t_{1}}^{0}]$\\ \end{tabular} \Big{)}\\ $\Big{(}\lor$&\begin{tabular}[]{c}$[a_{\pi_{2}}^{0}\leftrightarrow a_{t_{0}}^{0}\land b_{\pi_{2}}^{0}\leftrightarrow b_{t_{0}}^{0}]$\\ $[a_{\pi_{2}}^{0}\leftrightarrow a_{t_{1}}^{0}\land b_{\pi_{2}}^{0}\leftrightarrow b_{t_{1}}^{0}]$\\ \end{tabular} \Big{)}\\ \end{tabular}\right]\wedge(a^{0}_{\pi_{0}}\land(a^{0}_{\pi_{1}}\rightarrow\neg b^{0}_{\pi_{1}}\land a^{0}_{\pi_{2}}\rightarrow b^{0}_{\pi_{2}}))\right)$$

Full text

1 Introduction

HyperLTL [3] extends linear-time temporal logic (LTL) [20] with explicit quantification over traces. This makes it possible to express hyperproperties [4] like noninterference [13] or symmetry [11], which refer to multiple traces at the same time. Such properties are not expressible in LTL, or even in the branching-time temporal logics CTL [2] and CTL∗ [6]. For example, noninference [18] is a variant of noninterference stating that, for all system traces, the low-observable behavior must not change when all high inputs are replaced by a dummy input. The following HyperLTL formula expresses this policy: \forall\pi.\;\exists\pi^{\prime}.\;(\mbox{\sf G}\lambda_{\pi^{\prime}})\wedge\pi=_{L,out}{\pi^{\prime}}. HyperLTL is supported by model checking [11] and runtime monitoring tools [9, 10]. There is also a decision procedure, EAHyper [8], which checks the satisfiability of a given formula from the $\exists^{*}\forall^{*}$ fragment of HyperLTL. EAHyper is based on a reduction from HyperLTL satisfiability to LTL satisfiability [7]. A major application of EAHyper is to check equivalences between alternation-free HyperLTL formulas, i.e., formulas that either contain only universal quantifiers or only existential quantifers. Such equivalences can be expressed in the $\exists^{*}\forall^{*}$ fragment. It is impossible, however, to handle formulas that contain a $\forall\exists$ quantifier alternation, as, for example, in noninference. This is unfortunate, because such a quantifier alternation is often needed, in particular to account for nondeterminism. A popular example is generalized noninterference [14]: $\forall\pi.\forall\pi^{\prime}.\exists\pi^{\prime\prime}.~{}\pi\!=_{H,\mathsf{in}}\!\pi^{\prime\prime}\wedge\pi^{\prime}\!=_{L,out}\!\pi^{\prime\prime}$. The formula expresses that for every possible high-security input (seen on some trace $\pi$) and every possible low-security observations (seen on some trace $\pi^{\prime}$) there exists a nondeterministic execution $\pi^{\prime\prime}$ where the high-security input and the low-security observations happen together. Hence, the observer cannot conclude, after making the low-security observations, that any specific high-security input actually occurred. Other properties that need a $\forall\exists$ quantifier alternation include restrictiveness [15], separability [17], and forward correctability [19]. For formulas outside the $\exists^{*}\forall^{*}$ fragment, it is no longer possible to reduce the HyperLTL satisfiability problem to the LTL satsifiability problem: the HyperLTL satisfiability problem is, in fact, undecidable [7]. In this paper, we present the first semi-decisionprocedure for full HyperLTL. Our approach is based on a reduction to quantified boolean formulas (QBF) [12] and has been implemented in the MGHyper tool. MGHyper can be used to analyze and develop hyperproperties and, especially, generate models that disprove equivalences or implications between different hyperproperties or different formalizations of the same hyperproperty. For example, comparing noninference to generalized noninterference, MGHyper instantly demonstrates that the two properties are not equivalent.

2 A Semi-Decision Procedure for HyperLTL-SAT

A hyperproperty is a set of sets of traces. Hyperproperties can be expressed in HyperLTL, which generalizes LTL with explicit trace quantification:

[TABLE]

where $Q$ is an existential or universal quantifier, $a\in\mathit{AP}$ is an atomic proposition and $\pi\in\mathcal{V}$ is a trace variable of an infinitely supply $\mathcal{V}$. Logical connectives and the temporal operators $\sf F$, $\sf G$, $\,{\sf W}\,$ and $\,{\sf R}\,$ are defined as in LTL. The semantics of HyperLTL is defined as follows.

[TABLE]

,where $\Pi:\mathcal{V}\mapsto TR$ is the trace assignment function, which maps trace variables to traces, denoted by $\Pi[\pi\mapsto t]$. The suffixes of all traces $\pi$ starting at step $i$ is denoted by $\Pi[i,\infty]$. HyperLTL-SAT is the problem to decide, if a non-empty trace set $T$ exists, such that $\{\}\models_{T}\psi$.

MGHyper takes an arbitrary HyperLTL formula of the following form as input: $Q_{0}\vec{\pi_{0}}\ldots Q_{n}\vec{\pi_{n}}.\varphi$, where $Q_{i}\in\{\exists,\forall\}$ and $\vec{\pi_{0}}\dots\vec{\pi_{n}}$ are vectors over $\mathcal{V}$. MGHyper evaluates to “sat” if and only if the formula is satisfiable. Basically, MGHyper checks whether or not there exists a trace set of size $m$ that satisfies the HyperLTL formula under consideration. The procedure starts with trace sets of size $1$, and increment $m$ until a witness is found, leading to the following theorem.

Theorem 2.1

HyperLTL-SAT is RE-complete.

Proof

We prove membership by constructing a QBF formula $\varphi_{QBF}^{m}$, which is satisfiable if the given HyperLTL formula $\varphi$ is satisfiable by a trace set of size $m$. The basic idea of the encoding of a HyperLTL formula to a QBF formula is threefold: 1) we construct a quantifier prefix that resembles the quantifier structure in the given HyperLTL formula, 2) we construct a premise that links trace variables to actual traces, and 3) we unroll the LTL suffix into a SAT-encoding. The third step follows the unrolling presented in [1] and will, due to space reasons, not be discussed. We refer to the maximum trace-unrolling bound as $k$ (not to confuse with $m$), which is exponential in the size of the LTL suffix.

1) Prefix.

Let S be a set and $k$ a natural number, we define ${\mathit{Traces}^{k}_{S}}$ as ${\{a_{s}^{i}\mid 0\leq i<k,\forall s\in S,\forall a\in\mathit{AP}\}}$, which we use as the trace representation inside the QBF encoding. Let $\varphi:=Q_{0}\vec{\pi_{0}}\ldots Q_{n}\vec{\pi_{n}}.\psi$ be a HyperLTL formula. The quantifier prefix of the resulting QBF introduces existential quantifiers, representing the trace set $T$ of size $m$ (the witness for satisfiability). The trace variables are quantified according to their quantifier in the HyperLTL formula:

[TABLE]

2) Linking.

We construct a premise to link trace variables to the trace witnesses in $\mathit{Traces}^{k}_{T}$. For every quantifier $Q_{i}$ a subpremise $P_{Q_{i}}$ is constructed first, which represents the mapping of all trace variables in $\vec{\pi_{i}}$. Mapping each trace variable to traces reassembles the trace assignment function from the HyperLTL semantics and is encoded by ensuring that the boolean variables with the same atomic proposition in the same step share the same truth value.

[TABLE]

The linking mechanism is a combination of the subpremises. The boolean connective between the different supremises depends on the corresponding quantifier:

[TABLE]

where $\circ_{Q_{i}}$ equals $\rightarrow$, if $Q_{i}=\forall$, and $\circ_{Q_{i}}$ equals $\land$ if $Q_{i}=\exists$. Together with 3) the unrolling of the LTL suffix [1], the constructed $\varphi_{QBF}^{m}$ a QBF formula is satisfiable if the HyperLTL formula $\varphi$ is satisfiable. Hardness follows from a reduction from Post’s Correspondence Problem [7].∎

Example 1

Consider the HyperLTL formula $\varphi:=\forall\pi_{0}\exists\pi_{1}\exists\pi_{2}.(a_{\pi_{0}}\land(a_{\pi_{1}}\rightarrow\neg b_{\pi_{1}}\land a_{\pi_{2}}\rightarrow b_{\pi_{2}}))$. Note that, for the sake of simplicity, the example LTL formula does not contain temporal operators. In the first iteration, MGHyper tries to guess a trace set $T$ of size $1$ and will not find a satisfying assignment for the constructed QBF formula. In the second iteration, though, MGHyper constructs the following QBF formula, with $T_{2}=\{\{a^{0}_{t_{0}},b^{0}_{t_{0}}\},\{a^{0}_{t_{1}},b^{0}_{t_{1}}\}\}$.

[TABLE]

This QBF formula is satisfied by the assignment $\mathcal{A}=\{a^{0}_{t_{0}},b^{0}_{t_{0}},a^{0}_{t_{1}},\neg b^{0}_{t_{1}}\}$ for the existentially quantified variables, which represent the traces (of length one in this example). There are four possible assignment for the universally quantified boolean variables. For $\{a^{0}_{\pi_{0}},b^{0}_{\pi_{0}}\}$ or $\{a^{0}_{\pi_{0}},\neg b^{0}_{\pi_{0}}\}$ we can map the existentially quantified traces variables $\pi_{1}\mapsto t_{1}$ and $\pi_{2}\mapsto t_{0}$, which add $\{a_{\pi_{1}}^{0},\neg b_{\pi_{1}}^{0},a_{\pi_{2}}^{0},b_{\pi_{2}}^{0}\}$ to $\mathcal{A}$, such that $\mathcal{A}$ satisfies the formula. In the other two cases,$\{\neg a^{0}_{\pi_{0}},\neg b^{0}_{\pi_{0}}\}$ or $\{\neg a^{0}_{\pi_{0}},b^{0}_{\pi_{0}}\}$, we cannot map to $\neg a^{0}_{\pi_{0}}$, which leads to a false evaluation of $P_{Q_{0}}^{0}$ and therefore to a true evaluation of the formula. From $\mathcal{A}$ we can now follow that $\{\{a,b\}^{\omega},\{a\}^{\omega}\}$ is a model that satisfies $\varphi$.

3 Experimental Results

MGHyper is implemented in Ocaml and supports UNIX-based operation systems. We tested our tool against different benchmarks on a virtual machinerunning an Ubuntu (64-Bit) 14.04LTS installation on an Intel Core i7-4710MQ with 2,50GH on 4 kernels and 8GB RAM.

Counter Examples for Implication of Security Polices.

A main application of MGHyper is to check if two arbitrary HyperLTL formulas do not imply each other: we check if the negation of the implication is satisfiable. The first benchmark checks the implication of General Noninterference [4] ((GNI):\forall\pi_{1}.\forall\pi_{2}.\exists\pi_{3}\mbox{\sf G}(I^{high}_{\pi_{1}}=I^{high}_{\pi_{3}})\land\mbox{\sf G}(O^{low}_{\pi_{2}}=O^{low}_{\pi_{3}})), Noninerference ((NI): \forall\pi_{1}.\;\exists\pi_{2}.\;(\mbox{\sf G}\lambda_{\pi_{2}})\wedge\mbox{\sf G}(O_{\pi_{1}}=O_{\pi_{2}})) and several formalizations of Observational Determinsim [16, 21, 22]: (OD): \forall\pi_{1}.\forall\pi_{2}.(I^{low}_{\pi_{1}}=I^{low}_{\pi_{2}})\rightarrow\mbox{\sf G}(O^{low}_{\pi_{1}}=O^{low}_{\pi_{2}}), (GOD): \forall\pi_{1}.\forall\pi_{2}.\mbox{\sf G}(I^{low}_{\pi_{1}}=I^{low}_{\pi_{2}})\rightarrow\mbox{\sf G}(O^{low}_{\pi_{1}}=O^{low}_{\pi_{2}}), and (WOD):\forall\pi_{1}.\forall\pi_{2}.(I^{low}_{\pi_{1}}=I^{low}_{\pi_{2}})\mbox{,{\sf W},}(O^{low}_{\pi_{1}}\neq O^{low}_{\pi_{2}}). MGHyper shows that none of the formalizations of observational determinism does imply general non-interference or noninfernce. Furthermore, it shows that generalized non-interference does not imply noninference. Every check was done in under $0.05$ seconds.

Random Formulas.

We tested MGHyper against different benchmarks of random formulas. Quantfier Alternation: We created HyperLTL formulas with up to $49$ quantifier alternations and $15$ atomic propostion using randltl [5]. For each number of alternations we tested $100$ formulas of size $60$ and $120$, where 50 start with $\exists$ and 50 with $\forall$. The size is the size argument provided for randltl [5]. The runtimes are shown in Figure 1. Quantifier Ordering: $\exists^{n}\forall^{m}$ Formulas: For the sake of comparing MGHyper with EAHyper, we tested MGHyper on the largest decidable fragment of HyperLTL, which is the $\exists^{*}\forall^{*}$-fragment. We scaled in the number of existential and universal quantifiers, showing that MGHyper is able to solve formulas with up to $10$ existential and $10$ universal quantifier. In comparison, EAHyper, implementing the first decision procedure for HyperLTL-SAT, already runs out of memory after $5$ existential and $5$ universal quantifiers.

4 Conclusion

We have presented MGHyper, the first semi-decisionprocedure for checking the satisfiability of HyperLTL formulas beyond the decidable $\exists^{*}\forall^{*}$ fragment. An application of MGHyper is the analysis and development of hyperproperties and, especially, the generation of models that disprove equivalences or implications between different hyperproperties. In comparison to the existing decision procedure EAHyper, MGHyper not only handles the much larger class of hyperproperties, it also outperforms, as our experiments show, EAHyper within the $\exists^{*}\forall^{*}$ fragment.