HypreSpectre.SLH

Counterexample for Speculative Load Hardening in Loops+Memory Model

From HyPre Require Import
  NonInterference.

From HypreSpectre Require Import Lang Leak.
From Coq Require Import Program.Basics Program.Equality.
From Equations Require Import Equations.

Modeling Speculative Load Hardening

We use a special variable "__spec", which we assume is not used in the program. This is okay, as we know that our counterexample does not use it.
Definition pathcond := Not (Var "__spec"%string).
Definition update_pathcond e := Assign ("__spec"%string) (Plus (Var "__spec"%string) (Not e)).

Equations? speculative_load_hardening sl : list stmt by wf (stmt_depth_list sl) :=
speculative_load_hardening nil := nil;
speculative_load_hardening ((Assign x e) :: l) := Assign x (e) :: (speculative_load_hardening l);
speculative_load_hardening ((Read x e) :: l) := Read x (Mult pathcond e) :: (speculative_load_hardening l);
speculative_load_hardening ((Write x e) :: l) := Write x (Mult pathcond e) :: (speculative_load_hardening l);
speculative_load_hardening ((If i t e) :: l) := If i (update_pathcond i :: (speculative_load_hardening t)) (update_pathcond (Not i) :: (speculative_load_hardening e)) :: (speculative_load_hardening l);
speculative_load_hardening ((While e s1 s2) :: l) := While e (update_pathcond e :: (speculative_load_hardening s1)) (update_pathcond (Not e) :: (speculative_load_hardening s2)) :: (speculative_load_hardening l);
speculative_load_hardening ((Skip) :: l) := Skip :: (speculative_load_hardening l);
speculative_load_hardening ((Fence) :: l) := Fence :: (speculative_load_hardening l).
Proof.
  all: replace ((fix aux (sl : list stmt) : nat :=
                   match sl with
                   | nil => 0
                   | x :: xs => S (stmt_depth x + aux xs)
                   end)) with (stmt_depth_list).
  2, 4, 6, 8, 10, 12: reflexivity.
  all: lia.
Qed.

Open Scope program_scope.

Sample Program

The program performs the same memory access in both branches, but once within and once outside of the speculation window.
Definition p := (Read "x"%string (Lit (-1)%Z)) :: (If (Var "x"%string) (Read "y"%string (Lit 1%Z) :: Skip :: Skip :: Skip :: nil) (Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Skip :: Read "y"%string (Lit 1%Z) :: nil)) :: nil.

Input Heaps

The heaps only differ in a secret value at address -1.
Definition i0 : heap := alist_add decZ (-1)%Z 0%Z nil.
Definition i1 : heap := alist_add decZ (-1)%Z 1%Z nil.
Definition iv := Vector.cons _ i0 1 (Vector.cons _ i1 0 (Vector.nil _)).
Definition t0 := multi_step spec_step_fun ((None, nil, i0, (speculative_load_hardening p)) :: nil) 26.
Definition t1 := multi_step spec_step_fun ((None, nil, i1, (speculative_load_hardening p)) :: nil) 24.
Definition tv := Vector.cons _ t0 1 (Vector.cons _ t1 0 (Vector.nil _)).

Lemma compute_t0 : apply_lf' (rem_None ∘ leak_lm') t0 = Termination :: ReadAddress 1 :: ReadAddress 0 :: ReadAddress (-1) :: nil.
Proof.
  unfold t0, p. simp speculative_load_hardening.
  cbn.
  reflexivity.
Qed.

Lemma compute_t1 : apply_lf' (rem_None ∘ leak_lm') t1 = Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil.
Proof.
  unfold t1, p. simp speculative_load_hardening.
  cbn.
  reflexivity.
Qed.

