Hyperproperty¶

A system specification whose truth depends on the system's whole set of possible execution traces, allowing relations among multiple runs such as noninterference and observational determinism.

Version: v3 · 2026-09-06 · History
Domain-specific #: 2032
Origin domain: computer science
Subdomain: formal verification
Aliases: Hyper-property, Relational trace property

Core Idea¶

Let (Phi) be a universe of execution traces. An ordinary trace property is a set \(P\subseteq\Phi\): one trace either belongs or does not. A system is represented by its set of possible traces \(S\subseteq\Phi\). A hyperproperty is a set of such systems,

\[ H\subseteq\mathcal P(\Phi), \]

so satisfaction asks whether \(S\in H\).^[1] This one-level lift lets a specification compare alternative executions. Noninterference, for example, says that runs differing only in secret inputs must agree in their public observations; no verdict on one trace can establish that relation.

Hyperproperties generalize safety and liveness: every hyperproperty decomposes into hypersafety and hyperliveness components. A (k)-safety hyperproperty has every violation witnessed by at most (k) finite traces.^[1]

Structural Signature¶

A universe of traces (Phi).
Systems interpreted as trace sets \(S\subseteq\Phi\).
A predicate over systems rather than individual traces.
Formal type \(\mathcal P(\mathcal P(\Phi))\).
Quantification or relation across multiple executions.
Satisfaction defined at the trace-set level.
Hypersafety and hyperliveness decomposition.
Finite trace-set counterexamples for k-safety subclasses.
Security policies such as noninterference.
Logics with explicit trace variables.
Verification through self-composition, product programs, or hyper model checking.
Explicit handling of synchronous versus asynchronous trace alignment.

What It Is Not¶

It is not merely a difficult temporal property. LTL and ordinary safety/liveness inspect one execution at a time. It is not a property of source syntax, nor any informal relation among program variables. The subject must be the set of possible executions, and the condition must potentially distinguish two systems containing the same individual traces in different combinations.

It is also not every relational program proof: a relational proof qualifies only when it establishes a trace-set condition.

Scope of Application¶

Hyperproperties formalize information-flow confidentiality and integrity, observational determinism, noninterference, declassification policies, symmetry, robustness, quantitative leakage bounds, and some service-level or data-minimization conditions. HyperLTL adds explicit trace quantifiers to temporal logic for finite-state reasoning.^[2]

Verification cost rises sharply with quantifier alternation and number of traces. Some subclasses reduce to ordinary safety on a self-composed product; general hyperproperty verification need not.

Clarity¶

State the trace alphabet, system semantics, trace quantifiers, observation relation, alignment convention, and whether nondeterminism is demonic, angelic, or merely enumerated. Give the minimal counterexample shape. Calling noninterference a “property of outputs” hides the essential comparison across runs.

Manages Complexity¶

The abstraction unifies policies once treated as unrelated exceptions to trace logic. It tells a verifier why a single counterexample trace is insufficient, how many traces a violation needs, and which proof transformation may work. The semantic type itself becomes a routing rule from specification to tool.

Abstract Reasoning¶

Define the system's trace semantics.
Ask whether the desired verdict can be determined trace by trace.
If not, identify the required trace tuple or quantifier pattern.
Express the condition as membership of the complete trace set.
Classify it as hypersafety, hyperliveness, or a combination.
Determine whether it is k-safety.
Select self-composition, relational logic, or hyper-temporal model checking.
Produce counterexample trace sets rather than isolated traces.

Knowledge Transfer¶

The portable pattern is raise the object of evaluation from one behavior to a population of possible behaviors so cross-instance relations become expressible. It transfers to algorithmic fairness across individuals, differential privacy across adjacent datasets, robustness across perturbations, and relational program equivalence. The proposed immediate parent is Constraint.

Examples¶

Noninterference. For all pairs of traces with equal public inputs, public outputs must remain equal despite changes in secret inputs.

Observational determinism. All low-observable projections of executions agree, preventing nondeterminism from leaking secrets.

k-safety. Many two-run security policies become ordinary safety properties of a product program, while higher-arity algebraic properties may require more traces.^[3]

Structural Tensions¶

Expressive cross-run semantics versus verification complexity.
Whole-system trace sets versus finite counterexample witnesses.
Synchronous comparison versus asynchronous executions.
Universal security guarantees versus probabilistic or quantitative variants.
Semantic clarity versus tool-specific encodings.
Self-composition convenience versus state-space explosion.

Structural–Framed Character¶

Lifting a predicate's carrier, relation across instances, and finite witness arity are structural. Execution traces, program semantics, security policies, temporal logics, and model-checking algorithms are constitutive formal-methods machinery. The identity is domain-specific.

Structural Core vs. Domain Accent¶

The portable core is evaluate a set of behaviors as one object. The domain accent is computational trace semantics and verification of security or correctness across runs.

Constraint is the proposed immediate parent because a hyperproperty partitions trace-set systems into admissible and inadmissible ones. Relation, Quantifier, Verification, Non-Locality, and Local-to-Global Aggregation are related.

The prospective queue contains one strict edge to prime:constraint. No live DAG mutation is authorized.

Relationships to Other Abstractions¶

Current abstraction Hyperproperty Domain-specific

Parents (1) — more general patterns this builds on

Hyperproperty is a kind of Constraint Prime

Constraint is the proposed immediate parent because a hyperproperty partitions trace-set systems into admissible and inadmissible ones.

Hierarchy path (1) — routes to 1 parentless root

Hyperproperty → Constraint

Neighborhood in Abstraction Space¶

Hyperproperty sits in a sparse region of the domain-specific corpus (91^st percentile for distinctiveness): few abstractions share its structure, so a faithful description tends to retrieve it precisely.

Family — Unclustered & Miscellaneous (1565 abstractions)

Nearest neighbors

Model Checking — 0.79
Maximal set (computability theory) — 0.78
Computation Tree Logic — 0.78
Reduction (Computability Theory) — 0.78
Formal Verification — 0.77

Computed from structural-signature embeddings · 2026-09-08

Not to Be Confused With¶

Ordinary trace property.
Safety property on one execution.
Temporal logic formula lacking trace quantification.
Rice's theorem's semantic program property.
Universal property in category theory.
Hyperparameter in machine learning.

References¶

[1] Michael R. Clarkson and Fred B. Schneider, “Hyperproperties,” Journal of Computer Security 18, no. 6 (2010): 1157–1210, doi:10.3233/JCS-2009-0393, https://www.cs.cornell.edu/fbs/publications/1813-9480.pdf. registry ↩a ↩b

[2] Bernd Finkbeiner, Markus N. Rabe, and César Sánchez, “Algorithms for Model Checking HyperLTL and HyperCTL,” in *CAV 2015, LNCS 9206, pp. 30–48, doi:10.1007/978-3-319-21690-4_3. registry ↩

[3] Marcelo Sousa and Isil Dillig, “Cartesian Hoare Logic for Verifying k-Safety Properties,” Proceedings of PLDI 2016, pp. 57–69, doi:10.1145/2908080.2908092. registry ↩

[4] Thibault Dardinier and Peter Müller, “Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties,” Proceedings of the ACM on Programming Languages 8 (2024): 1485–1509, doi:10.1145/3656437. registry ↩