Skip to main content
Top

Hint

Swipe to navigate through the chapters of this book

2018 | OriginalPaper | Chapter

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

Authors : Bernd Finkbeiner, Christopher Hahn, Tobias Hans

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

share
SHARE

Abstract

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.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 69.000 Bücher
  • über 500 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 50.000 Bücher
  • über 380 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe



 


Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 58.000 Bücher
  • über 300 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko





Jetzt 90 Tage mit der neuen Mini-Lizenz testen!

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

Premium Partner