MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the $\exists^*\forall^*$ Fragment
Bernd Finkbeiner Christopher Hahn Tobias Hans

	
	
	Reactive Systems Group
Saarland University
lastname@react.uni-saarland.de
	: Checking Satisfiability of HyperLTL Formulas Beyond the ∃^*∀^* FragmentThis work was partially supported by the German Research Foundation (DFG) in the Collaborative Research Center 1223 and by the European Research Council (ERC) Grant OSARES (No. 683300).
    Bernd Finkbeiner Christopher Hahn Tobias Hans
    Received <date>/ Accepted <date>
==================================================================================================================================================================================================================================================================


	
	
	

	
	
          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 , a tool for
          automatic satisfiability checking and model generation for
          hyperproperties expressed in HyperLTL. Unlike previous
          satisfiability checkers, is not limited to the
          decidable ∃^*∀^* fragment of HyperLTL, but
          provides a semi-decisionprocedure for the full logic.  An
          important application of 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 and report on experimental results
          obtained both with typical hyperproperties from the
          literature and with randomly generated HyperLTL formulas.





	
	
	

§ INTRODUCTION

	

	
	HyperLTL <cit.> extends linear-time temporal logic (LTL) <cit.> with explicit quantification over traces. This makes it possible to express hyperproperties <cit.> like noninterference <cit.> or symmetry <cit.>, 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 <cit.> and CTL^* <cit.>.
	For example, noninference <cit.> 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:
	∀π. ∃π'. (λ_π' ) ∧π =_L, outπ'.
	
	HyperLTL is supported by model checking <cit.> and runtime monitoring tools <cit.>. There is also a decision procedure, EAHyper <cit.>, which checks the satisfiability of a given formula from the ∃^*∀^* fragment of HyperLTL. EAHyper is based on a reduction from HyperLTL satisfiability to LTL satisfiability <cit.>. 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 ∃^*∀^* fragment. It is impossible, however, to handle formulas that contain a ∀∃ 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 <cit.>:
