Hyper Hoare Logic

Origin. Dardinier, Müller, and colleagues developed hyper Hoare logic (2020s). Reasons about hyperproperties: properties of sets of traces. Standard Hoare: single execution. Hyper: relationships between executions. Non-interference, observational determinism.

Models. Properties of trace sets. Trace property: set of allowed traces. Hyperproperty: set of allowed trace sets. Non-interference: high inputs don't affect low outputs — relates traces with different inputs. Hyperlogics reason about trace relationships.

Formalism.

Hyperproperties: Standard: P ⊆ Traces (which traces allowed). Hyper: H ⊆ P(Traces) (which trace sets allowed).

Hyper-triple: ⟨P⟩ C ⟨Q⟩ P, Q: predicates over sets of states (not single states).

Semantics: Valid if: for all sets of initial states S satisfying P, the set of final states (running C from each s ∈ S) satisfies Q.

Example — determinism: ∀(s, t₁), (s, t₂) ∈ final(S). t₁ = t₂ "One initial state never yields two different final states." The quantification has to be over outcomes. Writing it over inputs — ∀s₁, s₂ ∈ S. s₁ = s₂ → final(s₁) = final(s₂) — says nothing at all, since equal inputs are the same input; the content of determinism lives entirely on the output side of a possibly nondeterministic program.

Example — non-interference: ∀s₁,s₂ ∈ S. low(s₁) = low(s₂) → low(final(s₁)) = low(final(s₂)) "Low inputs determine low outputs (regardless of high)."

Rules: Sequential composition: ⟨P⟩ C₁ ⟨R⟩ ⟨R⟩ C₂ ⟨Q⟩ ──────────────────────────── ⟨P⟩ C₁;C₂ ⟨Q⟩

Relational reasoning: relate variables across executions.

Self-composition: C; C' verifies 2-safety by sequential analysis. Product programs for verification.

Symbols.

Metatheory. The framing result is Clarkson and Schneider's (2010): a hyperproperty is a set of sets of traces, not a set of traces, so no method that checks each execution in isolation can decide one; they also showed every hyperproperty is the intersection of a hypersafety and a hyperliveness property, generalizing the Alpern–Schneider decomposition. Hyper Hoare logic (Dardinier and Müller, 2024) takes the assertions to be predicates on the set of states, so the hyper-triple ⟨P⟩ C ⟨Q⟩ quantifies over an arbitrary set of initial states and its image under C; this is what lets a single system express both hypersafety, such as noninterference, and hyperliveness, and the system is proved sound and complete for hyperproperties of the terminating executions, and capable of disproving as well as proving them. The classical reduction for k-safety is self-composition (Barthe, D'Argenio, and Rezk 2004; Terauchi and Aiken 2005): verifying C against a 2-safety property becomes ordinary safety verification of C composed with a renamed copy, refined into product programs by Barthe, Crespo, and Kunz. At the temporal level the corresponding logic is HyperLTL, whose model-checking problem over finite-state systems is decidable but non-elementary in the number of quantifier alternations (Finkbeiner, Rabe, and Sánchez 2015), and whose satisfiability problem is undecidable.

Applies to. Information flow security. Non-interference. Determinism verification. Cryptographic constant-time. Observational equivalence. Differential privacy. Secure multi-execution.

Limitations. The hyper-triple relates a set of initial states to the set of final states, so what it captures are hyperproperties of terminating executions; timing-sensitive noninterference, observational determinism over infinite runs, and any property of intermediate states require a trace-based rather than a state-set semantics. Self-composition and product programs, the standard route to automation, reduce k-safety to safety at the cost of a k-fold copy of the program, and the reduction does not extend to hyperliveness — "some execution eventually leaks" is not a safety property of any composed program. Hyperproperties are not preserved under refinement: reducing nondeterminism can turn a secure specification into an insecure implementation, so the ordinary correctness-preserving development chain is unsound here. Verification is undecidable in general, and even over finite state the temporal counterpart is non-elementary in quantifier alternation with undecidable satisfiability. Quantitative notions such as differential privacy and quantitative information flow are measures on the execution set rather than Boolean predicates on it, and fall outside the assertion language.

© 2026 Lingenic LLC