Skip to main content

2018 | OriginalPaper | Buchkapitel

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

verfasst von : Bernd Finkbeiner, Christopher Hahn, Tobias Hans

Erschienen in: Automated Technology for Verification and Analysis

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 102.000 Bücher
  • über 537 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 Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comp. Sec. (2010) Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comp. Sec. (2010)
5.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: CONCUR (2016) Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: CONCUR (2016)
8.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat Millen, J.K.: Unwinding forward correctability. J. Comput. Secur. (1995) Millen, J.K.: Unwinding forward correctability. J. Comput. Secur. (1995)
20.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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)
Metadaten
Titel
MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the Fragment
verfasst von
Bernd Finkbeiner
Christopher Hahn
Tobias Hans
Copyright-Jahr
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_31

Premium Partner