HypreSpectre.Prefix_sens

Prefix Relation for Termination-Sensitive Leakage Equivalence

From HypreSpectre Require Import
  Lang
  Mitigation
  Leak.

From HyPre Require Import
  HyperPreserve
  HyperPreserveBarrier
  NonInterference.

This definition captures the requirements for trace prefixes to satisfy Termination-Sensitive leakage equivalence. The two trace prefixes must produce leakages such that one is a prefix of the other, and it must be possible to extend the prefixes until they produce the same leakage.

Definition ll_pre_sens {State LL P I: Type} (leakS: State -> list LL) (sem: P -> I -> list State -> Prop) p_src (i: Vector.t I 2) (sl1 sl2: list State) := ll_pre leakS sl1 sl2 /\ exists b1 b2 , (ll_eq leakS (b1 ++ sl1) (b2 ++ sl2) /\ sem p_src (i [[Fin.F1 ]]) (b1 ++ sl1) /\ sem p_src (i [[Fin.FS Fin.F1 ]]) (b2 ++ sl2)).

This relation is a safety hyperproperty.

Lemma vl_ll_pre_sens_safety
(iv : Vector.t heap 2)
(p_tgt : list stmt)
(leakS : list specstate -> list observation):
veclist_safety
  (v2
     (ll_pre_sens leakS spec_am_trace p_tgt iv)).
Proof.
  unfold veclist_safety. unfold Safety.safety_property.
  clear.
  intros.
  unfold veclist_prefix in H.
  unfold v2, ll_pre_sens, ll_pre in *.
  split.
  + pose proof (vl_ll_pre_safety leakS).
    unfold veclist_safety, Safety.safety_property in H1.
    specialize (H1 _ _ H).
    destruct H0 as [H0 _].
    specialize (H1 H0). exact H1.
  + destruct H0 as [_ H0].
    destruct H0 as (b1 & b2 & Heq & Hb1 & Hb2).
    rewrite Vec_Forall2_forall2 in H.
    pose proof (H (Fin.F1)).
    pose proof (H (Fin.FS Fin.F1)).
    apply prefix_eq in H0 as [h1 H0].
    apply prefix_eq in H1 as [h2 H1].
    exists (b1 ++ h1). exists (b2 ++ h2).
    rewrite <-! app_assoc.
    rewrite <- H0, <- H1. easy.
Qed.

Equal leakage implies this relation.

Lemma vl_ll_eq_ll_pre_sens
(iv : Vector.t heap 2)
(p_tgt: list stmt)
(leakS : list specstate -> list observation):
forall α0 : Vector.t (list (list specstate)) 2,
Vector.Forall2 (spec_am_trace p_tgt) iv α0 ->
v2 (ll_eq leakS) α0 ->
v2 (ll_pre_sens leakS spec_am_trace p_tgt iv)
  α0.
Proof.
  unfold v2. intros.
  unfold ll_pre_sens.
  split.
  + exact (vl_ll_eq_ll_pre leakS α0 H0).
  + exists nil, nil. simpl.
    split. easy.
    rewrite Vec_Forall2_forall2 in H. easy.
Qed.