Temporal Hyperproperties
Abstract
Hyperproperties generalize trace properties, which are sets of traces, to
sets of sets of traces. The most prominent application of hyperproperties is
information flow security: information flow policies characterize the secrecy
and integrity of a system by comparing two or more execution traces, for example
by comparing the outputs on execution traces that result from dierent
values of a secret input. HyperLTL is an extension of linear-time temporal
logic (LTL) with explicit quantification over traces. In this overview paper,
we survey recent results on the expressiveness of HyperLTL and on the satisfiability
and model checking problems. We also consider HyperCTL, the
extension of HyperLTL to branching time, and HyperFOLTL, the extension
of HyperLTL with first-order quantification.
sets of sets of traces. The most prominent application of hyperproperties is
information flow security: information flow policies characterize the secrecy
and integrity of a system by comparing two or more execution traces, for example
by comparing the outputs on execution traces that result from dierent
values of a secret input. HyperLTL is an extension of linear-time temporal
logic (LTL) with explicit quantification over traces. In this overview paper,
we survey recent results on the expressiveness of HyperLTL and on the satisfiability
and model checking problems. We also consider HyperCTL, the
extension of HyperLTL to branching time, and HyperFOLTL, the extension
of HyperLTL with first-order quantification.
Full Text:
PDFRefbacks
- There are currently no refbacks.