Skip to main content
EXTENDED SEARCH
Log in
Top
Published in:
Read chapter Read first chapter

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

Log in

Activate our intelligent search to find suitable subject content or patents.

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Business + Economics & Engineering + Technology"

Online-Abonnement

Springer Professional "Business + Economics & Engineering + Technology" gives you access to:

  • more than 102.000 books
  • more than 537 journals

from the following subject areas:

  • Automotive
  • Construction + Real Estate
  • Business IT + Informatics
  • Electrical Engineering + Electronics
  • Energy + Sustainability
  • Finance + Banking
  • Management + Leadership
  • Marketing + Sales
  • Mechanical Engineering + Materials
  • Insurance + Risk


Secure your knowledge advantage now!

inform now

Springer Professional "Engineering + Technology"

Online-Abonnement

Springer Professional "Engineering + Technology" gives you access to:

  • more than 67.000 books
  • more than 390 journals

from the following specialised fileds:

  • Automotive
  • Business IT + Informatics
  • Construction + Real Estate
  • Electrical Engineering + Electronics
  • Energy + Sustainability
  • Mechanical Engineering + Materials





 

Secure your knowledge advantage now!

inform now

Springer Professional "Business + Economics"

Online-Abonnement

Springer Professional "Business + Economics" gives you access to:

  • more than 67.000 books
  • more than 340 journals

from the following specialised fileds:

  • Construction + Real Estate
  • Business IT + Informatics
  • Finance + Banking
  • Management + Leadership
  • Marketing + Sales
  • Insurance + Risk



Secure your knowledge advantage now!

inform now
previous chapter EthIR: A Framework for High-Level Analysis of Ethereum Bytecode
next chapter Verifying Rust Programs with SMACK
Literature
1.
Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. (2003)
2.
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop (1981)
3.
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. POST (2014)
4.
Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comp. Sec. (2010)
5.
Duret-Lutz, A.: Manipulating LTL formulas using spot 1.0. In: ATVA (2013)
6.
Emerson, E.A., Halpern, J.Y.: “sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM (1986)
7.
Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: CONCUR (2016)
8.
Finkbeiner, B., Hahn, C., Stenger, M.: Eahyper: satisfiability, implication, and equivalence checking of hyperproperties. In: CAV (2017)CrossRef
9.
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. In: RV (2017)CrossRef
10.
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Rvhyper : a runtime verification tool for temporal hyperproperties. In: TACAS (2018)
11.
Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking hyperltl and hyperctl \(\hat{}\) *. In: CAV (2015)
12.
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.
Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P (1982)
14.
McCullough, D.: Noninterference and the composability of security properties. In: S&P (1988)
15.
McCullough, D.: A hookup theorem for multilevel security. IEEE Trans. Softw. Eng. (1990)
16.
McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37–58 (1992)CrossRef
17.
McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: S&P (1994)
18.
McLean, J.: A general theory of composition for a class of “possibilistic” properties. IEEE Trans. Softw. Eng. (1996)
19.
Millen, J.K.: Unwinding forward correctability. J. Comput. Secur. (1995)
20.
Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science (1977)
21.
Roscoe, A.W.: CSP and determinism in security modelling. In: S&P (1995)
22.
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
Book
Automated Technology for Verification and Analysis

Print ISBN: 978-3-030-01089-8

Electronic ISBN: 978-3-030-01090-4

Copyright Year: 2018

DOI
https://doi.org/10.1007/978-3-030-01090-4_31

Premium Partner

    Image Credits