MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \(\exists ^*\forall ^*\) Fragment

  • Bernd Finkbeiner
  • Christopher Hahn
  • Tobias HansEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)


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


  1. 1.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. (2003)Google Scholar
  2. 2.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop (1981)Google Scholar
  3. 3.
    Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. POST (2014)Google Scholar
  4. 4.
    Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comp. Sec. (2010)Google Scholar
  5. 5.
    Duret-Lutz, A.: Manipulating LTL formulas using spot 1.0. In: ATVA (2013)Google Scholar
  6. 6.
    Emerson, E.A., Halpern, J.Y.: “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM (1986)Google Scholar
  7. 7.
    Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: CONCUR (2016)Google Scholar
  8. 8.
    Finkbeiner, B., Hahn, C., Stenger, M.: Eahyper: satisfiability, implication, and equivalence checking of hyperproperties. In: CAV (2017)CrossRefGoogle Scholar
  9. 9.
    Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. In: RV (2017)CrossRefGoogle Scholar
  10. 10.
    Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Rvhyper : a runtime verification tool for temporal hyperproperties. In: TACAS (2018)Google Scholar
  11. 11.
    Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking hyperltl and hyperctl \(\hat{}\) *. In: CAV (2015)Google Scholar
  12. 12.
    Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H Freeman, New York (1979)zbMATHGoogle Scholar
  13. 13.
    Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P (1982)Google Scholar
  14. 14.
    McCullough, D.: Noninterference and the composability of security properties. In: S&P (1988)Google Scholar
  15. 15.
    McCullough, D.: A hookup theorem for multilevel security. IEEE Trans. Softw. Eng. (1990)Google Scholar
  16. 16.
    McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37–58 (1992)CrossRefGoogle Scholar
  17. 17.
    McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: S&P (1994)Google Scholar
  18. 18.
    McLean, J.: A general theory of composition for a class of “possibilistic” properties. IEEE Trans. Softw. Eng. (1996)Google Scholar
  19. 19.
    Millen, J.K.: Unwinding forward correctability. J. Comput. Secur. (1995)Google Scholar
  20. 20.
    Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (1977)Google Scholar
  21. 21.
    Roscoe, A.W.: CSP and determinism in security modelling. In: S&P (1995)Google Scholar
  22. 22.
    Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: CSFW-2016 (2016)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Bernd Finkbeiner
    • 1
  • Christopher Hahn
    • 1
  • Tobias Hans
    • 1
    Email author
  1. 1.Reactive Systems GroupSaarland UniversitySaarbrückenGermany

Personalised recommendations