Lemma compute_s0: apply_lf' (rem_None ∘ leak_lm) (multi_nonspec (nil, i0, p) 20) = Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil.
Proof. reflexivity. Qed.
Lemma compute_s0': apply_lf' (rem_None ∘ leak_lm) (multi_step nonspec_step_fun (nil, i0, p) 19) = Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil.
Proof. reflexivity. Qed.
Lemma prefix_s0 n: n < 21 -> PreSuffix.prefix (apply_lf' (rem_None ∘ leak_lm) (multi_nonspec (nil, i0, p) n)) (Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil).
Proof.
  intros.
  do 21 try destruct n.
  22: lia.
  all: cbn.
  all: repeat econstructor.
Qed.
Lemma compute_s1: apply_lf' (rem_None ∘ leak_lm) (multi_nonspec (nil, i1, p) 7) = Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil.
Proof. reflexivity. Qed.
Lemma compute_s1': apply_lf' (rem_None ∘ leak_lm) (multi_step nonspec_step_fun (nil, i1, p) 6) = Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil.
Proof. reflexivity. Qed.
Lemma prefix_s1 n: n < 8 -> PreSuffix.prefix (apply_lf' (rem_None ∘ leak_lm) (multi_nonspec (nil, i1, p) n)) (Termination :: ReadAddress 1 :: ReadAddress (-1) :: nil).
Proof.
  intros.
  do 8 try destruct n.
  9: lia.
  all: cbn.
  all: repeat econstructor.
Qed.

Lemma prefix_app_help {T} (a b c : list T):
  PreSuffix.prefix a b -> PreSuffix.prefix (a ++ c) (b ++ c).
Proof.
  induction 1.
  - constructor.
  - now apply PreStep.
Qed.

Lemma stut_term_0 n:
  (apply_lf' (rem_None ∘ leak_lm)
     (multi_step nonspec_step_fun
        (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 0%Z nil), i0, nil) n)) = Nat.iter n (fun a => Termination :: a) (Termination :: nil).
Proof.
  enough ((apply_lf' (rem_None ∘ leak_lm)
     (multi_step nonspec_step_fun
        (alist_add RelDec_string "y"%string 0%Z
     (alist_add RelDec_string "x"%string 0%Z nil), i0, nil) n)) = Nat.iter n (fun a => Termination :: a) (Termination :: nil) /\ multi_step_hd nonspec_step_fun
        (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 0%Z nil), i0, nil) n = (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 0%Z nil), i0, nil)). easy.
  induction n.
  - cbn. split; reflexivity.
  - split.
    + rewrite multi_step_S2.
      rewrite apply_lf'_S.
      destruct IHn as [IHn1 IHn2].
      rewrite IHn1, IHn2.
      cbn. reflexivity.
    + unfold multi_step_hd.
      rewrite multi_step_S2.
      destruct IHn as [IHn1 IHn2].
      rewrite IHn2. cbn. reflexivity.
Qed.
Lemma stut_term_1 n:
  (apply_lf' (rem_None ∘ leak_lm)
     (multi_step nonspec_step_fun
        (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 1%Z nil), i1, nil) n)) = Nat.iter n (fun a => Termination :: a) (Termination :: nil).
Proof.
  enough ((apply_lf' (rem_None ∘ leak_lm)
     (multi_step nonspec_step_fun
        (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 1%Z nil), i1, nil) n)) = Nat.iter n (fun a => Termination :: a) (Termination :: nil) /\ multi_step_hd nonspec_step_fun
        (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 1%Z nil), i1, nil) n = (alist_add RelDec_string "y"%string 0%Z
           (alist_add RelDec_string "x"%string 1%Z nil), i1, nil)). easy.
  induction n.
  - cbn. split; reflexivity.
  - split.
    + rewrite multi_step_S2.
      rewrite apply_lf'_S.
      destruct IHn as [IHn1 IHn2].
      rewrite IHn1, IHn2.
      cbn. reflexivity.
    + unfold multi_step_hd.
      rewrite multi_step_S2.
      destruct IHn as [IHn1 IHn2].
      rewrite IHn2. cbn. reflexivity.
Qed.

Lemma iter_term_prefix n1 n2:
  n1 <= n2 ->
  PreSuffix.prefix
  (Nat.iter n1 (fun a : list observation => Termination :: a)
     (Termination :: nil))
  (Nat.iter n2 (fun a : list observation => Termination :: a)
     (Termination :: nil)).
Proof.
  intros.
  assert (n1 < n2 \/ n1 = n2) as [H1 | H1] by lia.
  - clear H.
    induction n2.
    + lia.
    + assert (n1 < n2 \/ n1 = n2) as [H | H] by lia.
      * simpl. apply PreStep. auto.
      * simpl. apply PreStep. rewrite H. constructor.
  - rewrite H1. constructor.
Qed.

Source Traces are Leakage Equivalent

Lemma Hsrc_safe:
 (forall a, Vector.Forall2 (nonspec_trace p) iv a -> v2 (ll_pre (rem_None ∘ leak_lm)) a).
