---
title: Hyperproperties
tags:
  - hyperproperties
  - access control
  - information flow
---

This module formalises hyperproperties from the AVM green paper.

```agda
{-# OPTIONS --type-in-type --guardedness --exact-split --without-K #-}

module Foundation.Hyperproperties where
```

## Imports

```agda
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).

```agda
size : {A : Set} → FinSet A → ℕ
size = length
```

## Traces and Systems

### Infinite Traces

Infinite traces are coinductive streams of states.

```agda
record Stream {ℓ : Level} (A : Set ℓ) : Set ℓ where
  coinductive
  field
    head : A
    tail : Stream A
```

```agda
open Stream public
```

### Finite and Infinite Traces

Finite traces are modeled as lists, infinite traces as streams, parameterized by
a state space type.

```agda
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.

```agda
record System {ℓ : Level} (Σᵀ : Set ℓ) : Set (lsuc ℓ) where
  field
    Traces   : Pred (TraceInf Σᵀ)
    nonEmpty : ∃ λ (t : TraceInf Σᵀ) → Traces t
```

```agda
open System
```

## Trace Properties

Trace properties are predicates over infinite traces, representing sets of
infinite traces.

```agda
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.

```agda
_⊨_ : {ℓ : Level} {Σᵀ : Set ℓ} 
  → System Σᵀ 
  → TraceProp Σᵀ 
  ----------------------------
  → Set (lsuc ℓ)
S ⊨ P = Traces S ⊆ P
```

## Hyperproperties

Hyperproperties are predicates over trace properties, representing sets of trace
properties.

```agda
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.

```agda
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`.

```agda
_⊨ᴴ_ : {ℓ : 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`.

```agda
[_] : {ℓ : 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`.

```agda
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.

```agda
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`.

```agda
_≤ᴼ_ : {ℓ : 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.

```agda
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.

```agda
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.

```agda
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:

```agda
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.

```agda
postulate
  OD : {ℓ : Level} {Σᵀ : Set ℓ} → System Σᵀ → Set
```

Classification of observational determinism as 2-safety:

```agda
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.

```agda
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.

```agda
postulate
  α : {ℓ : Level} {Σᵀ : Set ℓ} → TraceInf Σᵀ → TraceInf Σᵀ
```

Lifting `α` to trace properties:

```agda
α⋆ : {ℓ : Level} {Σᵀ : Set ℓ} → TraceProp Σᵀ → TraceProp Σᵀ
α⋆ P = λ t → P (α t)
```

α-satisfaction relates systems to trace properties via interpretation:

```agda
_⊨α_ : {ℓ : 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.
