Temporal Logics for Hyperproperties

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

329 citations recorded by the source corpus.

Hyperproperties, as introduced by Clarkson and Schneider, characterize the correctness of a computer program as a condition on its set of computation paths. Standard temporal logics can only refer to a single path at a time, and therefore cannot express many hyperproperties of interest, including noninterference and other important properties in security and coding theory. In this paper, we investigate an extension of temporal logic with explicit path variables. We show that the quantification over paths naturally subsumes other extensions of temporal logic with operators for information flow and knowledge. The model checking problem for temporal logic with path quantification is decidable. For alternation depth 1, the complexity is PSPACE in the length of the formula and NLOGSPACE in the size of the system, as for linear-time temporal logic.

Subfields: Artificial Intelligence, Computational Theory and Mathematics, Program Analysis & Verification

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

In Program Analysis & Verification

Citations in the corpus

Evaluating Large Language Models Trained on Code (2021, background): “• Hyperproperties (Clarkson et al., 2014): Informationflow policies and cryptographic algorithms requiring observational determinism which requires programs to behave as (deterministic) functions from low-security inputs to low-security outputs such as:”
A Hazard Analysis Framework for Code Synthesis Large Language Models (2022, neutral): “• Hyperproperties [14]: Information-flow policies and cryptographic algorithms requiring observational determinism which requires programs to behave as (deterministic) functions from low-security inputs to low-security outputs, for example: – Noninterference: when the outputs observed by low-securit”
Proving Differential Privacy in Hoare Logic (2014, background): “On a more practical side, it would be interesting to implement our transformation for a realistic setting, for instance modeling thePINQ language [30].”
A Roadmap Toward the Resilient Internet of Things for Cyber-Physical Systems (2018, methodology): “In order to specify hyperproperties, both LTL and STL have been extended respectively in HyperLTL [120] and HyperSTL [121] adding in the syntax both universal and existential quantiﬁers over a set of traces.”