Hyperproperties for Privacy, Fairness, and Legal Requirements

Properties and hyperproperties

A trace records one possible execution of a system. A trace property specifies which individual traces are allowed. For example, a safety property can require that no execution enters an unsafe state.

A hyperproperty specifies which sets of traces are allowed. If two systems each produce individually acceptable executions but reveal different information when their executions are compared, a trace property may miss the distinction.

Trace property: P ⊆ Σ^ω
Hyperproperty: H ⊆ 𝒫(Σ^ω)

Here Σ is an alphabet of observations, Σ^ω is the set of infinite traces, and 𝒫 denotes the power set. A system satisfies P when all its traces belong to P; it satisfies H when its set of traces belongs to H.

Privacy as noninterference

In the deterministic setting used here, let O(s, p) be the observable output for secret input s and public input p. Noninterference requires:

For every s₁, s₂, and p: O(s₁, p) = O(s₂, p).

The secret may affect internal computation. It must not affect the chosen observation. That choice matters: an output-only model says nothing about timing unless timing is included in the observations.

Opacity: another explanation for what we observe

The talk’s cyber-physical example combines a recurring mission—visiting Parking and Quay infinitely often—with an information-flow objective: the observer must not infer that the vehicle started in a secret location.

Initial-state opacity asks for an alternative explanation. For every execution starting in a secret state, there must be an execution starting in a nonsecret state with the same observations. This is a for every … there exists … requirement.

Certificates for relationships between executions

Testing examples is useful, but a proof must cover the behaviors required by the specification. For dynamical systems, the talk develops this through functional certificates.

Barrier certificates

A barrier certificate B separates initial states from unsafe states and is preserved by the dynamics. For a deterministic discrete-time system x′ = f(x), sufficient conditions are:

• B(x) ≤ 0 for initial states.
• B(x) > 0 for unsafe states.
• B(f(x)) ≤ B(x) for safe states.

Augmented barrier certificates

For a relational requirement, reason about pairs of states (x, y) in a self-composition of the system. A certificate over that product space can keep paired executions inside a region with matching observations.

For an opacity-style requirement, an existential player tries to match the universally chosen execution. A suitable certificate establishes that the matching player can respond while preserving the relation.

Closure certificates

Closure certificates describe relationships between states connected by transitions, rather than just a region of individual states. Inductive transition invariants include one-step transitions and extend along paths. Additional decrease conditions can establish properties such as finitely many visits to a designated set.

The talk explores how transition-based reasoning may help with the lookahead needed for hyperproperties. Its questions about arbitrary and infinite lookahead are research directions, not a claim of a general complete verification procedure.

Read the papers: Verification of Hyperproperties for Dynamical Systems via Barrier Certificates · Closure Certificates.

Fairness depends on the relation we specify

The talk introduces a requirement that otherwise identical individuals receive the same outcome when only a protected feature changes. This is one precise comparison to test; it is not a complete definition of fairness.

A test can expose a counterexample to the chosen relation. Agreement on one pair cannot establish that a model is fair. Even agreement on all these toy inputs says nothing about omitted features or an unsuitable definition of similarity.

The talk also considers similarity-based individual fairness, causal formulations, and group criteria such as statistical parity and equal opportunity. Removing a protected attribute does not necessarily remove its influence through correlated features. Choosing the relation is part of the specification problem.

Related work: Fairness Testing through Extreme Value Theory · Uncovering Discrimination Clusters.

Testing without a complete output oracle

For complex software, we may not know the correct output for every input. Metamorphic testing instead checks a relation between related inputs and outputs. A simple mathematical example from the talk is sin(x) = sin(π − x).

For legal-critical software, the challenge is to derive justified relations from requirements and identify the assumptions under which they apply. The talk uses age-related benefits in tax preparation as an example of this reasoning.

A violation identifies a failure of the relation, even without an oracle for every output. Passing does not establish complete correctness: an implementation that always returns zero would satisfy this monotonicity check while violating the stated benefit amounts.

Read Metamorphic Testing and Debugging of Tax Preparation Software for the actual software-testing study.

What a relational specification makes explicit

Each example requires a choice: what is observable, which inputs are comparable, and which outcomes should agree or be ordered. Once those choices are explicit, testing can search for counterexamples and verification can establish guarantees under stated assumptions.

The difficult questions remain mathematical and contextual: which relation captures the intended requirement, and which proof or testing method can handle the system’s behaviors?

Original talk slides · All publications · Research themes