EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties

Abstract

We introduce EAHyper, the first tool for the automatic checking of satisfiability, implication, and equivalence of hyperproperties. Hyperproperties are system properties that relate multiple computation traces. A typical example is an information flow policy that compares the observations made by an external observer on execution traces that result from different values of a secret variable. EAHyper analyzes hyperproperties that are specified in HyperLTL, a recently introduced extension of linear-time temporal logic (LTL). HyperLTL uses trace variables and trace quantifiers to refer to multiple execution traces simultaneously. Applications of EAHyper include the automatic detection of specifications that are inconsistent or vacuously true, as well as the comparison of multiple formalizations of the same policy, such as different notions of observational determinism.

This work was partially supported by the German Research Foundation (DFG) in the Collaborative Research Center 1223 and by the Graduate School of Computer Science at Saarland University.

1 Introduction

HyperLTL [3] is a recently introduced temporal logic for the specification of hyperproperties [4]. HyperLTL characterizes the secrecy and integrity of a system by comparing two or more execution traces. For example, we might express that the contents of a variable is secret by specifying that an external observer makes the same observations on all execution traces that result from different values of the variable. Such a specification cannot be expressed as a standard trace property, because it refers to multiple traces. The specification can, however, be expressed as a hyperproperty, which is a set of sets of traces.

HyperLTL has been used to specify and verify the information flow in communication protocols and web applications, the symmetric access to critical resources in mutex protocols, and Hamming distances between code words in error resistant codes [8, 9, 13]. The logic is already supported by both model checking [8] and runtime verification [1] tools. In this paper, we present the first tool for HyperLTL satisfiability. Our tool, which we call EAHyper, can be used to automatically detect specifications that are inconsistent or vacuously true, and to check implication and equivalence between multiple formalizations of the same requirement.