∀π.∀π'.∃π”. π=_H,𝗂𝗇π”∧π'=_L, outπ”.
The formula expresses that for every possible high-security input (seen on some trace π) and every possible low-security observations (seen on some trace π') there exists a nondeterministic execution π” 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 ∀∃ quantifier alternation include restrictiveness <cit.>, separability <cit.>, and forward correctability <cit.>.

For formulas outside the ∃^*∀^* 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 <cit.>. In this paper, we present the first semi-decisionprocedure for full HyperLTL. Our approach is based on a reduction to quantified boolean formulas (QBF) <cit.> and has been implemented in the tool. 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, instantly demonstrates that the two properties are not equivalent.

	



§ 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:




    ψ    ::= ∃π. ψ  |  ∀π. ψ  |  φ
    φ    ::= a_π  | φ  |  φ ∨ φ  |   φ  |  φ φ  |  true

where Q is an existential or universal quantifier, a ∈ is an atomic proposition and π∈ is a trace variable of an infinitely supply .
Logical connectives and the temporal operators  , ,  and  are defined as in LTL.

The semantics of HyperLTL is defined as follows.



    Π_T ∃π. ψ      iffthere exists t ∈ T : Π[π↦ t] _T ψ
       Π_T ∀π. ψ      ifffor all t ∈ T : Π[π↦ t] _T ψ
       Π_T a_π      iff a ∈Π(π)[0] 
       Π_T ψ      iffΠ_T ψ
       Π_T ψ_1 ∨ψ_2       iffΠ_T ψ_1 or Π_T ψ_2 
       Π_T ψ      iffΠ[1,∞] _T ψ
       Π_T ψ_1 ψ_2       iffthere exists i ≥ 0 : Π[i,∞] _T ψ_2 
             and for all 0 ≤ j < i we have Π[j,∞] _T ψ_1

,where Π:↦ TR is the trace assignment function, which maps trace variables to traces, denoted by Π[π↦ t]. 

The suffixes of all traces π starting at step i is denoted by Π [ i, ∞ ].
HyperLTL-SAT is the problem to decide, if a non-empty trace set T exists, such that {}_T ψ.

takes an arbitrary HyperLTL formula of the following form as input: Q_0 π⃗_⃗0⃗… Q_n π⃗_⃗n⃗ . φ, where Q_i ∈{∃, ∀} and π⃗_⃗0⃗…π⃗_⃗n⃗ are vectors over 𝒱. evaluates to “sat” if  and only if the formula is  satisfiable. Basically, 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.






	HyperLTL-SAT is RE-complete.



	We prove membership by constructing a QBF formula φ_QBF^m, which is satisfiable if the given HyperLTL formula φ 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 <cit.> 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 𝑇𝑟𝑎𝑐𝑒𝑠^k_S as { a_s^i | 0 ≤ i < k ,∀ s ∈ S,∀ a ∈}, which we use as the trace representation inside the QBF encoding. Let φ:=Q_0 π⃗_⃗0⃗… Q_n π⃗_⃗n⃗ . ψ 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:
	
	

	
	
    𝑃𝑟𝑒𝑓𝑖𝑥(φ) = ∃𝑇𝑟𝑎𝑐𝑒𝑠^k_T.Q_0 𝑇𝑟𝑎𝑐𝑒𝑠^k_π⃗_⃗0⃗.Q_1 𝑇𝑟𝑎𝑐𝑒𝑠^k_π⃗_⃗1⃗.… . Q_n 𝑇𝑟𝑎𝑐𝑒𝑠^k_π⃗_⃗n⃗.

	
	

	
	

  
2) Linking.	
	We construct a premise to link trace variables to the trace witnesses in 𝑇𝑟𝑎𝑐𝑒𝑠^k_T.
	For every quantifier Q_i a subpremise P_Q_i is constructed first, which represents the mapping of all trace variables in π⃗_⃗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.


	
    P_Q_i := [  ⋀_π∈π⃗_⃗i⃗⋁_t_i ∈ T[  ⋀_ (a^j_t_i , a^j_π) ∈
    𝑇𝑟𝑎𝑐𝑒𝑠^k_t_i×𝑇𝑟𝑎𝑐𝑒𝑠^k_πa^j_t_i↔ a^j_π]  ]

	The linking mechanism is a combination of the subpremises. The boolean connective between the different supremises depends on the corresponding quantifier:
	
	
	
    𝐿𝑖𝑛𝑘𝑖𝑛𝑔(φ) := P_Q_0^k ∘_Q_0 P_Q_1^k ∘_Q_1… P_Q_n-1^k ∘_Q_n-1 P_Q_n^k ∘_Q_n,

	where ∘_Q_i equals →, if Q_i = ∀, and ∘_Q_i equals  if Q_i = ∃.
	Together with 3) the unrolling of the LTL suffix <cit.>, the  constructed φ_QBF^m  a QBF formula is satisfiable if the HyperLTL formula φ is satisfiable. 
	Hardness follows from a reduction from Post's Correspondence Problem <cit.>.


	Consider the HyperLTL formula φ:= ∀π_0 ∃π_1 ∃π_2 . (a_π_0  ( a_π_1→ b_π_1  a_π_2→   b_π_2) ). 
	Note that, for the sake of simplicity, the example LTL formula does not contain temporal operators. 
	
	
	In the first iteration, 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, constructs the following QBF formula, with T_2= {{ a^0_t_0 , b^0_t_0}, { a^0_t_1 , b^0_t_1}}.
	
	
	
    ∃𝑇𝑟𝑎𝑐𝑒𝑠^0_T_2∀𝑇𝑟𝑎𝑐𝑒𝑠^0_π_0∃𝑇𝑟𝑎𝑐𝑒𝑠^0_π_1∃𝑇𝑟𝑎𝑐𝑒𝑠^0_π_2. 
    	[ ( a_π_0^0↔  a_t_0^0  b_π_0^0↔  b_t_0^0 )
    (  a_π_0^0↔  a_t_1^0  b_π_0^0↔  b_t_1^0)
    ] 
       →(  [ (   [ a_π_1^0↔  a_t_0^0  b_π_1^0↔  b_t_0^0 ]
    [ a_π_1^0↔  a_t_1^0  b_π_1^0↔  b_t_1^0 ]
    ) 
    (   [ a_π_2^0↔  a_t_0^0  b_π_2^0↔  b_t_0^0 ]
    [ a_π_2^0↔  a_t_1^0  b_π_2^0↔  b_t_1^0 ]
    ) 
    ] 
    	∧ (a^0_π_0  ( a^0_π_1→ b^0_π_1  a^0_π_2→   b^0_π_2) )  )

	
	This QBF formula is satisfied by the assignment 𝒜 =  { a^0_t_0, b^0_t_0, a^0_t_1 ,  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_π_0 , b^0_π_0} or {a^0_π_0 ,   b^0_π_0} we can map the existentially quantified traces variables π_1↦ t_1 and π_2 ↦ t_0,
	which add {a_π_1^0 ,  b_π_1^0, a_π_2^0, b_π_2^0} to 𝒜, such that 𝒜 satisfies the formula.
	In the other two cases,{ a^0_π_0,  b^0_π_0} or { a^0_π_0 ,  b^0_π_0}, we cannot map to a^0_π_0, which leads to a false evaluation of 
	P_Q_0^0 and therefore to a true evaluation of the formula. 
	From 𝒜 we can now follow that {{a,b}^ω , { a}^ω}  is a model that satisfies φ.






§ EXPERIMENTAL RESULTS


is implemented in Ocaml and supports UNIX-based operation systems.


We tested our tool against different benchmarks on a virtual machine
running 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 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 <cit.> ((GNI):∀π_1 .∀π_2. ∃π_3 ( I^high_π_1 = I^high_π_3 ) (O^low_π_2 = O^low_π_3 )),
Noninerference ((NI): 	∀π_1. ∃π_2. (λ_π_2 ) ∧ (O_π_1 = O_π_2))
and several formalizations of Observational Determinsim <cit.>:
(OD): ∀π_1 .∀π_2.( I^low_π_1 = I^low_π_2 ) →(O^low_π_1 = O^low_π_2 ),
(GOD): ∀π_1 .∀π_2.  ( I^low_π_1 = I^low_π_2 ) → (O^low_π_1 = O^low_π_2 ), and
(WOD):∀π_1 .∀π_2.( I^low_π_1 = I^low_π_2 )  (O^low_π_1≠ O^low_π_2 ).
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 against different benchmarks of random formulas.
Quantfier Alternation:
We created HyperLTL formulas with up to 49 quantifier alternations and 15 atomic propostion  using randltl <cit.>.
For each number of alternations we tested 100 formulas of size 60 and 120, where 50 start with ∃ and 50 with ∀. The size is the size argument provided for randltl <cit.>. The runtimes are shown in Figure <ref>.

Quantifier Ordering:


∃^n∀^m Formulas: For the sake of comparing with EAHyper, we tested on the largest decidable fragment of HyperLTL, which is the ∃^*∀^*-fragment. We scaled in the number of existential and universal quantifiers, showing that 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.





	






























































§ CONCLUSION



We have presented , the first semi-decisionprocedure for checking the satisfiability of HyperLTL formulas beyond the decidable ∃^*∀^* fragment. An application of 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 ∃^*∀^* fragment.
	

splncs03
	




	
