EAHyper – A Satisfiability Solver for Hyperproperties
Copyright © 2017 Christopher Hahn, Marvin Stenger, Saarland University
Introduction
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.
Availability
The source code is available at GitHub: EAHyper.
Try EAHyper directly in your browser 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 the latest version of VirtualBox.
Related Publications
EAHyper: Satisfiability, Implication,
and Equivalence Checking of Hyperproperties.
Bernd Finkbeiner, Christopher Hahn, and Marvin Stenger.29th International Conference on Computer-Aided Verification (CAV 2017).
Deciding Hyperproperties.
Bernd Finkbeiner and Christopher Hahn.27th International Conference on Concurrency Theory (CONCUR 2016).
Temporal Logics for Hyperproperties.
Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinksi, Markus N. Rabe, and César Sánchez.3rd International Conference on Principles of Security and Trust (POST 2014).
Contact
If you have questions or problems, please do not hesitate to contact Christopher Hahn.