HyperLTL extends linear-time temporal logic (LTL) with trace variables and trace quantifiers. The requirement that the external observer makes the same observations on all traces is, for example, expressed as the HyperLTL formula $\forall \pi . \forall \pi '.\; \mathsf G(O_\pi = O_{\pi '})$, where O is the set of observable outputs. A more general property is observational determinism [12, 14, 17], which requires that a system appears deterministic to an observer who sees inputs I and outputs O. Observational determinism can be formalized as the HyperLTL formula $\forall \pi . \forall \pi '.\;\mathsf G(I_\pi =I_{\pi '})\rightarrow \mathsf G(O_\pi =O_{\pi '}),$ or, alternatively, as the HyperLTL formula $\forall \pi . \forall \pi '.\;(O_\pi =O_{\pi '}) ~{\mathcal W}~ (I_\pi \ne I_{\pi '})$. The first formalization states that on any pair of traces, where the inputs are the same, the outputs must be the same as well; the second formalization states that differences in the observable output may only occur after differences in the observable input have occurred. As can be easily checked with EAHyper, the second formalization is the stronger requirement.

EAHyper implements the decision procedure for the $\exists ^*\forall ^*$ fragment of HyperLTL [7]. The $\exists ^*\forall ^*$ fragment consists of all HyperLTL formulas with at most one quantifier alternation, where no existential quantifier is in the scope of a universal quantifier. Many practical HyperLTL specifications are in fact alternation-free, i.e., they contain either only universal or only existential quantifiers. The $\exists ^*\forall ^*$ fragment is the largest decidable fragment. It contains in particular all alternation-free formulas and also all implications and equivalences between alternation-free formulas.

In the remainder of this paper, we give a quick summary of the syntax and semantics of HyperLTL, describe the implementation of EAHyper, and report on experimental results.

2 HyperLTL

HyperLTL Syntax. HyperLTL extends LTL with trace variables and trace quantifiers. Let $\mathcal {V}$ be an infinite supply of trace variables, $AP$ the set of atomic propositions, and $TR$ the set of infinite traces over $AP$. The syntax of HyperLTL is given by the following grammar:

where $a\in AP$ is an atomic proposition and $\pi \in \mathcal V$ is a trace variable. The derived temporal operators $\mathsf F$, $\mathsf G$, and $\, \mathsf{W}\,$ are defined as for LTL. Logical connectives, i.e., $\wedge$, $\rightarrow$, and $\leftrightarrow$ are derived in the usual way. We also use syntactic sugar like $O_\pi = O_{\pi '}$, which abbreviates $\bigwedge _{a \in O } a_\pi \leftrightarrow a_{\pi '}$ for a set O of atomic propositions.

The $\exists ^*$ fragment of HyperLTL consists of all formulas that only contain existential quantifiers. The $\forall ^*$ fragment of HyperLTL consists of all formulas that only contain universal quantifiers. The union of the two fragments is the alternation-free fragment. The $\exists ^*\forall ^*$ fragment consists of all formulas with at most one quantifier alternation, where no existential quantifier is in the scope of a universal quantifier.

HyperLTL Semantics. A HyperLTL formula defines a hyperproperty, which is a set of sets of traces. A set T of traces satisfies the hyperproperty if it is an element of this set of sets. Formally, the semantics of HyperLTL formulas is given with respect to trace assignment $\varPi$ from $\mathcal {V}$ to $TR$, i.e., a partial function mapping trace variables to actual traces. $\varPi [\pi \mapsto t]$ denotes that $\pi$ is mapped to t, with everything else mapped according to $\varPi$. $\varPi [i,\infty ]$ denotes the trace assignment that is equal to $\varPi (\pi )[i,\infty ]$ for all $\pi$.

A HyperLTL formula $\varphi$ is satisfiable if and only if there exists a non-empty trace set T, such that $\varPi \models _T \psi$, where $\varPi$ is the empty trace assignment. The formula $\varphi$ is valid if and only if for all non-empty trace sets T it holds that $\varPi \models _T \psi$.

3 EAHyper

The input of EAHyper is either a HyperLTL formula in the $\exists ^* \forall ^*$ fragment, or an implication between two alternation-free formulas. For $\exists ^* \forall ^*$ formulas, EAHyper reports satisfiability; for implications between alternation-free formulas, validity. EAHyper proceeds in three steps:

• 1. Translation into the $\exists ^* \forall ^*$ fragment: If the input is an implication between two alternation-free formulas, we construct a formula in the $\exists ^* \forall ^*$ fragment that represents the negation of the implication. For example, for the implication of $\forall \pi _1 \dots \forall \pi _n.\;\psi$ and $\forall \pi '_1 \ldots \forall \pi '_m.\;\varphi$, we construct the $\exists ^*\forall ^*$ formula $\exists \pi _1' \ldots \exists \pi _m' \forall \pi _1 \ldots \forall \pi _n.\;\psi \wedge \lnot \varphi$. The implication is valid if and only if the resulting $\exists ^* \forall ^*$ formula is unsatisfiable.

• 2. Reduction to LTL satisfiability: EAHyper implements the decision procedure for the $\exists ^* \forall ^*$ fragment of HyperLTL [7]. The satisfiability of the HyperLTL formula is reduced to the satisfiability of an LTL formula:

  • Formulas in the $\forall ^*$ fragment are translated to LTL formulas by discarding the quantifier prefix and all trace variables. For example, $\forall \pi _1. \forall \pi _2.\;\mathsf Gb_{\pi _1} \wedge \mathsf G\lnot b_{\pi _2}$ is translated to the equisatisfiable LTL formula $\mathsf Gb \wedge \mathsf G\lnot b$.

  • Formulas in the $\exists ^*$ fragment are translated to LTL formulas by introducing a fresh atomic proposition $a_i$ for every atomic proposition a and every trace variable $\pi _i$. For example, $\exists \pi _1. \exists \pi _2.~a_{\pi _1} \wedge \mathsf G\lnot b_{\pi _1} \wedge \mathsf Gb_{\pi _2}$ is translated to the equisatisfiable LTL formula $a_1 \wedge \mathsf G\lnot b_1 \wedge \mathsf Gb_2$.

  • Formulas in the $\exists ^*\forall ^*$ fragment are translated into the $\exists ^*$ fragment (and then on into LTL) by unrolling the universal quantifiers. For example, $\exists \pi _1. \exists \pi _2. \forall \pi '_{1}. \forall \pi '_{2}.\;\mathsf Ga_{\pi '_1} \wedge \mathsf Gb_{\pi '_2} \wedge \mathsf Gc_{\pi _1} \wedge \mathsf Gd_{\pi _2}$ is translated to the equisatisfiable $\exists ^*$ formula .

• 3. LTL satisfiability: The satisfiability of the resulting LTL formula is checked through an external tool. Currently, EAHyper is linked to two LTL satisfiability checkers, pltl and Aalta.

  • Pltl [15] is a one-pass tableaux-based decision procedure for LTL, which not necessarily explores the full tableaux.

  • Aalta_2.0 [11] is a decision procedure for LTL based on a reduction to the Boolean satisfiability problem, which is in turn solved by minisat [6]. Aalta’s on-the-fly approach is based on so-called obligation sets and outperforms model-checking-based LTL satisfiability solvers.

EAHyper is implemented in OCaml and supports UNIX-based operating systems. Batch-processing of HyperLTL formulas is provided. Options such as the choice of the LTL satisfiability checker are provided via a command-line interface.

4 Experimental Results

We report on the performance of EAHyper on a range of benchmarks, including observational determinism, symmetry, error resistant code, as well as randomly generated formulas. The experiments were carried out in a virtual machine running Ubuntu 14.04 LTS on an Intel Core i5-2500K CPU with 3.3 GHZ and 2 GB RAM. We chose to run EAHyper in a virtual machine to make our results easily reproducible; running EAHyper natively results in (even) better performance.¹

• Observational Determinism [12, 14, 17]. Our first benchmark compares the following formalizations of observational determinism, with $|I|=|O|=1$: $( OD1 ):\forall \pi _1. \forall \pi _1'.\; \mathsf G(I_{\pi _1} = I_{\pi _1'}) \rightarrow \mathsf G(O_{\pi _1} = O_{\pi _1'})$, $( OD2 ):\forall \pi _2. \forall \pi _2'.\; (I_{\pi _2} = I_{\pi _2'}) \rightarrow \mathsf G(O_{\pi _2} = O_{\pi _2'})$, and $( OD3 ):\forall \pi _3. \forall \pi _3'.\;(O_{\pi _3} = O_{\pi _3'}) \, \mathsf{W}\,(I_{\pi _3} \not = I_{\pi _3'})$. EAHyper needs less then a second to order the formalizations with respect to implication: $OD2 \rightarrow OD1$, $OD2 \rightarrow OD3$, and $OD3 \rightarrow OD1$.

• Quantitative Noninterference [2]. The bounding problem of quantitative noninterference asks whether the amount of information leaked by a system is bounded by a constant c. This is expressed in HyperLTL as the requirement that there are no $c+1$ distinguishable traces for a low-security observer [16].

  

  In the benchmark, we check implications between different bounds. The performance of EAHyper is shown in Table 1. Using Aalta as the LTL satisfiability checker generally produces faster results, but pltl scales to larger bounds.

• Symmetry [8]. A violation of symmetry in a mutual exclusion protocol indicates that some concurrent process has an unfair advantage in accessing a critical section. The benchmark is derived from a model checking case study, in which various symmetry claims were verified and falsified for the Bakery protocol. EAHyper checks the implications between the four main symmetry properties from the case study in 13.86 s. Exactly one of the implications turns out to be true.

• Error resistant code [8]. Error resistant codes enable the transmission of data over noisy channels. A typical model of errors bounds the number of flipped bits that may happen for a given code word length. Then, error correction coding schemes must guarantee that all code words have a minimal Hamming distance. The following HyperLTL formula specifies that all code words $o\in O$ produced by an encoder have a minimal Hamming distance [10] of d: $\forall \pi .\; \forall \pi '.\; F (\bigvee _{i\in I} \lnot (i_\pi \leftrightarrow i_{\pi '})) \rightarrow \lnot Ham _O(d-1,\pi ,\pi ')$. $Ham_O$ is recursively defined as $Ham_O (-1,\pi ,\pi ') = false$ and $Ham_O (d,\pi ,\pi ') = (\bigwedge _{o\in O} o_\pi \leftrightarrow o_{\pi '}) \, \mathsf{W}\,(\bigvee _{o\in O} \lnot (o_\pi \leftrightarrow o_{\pi '}) \wedge \mathsf X\; Ham_O (d-1,\pi ,\pi ')).$ The benchmark checks implications between the HyperLTL formulas for different minimal Hamming distances. The performance of EAHyper is shown in Table 2.

• Random formulas. In the last benchmark, we randomly generated sets of 250 HyperLTL formulas containing five atomic propositions, using randltl [5] and assigning trace variables randomly to atomic propositions. As shown in Table 3, EAHyper reaches its limits, by running out of memory, after approximately five existential and five universal quantifiers.

Table 1. Quantitative noninterference benchmark: wall clock time in seconds for checking whether QN(row) implies QN(column). “–” denotes that the instance was not solved in 120 s.

Table 2. Error resistant codes benchmark: wall clock time in seconds for checking whether Ham(row) implies Ham(column).

Table 3. Random formulas benchmark: instances solved in 120 s and average wall clock time in seconds for 250 random formulas. Size denotes the tree-size argument for randltl.

5 Discussion

EAHyper is the first implementation of the decision procedure for the $\exists ^*\forall ^*$ fragment of HyperLTL [7]. For formulas with up to approximately five universal quantifiers, EAHyper performs reliably well on our broad range of benchmarks, which represent different types of hyperproperties studied in the literature as well as randomly generated formulas.