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₁,s₂ ∈ S. s₁ = s₂ → final(s₁) = final(s₂) "Same inputs give same outputs."

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.

Symbol	Unicode	Name	Meaning
⟨P⟩C⟨Q⟩	—	Hyper-triple	Hyper specification
S	—	State set	Multiple states
∀s₁,s₂	—	Trace quantification	Relating traces
low, high	—	Security levels	Classification
≈	U+2248	Equivalence	Same observable
⊆	U+2286	Subset	Trace sets

Metatheory. Hyper Hoare logic sound for hypertrace semantics. Relates to self-composition. Product construction. Complete for certain fragments. Decidability: undecidable in general. Connects to HyperLTL at temporal level.

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

Limitations. More complex than standard Hoare. Automation challenging. Product programs can explode. Quantitative hyperproperties harder. Tool support emerging. Requires hyperproperty specification.