Proof.
  intros.
  repeat dependent destruction a.
  rewrite Vec_Forall2_forall2 in H.
  specialize (H (Fin.FS Fin.F1)) as H0.
  specialize (H Fin.F1).
  simpl in H, H0.
  unfold v2, ll_pre.
  unfold nonspec_trace in *.
  simpl.
  destruct (Nat.lt_ge_cases (| h |) 21), (Nat.lt_ge_cases (| h0 |) 8).
  - apply prefix_s0 in H1. apply prefix_s1 in H2.
    eapply prefix_order_destruct;
    fold value in *; fold heap in *; rewrite H in H1; rewrite H0 in H2; eauto.
  - assert (exists n, | h0 | = n + 8) as [n Hn]. exists (| h0 | - 8). lia.
    rewrite Hn in *.
    unfold multi_nonspec, multi_step' in H0.
    rewrite Nat.add_succ_r in H0.
    rewrite <- Nat.add_succ_comm in H0.
    rewrite multi_step_app in H0.
    left.
    rewrite <- H0.
    rewrite apply_lf'_app.
    apply prefix_app_r.
    rewrite compute_s1'.
    rewrite <- H.
    now apply prefix_s0.
  - assert (exists n, | h | = n + 21) as [n Hn]. exists (| h | - 21). lia.
    rewrite Hn in *.
    unfold multi_nonspec, multi_step' in H.
    rewrite Nat.add_succ_r in H.
    rewrite <- Nat.add_succ_comm in H.
    rewrite multi_step_app in H.
    right.
    rewrite <- H.
    rewrite apply_lf'_app.
    apply prefix_app_r.
    rewrite compute_s0'.
    rewrite <- H0.
    now apply prefix_s1.
  - assert (exists n, | h | = n + 21) as [n Hn]. exists (| h | - 21); lia.
    assert (exists n0, | h0 | = n0 + 8) as [n0 Hn0]. exists (| h0 | - 8); lia.
    rewrite Hn, Hn0 in *.
    rewrite Nat.add_succ_r in H, H0.
    unfold multi_nonspec, multi_step' in *.
    rewrite <- Nat.add_succ_comm in H, H0.
    rewrite multi_step_app in H, H0.
    rewrite <- H, <- H0.
    rewrite! apply_lf'_app.
    rewrite compute_s1', compute_s0'.
    rewrite stut_term_0, stut_term_1.
    destruct (Nat.lt_ge_cases n n0).
    + left. apply prefix_app_help. apply iter_term_prefix. lia.
    + right. apply prefix_app_help. apply iter_term_prefix. assumption.
Qed.

Target Traces are not Leakage Equivalent

Theorem SLH_not_preserve_lm:
  ~ (
  forall (iv: Vector.t heap 2),
  forall (p_src: list stmt),
  (forall a, Vector.Forall2 (nonspec_trace p_src) iv a -> v2 (ll_pre (rem_None ∘ leak_lm)) a) ->
  (forall α, Vector.Forall2 (spec_am_trace (speculative_load_hardening p_src)) iv α -> v2 (ll_pre (rem_None ∘ leak_lm')) α)
  ).
Proof.
  intros H.
  specialize (H iv p).
  specialize (H Hsrc_safe tv).
  assert (Vector.Forall2 (spec_am_trace (speculative_load_hardening p)) iv tv).
  { rewrite Vec_Forall2_forall2.
    intros i. repeat dependent induction i; simpl.
    + unfold spec_am_trace, multi_spec_am, multi_step', t0. rewrite multi_step_len. reflexivity.
    + unfold spec_am_trace, multi_spec_am, multi_step', t1. rewrite multi_step_len. reflexivity.
  }
  specialize (H H0). clear H0.
  unfold v2, ll_pre in H.
  unfold tv in H. simpl in H. rewrite compute_t0, compute_t1 in H.
  destruct H.
    + inversion H; subst. inversion H2; subst. inversion H3; subst. inversion H4.
    + inversion H; subst. inversion H2; subst. inversion H2; subst. inversion H4; subst. inversion H5; subst. inversion H6.
Qed.

The proof relies on the following assumtions:
Print Assumptions SLH_not_preserve_lm.

functional_extensionality_dep
  : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
    (forall x : A, f x = g x) -> f = g
Eqdep.Eq_rect_eq.eq_rect_eq
  : forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
    x = eq_rect p Q x p h