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: v4 · 2026-09-19 · History
Domain-specific #: 2032
Domain group: Applied Sciences & Engineering
Origin domain: Computer Science & Software Engineering
Subdomain: Formal Verification → Computer Science & Software Engineering
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]

How would you explain it like I'm…

Compare-the-Runs Rules

Some rules can be checked by watching a computer do its job just once. Other rules can only be checked by comparing different times it did its job. For example, 'keep my secret' means that if only the secret changes, what everyone else sees must stay exactly the same. A hyperproperty is a rule like that, about all the runs together.

Rules About All Runs

When a program runs, it leaves a trace: a record of everything that happened. A normal rule, called a trace property, looks at one trace and says yes or no. Some rules can't be judged from one trace, though. For example, "secret inputs must not change what the public sees" needs you to compare runs that differ only in the secret. A hyperproperty is a rule about the whole collection of possible runs, so it can compare runs against each other.

Properties of Trace Sets

A trace is a record of one execution of a system, and the system itself can be described as the set of all traces it can produce. An ordinary trace property is a set of traces: each individual trace either satisfies it or doesn't. A hyperproperty goes one level up: it is a set of systems, meaning a set of sets of traces, and a system satisfies it if its whole trace set belongs to that set. This lets a specification compare different executions. Noninterference is the classic example: runs that differ only in secret inputs must give the same public outputs, which no check of a single trace can confirm. Just as trace properties split into safety and liveness, hyperproperties split into hypersafety and hyperliveness.

Let Φ be the universe of execution traces. A trace property P ⊆ Φ classifies individual traces. A system is its set of possible traces S ⊆ Φ. A hyperproperty is H ⊆ 𝒫(Φ), and S satisfies H exactly when S ∈ H. Lifting from sets of traces to sets of sets allows specifications that relate alternative executions. Noninterference is the standard example: any two runs that agree on public inputs and differ only in secret inputs must give identical public observations. That condition cannot be decided trace by trace. The classical safety/liveness framework carries over: every hyperproperty is the intersection of a hypersafety and a hyperliveness hyperproperty. A k-safety hyperproperty is one where every violation is witnessed by at most k finite traces.

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.

This entry is a kind of Constraint.

Constraint is the broader abstraction this entry instantiates because a hyperproperty partitions trace-set systems into admissible and inadmissible ones. Relation, Quantifier, Verification, Non-Locality, and Local-to-Global Aggregation are related.

Relationships to Other Abstractions¶

Current abstraction Hyperproperty Domain-specific

Parents (1) — outgoing typed relations

Hyperproperty is a kind of Constraint Prime

Constraint is the broader abstraction this entry instantiates because a hyperproperty partitions trace-set systems into admissible and inadmissible ones.

Hierarchy path (1) — routes to 1 parentless root

Hyperproperty → is a kind of Constraint

Neighborhood in Abstraction Space¶

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

Family — Unclustered & Miscellaneous (2769 abstractions)

Nearest neighbors

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

Computed from structural-signature embeddings · 2026-10-25

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 Show verification details

[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 ↩ Show verification details

[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 ↩ Show verification details

[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 ↩ Show verification details