Hyperproperties
This module formalises hyperproperties from the AVM green paper.
{-# OPTIONS --type-in-type --guardedness --exact-split --without-K #-} module Foundation.Hyperproperties where
Imports
open import Agda.Primitive using (Level; lsuc) open import Foundation.BasicTypes using (Pred; _⊆_; _↔_; ⊥; ¬; Σ; ℕ; _≤_; List; []; _∷_; _≡_; refl; _×_; suc; zero; ∃; ∃-syntax; FinSet; length; _∈_) renaming (_∈Pred_ to _∈ₚ_)
Finite Sets
Finite sets are modeled as lists for convenience (imported from BasicTypes).
size : {A : Set} → FinSet A → ℕ size = length
Traces and Systems
Infinite Traces
Infinite traces are coinductive streams of states.
record Stream {ℓ : Level} (A : Set ℓ) : Set ℓ where coinductive field head : A tail : Stream A
open Stream public
Finite and Infinite Traces
Finite traces are modeled as lists, infinite traces as streams, parameterized by a state space type.
TraceFin : {ℓ : Level} → Set ℓ → Set ℓ TraceFin Σᵀ = List Σᵀ TraceInf : {ℓ : Level} → Set ℓ → Set ℓ TraceInf Σᵀ = Stream Σᵀ
Systems
A system is a non-empty set of infinite traces, modeled as a predicate over infinite traces.
record System {ℓ : Level} (Σᵀ : Set ℓ) : Set (lsuc ℓ) where field Traces : Pred (TraceInf Σᵀ) nonEmpty : ∃ λ (t : TraceInf Σᵀ) → Traces t
open System
Trace Properties
Trace properties are predicates over infinite traces, representing sets of infinite traces.
TraceProp : {ℓ : Level} → Set ℓ → Set (lsuc ℓ) TraceProp Σᵀ = Pred (TraceInf Σᵀ)
Satisfaction for Trace Properties
System S satisfies trace property P if all traces in S belong to P. This
corresponds to the subset relation S ⊆ P in the paper.
_⊨_ : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → TraceProp Σᵀ ---------------------------- → Set (lsuc ℓ) S ⊨ P = Traces S ⊆ P
Hyperproperties
Hyperproperties are predicates over trace properties, representing sets of trace properties.
HyperProp : {ℓ : Level} → Set ℓ → Set (lsuc (lsuc ℓ)) HyperProp Σᵀ = Pred (TraceProp Σᵀ)
System as Trace Property
To check if a system satisfies a hyperproperty, we view the system as a trace property by taking its trace set.
SysAsProp : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → TraceProp Σᵀ SysAsProp S = Traces S
Satisfaction for Hyperproperties
System S satisfies hyperproperty H if the trace property corresponding to
S belongs to H.
_⊨ᴴ_ : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → HyperProp Σᵀ → Set (lsuc (lsuc ℓ)) S ⊨ᴴ H = SysAsProp S ∈ₚ H
Lifting Trace Properties
Every trace property P can be lifted to a hyperproperty [P] that contains
exactly those trace properties that are subsets of P.
[_] : {ℓ : Level} {Σᵀ : Set ℓ} → TraceProp Σᵀ → HyperProp Σᵀ [ P ] T = (T ⊆ P)
Prefixes and Observations
Prefix Relation
The prefix relation l ⊑ t expresses that finite trace l is a prefix of
infinite trace t.
data _⊑_ {ℓ : Level} {Σᵀ : Set ℓ} : TraceFin Σᵀ → TraceInf Σᵀ → Set ℓ where []-⊑ : ∀ {t} → [] ⊑ t _∷_-⊑ : ∀ {x xs t} → head t ≡ x → xs ⊑ tail t → (x ∷ xs) ⊑ t
Observations
Observation sets are finite sets of finite traces, representing finite observations of system behavior.
Obs : {ℓ : Level} → Set ℓ → Set (lsuc ℓ) Obs Σᵀ = FinSet (TraceFin Σᵀ)
Observation Satisfiability
Observation set M is satisfied by trace property T (written M ≤ T) if
every finite trace in M is a prefix of some infinite trace in T.
_≤ᴼ_ : {ℓ : Level} {Σᵀ : Set ℓ} → Obs Σᵀ → TraceProp Σᵀ → Set (lsuc ℓ) _≤ᴼ_ {ℓ} {Σᵀ} M T = ∀ {m} → m ∈ M → ∃ λ (t : TraceInf Σᵀ) → (t ∈ₚ T) × (m ⊑ t)
Hypersafety and Hyperliveness
Hypersafety
A hyperproperty is a hypersafety property if every trace property that violates it admits finite irremediable evidence: an observation set that witnesses the violation and ensures no extension can satisfy the property.
Hypersafety : {ℓ : Level} {Σᵀ : Set ℓ} → HyperProp Σᵀ → Set (lsuc (lsuc ℓ)) Hypersafety {ℓ} {Σᵀ} Sᴴ = ∀ (T : TraceProp Σᵀ) → (¬ (T ∈ₚ Sᴴ)) → ∃ λ (M : Obs Σᵀ) → (M ≤ᴼ T) × (∀ (T' : TraceProp Σᵀ) → (M ≤ᴼ T') → ¬ (T' ∈ₚ Sᴴ))
k-Safety
A hyperproperty is k-safety if every violation admits finite irremediable evidence of size at most k.
kSafety : {ℓ : Level} {Σᵀ : Set ℓ} → (k : ℕ) → HyperProp Σᵀ → Set (lsuc (lsuc ℓ)) kSafety {ℓ} {Σᵀ} k Sᴴ = ∀ (T : TraceProp Σᵀ) → (¬ (T ∈ₚ Sᴴ)) → ∃ λ (M : Obs Σᵀ) → (M ≤ᴼ T) × (size M ≤ k) × (∀ (T' : TraceProp Σᵀ) → (M ≤ᴼ T') → ¬ (T' ∈ₚ Sᴴ))
1-Safety and Safety Properties
1-safety hyperproperties correspond exactly to lifted safety properties. This establishes that traditional safety properties are a special case of k-safety.
postulate SafetyTraceProp : {ℓ : Level} {Σᵀ : Set ℓ} → TraceProp Σᵀ → Set KSH₁⇔LiftSafety : {ℓ : Level} {Σᵀ : Set ℓ} {P : TraceProp Σᵀ} → (kSafety 1 [ P ]) ↔ (SafetyTraceProp P)
Self-Composition
Self-composition constructs the product of systems, modeling traces over product state spaces. This is essential for proving k-safety properties with k > 1.
Product of two systems:
record Sys× {ℓ : Level} {Σᵀ : Set ℓ} (S₁ S₂ : System Σᵀ) : Set (lsuc ℓ) where field Traces× : Pred (Stream (Σᵀ × Σᵀ))
Examples
Observational Determinism
Observational determinism is a 2-safety hyperproperty relating pairs of traces that agree on low observations.
postulate OD : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → Set
Classification of observational determinism as 2-safety:
postulate OD-is-2Safety : {ℓ : Level} {Σᵀ : Set ℓ} → kSafety {ℓ} {Σᵀ} 2 (λ T → ∃ λ (S : System Σᵀ) → (Traces S ⊆ T) × OD S)
Generalized Noninterference
Generalized noninterference is a hyperliveness hyperproperty, meaning it cannot be characterized by finite bad prefixes.
postulate GNI : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → Set GNI-is-Hyperliveness : {ℓ : Level} {Σᵀ : Set ℓ} → ¬ (Hypersafety {ℓ} {Σᵀ} (λ T → ∃ λ (S : System Σᵀ) → (Traces S ⊆ T) × GNI S))
Refinement via Interpretation Functions
Interpretation functions α : Ψ → Ψ map traces to traces, modeling abstraction
and refinement.
postulate α : {ℓ : Level} {Σᵀ : Set ℓ} → TraceInf Σᵀ → TraceInf Σᵀ
Lifting α to trace properties:
α⋆ : {ℓ : Level} {Σᵀ : Set ℓ} → TraceProp Σᵀ → TraceProp Σᵀ α⋆ P = λ t → P (α t)
α-satisfaction relates systems to trace properties via interpretation:
_⊨α_ : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → TraceProp Σᵀ → Set (lsuc ℓ) S ⊨α P = (α⋆ (Traces S)) ⊆ P
Note that subset inclusion of trace properties does not imply refinement for hyperproperties, as demonstrated by the π versus π′ example in the paper.