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\). 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.

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.

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.

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

1. Define the system's trace semantics.
2. Ask whether the desired verdict can be determined trace by trace.
3. If not, identify the required trace tuple or quantifier pattern.
4. Express the condition as membership of the complete trace set.
5. Classify it as hypersafety, hyperliveness, or a combination.
6. Determine whether it is k-safety.
7. Select self-composition, relational logic, or hyper-temporal model checking.
8. 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.

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