EAHyper is a satisfiability solver for hyperproperties expressed in the decidable fragment of HyperLTL.
See also https://www.react.uni-saarland.de/tools/eahyper/.
Copyright © 2017, 2018 Christopher Hahn, Marvin Stenger (Reactive Systems Group @ Saarland University)
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.
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 EAHyper directly in our online interface.
We preinstalled EAHyper on a virtual machine including the corresponding benchmarks given in [FHS17]. You can import this virtual machine by using VirtualBox.
-
Fulfill dependencies:
-
Clone this repository:
git clone https://github.com/reactive-systems/eahyper -
Build EAHyper:
cd eahyper make -
(Optional) Build benchmarks:
make benchmarks -
(Optional) Run demo to see if everything works properly:
make demo