EAHyper

Hyperproperties generalize properties of individual computation traces in that they relate such traces to each other. This is needed to express information flow security policies, such as observational determinism: A systems behavior should appear to be deterministic to an external observer, i.e., there should be no information leakage of certain secrets into the public domain.

HyperLTL, which extends linear-time temporal logic (LTL) with explicit trace quantification, is a recently introduced temporal logic capable of formalizing many hyperproperties of interest. However, formalizing hyperproperties in HyperLTL can be error-prone, since we have to consider multiple traces at the same time.

We introduce EAHyper, the first satisfiability solver for hyperproperties expressed in the decidable fragment of HyperLTL. EAHyper can be used to automatically detect specifications which are vacuously true or inconsistent and to check implication and equivalence between multiple formalizations of the same requirement. With EAHyper, an overhead in verification processes, such as model checking (check out MCHyper) or monitoring, may be avoided by detecting erroneous or redundant specifications reliably and easily at an early stage during the verification process. EAHyper can also be used to understand formalized hyperproperties better, for example, the many different variations of information flow policies considered by the security community.

Try the online interface:

Checkout the Source

Publications

• EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties
  Bernd Finkbeiner, Christopher Hahn and Marvin Stenger · CAV 2017
• Deciding Hyperproperties
  Bernd Finkbeiner and Christopher Hahn · CONCUR 2016
• Temporal Logics for Hyperproperties
  Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe and César Sánchez · POST14