Temporal logics for hyperproperties

Michael R. Clarkson; Bernd Finkbeiner; Masoud Koleini; Kristopher K. Micinski; Markus N. Rabe; César Sánchez

doi:10.1007/978-3-642-54792-8_15

Temporal logics for hyperproperties

Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez

Research output: Chapter in Book/Entry/Poem › Conference contribution

196 Scopus citations

Abstract

Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.

Original language	English (US)
Title of host publication	Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings
Publisher	Springer Verlag
Pages	265-284
Number of pages	20
ISBN (Print)	9783642547911
DOIs	https://doi.org/10.1007/978-3-642-54792-8_15
State	Published - 2014
Externally published	Yes
Event	3rd International Conference on Principles of Security and Trust, POST 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - Grenoble, France Duration: Apr 5 2014 → Apr 13 2014

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	8414 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	3rd International Conference on Principles of Security and Trust, POST 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
Country/Territory	France
City	Grenoble
Period	4/5/14 → 4/13/14

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-642-54792-8_15

Cite this

Clarkson, M. R., Finkbeiner, B., Koleini, M., Micinski, K. K., Rabe, M. N., & Sánchez, C. (2014). Temporal logics for hyperproperties. In Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings (pp. 265-284). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8414 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-54792-8_15

Temporal logics for hyperproperties. / Clarkson, Michael R.; Finkbeiner, Bernd; Koleini, Masoud et al.
Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, 2014. p. 265-284 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8414 LNCS).

Research output: Chapter in Book/Entry/Poem › Conference contribution

Clarkson, MR, Finkbeiner, B, Koleini, M, Micinski, KK, Rabe, MN & Sánchez, C 2014, Temporal logics for hyperproperties. in Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8414 LNCS, Springer Verlag, pp. 265-284, 3rd International Conference on Principles of Security and Trust, POST 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, 4/5/14. https://doi.org/10.1007/978-3-642-54792-8_15

Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, Sánchez C. Temporal logics for hyperproperties. In Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag. 2014. p. 265-284. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-54792-8_15

Clarkson, Michael R. ; Finkbeiner, Bernd ; Koleini, Masoud et al. / Temporal logics for hyperproperties. Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings. Springer Verlag, 2014. pp. 265-284 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2c6e4ac032774f7b8ab8b940594720bf,

title = "Temporal logics for hyperproperties",

abstract = "Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.",

author = "Clarkson, {Michael R.} and Bernd Finkbeiner and Masoud Koleini and Micinski, {Kristopher K.} and Rabe, {Markus N.} and C{\'e}sar S{\'a}nchez",

year = "2014",

doi = "10.1007/978-3-642-54792-8_15",

language = "English (US)",

isbn = "9783642547911",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "265--284",

booktitle = "Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings",

note = "3rd International Conference on Principles of Security and Trust, POST 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 ; Conference date: 05-04-2014 Through 13-04-2014",

}

TY - GEN

T1 - Temporal logics for hyperproperties

AU - Clarkson, Michael R.

AU - Finkbeiner, Bernd

AU - Koleini, Masoud

AU - Micinski, Kristopher K.

AU - Rabe, Markus N.

AU - Sánchez, César

PY - 2014

Y1 - 2014

N2 - Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.

AB - Two new logics for verification of hyperproperties are proposed. Hyperproperties characterize security policies, such as noninterference, as a property of sets of computation paths. Standard temporal logics such as LTL, CTL, and CTL* can refer only to a single path at a time, hence cannot express many hyperproperties of interest. The logics proposed here, HyperLTL and HyperCTL*, add explicit and simultaneous quantification over multiple paths to LTL and to CTL*. This kind of quantification enables expression of hyperproperties. A model checking algorithm for the proposed logics is given. For a fragment of HyperLTL, a prototype model checker has been implemented.

UR - http://www.scopus.com/inward/record.url?scp=84900551171&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84900551171&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-54792-8_15

DO - 10.1007/978-3-642-54792-8_15

M3 - Conference contribution

AN - SCOPUS:84900551171

SN - 9783642547911

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 265

EP - 284

BT - Principles of Security and Trust - Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Proceedings

PB - Springer Verlag

T2 - 3rd International Conference on Principles of Security and Trust, POST 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014

Y2 - 5 April 2014 through 13 April 2014

ER -

Temporal logics for hyperproperties

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this