Source-linked AI summary
Temporal Logics for Hyperproperties
Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, César Sánchez
TL;DR
Important security policies cannot always be expressed as properties of individual execution traces, motivating logics that quantify over multiple traces. The paper proposes HyperLTL and HyperCTL*, establishes decidable model checking with efficient bounds for a low HyperCTL* fragment, and demonstrates HyperLTL verification with a prototype.
Problem
Important security policies cannot be characterized as properties of individual execution traces, motivating a logic for properties of trace sets.
Method
The paper proposes HyperLTL and HyperCTL*, which add simultaneous quantification over multiple execution traces to LTL- and CTL*-style logics.
Results
The model checking problem is decidable, and the lowest HyperCTL* fragment without quantifier alternation is checkable in NLOGSPACE in the number of program states.
Takeaways & Limitations
The logics provide a familiar syntax for expressing well-known hyperproperties and information-flow security policies.
Takeaways & Limitations
The paper leaves probabilistic policy specifications unexplored and notes that the relative expressiveness and verifiability of alternative logics remain open questions.
Abstract
from arXiv · showhide
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.
1 Introduction
The paper introduces HyperLTL and HyperCTL*, temporal logics that quantify over multiple execution traces to express hyperproperties and security policies beyond ordinary trace properties. It establishes decidable model checking, characterizes complexity for fragments, and prototypes verification for an important HyperLTL fragment.
- Motivation: Hyperproperties describe sets of execution traces, so standard trace-based verification cannot directly express some important security policies.Specialized techniques exist for particular hyperproperties, but a unifying logic could support automated verification across a wider range of policies.
- HyperLTL: HyperLTL extends LTL with simultaneous quantification over multiple traces and can express information-flow policies such as observational determinism.The paper presents HyperLTL as a simple, unifying logic for directly expressing many information-flow policies.
- Security policies: The paper formalizes security policies in HyperLTL, including policies appropriate for differing adversary powers and observations.The examples address nondeterministic choices, adversarial influence over those choices, and execution-time monitoring.
- HyperCTL*: HyperCTL* generalizes CTL* by permitting multiple execution traces to remain in scope simultaneously, unlike CTL*’s single trace in scope.HyperLTL is the prenex-form fragment of HyperCTL*, making HyperCTL* a strict generalization.
- Model checking: HyperCTL* model checking is decidable via reduction to quantified propositional temporal logic, yielding a hierarchy based on quantifier alternations.The lowest fragment, with no quantifier alternation, is checkable in NLOGSPACE in the number of program states.
- Prototype: A prototype model checker handles an important HyperLTL fragment, including the paper’s examples, using LTL algorithms and self-composition.Its complexity is exponential in program size and doubly exponential in formula size, which the paper describes as impractical for real-world programs.
2 HyperLTL
HyperLTL extends LTL with trace quantification and trace-indexed propositions, while its temporal operators evaluate corresponding positions across quantified traces. Formulas are interpreted over trace sets and assignments generated from Kripke structures.
- Syntax: HyperLTL formulas quantify explicitly over traces using existential and universal trace variables.A formula may combine quantifiers, such as ∀π1. ∀π2. ∃π3. ψ, to relate several traces.
- Syntax: Atomic propositions are annotated with trace variables so formulas can distinguish the trace on which each proposition is evaluated.Boolean connectives retain their classical meanings, while implication, conjunction, and bi-implication are syntactic sugar.
- Semantics: The temporal operators X and U evaluate states at matching indices across all quantified traces.Standard operators including F, G, W, and R are defined syntactically from the basic temporal operators.
- Trace comparison: Trace-comparison notation specifies agreement or disagreement between assigned traces on selected propositions at the initial state or throughout execution.The notation supports expressing relationships among traces, which is central to hyperproperty specifications.
- Semantics: HyperLTL semantics uses a trace set and a partial assignment mapping trace variables to traces.Existential quantification extends the assignment with one trace from the set, whereas universal quantification checks every trace in the set.
- Program models: Programs are represented by Kripke structures, whose infinite labeled paths generate the trace set used for formula satisfaction.Nonempty transitions ensure that every generated trace is infinite; a structure satisfies a formula when its trace set satisfies it.
3 Security Policies in HyperLTL
HyperLTL formalizes diverse information-flow policies by relating multiple traces, including noninterference variants, declassification, quantitative leakage bounds, and asynchronous executions.
- HyperLTL formulates information-flow policies that constrain how information propagates from inputs to outputs.
- Noninterference: Noninference requires low-observable behavior to remain unchanged when high inputs are replaced by a dummy input λ.
- Nondeterminism: Observational determinism requires traces with identical initial low observations to remain indistinguishable to low users.
- Nondeterminism: Generalized noninterference permits nondeterministic low behavior while prohibiting high-input injection from altering low-security outputs.
- Declassification: HyperLTL specifies customized declassification policies that permit designated disclosures while retaining other observational-determinism requirements.
- Quantitative noninterference: Under deterministic programs and uniformly distributed secrets, min-entropy bounding reduces to excluding 2n +1 low-distinguishable traces; probabilistic extensions remain unexplored.
- Event-based systems: HyperLTL also expresses security policies for asynchronous event-based executions, including original noninterference and observational determinism.
4 HyperCTL∗
HyperCTL∗ extends HyperLTL with branching-time path quantification, allowing quantified formulas inside temporal operators and thereby expressing properties unavailable to HyperLTL.
- Syntax: HyperCTL∗ extends HyperLTL and CTL∗ by quantifying over multiple paths through a Kripke structure.
- Semantics: HyperCTL∗ formulas use path assignments, temporal operators, and existential path quantification over paths beginning at the relevant current state.
- Model checking: HyperCTL∗ model checking asks whether a Kripke structure satisfies a specification under the empty path assignment.
- Syntax: Unlike HyperLTL, HyperCTL∗ permits path quantifiers anywhere within formulas, including inside the scope of temporal operators.
- HyperCTL∗ vs. HyperLTL: HyperLTL is the prenex fragment of HyperCTL∗, while HyperCTL∗ is a strict generalization allowing quantified subformulas under temporal operators.
- HyperCTL∗ vs. HyperLTL: The formula ∀π. X ∀π′. X (lπ ↔lπ′) has no equivalent HyperLTL formula, demonstrating HyperCTL∗’s additional expressive power.
- HyperCTL∗ vs. HyperLTL: SecLTL can be encoded in HyperCTL∗ but not in HyperLTL, providing another distinction between the logics.
5 Related Logics
HyperLTL and HyperCTL* are compared with temporal, propositional, epistemic, and security logics, showing both expressive relationships and model-checking consequences.
- Temporal Logics: LTL, CTL, and CTL* cannot directly express information-flow policies because their path quantifiers do not retain multiple paths in scope.HyperCTL* extends CTL*, while HyperLTL extends LTL with explicit simultaneous path quantification.
- QPTL: HyperLTL subsumes QPTL, but QPTL cannot express properties requiring the existence of system paths.The translation replaces propositional quantifiers with path quantifiers, while formulas such as ∃π. X aπ have no QPTL equivalent.
- Epistemic Logics: HyperLTL subsumes a common epistemic temporal logic under both synchronous and asynchronous semantics.The asynchronous correspondence assumes a structure that permits stuttering and marks stuttering steps propositionally.
- Epistemic Logics: HyperLTL and epistemic temporal logic have the same non-elementary worst-case model-checking complexity, while selected information-flow policies admit NLOGSPACE or PSPACE algorithms.The NLOGSPACE cases include observational determinism, declassification, and fixed-bit quantitative noninterference; noninference and generalized noninterference are PSPACE.
- SecLTL: SecLTL specifications can be encoded in HyperCTL*, transferring PSPACE-hardness to HyperCTL* and, for the construction used, to HyperLTL.The HyperCTL* hardness result applies for fixed alternation depth at least 1.
6 Model Checking and Satisfiability
The paper reduces HyperCTL* model checking to QPTL satisfiability and characterizes complexity by quantifier alternation, while distinguishing model checking from satisfiability.
- Model Checking: HyperCTL* model checking is decidable through a reduction to quantified propositional temporal logic and a hierarchy based on quantifier alternations.Alternation depth is defined along syntax-tree paths, with until and release counted as additional alternations.
- Complexity: HyperCTL* model checking with alternation depth k is complete for NSPACE(gc(k, |ϕ|)) and belongs to NSPACE(gc(k−1, |K|)) for the structure size.Here gc denotes a tower of exponentials, with the convention that the height −1 case yields logarithmic space.
- Model Checking: The encoding uses automata constructions, projection, complementation, and representations of Kripke structures and paths as quantified propositions.HyperCTL* path quantifiers become quantified proposition sets encoding path labels and states.
- Complexity: Alternation depth 0 yields an NLOGSPACE result in the number of system states, while alternation depth at least 1 is PSPACE-hard in system size.The lower bounds derive from nondeterministic Büchi automata non-emptiness and the encoding of SecLTL, respectively.
- Satisfiability: The model-checking result does not extend positively to satisfiability; finite-state satisfiability is instead shown hard for a high complexity class.The proof reduces distributed-system LTL synthesis to HyperCTL* satisfiability.
7 Prototype Model Checker
A prototype model checker implements an expressive HyperLTL fragment using automata-based model checking and self-composition, demonstrating feasibility while exposing severe worst-case scaling.
- Scope: The prototype targets HyperLTL2, a fragment with at most one quantifier alternation that expresses all security policies formulated in Section 3.Allowed prefixes contain a sequence of universal quantifiers followed by existential quantifiers, or the reverse.
- Algorithm: The HyperLTL2 algorithm combines LTL model-checking automata, language containment, self-composition, and a new projection construction.The implementation is based on established LTL algorithms but adds constructions needed for trace quantification.
- Implementation: The roughly 3,000-line OCaml prototype accepts a Kripke structure and HyperLTL2 formula, constructs automata, and returns a countermodel when verification fails.Automata complementation is delegated to GOAL, and the prototype verifies noninference, observational determinism, and generalized noninference.
- Limitations: The prototype demonstrates model checking of hyperproperties but has worst-case exponential dependence on program size and doubly exponential dependence on formula size.The authors describe this complexity as impractical for real-world programs.
8 Related Work
Related work includes trace-set security formalisms, self-composition methods, epistemic and branching-time logics, and alternative hyperproperty logics whose relationships remain partly unresolved.
- Hyperproperties: Trace properties cannot express security policies such as noninterference when those policies depend on sets of execution traces rather than individual traces.Prior work formalizes such policies through selective interleaving functions and security predicates.
- Self-Composition: Self-composition enables CTL or CTL* verification of some relational policies, but it does not directly cover policies combining universal and existential quantification over infinite executions.HyperCTL* expresses policies over the original system rather than a self-composed one.
- Epistemic Logics: Temporal epistemic logics express several information-flow policies, but the paper leaves their relative power compared with HyperLTL open while proving HyperLTL subsumes a common epistemic logic.The related-work comparison notes differences in policy coverage and system assumptions.
- Alternative Logics: Alternative logics include holistic and incremental hyperproperty formalisms, with some automated techniques but unresolved exact expressive limitations.Holistic logic is described as straightforward to specify but lacking a general verification approach, whereas HyperLTL and HyperCTL* provide one.
- Open Questions: The expressiveness and verification efficiency of HyperLTL and HyperCTL* relative to other logics remain open questions.The paper presents its contribution as exploring a familiar temporal-logic-based design option for expressing known hyperproperties.
9 Concluding Remarks
The paper presents HyperLTL2 as a natural fragment for information-flow security and extends HyperLTL naturally to HyperCTL* by removing restrictions on quantifier placement. The work acknowledges contributors and support from multiple research grants.
- Concluding remarks: HyperLTL2 was selected because it expresses information-flow security policies while permitting at most one quantifier alternation.The authors describe this restriction as the fragment needed for information-flow security policies.
- Concluding remarks: HyperCTL* extends HyperLTL by removing restrictions on where quantifiers may appear.The paper presents this extension as a natural step from HyperLTL.
- Concluding remarks: The work was supported by AFOSR, NSF, DFG, and Spanish project funding, with contributions and discussions from several researchers.The acknowledgements name Fred B. Schneider and other contributors alongside the listed grants.
A.1 Goguen and Meseguer’s noninterference
The section formalizes Goguen and Meseguer’s noninterference model and shows how it is encoded and expressed with HyperLTL. The resulting theorem establishes equivalence between the encoded Kripke structure and noninterference in the original state machine.
- System model: Deterministic state machines evolve through user-issued commands and expose user-specific observations via transition and observation functions.The model uses do : S × U × C → S and out : S × U → Out.
- Noninterference: Noninterference asks whether removing all actions from high users GH leaves the low users GL observations unchanged.The definition compares outputs after projecting command sequences to selected user groups.
- Encoding: The Kripke encoding records the last command and responsible user, together with observations available to each user.The construction adds labeled states for the initial state and state-command-user combinations.
- Result: Theorem 8 states that the encoding satisfies the noninterference formula exactly when GH does not interfere with GL.This establishes correspondence for every state machine and user-group pair.
- Formula: The HyperLTL formula compares paths at the first input difference and requires low-observation equivalence when the difference is an additional secret action by GH.The next operator permits comparison of different trace positions.
- Related security properties: HyperCTL* can also express observational determinism by quantifying over two paths in an encoding based on self-composition with stuttering steps.The construction adapts a CTL* formula so its two program copies refer to separate paths.
A.3 Declassification
HyperLTL expresses declassification properties, including customized policies that permit specific disclosures while retaining observational determinism otherwise. This follows from its ability to subsume epistemic temporal logic.
- Declassification: HyperLTL supports customized declassification policies for controlled disclosures in programming-language settings.The example permits revealing whether an initially entered password is correct in the next state.
- Declassification: HyperLTL can express declassification properties discussed in prior work.The paper states this as Corollary 1.
- Declassification: The declassification result follows from encoding those properties in epistemic temporal logic and HyperLTL subsuming that logic.The paper also notes that HyperLTL can express such policies in a programming-language setting.
B Epistemic Logics
The paper shows that epistemic temporal logic can be encoded in HyperLTL under synchronous and asynchronous semantics. The asynchronous construction restricts stutter-expanded paths using progress and synchronization conditions.
- Synchronous semantics: The synchronous proof relies on stepwise comparison using an atomic proposition that switches value at every step.This assumption collapses stutter-equivalent comparison to step-wise comparison.
- Synchronous semantics: Under synchronous time, HyperLTL can express every epistemic temporal logic formula over Kripke structures.The equivalence holds for every formula and agent set under the stated synchronous semantics.
- Encoding: The encoding eliminates knowledge operators by repeatedly replacing their occurrences with propositions and auxiliary path quantification.The transformation continues until no knowledge operators remain.
- Encoding: Auxiliary proposition sequences mark evaluation positions and select a time through which two paths agree on an agent’s observations.The propositions u and t carry evaluation-position and time-selection information.
- Encoding limitation: Past operators would substantially simplify the encoding by making the initial branching state easier to reference.The paper identifies this as a simplification rather than part of the presented construction.
- Asynchronous semantics: For asynchronous systems, the construction restricts paths to those making progress and synchronizes observation changes by inserting stuttering steps.Theorem 11 states that every epistemic temporal logic formula has an equivalent HyperLTL formula for asynchronous Kripke structures.
C Satisfiability
The paper establishes satisfiability and model-checking foundations for HyperCTL* and HyperLTL using reductions and automata constructions. It also characterizes prototype complexity as exponential in the program and doubly exponential in the formula.
- Hardness: HyperCTL* finite-state satisfiability is shown hard via a reduction from distributed LTL synthesis with two processes and disjoint variable sets.The reduction constructs a formula whose finite models correspond exactly to finite solutions of the synthesis problem.
- Hardness: The reduction uses conjuncts enforcing the specification on all paths, input-complete successors, and output independence from the other process’s inputs.Together, these conjuncts encode the distributed architecture and its information-flow constraints.
- Automata constructions: An n-fold self-composition of a Büchi automaton recognizes exactly the zipped tuples of n strings recognized by the original automaton.The product construction synchronizes component transitions across the tuple alphabet.
- Automata constructions: For a HyperLTL2 formula, the construction preprocesses the formula, builds a generalized Büchi automaton from maximal consistent sets, and tracks trace-tuple suffixes.States describe formulas satisfied by trace tuples, while transitions enforce temporal progression and accepting sets ensure until obligations are eventually fulfilled.
- Model checking: The model-checking procedure is decidable through a reduction of HyperCTL* model checking to quantified propositional temporal logic, with HyperLTL decidability following immediately.The procedure can use automata complementation and a final intersection and non-emptiness check; a nonempty result supplies a counterexample.
- Complexity: The prototype is exponential in the Kripke structure and doubly exponential in the formula, unlike LTL model checking, which is polynomial in the program and exponential in the formula.The dominant cost is Büchi automaton complementation.