SpecCTSpeculative Constant-Time

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From Coq Require Import Strings.String.
From SECF Require Import Maps.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Arith.EqNat.
From Coq Require Import Arith.PeanoNat. Import Nat.
From Coq Require Import Lia.
From Coq Require Import List. Import ListNotations.
Set Default Goal Selector "!".

This chapter starts by presenting the cryptographic constant-time (CCT) discipline, which we statically enforce using a simple type system. This static discipline is, however, not enough to protect cryptographic programs against speculative execution attacks. To secure CCT programs against this more powerful attacker model we additionally use a program transformation called Speculative Load Hardening (SLH). We prove formally that CCT programs protected by SLH achieve speculative constant-time security.

Cryptographic constant-time

Cryptographic constant-time (CCT) is a software countermeasure against timing side-channel attacks that is widely deployed for cryptographic implementations, for instance to prevent leakage of crypto keys.

More generally, each program input has to be identified as public or secret, and intuitively the execution time of the program should not depend on secret inputs, even on processors with instruction and data caches.

We, however, do not want to explicitly model execution time or caches,

since that would be very hard to do right and
that would bring in too many extremely low-level details of the concrete compiler (Clang/LLVM 20.1.6) and hardware microarchitecture (Intel Core i₇-8650U).

Instead CCT works with a more abstract model of leakage, which simply assumes that:

all branches the program takes are leaked;
- since the path the program takes can greatly influence how long execution takes
- this is exactly like in the "program counter" (PC) security model from StaticIFC
all accessed memory addresses are leaked;
- since timing attacks can also exploit the latency difference between hits and misses in the data cache
the operands influencing timing of variable-time operations are leaked;
- as an exercise we will add a division operation that leaks both operands.

To ensure security against this leakage model, the CCT discipline requires that:

the control flow of the program does not depend on secrets;
- intuitively this prevents the execution time of different program paths from directly depending on secrets:
  if Wsecret then ... slow computation ... else skip
the accessed memory addresses do not depend on secrets;
- intuitively this prevents secrets from leaking into the data cache:
  Vsecret <- AP[Wsecret]
the operands leaked by variable-time operations do not depend on secrets.
- this prevents leaking information about secrets e.g. via division:
  Usecret := div Vsecret Wsecret

To model memory accesses that depend on secrets we will make the Imp language more realistic by adding arrays.

We need such an extension, since otherwise variable accesses in the original Imp map to memory operations at constant locations, which thus cannot depend on secrets, so in Imp CCT trivially holds for all PC well-typed programs. Array indices on the other hand are computed at runtime, which leads to accessing memory addresses that can depend on secrets, making CCT non-trivial for Imp with arrays.

For instance, here is a simple program that is PC secure (since it does no branches), but not CCT secure (since it accesses memory based on secret information):

Vsecret <- A[Wsecret]

Adding constant-time conditional and refactoring expressions

But first, we add a b ? e₁ : e₂ conditional expression that executes in constant time (for instance by being compiled to a special constant-time conditional move instruction). This constant-time conditional will also be used in our SLH countermeasure below.

Technically, adding such conditionals to Imp arithmetic expressions would make them dependent on boolean expressions. But boolean expressions are already dependent on arithmetic expressions.

To avoid making the definitions of arithmetic and boolean expressions mutually inductive, we drop boolean expressions altogether and encode them using arithmetic expressions. Our encoding of bools in terms of nats is similar to that of C, where zero means false, and non-zero means true.

We also refactor the semantics of binary operators in terms of the binop enumeration below, to avoid the duplication in Imp:

We define the semantics of binops directly on nats. We are careful to allow other representations of true (any non-zero number).

Definition not_zero (n : nat) : bool := negb (n =? 0).
Definition bool_to_nat (b : bool) : nat := if b then 1 else 0.

Definition eval_binop (o:binop) (n₁ n₂ : nat) : nat :=
  match o with
  | BinPlus ⇒ n₁ + n₂
  | BinMinus ⇒ n₁ - n₂
  | BinMult ⇒ n₁ × n₂
  | BinEq ⇒ if n₁ =? n₂ then 1 else 0
  | BinLe ⇒ if n₁ <=? n₂ then 1 else 0
  | BinAnd ⇒ bool_to_nat (not_zero n₁ && not_zero n₂)
  | BinImpl ⇒ bool_to_nat (negb (not_zero n₁) || not_zero n₂)
  end.

Inductive exp : Type :=
  | ANum (n : nat)
  | AId (x : string)
  | ABin (o : binop) (e₁ e₂ : exp) (* <--- REFACTORED *)
  | ACTIf (b : exp) (e₁ e₂ : exp). (* <--- NEW *)

We encode all the previous arithmetic and boolean operations:

Definition APlus := ABin BinPlus.
Definition AMinus := ABin BinMinus.
Definition AMult := ABin BinMult.
Definition BTrue := ANum 1.
Definition BFalse := ANum 0.
Definition BAnd := ABin BinAnd.
Definition BImpl := ABin BinImpl.
Definition BNot b := BImpl b BFalse.
Definition BOr e₁ e₂ := BImpl (BNot e₁) e₂.
Definition BEq := ABin BinEq.
Definition BNeq e₁ e₂ := BNot (BEq e₁ e₂).
Definition BLe := ABin BinLe.
Definition BGt e₁ e₂ := BNot (BLe e₁ e₂).
Definition BLt e₁ e₂ := BGt e₂ e₁.

Hint Unfold eval_binop : core.
Hint Unfold APlus AMinus AMult : core.
Hint Unfold BTrue BFalse : core.
Hint Unfold BAnd BImpl BNot BOr BEq BNeq BLe BGt BLt : core.

The notations we use for expressions are the same as in Imp, except the notation for be?e₁:e₂ which is new:

Definition U : string := "U".
Definition V : string := "V".
Definition W : string := "W".
Definition X : string := "X".
Definition Y : string := "Y".
Definition Z : string := "Z".
Definition AP : string := "AP".
Definition AS : string := "AS".

Coercion AId : string >-> exp.
Coercion ANum : nat >-> exp.

Declare Custom Entry com.
Declare Scope com_scope.

Notation "<{ e }>" := e (at level 0, e custom com at level 99) : com_scope.
Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.
Notation "x + y" := (APlus x y) (in custom com at level 50, left associativity).
Notation "x - y" := (AMinus x y) (in custom com at level 50, left associativity).
Notation "x * y" := (AMult x y) (in custom com at level 40, left associativity).
Notation "'true'" := true (at level 1).
Notation "'true'" := BTrue (in custom com at level 0).
Notation "'false'" := false (at level 1).
Notation "'false'" := BFalse (in custom com at level 0).
Notation "x <= y" := (BLe x y) (in custom com at level 70, no associativity).
Notation "x > y" := (BGt x y) (in custom com at level 70, no associativity).
Notation "x < y" := (BLt x y) (in custom com at level 70, no associativity).
Notation "x = y" := (BEq x y) (in custom com at level 70, no associativity).
Notation "x <> y" := (BNeq x y) (in custom com at level 70, no associativity).
Notation "x && y" := (BAnd x y) (in custom com at level 80, left associativity).
Notation "'~' b" := (BNot b) (in custom com at level 75, right associativity).

Open Scope com_scope.

Notation "be '?' e₁ ':' e₂" := (ACTIf be e₁ e₂) (* <-- NEW *)
(in custom com at level 20, no associativity).

Adding arrays

Now back to adding array loads and stores to commands:

Notation "<{{ e }}>" := e (at level 0, e custom com at level 99) : com_scope.
Notation "( x )" := x (in custom com, x at level 99) : com_scope.
Notation "x" := x (in custom com at level 0, x constr at level 0) : com_scope.
Notation "f x .. y" := (.. (f x) .. y)
                  (in custom com at level 0, only parsing,
                  f constr at level 0, x constr at level 9,
                  y constr at level 9) : com_scope.

Open Scope com_scope.

Notation "x '<-' a '[[' i ']]'" := (ALoad x a i) (* <--- NEW *)
     (in custom com at level 0, x constr at level 0,
      a at level 85, i custom com at level 85, no associativity) : com_scope.
Notation "a '[' i ']' '<-' e" := (AStore a i e) (* <--- NEW *)
     (in custom com at level 0, a constr at level 0,
      i custom com at level 0, e custom com at level 85,
         no associativity) : com_scope.

Definition state := total_map nat.
Definition astate := total_map (list nat). (* <--- NEW *)

Fixpoint eval (st : state) (e: exp) : nat :=
  match e with
  | ANum n ⇒ n
  | AId x ⇒ st x
  | ABin b e₁ e₂ ⇒ eval_binop b (eval st e₁) (eval st e₂)
  | <{b ? e₁ : e₂}> ⇒ if not_zero (eval st b) then eval st e₁
                           (* ^- NEW -> *) else eval st e₂
  end.

A couple of obvious lemmas that will be useful in the proofs:

Lemma not_zero_eval_S : ∀ b n st,
eval st b = S n →
not_zero (eval st b) = true.

Proof. intros b n st H. rewrite H. reflexivity. Qed.

Lemma not_zero_eval_O : ∀ b st,
eval st b = O →
not_zero (eval st b) = false.

Proof. intros b st H. rewrite H. reflexivity. Qed.

We also define an array update operation, to be used in the semantics of array stores below:

Fixpoint upd (i:nat) (ns:list nat) (n:nat) : list nat :=
  match i, ns with
  | 0, _ :: ns' ⇒ n :: ns'
  | S i', n' :: ns' ⇒ n' :: upd i' ns' n
  | _, _ ⇒ ns
  end.

Instrumenting semantics with observations

In addition to the boolean branches, which are observable in the PC security model, for CCT security also the index of array loads and stores are observable:

Inductive observation : Type :=
  | OBranch (b : bool)
  | OALoad (a : string) (i : nat)
  | OAStore (a : string) (i : nat).

Definition obs := list observation.

We define an instrumented big-step operational semantics producing these observations:

<(st, ast)> =[ c ]=> <(st', ast', os)>

Intuitively, variables act like registers (not observable), while arrays act like the memory (addresses observable).

	(CTE_Skip)

<(st, ast)> =[ skip ]=> <(st, ast, [])>

eval st e = n	(CTE_Asgn)

<(st, ast)> =[ x := e ]=> <(x !-> n; st, ast, [])>

<(st, ast)> =[ c₁ ]=> <(st', ast', os₁)>
<(st', ast')> =[ c₂ ]=> <(st'', ast'', os₂)>	(CTE_Seq)

<(st, ast)> =[ c₁ ; c₂ ]=> <(st'', ast'', os₁ ++ os₂)>

let c := if not_zero (eval st be) then c₁ else c₂ in
<(st,ast)> =[ c ]=> <(st',ast',os₁)>	(CTE_If)

<(st, ast)> =[ if be then c₁ else c₂ end]=>
<(st', ast', [OBranch (not_zero (eval st be))] ++ os₁)>

<(st,ast)> =[ if be then c; while be do c end else skip end ]=> <(st',ast',os)>	(CTE_While)

<(st,ast)> =[ while be do c end ]=> <(st', ast', os)>

eval st ie = i i < length (ast a)	(CTE_ALoad)

<(st,ast)> =[ x <- a[[ie]] ]=> <(x!->nth i (ast a) 0; st, ast,[OALoad a i])>

eval st e = n eval st ie = i i < length (ast a)	(CTE_AStore)

<(st,ast)> =[ a[ie] <- e ]=> <(st, a!->upd i (ast a) n; ast,[OAStore a i])>

Reserved Notation
         "'<(' st , ast ')>' '=[' c ']=>' '<(' stt , astt , os ')>'"
         (at level 40, c custom com at level 99,
          st constr, ast constr, stt constr, astt constr at next level).

Inductive cteval : com → state → astate → state → astate → obs → Prop :=
  | CTE_Skip : ∀ st ast,
      <(st , ast )> =[ skip ]=> <(st , ast , [])>
  | CTE_Asgn : ∀ st ast e n x,
      eval st e = n →
      <(st , ast )> =[ x := e ]=> <(x !-> n; st , ast , [])>
  | CTE_Seq : ∀ c₁ c₂ st ast st' ast' st'' ast'' os₁ os₂,
      <(st , ast )> =[ c₁ ]=> <(st', ast', os₁ )> →
      <(st', ast')> =[ c₂ ]=> <(st'', ast'', os₂ )> →
      <(st , ast )> =[ c₁ ; c₂ ]=> <(st'', ast'', os₁ ++os₂ )>
  | CTE_If : ∀ st ast st' ast' be c₁ c₂ os₁,
      let c := if not_zero (eval st be) then c₁ else c₂ in
      <(st , ast )> =[ c ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if be then c₁ else c₂ end ]=> <(st', ast', [OBranch (not_zero (eval st be))] ++ os₁ )>
  | CTE_While : ∀ b st ast st' ast' os c,
      <(st ,ast )> =[ if b then c ; while b do c end else skip end ]=>
        <(st', ast', os )> → (* <^- Nice trick; from small-step semantics *)
      <(st ,ast )> =[ while b do c end ]=> <(st', ast', os )>
  | CTE_ALoad : ∀ st ast x a ie i,
      eval st ie = i →
      i < length (ast a) →
      <(st , ast )> =[ x <- a [[ie ]] ]=> <(x !-> nth i (ast a) 0; st , ast , [OALoad a i ])>
  | CTE_AStore : ∀ st ast a ie i e n,
      eval st e = n →
      eval st ie = i →
      i < length (ast a) →
      <(st , ast )> =[ a [ie ] <- e ]=> <(st , a !-> upd i (ast a) n; ast , [OAStore a i ])>

  where "<( st , ast )> =[ c ]=> <( stt , astt , os )>" := (cteval c st ast stt astt os).

Hint Constructors cteval : core.

Constant-time security definition

Definition label := bool.

Definition public : label := true.
Definition secret : label := false.

Definition pub_vars := total_map label.
Definition pub_arrs := total_map label.

Definition pub_equiv (P : total_map label) {X:Type} (s₁ s₂ : total_map X) :=
∀ x:string, P x = true → s₁ x = s₂ x.

Lemma pub_equiv_refl : ∀ {X:Type} (P : total_map label) (s : total_map X),
pub_equiv P s s.
Proof. intros X P s x Hx. reflexivity. Qed.

Lemma pub_equiv_sym : ∀ {X:Type} (P : total_map label) (s₁ s₂ : total_map X),
pub_equiv P s₁ s₂ →
pub_equiv P s₂ s₁.
Proof. unfold pub_equiv. intros X P s₁ s₂ H x Px. rewrite H; auto. Qed.

Lemma pub_equiv_trans : ∀ {X:Type} (P : total_map label) (s₁ s₂ s₃ : total_map X),
  pub_equiv P s₁ s₂ →
  pub_equiv P s₂ s₃ →
  pub_equiv P s₁ s₃.
Proof.
  unfold pub_equiv. intros X P s₁ s₂ s₃ H₁₂ H₂₃ x Px.
  rewrite H₁₂; try rewrite H₂₃; auto.
Qed.

Lemma pub_equiv_update_secret :
  ∀ {X: Type} (P : total_map label) (s₁ s₂ : total_map X) (x: string) (e₁ e₂: X),
    pub_equiv P s₁ s₂ →
    P x = secret →
    pub_equiv P (x !-> e₁; s₁) (x !-> e₂; s₂).
Proof.
  unfold pub_equiv. intros X P s₁ s₂ x e H Pe Px y Py.
  destruct (String.eqb_spec x y) as [Hxy | Hxy]; subst.
  - rewrite Px in Py. discriminate.
  - repeat rewrite t_update_neq; auto.
Qed.

Lemma pub_equiv_update_public :
  ∀ {X: Type} (P : total_map label) (s₁ s₂ : total_map X) (x: string) {e₁ e₂: X},
    pub_equiv P s₁ s₂ →
    e₁ = e₂ →
    pub_equiv P (x !-> e₁; s₁) (x !-> e₂; s₂).
Proof.
  unfold pub_equiv. intros X P s₁ s₂ x e₁ e₂ H Eq y Py.
  destruct (String.eqb_spec x y) as [Hxy | Hxy]; subst.
  - repeat rewrite t_update_eq; auto.
  - repeat rewrite t_update_neq; auto.
Qed.

Definition cct_secure P PA c :=
  ∀ st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 )> =[ c ]=> <(st₁', ast1', os₁ )> →
    <(st₂ , ast2 )> =[ c ]=> <(st₂', ast2', os₂ )> →
    os₁ = os₂.

Example PC secure program that is not CCT secure

Definition cct_insecure_prog :=
<{{ V <- AP [[W ]] }}> .

Let's assume that W and V are secret variables. This program is trivially PC secure, because it does not branch at all. But it is not CCT secure.

This is proved below. We first define the public variables and arrays, which we will use in this kind of examples:

Definition XYZpub : pub_vars := (X!-> public; Y!-> public; Z!-> public; _ !-> secret).
Definition APpub : pub_arrs := (AP!-> public; _ !-> secret).

Lemma XYZpub_true : ∀ x, XYZpub x = true → x = X ∨ x = Y ∨ x = Z.

Proof.
  unfold XYZpub. intros x Hxyz.
  destruct (String.eqb_spec x X); auto.
  rewrite t_update_neq in Hxyz; auto.
  destruct (String.eqb_spec x Y); auto.
  rewrite t_update_neq in Hxyz; auto.
  destruct (String.eqb_spec x Z); auto.
  rewrite t_update_neq in Hxyz; auto.
  rewrite t_apply_empty in Hxyz. discriminate.
Qed.

Lemma APpub_true : ∀ a, APpub a = true → a = AP.

Proof.
  unfold APpub. intros a Ha.
  destruct (String.eqb_spec a AP); auto.
  rewrite t_update_neq in Ha; auto. discriminate Ha.
Qed.

Lemma XYZpubXYZ : ∀ x, x = X ∨ x = Y ∨ x = Z → XYZpub x = true.

Proof.
  intros x Hx.
  destruct Hx as [HX | HYZ]; subst.
  - reflexivity.
  - destruct HYZ as [HY | HZ]; subst; reflexivity.
Qed.

Example cct_insecure_prog_is_not_cct_secure :
  ¬ (cct_secure XYZpub APpub cct_insecure_prog ).
Proof.
  unfold cct_secure, cct_insecure_prog; intros CTSEC.
  remember (W!-> 1; _ !-> 0) as st₁.
  remember (W!-> 2; _ !-> 0) as st₂.
  remember (AP!-> [1;2;3]; _!-> []) as ast.
  specialize (CTSEC st₁ st₂ ast ast).

  assert (Contra: [OALoad AP 1] = [OALoad AP 2]).
  { eapply CTSEC; subst.
    (* public variables equivalent *)
    - apply pub_equiv_update_secret; auto.
      apply pub_equiv_refl.
    (* public arrays equivalent *)
    - apply pub_equiv_refl.
    - eapply CTE_ALoad; simpl; auto.
    - eapply CTE_ALoad; simpl; auto. }

  discriminate.
Qed.

Exercise: 2 stars, standard (cct_insecure_prog'_is_not_cct_secure)

Show that also the following program is not CCT secure.

Definition cct_insecure_prog' :=
<{{ AS [W ] <- 42 }}> .

Example cct_insecure_prog'_is_not_cct_secure :
¬ (cct_secure XYZpub APpub cct_insecure_prog').
Proof.
(* FILL IN HERE *) Admitted.
☐

Type system for cryptographic constant-time programming

In our CCT type system, the label assigned to the result of a constant-time conditional expression simply joins the labels of the 3 involved expressions:

P ⊢ be ∈ l P ⊢ e₁ ∈ l₁ P ⊢ e₂ ∈ l₂	(T_CTIf)

P ⊢ be?e₁:e₂ ∈ join l (join l₁ l₂)

The rules for the other expressions are standard, and a lot fewer because of our refactoring:

	(T_Num)

P ⊢ n ∈ public

	(T_Id)

P ⊢ X ∈ (P X)

P ⊢ e₁ ∈ l₁ P ⊢ e₂ ∈ l₂	(T_Bin)

P ⊢ (e₁ `op` e₂) ∈ (join l₁ l₂)

Definition join (l₁ l₂ : label) : label := l₁ && l₂.

Lemma join_public : ∀ {l₁ l₂},
join l₁ l₂ = public → l₁ = public ∧ l₂ = public.
Proof. apply andb_prop. Qed.

Lemma join_public_l : ∀ {l},
join public l = l.
Proof. reflexivity. Qed.

Definition can_flow (l₁ l₂ : label) : bool := l₁ || negb l₂.

Reserved Notation "P '⊢' a ∈ l" (at level 40).

Inductive exp_has_label (P:pub_vars) : exp → label → Prop :=
  | T_Num : ∀ n,
       P ⊢ (ANum n ) \in public
  | T_Id : ∀ X,
       P ⊢ (AId X ) \in (P X )
  | T_Bin : ∀ op e₁ l₁ e₂ l₂,
       P ⊢ e₁ \in l₁ →
       P ⊢ e₂ \in l₂ →
       P ⊢ (ABin op e₁ e₂ ) \in (join l₁ l₂ )
  | T_CTIf : ∀ be l e₁ l₁ e₂ l₂,
       P ⊢ be \in l →
       P ⊢ e₁ \in l₁ →
       P ⊢ e₂ \in l₂ →
       P ⊢ <{ be ? e₁ : e₂ }> \in (join l (join l₁ l₂))

where "P '⊢' e '∈' l" := (exp_has_label P e l).

Hint Constructors exp_has_label : core.

Theorem noninterferent_exp : ∀ {P s₁ s₂ e},
  pub_equiv P s₁ s₂ →
  P ⊢ e \in public →
  eval s₁ e = eval s₂ e.

Proof.
  intros P s₁ s₂ e Heq Ht. remember public as l.
  generalize dependent Heql.
  induction Ht; simpl; intros.
  - reflexivity.
  - eapply Heq; auto.
  - eapply join_public in Heql.
    destruct Heql as [HP₁ HP₂]. subst.
    rewrite IHHt1, IHHt2; reflexivity.
  - eapply join_public in Heql.
    destruct Heql as [HP HP']. subst.
    eapply join_public in HP'.
    destruct HP' as [HP₁ HP₂]. subst.
    rewrite IHHt1, IHHt2, IHHt3; reflexivity.
Qed.

All rules for commands are exactly the same as for pc_well_typed (from StaticIFC), except CCT_ALoad and CCT_AStore, which are new.

	(CCT_Skip)

P ;; PA ⊢ct- skip

P ⊢ e ∈ l can_flow l (P X) = true	(CCT_Asgn)

P ;; PA ⊢ct- X := e

P ;; PA ⊢ct- c₁ P ;; PA ⊢ct- c₂	(CCT_Seq)

P ;; PA ⊢ct- c₁;c₂

P ⊢ be ∈ public P ;; PA ⊢ct- c₁ P ;; PA ⊢ct- c₂	(CCT_If)

P ;; PA ⊢ct- if be then c₁ else c₂

P ⊢ be ∈ public P ⊢ct- c	(CCT_While)

P ;; PA ⊢ct- while be then c end

P ⊢ i ∈ public can_flow (PA a) (P x) = true	(CCT_ALoad)

P ;; PA ⊢ct- x <- a[[i]]

P ⊢ i ∈ public P ⊢ e ∈ l can_flow l (PA a) = true	(CCT_AStore)

P ;; PA ⊢ct- a[i] <- e

Reserved Notation "P ';;' PA '⊢ct-' c" (at level 40).

Inductive cct_well_typed (P:pub_vars) (PA:pub_arrs) : com → Prop :=
  | CCT_Skip :
      P ;; PA ⊢ct - <{{ skip }}>
  | CCT_Asgn : ∀ X e l,
      P ⊢ e \in l →
      can_flow l (P X) = true →
      P ;; PA ⊢ct - <{{ X := e }}>
  | CCT_Seq : ∀ c₁ c₂,
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ c₁ ; c₂ }}>
  | CCT_If : ∀ b c₁ c₂,
      P ⊢ b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ if b then c₁ else c₂ end }}>
  | CCT_While : ∀ b c₁,
      P ⊢ b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - <{{ while b do c₁ end }}>
  | CCT_ALoad : ∀ x a i,
      P ⊢ i \in public →
      can_flow (PA a) (P x) = true →
      P ;; PA ⊢ct - <{{ x <- a [[i ]] }}>
  | CCT_AStore : ∀ a i e l,
      P ⊢ i \in public →
      P ⊢ e \in l →
      can_flow l (PA a) = true →
      P ;; PA ⊢ct - <{{ a [i ] <- e }}>

where "P ;; PA '⊢ct-' c" := (cct_well_typed P PA c).

Hint Constructors cct_well_typed : core.

Exercise: CCT Type-Checker

In these exercises you will write a type-checker for the CCT type system above and prove your type-checker sound and complete. If you get stuck, you can take inspiration in the similar type-checkers from StaticIFC.

Exercise: 1 star, standard (label_of_exp)

Fixpoint label_of_exp (P:pub_vars) (e:exp) : label
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Exercise: 1 star, standard (label_of_exp_sound)

Lemma label_of_exp_sound : ∀ P e,
P ⊢ e \in label_of_exp P e.
Proof.
(* FILL IN HERE *) Admitted.
☐

Exercise: 1 star, standard (label_of_exp_unique)

Lemma label_of_exp_unique : ∀ P e l,
  P ⊢ e \in l →
  l = label_of_exp P e.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard (cct_typechecker)

Fixpoint cct_typechecker (P PA:pub_vars) (c:com) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
☐

Exercise: 2 stars, standard (cct_typechecker_sound)

Theorem cct_typechecker_sound : ∀ P PA c,
    cct_typechecker P PA c = true →
    P ;; PA ⊢ct - c.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Exercise: 2 stars, standard (cct_typechecker_complete)

Theorem cct_typechecker_complete : ∀ P PA c,
    cct_typechecker P PA c = false →
    ¬ (P ;; PA ⊢ct - c ).
Proof.
  (* FILL IN HERE *) Admitted.
☐

Finally, we use the type-checker to show that the cct_insecure_prog and cct_insecure_prog' examples above are not well-typed.

Print cct_insecure_prog. (* <{{ X <- A[W] }}> *)
Print XYZpub. (* (X!-> public; Y!-> public; Z!-> public; _ !-> secret) *)
Print APpub. (* (AP!-> public; _ !-> secret) *)

Exercise: 1 star, standard (cct_insecure_prog_ill_typed)

Theorem cct_insecure_prog_ill_typed :
~(XYZpub ;; APpub ⊢ct - cct_insecure_prog ).
Proof.
(* FILL IN HERE *) Admitted.
☐

Exercise: 1 star, standard (cct_insecure_prog'_ill_typed)

Theorem cct_insecure_prog'_ill_typed :
~(XYZpub ;; APpub ⊢ct - cct_insecure_prog').
Proof.
(* FILL IN HERE *) Admitted.
☐

Noninterference lemma

To prove the security of our type system, we first show a noninterference lemma, which is not that hard, given that our very restrictive type system ensures the two executions run in lock-step, since it disallows branching on secrets.

Lemma cct_well_typed_noninterferent :
  ∀ P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 )> =[ c ]=> <(st₁', ast1', os₁ )> →
    <(st₂ , ast2 )> =[ c ]=> <(st₂', ast2', os₂ )> →
    pub_equiv P st₁' st₂' ∧ pub_equiv PA ast1' ast2'.

Proof.
  intros P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂
    Hwt Heq Haeq Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂.
  induction Heval1; intros os₂' ast2 Haeq ast2' st₂ Heq st₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  (* Most cases are similar as for pc_well_typed *)
  - split; auto.
  - split; auto. destruct l.
    + rewrite (noninterferent_exp Heq H₁₀).
      eapply pub_equiv_update_public; auto.
    + simpl in H₁₁. rewrite negb_true_iff in H₁₁.
      eapply pub_equiv_update_secret; auto.
  - edestruct IHHeval1_2; eauto.
    + eapply IHHeval1_1; eauto.
    + eapply IHHeval1_1; eauto.
  - eapply IHHeval1; eauto.
    + subst c. destruct (eval st be); simpl; auto.
    + subst c c₄. rewrite (noninterferent_exp Heq H₁₁); eauto.
  - eapply IHHeval1; eauto.
  - (* NEW CASE: ALoad *)
    split; eauto.
    erewrite noninterferent_exp; eauto.
    destruct (PA a) eqn:PAa.
    + eapply pub_equiv_update_public; auto.
      eapply Haeq in PAa. rewrite PAa. reflexivity.
    + simpl in H₁₅. rewrite negb_true_iff in H₁₅.
      eapply pub_equiv_update_secret; auto.
  - (* NEW CASE: AStore *)
    split; eauto.
    destruct (PA a) eqn:PAa; simpl in ×.
    + eapply Haeq in PAa. rewrite PAa.
      destruct l; [|discriminate].
      eapply pub_equiv_update_public; auto.
      repeat erewrite (noninterferent_exp Heq); auto.
    + eapply pub_equiv_update_secret; auto.
Qed.

Final theorem: cryptographic constant-time security

Module Remember.
Definition cct_secure P PA c :=
  ∀ st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 )> =[ c ]=> <(st₁', ast1', os₁ )> →
    <(st₂ , ast2 )> =[ c ]=> <(st₂', ast2', os₂ )> →
    os₁ = os₂.
End Remember.

Theorem cct_well_typed_secure : ∀ P PA c,
P ;; PA ⊢ct - c →
cct_secure P PA c.

Proof.
  unfold cct_secure.
  intros P PA c Hwt st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂
    Heq Haeq Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂.
  induction Heval1; intros os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - reflexivity.
  - reflexivity.
  - erewrite IHHeval1_2; [erewrite IHHeval1_1 | | | |];
      try reflexivity; try eassumption.
    + eapply cct_well_typed_noninterferent with (c:=c₁); eauto.
    + eapply cct_well_typed_noninterferent with (c:=c₁); eauto.
  - rewrite (noninterferent_exp Heq H₁₁).
    f_equal; auto. eapply IHHeval1; eauto.
    + subst c. destruct (eval st be); simpl; auto.
    + subst c c₄. rewrite (noninterferent_exp Heq H₁₁); eauto.
  - eapply IHHeval1; eauto.
  - (* NEW CASE: ALoad *)
    f_equal. f_equal. eapply noninterferent_exp; eassumption.
  - (* NEW CASE: AStore *)
    f_equal. f_equal. eapply noninterferent_exp; eassumption.
Qed.

Most cases of this proof are similar to the security proof for pc_well_typed from StaticIFC. In particular, noninterference is used to prove the sequence case in both proofs.

The only new cases here are for array operations, and they follow immediately from noninterferent_exp, since the CCT type system requires array indices to be public.

Exercise: Adding division (non-constant-time operation)

The CCT discipline also prevents passing secrets to operations that are not constant time. For instance, division often takes time that depends on the values of the two operands. In this exercise we will add a new x := e₁ div e₂ command for division, add corresponding evaluation and typing rules, and extend the security proofs with the new division case.

Module Div.

Open Scope com_scope.

Notations for the old commands are the same as before:

Notation "'skip'" :=
  Skip (in custom com at level 0) : com_scope.
Notation "x := y" :=
  (Asgn x y)
    (in custom com at level 0, x constr at level 0,
      y custom com at level 85, no associativity) : com_scope.
Notation "x ; y" :=
  (Seq x y)
    (in custom com at level 90, right associativity) : com_scope.
Notation "'if' x 'then' y 'else' z 'end'" :=
  (If x y z)
    (in custom com at level 89, x custom com at level 99,
     y at level 99, z at level 99) : com_scope.
Notation "'while' x 'do' y 'end'" :=
  (While x y)
    (in custom com at level 89, x custom com at level 99, y at level 99) : com_scope.
Notation "x '<-' a '[[' i ']]'" := (ALoad x a i)
     (in custom com at level 0, x constr at level 0,
      a at level 85, i custom com at level 85, no associativity) : com_scope.
Notation "a '[' i ']' '<-' e" := (AStore a i e)
     (in custom com at level 0, a constr at level 0,
      i custom com at level 0, e custom com at level 85,
         no associativity) : com_scope.

Notation for division:

Notation "x := y 'div' z" := (* <--- NEW *)
  (Div x y z)
    (in custom com at level 0, x constr at level 0,
        y custom com at level 85, z custom com at level 85, no associativity) : com_scope.

Inductive observation : Type :=
| OBranch (b : bool)
| OALoad (a : string) (i : nat)
| OAStore (a : string) (i : nat)
| ODiv (n₁ n₂: nat). (* <--- NEW *)

Definition obs := list observation.

We add a new rule to the big-step operational semantics that produces an ODiv observation:

eval st e₁ = n₁ eval st e₂ = n₂	(CTE_Div)

<(st,ast)> =[x := e₁ div e₂]=> <(x!->(n₁/n2);st,ast,[ODiv n₁ n₂])>

Formally this looks as follows:

Inductive cteval : com → state → astate → state → astate → obs → Prop :=
  | CTE_Skip : ∀ st ast,
      <(st , ast )> =[ skip ]=> <(st , ast , [])>
  | CTE_Asgn : ∀ st ast e n x,
      eval st e = n →
      <(st , ast )> =[ x := e ]=> <(x !-> n; st , ast , [])>
  | CTE_Seq : ∀ c₁ c₂ st ast st' ast' st'' ast'' os₁ os₂,
      <(st , ast )> =[ c₁ ]=> <(st', ast', os₁ )> →
      <(st', ast')> =[ c₂ ]=> <(st'', ast'', os₂ )> →
      <(st , ast )> =[ c₁ ; c₂ ]=> <(st'', ast'', os₁ ++os₂ )>
  | CTE_IfTrue : ∀ st ast st' ast' b c₁ c₂ os₁ n,
      (eval st b =? S n ) = true →
      <(st , ast )> =[ c₁ ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if b then c₁ else c₂ end ]=> <(st', ast', [OBranch true ] ++ os₁ )>
  | CTE_IfFalse : ∀ st ast st' ast' b c₁ c₂ os₁,
      (eval st b =? 0) = true →
      <(st , ast )> =[ c₂ ]=> <(st', ast', os₁ )> →
      <(st , ast )> =[ if b then c₁ else c₂ end ]=> <(st', ast', [OBranch false ] ++ os₁ )>
  | CTE_While : ∀ b st ast st' ast' os c,
      <(st ,ast )> =[ if b then c ; while b do c end else skip end ]=>
        <(st', ast', os )> →
      <(st ,ast )> =[ while b do c end ]=> <(st', ast', os )>
  | CTE_ALoad : ∀ st ast x a ie i,
      eval st ie = i →
      i < length (ast a) →
      <(st , ast )> =[ x <- a [[ie ]] ]=> <(x !-> nth i (ast a) 0; st , ast , [OALoad a i ])>
  | CTE_AStore : ∀ st ast a ie i e n,
      eval st e = n →
      eval st ie = i →
      i < length (ast a) →
      <(st , ast )> =[ a [ie ] <- e ]=> <(st , a !-> upd i (ast a) n; ast , [OAStore a i ])>
  | CTE_Div : ∀ st ast e₁ n₁ e₂ n₂ x, (* <--- NEW *)
      eval st e₁ = n₁ →
      eval st e₂ = n₂ →
      <(st , ast )> =[ x := e₁ div e₂ ]=> <(x !-> (n₁ / n₂)%nat; st , ast , [ODiv n₁ n₂ ] )>
  where "<( st , ast )> =[ c ]=> <( stt , astt , os )>" := (cteval c st ast stt astt os).

Hint Constructors cteval : core.

Reserved Notation "P ';;' PA '⊢ct-' c" (at level 40).

Exercise: 1 star, standard (cct_well_typed_div)

Add a new typing rule for division to cct_well_typed below. Your rule should prevent leaking secret division operands via observations.

Inductive cct_well_typed (P:pub_vars) (PA:pub_arrs) : com → Prop :=
  | CCT_Skip :
      P ;; PA ⊢ct - <{{ skip }}>
  | CCT_Asgn : ∀ X e l,
      P ⊢ e \in l →
      can_flow l (P X) = true →
      P ;; PA ⊢ct - <{{ X := e }}>
  | CCT_Seq : ∀ c₁ c₂,
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ c₁ ; c₂ }}>
  | CCT_If : ∀ b c₁ c₂,
      P ⊢ b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - c₂ →
      P ;; PA ⊢ct - <{{ if b then c₁ else c₂ end }}>
  | CCT_While : ∀ b c₁,
      P ⊢ b \in public →
      P ;; PA ⊢ct - c₁ →
      P ;; PA ⊢ct - <{{ while b do c₁ end }}>
  | CCT_ALoad : ∀ x a i,
      P ⊢ i \in public →
      can_flow (PA a) (P x) = true →
      P ;; PA ⊢ct - <{{ x <- a [[i ]] }}>
  | CCT_AStore : ∀ a i e l,
      P ⊢ i \in public →
      P ⊢ e \in l →
      can_flow l (PA a) = true →
      P ;; PA ⊢ct - <{{ a [i ] <- e }}>
(* FILL IN HERE *)
   (* <--- Add your new typing rule here *)
  where "P ;; PA '⊢ct-' c" := (cct_well_typed P PA c).
(* Do not modify the following line: *)
Definition manual_grade_for_cct_well_typed_div : option (nat ×string) := None.
☐

Hint Constructors cct_well_typed : core.

Exercise: 2 stars, standard (cct_well_typed_div_noninterferent)

Theorem cct_well_typed_div_noninterferent :
  ∀ P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 )> =[ c ]=> <(st₁', ast1', os₁ )> →
    <(st₂ , ast2 )> =[ c ]=> <(st₂', ast2', os₂ )> →
    pub_equiv P st₁' st₂' ∧ pub_equiv PA ast1' ast2'.
Proof.
  intros P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂
    Hwt Heq Haeq Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂.
  induction Heval1; intros os₂' ast2 Haeq ast2' st₂ Heq st₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - split; auto.
  - split; auto. destruct l.
    + rewrite (noninterferent_exp Heq H₁₀).
      eapply pub_equiv_update_public; auto.
    + simpl in H₁₁. rewrite negb_true_iff in H₁₁.
      eapply pub_equiv_update_secret; auto.
  - edestruct IHHeval1_2; eauto.
    + eapply IHHeval1_1; eauto.
    + eapply IHHeval1_1; eauto.
  - eapply IHHeval1; eauto.
  - rewrite (noninterferent_exp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈. rewrite H in H₈. discriminate H₈.
  - rewrite (noninterferent_exp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈. rewrite H in H₈. discriminate H₈.
  - eapply IHHeval1; eassumption.
  - eapply IHHeval1; eauto.
  - split; eauto.
    erewrite noninterferent_exp; eauto.
    destruct (PA a) eqn:PAa.
    + eapply pub_equiv_update_public; auto.
      eapply Haeq in PAa. rewrite PAa. reflexivity.
    + simpl in H₁₅. rewrite negb_true_iff in H₁₅.
      eapply pub_equiv_update_secret; auto.
  - split; eauto.
    destruct (PA a) eqn:PAa; simpl in ×.
    + eapply Haeq in PAa. rewrite PAa.
      destruct l; [|discriminate].
      eapply pub_equiv_update_public; auto.
      repeat erewrite (noninterferent_exp Heq); auto.
    + eapply pub_equiv_update_secret; auto.
(* FILL IN HERE *) Admitted.
☐

We need to redefine cct_secure for our new command definition

Exercise: 2 stars, standard (cct_well_typed_div_secure)

Reprove CCT security of the type system. Hint: If this proof doesn't go through easily, you may need to go back and fix your div rule.

Theorem cct_well_typed_div_secure : ∀ P PA c,
  P ;; PA ⊢ct - c →
  cct_secure P PA c.
Proof.
  unfold cct_secure.
  intros P PA c Hwt st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂
    Heq Haeq Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂.
  induction Heval1; intros os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - reflexivity.
  - reflexivity.
  - erewrite IHHeval1_2; [erewrite IHHeval1_1 | | | |];
      try reflexivity; try eassumption.
    + eapply cct_well_typed_div_noninterferent with (c:=c₁); eauto.
    + eapply cct_well_typed_div_noninterferent with (c:=c₁); eauto.
  - rewrite (noninterferent_exp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈.
    rewrite H in H₈. inversion H₈. subst.
    f_equal. eapply IHHeval1; try eassumption.
  - rewrite (noninterferent_exp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈.
    rewrite H₈ in H. discriminate H.
  - rewrite (noninterferent_exp Heq H₁₃) in H.
    rewrite eqb_eq in H, H₈.
    rewrite H in H₈. discriminate H₈.
  - f_equal. eapply IHHeval1; eassumption.
  - eapply IHHeval1; eauto.
  - f_equal. f_equal. eapply noninterferent_exp; eassumption.
  - f_equal. f_equal. eapply noninterferent_exp; eassumption.
  (* FILL IN HERE *) Admitted.
☐

End Div.

Speculative constant-time

This second part of the chapter is based on the "Spectre Declassified" paper from IEEE SP 2023, just in simplified form (e.g. without declassification). Like in this paper, we only look at a class of speculative execution attacks called Spectre v₁.

CCT programs can be insecure under speculative execution

All variables mentioned in the program below (X, Y, AP) are public, so this program respects the CCT discipline, yet this program is not secure under speculative execution.

The size of public array AP is 3 and we check we're in bounds, yet this check can mispeculate!

Definition spec_insecure_prog :=
  <{{ if Y < 3 then (* <- this check can mispeculate for Y >= 3! *)
        X <- AP [[Y ]]; (* <- speculative out of bounds access
                            loads _a secret_ to public variable X *)
        if X ≤ 5 then X := 5 else skip end (* <- speculatively leak X *)
      else skip end }}> .

Example spec_insecure_prog_is_ct_well_typed :
XYZpub ;; APpub ⊢ct - spec_insecure_prog.

Proof.
  unfold spec_insecure_prog.
  - apply CCT_If; auto.
    + rewrite <- join_public_l.
      eapply T_Bin.
      × rewrite <- join_public_l.
        eapply T_Bin; auto.
      × eapply T_Num.
    + eapply CCT_Seq.
      × eapply CCT_ALoad; auto.
      × eapply CCT_If; auto.
        { rewrite <- join_public_l.
          eapply T_Bin; auto. }
        { eapply CCT_Asgn; eauto. }
Qed.

Here is a more realistic version of this example:

Definition spec_insecure_prog_2 :=
  <{{ X := 0;
      Y := 0;
      while Y < 3 do
        Z <- AP [[Y ]];
        X := X + Z ;
        Y := Y + 1
      end ;
      if X ≤ 5 then X := 5 else skip end }}> .

All variables mentioned in the program are again public, so also this program respects the CCT discipline, yet it is also not secure under speculative execution.

This example is formalized at the end of the chapter.

Speculative semantics

To reason about the security of these examples against Spectre v₁ we will introduce a speculative semantics. To model leakage the semantics uses the same CCT observations as above (OBranch, OALoad, and OAStore).

More interestingly, to model speculative execution we add to the semantics adversary-provided directions, which control the speculation behavior:

Inductive direction :=
| DStep (* adversary chooses the correct branch of conditional *)
| DForce (* adversary forces us take the wrong branch of conditional *)
| DLoad (a : string) (i : nat) (* for speculative OOB array accesses *)
| DStore (a : string) (i : nat). (* adversary chooses array and index *)

Definition dirs := list direction.

This gives us a very high-level model of speculation that abstracts away low-level details such as the compiler, branch predictors, memory layout, speculation window, rollbacks, etc. We do this in a way that tries to overapproximate the adversary's power.

This kind of speculation model is actually used by the Jasmin language for high-assurance crypto.

Compared to the CCT semantics with observations as output, we now add the directions as input to the evaluation judgement and we also track a mispeculation bit b.

	(Spec_Skip)

<(st,ast,b,[])> =[skip]=> <(st,ast,b,[])>

eval st e = n	(Spec_Asgn)

<(st,ast,b,[])> =[x:=e]=> <(x!->n;st,ast,b,[])>

<(st,ast,b,ds₁)> =[c₁]=> <(st',ast',b',os₁)>
<(st',ast',b',ds₂)> =[c₂]=> <(st'',ast'',b'',os₂)>	(Spec_Seq)

<(st,ast,b,ds₁++ds₂)> =[c₁;c₂]=> <(st'',ast'',b'',os₁++os₂)>

<(st,ast,b,ds)> =[ if be then c; while be do c end ]=>
<(st',ast',b',os)>	(Spec_While)

<(st,ast,b,ds)> =[ while be do c end ]=> <(st',ast',b',os)>

let c := if not_zero (eval st be) then c₁ else c₂ in
<(st,ast,b,ds)> =[ c ]=> <(st',ast',b',os₁)>	(Spec_If)

<(st,ast,b, DStep::ds)> =[ if be then c₁ else c₂ end ]=>
<(st',ast',b', [OBranch (not_zero (eval st be))]++os₁)>

let c := if not_zero (eval st be) then c₂ else c₁ in
<(st,ast,true,ds)> =[ c ]=> <(st',ast',b',os₁)>	(Spec_If_F)

<(st,ast,b, DForce::ds)> =[ if be then c₁ else c₂ end ]=>
<(st',ast',b', [OBranch (not_zero (eval st be))]++os₁)>

eval st ie = i i < length(ast a)	(Spec_ALoad)

<(st, ast, b, [DStep])> =[ x <- a[[ie]] ]=>
<(x !-> nth i (ast a) 0; st, ast, b, [OALoad a i])>

eval st ie = i i >= length(ast a) i' < length(ast a')	(Spec_ALoad_U)

<(st, ast, true, [DLoad a' i'])> =[ x <- a[[ie]] ]=>
<(x !-> nth i' (ast a') 0; st, ast, true, [OALoad a i])>

eval st e = n eval st ie = i i < length(ast a)	(Spec_AStore)

<(st, ast, b, [DStep])> =[ a[ie] <- e ]=>
<(st, a !-> upd i (ast a) n; ast, b, [OAStore a i])>

eval st e = n eval st ie = i
i >= length(ast a) i' < length(ast a')	(Spec_AStore_U)

<(st, ast, true, [DStore a' i'])> =[ a[ie] <- e ]=>
<(st, a' !-> upd i' (ast a') n; ast, true, [OAStore a i])>

Formally this definition looks as follows:

Reserved Notation
  "'<(' st , ast , b , ds ')>' '=[' c ']=>' '<(' stt , astt , bb , os ')>'"
  (at level 40, c custom com at level 99,
   st constr, ast constr, stt constr, astt constr at next level).

Inductive spec_eval : com → state → astate → bool → dirs →
                             state → astate → bool → obs → Prop :=
  | Spec_Skip : ∀ st ast b,
      <(st , ast , b , [])> =[ skip ]=> <(st , ast , b , [])>
  | Spec_Asgn : ∀ st ast b e n x,
      eval st e = n →
      <(st , ast , b , [])> =[ x := e ]=> <(x !-> n; st , ast , b , [])>
  | Spec_Seq : ∀ c₁ c₂ st ast b st' ast' b' st'' ast'' b'' os₁ os₂ ds₁ ds₂,
      <(st , ast , b , ds₁ )> =[ c₁ ]=> <(st', ast', b', os₁ )> →
      <(st', ast', b', ds₂ )> =[ c₂ ]=> <(st'', ast'', b'', os₂ )> →
      <(st , ast , b , ds₁ ++ds₂ )> =[ c₁ ; c₂ ]=> <(st'', ast'', b'', os₁ ++os₂ )>
  | Spec_If : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      let c := (if (not_zero (eval st be)) then c₁ else c₂) in
      <(st , ast , b , ds )> =[ c ]=> <(st', ast', b', os₁ )> →
      <(st , ast , b , DStep :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (eval st be))] ++ os₁ )>
  | Spec_If_F : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      let c := (if (not_zero (eval st be)) then c₂ else c₁) in (* <-- branches swapped *)
      <(st , ast , true , ds )> =[ c ]=> <(st', ast', b', os₁ )> →
      <(st , ast , b , DForce :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (eval st be))] ++ os₁ )>
  | Spec_While : ∀ be st ast b ds st' ast' b' os c,
      <(st , ast , b , ds )> =[ if be then c ; while be do c end else skip end ]=>
        <(st', ast', b', os )> →
      <(st , ast , b , ds )> =[ while be do c end ]=> <(st', ast', b', os )>
  | Spec_ALoad : ∀ st ast b x a ie i,
      eval st ie = i →
      i < length (ast a) →
      <(st , ast , b , [DStep ])> =[ x <- a [[ie ]] ]=>
        <(x !-> nth i (ast a) 0; st , ast , b , [OALoad a i ])>
  | Spec_ALoad_U : ∀ st ast x a ie i a' i',
      eval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      <(st , ast , true , [DLoad a' i'])> =[ x <- a [[ie ]] ]=>
        <(x !-> nth i' (ast a') 0; st , ast , true , [OALoad a i ])>
  | Spec_AStore : ∀ st ast b a ie i e n,
      eval st e = n →
      eval st ie = i →
      i < length (ast a) →
      <(st , ast , b , [DStep ])> =[ a [ie ] <- e ]=>
        <(st , a !-> upd i (ast a) n; ast , b , [OAStore a i ])>
  | Spec_AStore_U : ∀ st ast a ie i e n a' i',
      eval st e = n →
      eval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      <(st , ast , true , [DStore a' i'])> =[ a [ie ] <- e ]=>
        <(st , a' !-> upd i' (ast a') n; ast , true , [OAStore a i ])>

  where "<( st , ast , b , ds )> =[ c ]=> <( stt , astt , bb , os )>" :=
    (spec_eval c st ast b ds stt astt bb os).

Hint Constructors spec_eval : core.

Speculative constant-time security definition

The definition of speculative constant-time security is very similar to CCT security, just applied to the speculative semantics. The two executions receive the same directions ds:

Definition spec_ct_secure P PA c :=
  ∀ st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    <(st₁ , ast1 , false , ds )> =[ c ]=> <(st₁', ast1', b₁', os₁ )> →
    <(st₂ , ast2 , false , ds )> =[ c ]=> <(st₂', ast2', b₂', os₂ )> →
    os₁ = os₂.

We can use this definition to show that our first example is speculatively insecure:

Print spec_insecure_prog.
(* <{{ if Y < 3 then
         X <- AP [Y];
         if X <= 5 then X := 5 else skip end
       else skip end }}> *)

For this we build a counterexample where the attacker chooses an out-of-bounds index Y = 3 and then passes the directions: [DForce; DLoad AS 0; DStep]. This causes the two executions to load different values for X from index 0 of secret array AS. If the different values loaded from AS[0] are well chosen (e.g., 4 ≤ 5 in the first execution and 7 > 5 in the second) this causes two different observations: - [OBranch false; OALoad AP 3; OBranch true] and - [OBranch false; OALoad AP 3; OBranch false].

Example spec_insecure_prog_is_spec_insecure :
~(spec_ct_secure XYZpub APpub spec_insecure_prog ).

Proof.
  unfold spec_insecure_prog. intros Hcs.
  remember (Y!-> 3; _ !-> 0) as st.
  remember (AP!-> [0;1;2]; AS!-> [4;1]; _ !-> []) as ast1.
  remember (AP!-> [0;1;2]; AS!-> [7;1]; _ !-> []) as ast2.
  remember (DForce :: ([DLoad AS 0] ++ [DStep ])) as ds.
  remember (([OBranch false ] ++ ([OALoad AP 3]) ++ [OBranch true ])) as os₁.
  remember (([OBranch false ] ++ ([OALoad AP 3])++ [OBranch false ])) as os₂.

  assert (Heval1:
  <(st, ast1, false , ds )> =[ spec_insecure_prog ]=> <( X!-> 5; X!-> 4; st, ast1, true , os₁)>).
  { unfold spec_insecure_prog; subst.
    eapply Spec_If_F. eapply Spec_Seq.
    - eapply Spec_ALoad_U; simpl; eauto.
    - replace ([OBranch true ]) with ([] ++ [OBranch true ]) by reflexivity.
      eapply Spec_If; simpl. eapply Spec_Asgn; eauto. }

  assert (Heval2:
    <(st, ast2, false , ds )> =[ spec_insecure_prog ]=> <( X!-> 7; st, ast2, true , os₂)>).
    { unfold spec_insecure_prog; subst.
      eapply Spec_If_F. eapply Spec_Seq.
      - eapply Spec_ALoad_U; simpl; eauto.
      - replace ([OBranch false ]) with ([] ++ [OBranch false ]) by reflexivity.
        eapply Spec_If; simpl. auto. }

  subst. eapply Hcs in Heval1.
  + eapply Heval1 in Heval2. inversion Heval2.
  + eapply pub_equiv_refl.
  + apply pub_equiv_update_public; auto.
    apply pub_equiv_update_secret; auto.
    apply pub_equiv_refl.
Qed.

Exercise: 1 star, standard (speculation_bit_monotonic)

As mentioned above, our speculative semantics is very high-level, and doesn't have to deal with detecting mispeculation and rolling back. So in our semantics once the mispeculation bit is set to true, it will stay set:

Lemma speculation_bit_monotonic : ∀ c s a b ds s' a' b' os,
  <(s , a , b , ds )> =[ c ]=> <(s', a', b', os )> →
  b = true →
  b' = true.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Lemma speculation_needs_force : ∀ c s a b ds s' a' b' os,
  <(s , a , b , ds )> =[ c ]=> <(s', a', b', os )> →
  b = false →
  b' = true →
  In DForce ds.
Proof.
  intros c s a b ds s' a' b' os Heval Hb Hb'.
  induction Heval; subst; simpl; eauto; try discriminate.
  apply in_or_app. destruct b'; eauto.
Qed.

We can recover sequential execution from spec_eval if there is no speculation, so all directives are DStep and speculation flag starts false.

Definition seq_spec_eval (c :com) (st :state) (ast :astate)
    (st' :state) (ast' :astate) (os :obs) : Prop :=
  ∃ ds , (∀ d, In d ds → d = DStep ) ∧
    <(st , ast , false , ds )> =[ c ]=> <(st', ast', false , os )>.

(* We prove that this new definition for sequential execution is equivalent to
the old one, i.e. cteval. *)

Lemma cteval_equiv_seq_spec_eval : ∀ c st ast st' ast' os,
seq_spec_eval c st ast st' ast' os ↔ <(st , ast )> =[ c ]=> <(st', ast', os )>.

Proof.
  intros c st ast st' ast' os. unfold seq_spec_eval. split; intros H.
  - (* -> *)
    destruct H as [ds [Hstep Heval] ].
    induction Heval; try (now econstructor; eauto).
    + (* Spec_Seq *)
      eapply CTE_Seq.
      × eapply IHHeval1. intros d HdIn.
        assert (L: In d ds₁ ∨ In d ds₂) by (left; assumption).
        eapply in_or_app in L. eapply Hstep in L. assumption.
      × eapply IHHeval2. intros d HdIn.
        assert (L: In d ds₁ ∨ In d ds₂) by (right; assumption).
        eapply in_or_app in L. eapply Hstep in L. assumption.
    + (* Spec_If *)
      eapply CTE_If. destruct (eval st be) eqn:Eqbe.
      × eapply IHHeval. intros d HdIn.
        apply (in_cons DStep d) in HdIn. apply Hstep in HdIn. assumption.
      × eapply IHHeval. intros d HdIn.
        apply (in_cons DStep d) in HdIn. apply Hstep in HdIn. assumption.
    + (* Spec_IF_F; contra *)
      exfalso.
      assert (L: ~(DForce = DStep )) by discriminate. apply L.
      apply (Hstep DForce). apply in_eq.
    + (* Spec_ALoad_U; contra *)
      exfalso.
      assert (L: ~(DLoad a' i' = DStep )) by discriminate. apply L.
      apply (Hstep (DLoad a' i')). apply in_eq.
    + (* Spec_AStore_U; contra *)
      exfalso.
      assert (L: ~(DStore a' i' = DStep )) by discriminate. apply L.
      apply (Hstep (DStore a' i')). apply in_eq.
  - (* <- *)
    induction H.
    + (* CTE_Skip *)
      ∃ []; split; [| eapply Spec_Skip].
      simpl. intros d Contra; destruct Contra.
    + (* CTE_Asgn *)
      ∃ []; split; [| eapply Spec_Asgn; assumption].
      simpl. intros d Contra; destruct Contra.
    + (* CTE_Seq *)
      destruct IHcteval1 as [ds₁ [Hds1 Heval1] ].
      destruct IHcteval2 as [ds₂ [Hds2 Heval2] ].
      ∃ (ds₁ ++ ds₂). split; [| eapply Spec_Seq; eassumption].
      intros d HdIn. apply in_app_or in HdIn. destruct HdIn as [Hin1 | Hin2].
      × apply Hds1 in Hin1. assumption.
      × apply Hds2 in Hin2. assumption.
    + (* CTE_If *)
      destruct IHcteval as [ds [Hds Heval] ]. ∃ (DStep :: ds). split.
      × intros d HdIn. apply in_inv in HdIn.
        destruct HdIn as [Heq | HIn]; [symmetry; assumption | apply Hds; assumption].
      × subst c. eapply Spec_If. eauto.
    + (* CTE_While *)
      destruct IHcteval as [ds [Hds Heval] ]. ∃ ds.
      split; [assumption |]. eapply Spec_While; assumption.
    + (* CTE_ALoad *)
      ∃ [DStep ]. split.
      × simpl. intros d HdIn. destruct HdIn as [Heq | Contra]; [| destruct Contra].
        symmetry. assumption.
      × eapply Spec_ALoad; assumption.
    + (* CTE_AStore *)
      ∃ [DStep ]. split.
      × simpl. intros d HdIn. destruct HdIn as [Heq | Contra]; [| destruct Contra].
        symmetry. assumption.
      × eapply Spec_AStore; assumption.
Qed.

Exercise: 1 star, standard (ct_well_typed_seq_spec_eval_ct_secure)

Lemma ct_well_typed_seq_spec_eval_ct_secure :
  ∀ P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' os₁ os₂,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    pub_equiv PA ast1 ast2 →
    seq_spec_eval c st₁ ast1 st₁' ast1' os₁ →
    seq_spec_eval c st₂ ast2 st₂' ast2' os₂ →
    os₁ = os₂.
Proof.
  (* FILL IN HERE *) Admitted.
☐

Selective SLH transformation

Now how can we make CCT programs secure against speculative execution attacks? It turns out that we can protect such programs against Spectre v₁ by doing only two things:

Keep track of a misspeculation flag using constant-time conditionals;
Use this flag to mask the value of misspeculated public loads.

We implement this as a Selective Speculative Load Hardening (SLH) transformation that we will show enforces speculative constant-time security for all CCT programs.

This SLH transformation is "selective", since it only masks public loads. A non-selective SLH transformation was invented in LLVM, but what they implement is anyway much more complicated.

Definition msf : string := "msf".

Fixpoint sel_slh (P:pub_vars) (c:com) :=
  match c with
  | <{{skip }}> ⇒ <{{skip }}>
  | <{{x := e}}> ⇒ <{{x := e}}>
  | <{{c₁; c₂}}> ⇒ <{{sel_slh P c₁; sel_slh P c₂}}>
  | <{{if be then c₁ else c₂ end }}> ⇒
      <{{if be then msf := (be ? msf : 1); sel_slh P c₁
               else msf := (be ? 1 : msf ); sel_slh P c₂ end }}>
  | <{{while be do c end }}> ⇒
      <{{while be do msf := (be ? msf : 1); sel_slh P c end ;
         msf := (be ? 1 : msf )}}>
  | <{{x <- a[[i]]}}> ⇒
      if P x then <{{x <- a[[i]]; x := (msf ≠ 0) ? 0 : x}}>
             else <{{x <- a[[i]]}}>
  | <{{a[i] <- e}}> ⇒ <{{a[i] <- e}}>
  end.

Print spec_insecure_prog.
(* <{{ if Y < 3 then
         X <- AP [Y];
         if X <= 5 then X := 5 else skip end
       else skip end }}> *)

Definition sel_slh_spec_insecure_prog :=
<{{ if Y < 3 then
      msf := ((Y < 3) ? msf : 1);
      (X <- AP [[Y ]]; X := (msf ≠ 0) ? 0 : X );
      if X ≤ 5 then
        msf := ((X ≤ 5) ? msf : 1);
        X := 5
      else msf := ((X ≤ 5) ? 1 : msf ); skip end
    else msf := ((Y < 3) ? 1 : msf ); skip end }}>.

Lemma sel_slh_spec_insecure_prog_check:
sel_slh XYZpub spec_insecure_prog = sel_slh_spec_insecure_prog.

Proof. reflexivity. Qed.

When mispeculation occurs in the first condition if Z < 1, the transformation detects this mispeculation and sets msf (mispeculation flag) to 1. Then, although the secret value gets loaded into X via the out-of-bounds access X <- AP[[Z]], it is immediatly overwritten with 0 due to the masking code X := (msf ≠ 0) ? 0 : X that follows. As a result, all subsequent operations like if X ≤ 5 only uses the masked value 0 instead of the actual secret.

Main proof idea: use compiler correctness wrt ideal semantics

To prove this transformation secure, Spectre Declassified uses an ideal semantics, capturing selective speculative load hardening more abstractly. The proof effort is decomposed into:

a speculative constant-time proof for the ideal semantics;
a compiler correctness proof for the sel_slh transformation, taking source programs which are executed using the ideal semantics, to target programs executed using the speculative semantics.

In a little bit more detail, we're intuitively trying to prove:

forall P PA c, P;;PA ⊢ct- c -> spec_ct_secure P PA (sel_slh P c),

where the conclusion looks as follows:

forall st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
  pub_equiv P st₁ st₂ ->
  pub_equiv PA ast1 ast2 ->
  <(st₁,ast1,false,ds)> =[ sel_slh P c ]=> <(st₁',ast1',b₁',os₁)> ->
  <(st₂,ast2,false,ds)> =[ sel_slh P c ]=> <(st₂',ast2',b₂',os₂)> ->
  os₁ = os₂

Compiler correctness allows us to get rid of sel_slh P c in the premises and instead get an execution in terms of the ideal semantics:

  <(st,ast,b,ds)> =[ sel_slh P c ]=> <(st',ast',b',os)> ->
    P ⊢i <(st,ast,b,ds)> =[ c ]=> <(msf!->st msf;st',ast',b',os)>

One thing to note is that the ideal semantics doesn't track misspeculation in the msf variable, but instead directly uses the mispeculation bit in the speculative semantics for masking. This allows us to keep the ideal semantics simple, and then we show that msf correctly tracks mispeculation in our compiler correctness proof .

Ideal semantics definition

All rules of the ideal semantics are the same as for the speculative semantics, except the ones for array loads, which add the extra masking done by sel_slh on top of the speculative semantics.

eval st ie = i i < length(ast a)	(Ideal_ALoad)

let v := if b && P x then 0 else nth i (ast a) 0 in
P ⊢i <(st, ast, b, [DStep])> =[ x <- a[[ie]] ]=>
<(x !-> v; st, ast, b, [OALoad a i])>

eval st ie = i i >= length(ast a) i' < length(ast a')	(Ideal_ALoad_U)

let v := if P x then 0 else nth i' (ast a') 0 in
P ⊢i <(st, ast, true, [DLoad a' i'])> =[ x <- a[[ie]] ]=>
<(x !-> v; st, ast, true, [OALoad a i])>

Reserved Notation
  "P '⊢i' '<(' st , ast , b , ds ')>' '=[' c ']=>' '<(' stt , astt , bb , os ')>'"
  (at level 40, c custom com at level 99,
   st constr, ast constr, stt constr, astt constr at next level).

Inductive ideal_eval (P:pub_vars) :
    com → state → astate → bool → dirs →
           state → astate → bool → obs → Prop :=
  | Ideal_Skip : ∀ st ast b,
      P ⊢i <(st , ast , b , [])> =[ skip ]=> <(st , ast , b , [])>
  | Ideal_Asgn : ∀ st ast b e n x,
      eval st e = n →
      P ⊢i <(st , ast , b , [])> =[ x := e ]=> <(x !-> n; st , ast , b , [])>
  | Ideal_Seq : ∀ c₁ c₂ st ast b st' ast' b' st'' ast'' b'' os₁ os₂ ds₁ ds₂,
      P ⊢i <(st , ast , b , ds₁ )> =[ c₁ ]=> <(st', ast', b', os₁ )> →
      P ⊢i <(st', ast', b', ds₂ )> =[ c₂ ]=> <(st'', ast'', b'', os₂ )> →
      P ⊢i <(st , ast , b , ds₁ ++ds₂ )> =[ c₁ ; c₂ ]=> <(st'', ast'', b'', os₁ ++os₂ )>
  | Ideal_If : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      let c := (if (not_zero (eval st be)) then c₁ else c₂) in
      P ⊢i <(st , ast , b , ds )> =[ c ]=> <(st', ast', b', os₁ )> →
      P ⊢i <(st , ast , b , DStep :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (eval st be))] ++ os₁ )>
  | Ideal_If_F : ∀ st ast b st' ast' b' be c₁ c₂ os₁ ds,
      let c := (if (not_zero (eval st be)) then c₂ else c₁) in (* <-- branches swapped *)
      P ⊢i <(st , ast , true , ds )> =[ c ]=> <(st', ast', b', os₁ )> →
      P ⊢i <(st , ast , b , DForce :: ds )> =[ if be then c₁ else c₂ end ]=>
        <(st', ast', b', [OBranch (not_zero (eval st be))] ++ os₁ )>
  | Ideal_While : ∀ be st ast b ds st' ast' b' os c,
      P ⊢i <(st , ast , b , ds )> =[ if be then c ; while be do c end else skip end ]=>
        <(st', ast', b', os )> →
      P ⊢i <(st , ast , b , ds )> =[ while be do c end ]=> <(st', ast', b', os )>
  | Ideal_ALoad : ∀ st ast b x a ie i,
      eval st ie = i →
      i < length (ast a) →
      let v := if b && P x then 0 else nth i (ast a) 0 in
      P ⊢i <(st , ast , b , [DStep ])> =[ x <- a [[ie ]] ]=>
        <(x !-> v; st , ast , b , [OALoad a i ])>
  | Ideal_ALoad_U : ∀ st ast x a ie i a' i',
      eval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      let v := if P x then 0 else nth i' (ast a') 0 in
      P ⊢i <(st , ast , true , [DLoad a' i'])> =[ x <- a [[ie ]] ]=>
        <(x !-> v; st , ast , true , [OALoad a i ])>
  | Ideal_AStore : ∀ st ast b a ie i e n,
      eval st e = n →
      eval st ie = i →
      i < length (ast a) →
      P ⊢i <(st , ast , b , [DStep ])> =[ a [ie ] <- e ]=>
        <(st , a !-> upd i (ast a) n; ast , b , [OAStore a i ])>
  | Ideal_AStore_U : ∀ st ast a ie i e n a' i',
      eval st e = n →
      eval st ie = i →
      i ≥ length (ast a) →
      i' < length (ast a') →
      P ⊢i <(st , ast , true , [DStore a' i'])> =[ a [ie ] <- e ]=>
        <(st , a' !-> upd i' (ast a') n; ast , true , [OAStore a i ])>

  where "P ⊢i <( st , ast , b , ds )> =[ c ]=> <( stt , astt , bb , os )>" :=
    (ideal_eval P c st ast b ds stt astt bb os).

Hint Constructors ideal_eval : core.

Ideal semantics enforces speculative constant-time

Let's now prove that the ideal semantics does enforce speculative constant-time. As in the proofs we did before for constant-time and pc security, we rely on a proof of noninterference. For our ideal semantics this noninterference proof requires interesting generalization of the induction hypothesis (see ct_well_typed_ideal_noninterferent_general).

Generalization 1: We need to also deal with executions ending with b=true, but in that case we cannot ensure that the array states are publicly equivalent, since our selective SLH does not mask misspeculated stores (for efficiency, since it's not needed for security). This requires to generalize the pub_equiv PA ast1 ast2 premise of our statements too.

Generalization 2: To show that the two executions run in lock-step the proof uses not only the CCT type system (not branching on secrets) but also the fact that the directions are the same, which we need to establish as an extra invariant though.

Definition prefix {X:Type} (xs ys : list X) : Prop :=
∃ zs , xs ++ zs = ys.

Lemma prefix_refl : ∀ {X:Type} {ds : list X},
prefix ds ds.
Proof. intros X ds. ∃ []. apply app_nil_r. Qed.

Lemma prefix_nil : ∀ {X:Type} (ds : list X),
prefix [] ds.
Proof. intros X ds. unfold prefix. eexists. simpl. reflexivity. Qed.

Lemma prefix_heads_and_tails : ∀ {X:Type} (h₁ h₂ : X) (t₁ t₂ : list X),
  prefix (h₁ ::t₁) (h₂ ::t₂) → h₁ = h₂ ∧ prefix t₁ t₂.
Proof.
  intros X h₁ h₂ t₁ t₂. unfold prefix. intros Hpre.
  destruct Hpre as [zs Hpre]; simpl in Hpre.
  inversion Hpre; subst. eauto.
Qed.

Lemma prefix_heads : ∀ {X:Type} (h₁ h₂ : X) (t₁ t₂ : list X),
prefix (h₁ ::t₁) (h₂ ::t₂) → h₁ = h₂.
Proof.
intros X h₁ h₂ t₁ t₂ H. apply prefix_heads_and_tails in H; tauto.
Qed.

Lemma prefix_or_heads : ∀ {X:Type} (x y : X) (xs ys : list X),
  prefix (x :: xs) (y :: ys) ∨ prefix (y :: ys) (x :: xs) →
  x = y.
Proof.
  intros X x y xs ys H.
  destruct H as [H | H]; apply prefix_heads in H; congruence.
Qed.

Lemma prefix_cons : ∀ {X:Type} (d :X) (ds₁ ds₂: list X),
prefix ds₁ ds₂ ↔
prefix (d ::ds₁) (d ::ds₂).
Proof.
  intros X d ds₁ ds₂. split; [unfold prefix| ]; intros H.
  - destruct H; subst.
    eexists; simpl; eauto.
  - apply prefix_heads_and_tails in H. destruct H as [_ H]. assumption.
Qed.

Lemma prefix_app : ∀ {X:Type} {ds₁ ds₂ ds₀ ds₃ : list X},
  prefix (ds₁ ++ ds₂) (ds₀ ++ ds₃) →
  prefix ds₁ ds₀ ∨ prefix ds₀ ds₁.
Proof.
  intros X ds₁. induction ds₁ as [| d₁ ds₁' IH]; intros ds₂ ds₀ ds₃ H.
  - left. apply prefix_nil.
  - destruct ds₀ as [| d₀ ds₀'] eqn:D₀.
    + right. apply prefix_nil.
    + simpl in H; apply prefix_heads_and_tails in H.
      destruct H as [Heq Hpre]; subst.
      apply IH in Hpre; destruct Hpre; [left | right];
      apply prefix_cons; assumption.
Qed.

Lemma prefix_append_front : ∀ {X:Type} {ds₁ ds₂ ds₃ : list X},
  prefix (ds₁ ++ ds₂) (ds₁ ++ ds₃) →
  prefix ds₂ ds₃.
Proof.
  intros X ds₁. induction ds₁ as [| d₁ ds₁' IH]; intros ds₂ ds₃ H.
  - auto.
  - simpl in H; apply prefix_cons in H. apply IH in H. assumption.
Qed.

Lemma app_eq_prefix : ∀ {X:Type} {ds₁ ds₂ ds₁' ds₂' : list X},
  ds₁ ++ ds₂ = ds₁' ++ ds₂' →
  prefix ds₁ ds₁' ∨ prefix ds₁' ds₁.
Proof.
  intros X ds₁. induction ds₁ as [| h₁ t₁ IH]; intros ds₂ ds₁' ds₂' H.
  - left. apply prefix_nil.
  - destruct ds₁' as [| h₁' t₁'] eqn:D₁'.
    + right. apply prefix_nil.
    + simpl in H; inversion H; subst.
      apply IH in H₂. destruct H₂ as [HL | HR];
      [left | right]; apply prefix_cons; auto.
Qed.

Ltac split4 := split; [|split; [| split] ].

Lemma ct_well_typed_ideal_noninterferent_general : ∀ P PA c,
  ∀ st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds₁ ds₂,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    (b = false → pub_equiv PA ast1 ast2 ) → (* Generalization 1 *)
    (prefix ds₁ ds₂ ∨ prefix ds₂ ds₁ ) → (* <- Generalization 2 *)
    P ⊢i <(st₁ , ast1 , b , ds₁ )> =[ c ]=> <(st₁', ast1', b₁', os₁ )> →
    P ⊢i <(st₂ , ast2 , b , ds₂ )> =[ c ]=> <(st₂', ast2', b₂', os₂ )> →
    pub_equiv P st₁' st₂' ∧ b₁' = b₂' ∧
      (b₁' = false → pub_equiv PA ast1' ast2') ∧ (* <- Generalization 1 *)
      ds₁ = ds₂. (* <- Generalization 2 *)
Proof.
  intros P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds₁ ds₂
    Hwt Heq Haeq Hds Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂. generalize dependent b₂'.
  generalize dependent ds₂.
  induction Heval1; intros ds2X Hds b₂' os₂' a₂ Haeq a₂' s₂ Heq s₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - (* Skip *) auto.
  - (* Asgn *) split4; auto.
    destruct (P x) eqn:EqPx.
    + eapply pub_equiv_update_public; eauto.
      eapply noninterferent_exp; eauto.
      destruct l; [auto | simpl in H₁₄; discriminate].
    + eapply pub_equiv_update_secret; eauto.
  - (* Seq *)
    destruct Hds as [Hpre | Hpre]; apply prefix_app in Hpre as Hds1.
    + (* prefix (ds₁ ++ ds₂) (ds₀ ++ ds₃) *)
      eapply IHHeval1_1 in Hds1; eauto.
      destruct Hds1 as [ Hstates [Hbits [Hastates Hdirections] ] ]. subst.
      eapply prefix_append_front in Hpre as Hds2.
      eapply IHHeval1_2 in H₁₄; eauto. firstorder. subst. reflexivity.
    + (* prefix (ds₀ ++ ds₃) (ds₁ ++ ds₂) *)
      eapply IHHeval1_1 with (ds₂:=ds₀) in H₁₃; eauto; [| tauto].
      destruct H₁₃ as [ Hstates [Hbits [Hastates Hdirections] ] ]. subst.
      eapply prefix_append_front in Hpre as Hds2.
      eapply IHHeval1_2 in H₁₄; eauto. firstorder; subst; reflexivity.
  - (* If *)
    remember (if not_zero (eval st be) then c₁ else c₂) as c₅.
    assert(G : P ;; PA ⊢ct - c₅).
    { subst c₅. destruct (eval st be); assumption. }
    assert(Gds : prefix ds ds₀ ∨ prefix ds₀ ds).
    { destruct Hds as [Hds | Hds]; apply prefix_cons in Hds; tauto. }
    subst c₄ c₅. erewrite noninterferent_exp in H₁₀.
    + specialize (IHHeval1 G _ Gds _ _ _ Haeq _ _ Heq _ H₁₀).
      firstorder; congruence.
    + apply pub_equiv_sym. eassumption.
    + eassumption.
  - (* IF; contra *)
    apply prefix_or_heads in Hds; inversion Hds.
  - (* IF; contra *)
     apply prefix_or_heads in Hds; inversion Hds.
  - (* If_F; analog to If *)
    remember (if not_zero (eval st be) then c₂ else c₁) as c₅.
    assert(G : P ;; PA ⊢ct - c₅).
    { subst c₅. destruct (eval st be); assumption. }
    assert(Gds : prefix ds ds₀ ∨ prefix ds₀ ds).
    { destruct Hds as [Hds | Hds]; apply prefix_cons in Hds; tauto. }
    subst c₄ c₅. erewrite noninterferent_exp in H₁₀.
    + assert(GG: true = false → pub_equiv PA ast a₂). (* <- only difference *)
      { intro Hc. discriminate. }
      specialize (IHHeval1 G _ Gds _ _ _ GG _ _ Heq _ H₁₀).
      firstorder; congruence.
    + apply pub_equiv_sym. eassumption.
    + eassumption.
  - (* While *) eapply IHHeval1; try eassumption. repeat constructor; eassumption.
  - (* ALoad *) split4; eauto.
    destruct (P x) eqn:EqPx; simpl.
    + eapply pub_equiv_update_public; eauto.
      destruct b₂' eqn:Eqb2'; simpl; [reflexivity |].
      unfold can_flow in H₁₈. eapply orb_true_iff in H₁₈.
      destruct H₁₈ as [Hapub | Contra]; [| simpl in Contra; discriminate].
      subst v v₁ v₂. eapply Haeq in Hapub; [| reflexivity]. rewrite Hapub.
      eapply noninterferent_exp in Heq; eauto. rewrite Heq.
      reflexivity.
    + eapply pub_equiv_update_secret; eauto.
  - (* ALoad_U *)
    split4; eauto.
    + destruct (P x) eqn:EqPx.
      × simpl. eapply pub_equiv_update_public; eauto.
      × eapply pub_equiv_update_secret; eauto.
    + apply prefix_or_heads in Hds. inversion Hds.
  - (* ALoad *)
    split4; eauto.
    + destruct (P x) eqn:EqPx.
      × eapply pub_equiv_update_public; eauto.
      × eapply pub_equiv_update_secret; eauto.
    + apply prefix_or_heads in Hds. inversion Hds.
  - (* ALoad_U *)
    split4; eauto.
    + destruct (P x) eqn:EqPx.
      × eapply pub_equiv_update_public; eauto.
      × eapply pub_equiv_update_secret; eauto.
    + apply prefix_or_heads in Hds. inversion Hds. reflexivity.
  - (* AStore *)
    split4; eauto. intro Hb₂'.
    destruct (PA a) eqn:EqPAa.
    + eapply pub_equiv_update_public; eauto.
      destruct l eqn:Eql.
      × eapply noninterferent_exp in H₁₉, H₂₀; eauto. rewrite H₁₉, H₂₀.
        apply Haeq in Hb₂'. apply Hb₂' in EqPAa. rewrite EqPAa. reflexivity.
      × simpl in H₂₁. discriminate.
    + eapply pub_equiv_update_secret; eauto.
  - (* AStore_U; contra *) apply prefix_or_heads in Hds. inversion Hds.
  - (* AStore; contra *) apply prefix_or_heads in Hds. inversion Hds.
  - (* AStore_U; contra *)
    split4; eauto.
    + intro contra. discriminate contra.
    + apply prefix_or_heads in Hds. inversion Hds. reflexivity.
Qed.

Corollary ct_well_typed_ideal_noninterferent :
  ∀ P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    (b = false → pub_equiv PA ast1 ast2 ) →
    P ⊢i <(st₁ , ast1 , b , ds )> =[ c ]=> <(st₁', ast1', b₁', os₁ )> →
    P ⊢i <(st₂ , ast2 , b , ds )> =[ c ]=> <(st₂', ast2', b₂', os₂ )> →
    pub_equiv P st₁' st₂' ∧ b₁' = b₂' ∧ (b₁' = false → pub_equiv PA ast1' ast2').
Proof.
  intros P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds
    Hwt Heq Haeq Heval1 Heval2.
  eapply ct_well_typed_ideal_noninterferent_general in Heval2; eauto; try tauto.
  left. apply prefix_refl.
Qed.

This corollary (used below in the sequence case) also follows from noninterferent_general

Corollary aux : ∀ P PA st₁ st₂ ast1 ast2 b ds₁ ds₂ c st₁' st₂' ast1' ast2' b₁ b₂ os₁ os₂ ds₁' ds₂',
  ds₂ ++ ds₂' = ds₁ ++ ds₁' →
  P ;; PA ⊢ct - c →
  pub_equiv P st₁ st₂ →
  (b = false → pub_equiv PA ast1 ast2 ) →
  P ⊢i <(st₁ , ast1 , b , ds₁ )> =[ c ]=> <(st₁', ast1', b₁ , os₁ )> →
  P ⊢i <(st₂ , ast2 , b , ds₂ )> =[ c ]=> <(st₂', ast2', b₂ , os₂ )> →
  ds₁ = ds₂ ∧ ds₁' = ds₂'.
Proof.
  intros P PA st₁ st₂ ast1 ast2 b ds₁ ds₂ c st₁' st₂' ast1' ast2' b₁ b₂ os₁ os₂ ds₁' ds₂'
    Hds Hwt Heq Haeq Heval1 Heval2.
  pose proof Hds as H.
  symmetry in H.
  apply app_eq_prefix in H.
  eapply ct_well_typed_ideal_noninterferent_general in H;
    [ | | | | apply Heval1 | apply Heval2]; try eassumption.
  - destruct H as [ _ [ _ [ _ H] ] ]. subst. split; [reflexivity|].
    apply app_inv_head in Hds. congruence.
Qed.

Theorem ideal_spec_ct_secure :
  ∀ P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
    P ;; PA ⊢ct - c →
    pub_equiv P st₁ st₂ →
    (b = false → pub_equiv PA ast1 ast2 ) →
    P ⊢i <(st₁ , ast1 , b , ds )> =[ c ]=> <(st₁', ast1', b₁', os₁ )> →
    P ⊢i <(st₂ , ast2 , b , ds )> =[ c ]=> <(st₂', ast2', b₂', os₂ )> →
    os₁ = os₂.
Proof.
  intros P PA c st₁ st₂ ast1 ast2 b st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds
    Hwt Heq Haeq Heval1 Heval2.
  generalize dependent st₂'. generalize dependent st₂.
  generalize dependent ast2'. generalize dependent ast2.
  generalize dependent os₂. generalize dependent b₂'.
  induction Heval1; intros b₂' os₂' ast2 Haeq ast2' st₂ Heq st₂' Heval2;
    inversion Heval2; inversion Hwt; subst.
  - (* Skip *) reflexivity.
  - (* Skip *) reflexivity.
  - (* Seq *)
    eapply aux in H₁; [| | | | apply Heval1_1 | apply H₅ ]; eauto.
    destruct H₁ as [H₁ H₁']. subst.
    assert(NI₁ : pub_equiv P st' st'0 ∧ b' = b'0 ∧ (b' = false → pub_equiv PA ast' ast'0)).
    { eapply ct_well_typed_ideal_noninterferent; [ | | | eassumption | eassumption]; eauto. }
    destruct NI₁ as [NI1eq [NIb NIaeq] ]. subst.
    erewrite IHHeval1_2; [erewrite IHHeval1_1 | | | |];
      try reflexivity; try eassumption.
  - (* If *)
    f_equal.
    + f_equal. eapply noninterferent_exp in Heq; [| eassumption].
      rewrite Heq. reflexivity.
    + eapply IHHeval1; try eassumption; try (destruct (eval st be); eassumption).
      subst c c₄. erewrite (noninterferent_exp Heq H₁₄); eassumption.
  - (* If_F *)
    f_equal.
    + f_equal. eapply noninterferent_exp in Heq; [| eassumption].
      rewrite Heq. reflexivity.
    + eapply IHHeval1; try eassumption; try (destruct (eval st be); eassumption).
      × intro contra. discriminate contra.
      × subst c c₄. erewrite noninterferent_exp; eassumption.
  - (* While *) eapply IHHeval1; eauto.
  - (* ALoad *) f_equal. f_equal. eapply noninterferent_exp; eassumption.
  - (* ALoad_U *) f_equal. f_equal. eapply noninterferent_exp; eassumption.
  - (* AStore *) f_equal. f_equal. eapply noninterferent_exp; eassumption.
  - (* AStore *) f_equal. f_equal. eapply noninterferent_exp; eassumption.
Qed.

Correctness of sel_slh as a compiler from ideal to speculative semantics

We now prove that the ideal semantics correctly captures the programs produced by sel_slh when executed using the speculative semantics. We phrase this as a backwards compiler correctness proof for sel_slh, which intuitively looks as follows:

    <(st,ast,b,ds)> =[[ sel_slh P c ]]=> <(st',ast',b',os)> ->
    P ⊢i <(st,ast,b,ds)> =[[ c ]]=> <(msf!->st msf;st',ast',b',os)>

All results about sel_slh below assume that the original c doesn't already use the variable msf needed by the sel_slh translation.

Fixpoint e_unused (x:string) (e:exp) : Prop :=
  match e with
  | ANum n ⇒ True
  | AId y ⇒ y ≠ x
  | ABin _ e₁ e₂ ⇒ e_unused x e₁ ∧ e_unused x e₂
  | <{b ? e₁ : e₂}> ⇒ e_unused x b ∧ e_unused x e₁ ∧ e_unused x e₂
  end.

Fixpoint unused (x:string) (c:com) : Prop :=
  match c with
  | <{{skip }}> ⇒ True
  | <{{y := e}}> ⇒ y ≠ x ∧ e_unused x e
  | <{{c₁; c₂}}> ⇒ unused x c₁ ∧ unused x c₂
  | <{{if be then c₁ else c₂ end }}> ⇒
      e_unused x be ∧ unused x c₁ ∧ unused x c₂
  | <{{while be do c end }}> ⇒ e_unused x be ∧ unused x c
  | <{{y <- a[[i]]}}> ⇒ y ≠ x ∧ e_unused x i
  | <{{a[i] <- e}}> ⇒ e_unused x i ∧ e_unused x e
  end.

As a warm-up we prove that sel_slh properly updates the variable msf.

Proving this by induction on com or spec_eval leads to induction hypotheses, that are not strong enough to prove the Spec_While case. Therefore we will prove it by induction on the size of a the pair of the (c:com) and the (ds:dirs).

Fixpoint com_size (c:com) : nat :=
  match c with
  | <{{ c₁; c₂ }}> ⇒ 1 + (com_size c₁) + (com_size c₂)
  | <{{ if be then ct else cf end }}> ⇒ 1 + max (com_size ct) (com_size cf)
  | <{{ while be do cw end }}> ⇒ 1 + (com_size cw)
  | <{{ skip }}> ⇒ 1
  | _ ⇒ 1
  end.

Definition size (c:com) (ds:dirs) : nat := com_size c + length ds.

We prove a helpful induction principle on size:

Check measure_induction.

Lemma size_ind : ∀ P : com → dirs → Prop,
  (∀ c ds,
    (∀ c' ds', size c' ds' < size c ds → P c' ds') →
    P c ds ) →
  (∀ c ds, P c ds ).
Proof.
  intros.
  remember (fun c_ds ⇒ P (fst c_ds) (snd c_ds)) as P'.
  replace (P c ds) with (P' (c, ds)) by now rewrite HeqP'.
  eapply measure_induction with (f:=fun c_ds ⇒ size (fst c_ds) (snd c_ds)).
  intros. rewrite HeqP'.
  apply H. intros.
  remember (c', ds') as c_ds'.
  replace (P c' ds') with (P' c_ds') by now rewrite Heqc_ds', HeqP'.
  apply H₀. now rewrite Heqc_ds'.
Qed.

The proof of sel_slh_flag

Lemma size_decreasing: ∀ c₁ ds₁ c₂ ds₂,
  (com_size c₁ < com_size c₂ ∧ length ds₁ ≤ length ds₂ ) ∨
  (com_size c₁ ≤ com_size c₂ ∧ length ds₁ < length ds₂ ) →
  size c₁ ds₁ < size c₂ ds₂.
Proof.
  intros c₁ ds₁ c₂ ds₂ [ [Hcom Hdir] | [Hcom Hdir] ];
  unfold size; lia.
Qed.

Based on the Lemma size_decreasing we can build a tactic to solve the subgoals in the form of size c' ds' < size c ds, which will be produced by size_ind.

Ltac size_auto :=
  try ( apply size_decreasing; left; split; simpl;
        [| repeat rewrite app_length]; lia );
  try ( apply size_decreasing; right; split; simpl;
        [| repeat rewrite app_length]; lia);
  try ( apply size_decreasing; left; split; simpl;
        [auto | repeat rewrite app_length; lia] ).

To properly apply size_ind, we need to state sel_slh_flag as a proposition of type com → dirs → Prop. Therefore we define the following:

Definition sel_slh_flag_prop (c :com) (ds :dirs) :Prop :=
  ∀ P st ast (b:bool) st' ast' (b':bool) os,
  unused msf c →
  st msf = (if b then 1 else 0) →
  <(st , ast , b , ds )> =[ sel_slh P c ]=> <(st', ast', b', os )> →
  st' msf = (if b' then 1 else 0).

Lemma sel_slh_flag : ∀ c ds,
  sel_slh_flag_prop c ds.
Proof.
  eapply size_ind. unfold sel_slh_flag_prop.
  intros c ds IH P st ast b st' ast' b' os Hunused Hstb Heval.
  destruct c; simpl in *; try (now inversion Heval; subst; eauto).
  - (* Asgn *)
    inversion Heval; subst. rewrite t_update_neq; tauto.
  - (* Seq *)
    inversion Heval; subst; clear Heval.
    apply IH in H₁; try tauto.
    + apply IH in H₁₀; try tauto. size_auto.
    + size_auto.
  - (* IF *)
    inversion Heval; subst; clear Heval.
    + (* Spec_If *)
      destruct (eval st be) eqn:Eqnbe.
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. assumption. }
      × (* analog to true case *)
        inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁.
        { auto. }
        { size_auto. }
        { tauto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. assumption. }
    + (* Spec_If_F; analog to Spec_If case *)
      destruct (eval st be) eqn:Eqnbe.
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. simpl. reflexivity. }
      × inversion H₁₀; subst; clear H₁₀.
        inversion H₁; subst; clear H₁.
        apply IH in H₁₁; try tauto.
        { size_auto. }
        { rewrite t_update_eq. simpl. rewrite Eqnbe. simpl. reflexivity. }
  - (* While *)
      inversion Heval; subst; clear Heval.
      inversion H₁; subst; clear H₁.
      inversion H₁₁; subst; clear H₁₁.
      + (* non-speculative *)
        destruct (eval st be) eqn:Eqnbe.
        × inversion H₁₂; subst; clear H₁₂.
          inversion H₁₀; subst; simpl.
          rewrite t_update_eq, Eqnbe; simpl. assumption.
        × inversion H₁₂; subst; clear H₁₂.
          assert(Hwhile: <(st'1, ast'1, b'1, (ds₀ ++ ds₂)%list)>
              =[ sel_slh P <{{while be do c end }}> ]=> <(st', ast', b', (os₃++os₂)%list)> ).
          { simpl. eapply Spec_Seq; eassumption. }
          apply IH in Hwhile; eauto.
          { size_auto. }
          { clear Hwhile; clear H₁₁.
            inversion H₁; subst; clear H₁.
            inversion H₂; subst; clear H₂. simpl in H₁₂.
            apply IH in H₁₂; try tauto.
            - size_auto.
            - rewrite t_update_eq, Eqnbe; simpl. assumption. }
      + (* speculative; analog to non_speculative case *)
        destruct (eval st be) eqn:Eqnbe.
        × inversion H₁₂; subst; clear H₁₂.
          assert(Hwhile: <(st'1, ast'1, b'1, (ds₀ ++ ds₂)%list)>
              =[sel_slh P <{{while be do c end }}>]=> <(st', ast', b', (os₃++os₂)%list )>).
          { simpl. eapply Spec_Seq; eassumption. }
          apply IH in Hwhile; eauto.
          { size_auto. }
          { clear Hwhile; clear H₁₁.
            inversion H₁; subst; clear H₁.
            inversion H₂; subst; clear H₂. simpl in H₁₂.
            apply IH in H₁₂; try tauto.
            - size_auto.
            - rewrite t_update_eq, Eqnbe; simpl. reflexivity. }
        × inversion H₁₂; subst; clear H₁₂.
          inversion H₁₀; subst; simpl.
          rewrite t_update_eq, Eqnbe; simpl. reflexivity.
  - (* ALoad *)
    destruct (P x) eqn:Eqnbe.
    + inversion Heval; subst; clear Heval.
      inversion H₁₀; subst; clear H₁₀.
      rewrite t_update_neq; [| tauto].
      inversion H₁; subst;
      try (rewrite t_update_neq; [assumption| tauto]).
    + inversion Heval; subst;
      try (rewrite t_update_neq; [assumption| tauto]).
Qed.

We need a few more lemmas before we prove backwards compiler correctness

Lemma eval_unused_update : ∀ X st n,
  (∀ ae, e_unused X ae →
    eval (X !-> n; st) ae = eval st ae).
Proof.
  intros X st n. induction ae; intros; simpl in *; try reflexivity.
  - rewrite t_update_neq; eauto.
  - destruct H.
    rewrite IHae1; [| tauto]. rewrite IHae2; [| tauto].
    reflexivity.
  - destruct H. destruct H₀.
    rewrite IHae1, IHae2, IHae3; auto.
Qed.

Lemma ideal_unused_overwrite: ∀ P st ast b ds c st' ast' b' os X n,
  unused X c →
  P ⊢i <(st , ast , b , ds )> =[ c ]=> <(st', ast', b', os )> →
  P ⊢i <(X !-> n; st , ast , b , ds )> =[ c ]=> <(X !-> n; st', ast', b', os )>.
Proof.
  intros P st ast b ds c st' ast' b' os X n Hu H.
  induction H; simpl in Hu.
  - (* Skip *) econstructor.
  - (* Asgn *)
    rewrite t_update_permute; [| tauto].
    econstructor. rewrite eval_unused_update; tauto.
  - (* Seq *)
    econstructor.
    + apply IHideal_eval1; tauto.
    + apply IHideal_eval2; tauto.
  - (* If *)
    rewrite <- eval_unused_update with (X:=X) (n:=n); [| tauto].
    econstructor.
    rewrite eval_unused_update; [ | tauto].
    destruct (eval st be) eqn:D; apply IHideal_eval; tauto.
  - (* If_F *)
    rewrite <- eval_unused_update with (X:=X) (n:=n); [| tauto].
    econstructor.
    rewrite eval_unused_update; [ | tauto].
    destruct (eval st be) eqn:D; apply IHideal_eval; tauto.
  - (* While *)
    econstructor. apply IHideal_eval. simpl; tauto.
  - (* ALoad *)
    rewrite t_update_permute; [| tauto]. econstructor; [ | assumption].
    rewrite eval_unused_update; tauto.
  - (* ALoad_U *)
    rewrite t_update_permute; [| tauto]. econstructor; try assumption.
    rewrite eval_unused_update; tauto.
  - (* AStore *)
    econstructor; try assumption.
    + rewrite eval_unused_update; tauto.
    + rewrite eval_unused_update; tauto.
  - (* AStore_U *)
    econstructor; try assumption.
    + rewrite eval_unused_update; tauto.
    + rewrite eval_unused_update; tauto.
Qed.

Lemma ideal_unused_update : ∀ P st ast b ds c st' ast' b' os X n,
  unused X c →
  P ⊢i <(X !-> n; st , ast , b , ds )> =[ c ]=> <(X !-> n; st', ast', b', os )> →
  P ⊢i <(st , ast , b , ds )> =[ c ]=> <(X !-> st X; st', ast', b', os )>.
Proof.
  intros P st ast b ds c st' ast' b' os X n Hu Heval.
  eapply ideal_unused_overwrite with (X:=X) (n:=(st X)) in Heval; [| assumption].
  do 2 rewrite t_update_shadow in Heval. rewrite t_update_same in Heval. assumption.
Qed.

Lemma ideal_unused_update_rev : ∀ P st ast b ds c st' ast' b' os X n,
  unused X c →
  P ⊢i <(st , ast , b , ds )> =[ c ]=> <(X!-> st X; st', ast', b', os )> →
  P ⊢i <(X !-> n; st , ast , b , ds )> =[ c ]=> <(X !-> n; st', ast', b', os )>.
Proof.
  intros P st ast b ds c st' ast' b' os X n Hu H.
  eapply ideal_unused_overwrite in H; [| eassumption].
  rewrite t_update_shadow in H. eassumption.
Qed.

The backwards compiler correctness proof uses size_ind:

Definition sel_slh_compiler_correctness_prop (c:com) (ds:dirs) : Prop :=
  ∀ P st ast (b: bool) st' ast' b' os,
  unused msf c →
  st msf = (if b then 1 else 0) →
  <(st , ast , b , ds )> =[ sel_slh P c ]=> <(st', ast', b', os )> →
  P ⊢i <(st , ast , b , ds )> =[ c ]=> <(msf !-> st msf; st', ast', b', os )>.

Lemma sel_slh_compiler_correctness : ∀ c ds,
sel_slh_compiler_correctness_prop c ds.
Proof.
apply size_ind. unfold sel_slh_compiler_correctness_prop.

  intros c ds IH P st ast b st' ast' b' os Hunused Hstb Heval.
  destruct c; simpl in *; inversion Heval; subst; clear Heval;
  try (destruct (P x); discriminate).
  - (* Skip *)
    rewrite t_update_same. apply Ideal_Skip.
  - (* Asgn *)
    rewrite t_update_permute; [| tauto].
    rewrite t_update_same.
    constructor. reflexivity.
  - (* Seq *)
    eapply Ideal_Seq.
    + apply IH in H₁; try tauto.
      × eassumption.
      × size_auto.
    + apply sel_slh_flag in H₁ as Hstb'0; try tauto.
      apply IH in H₁₀; try tauto.
      × eapply ideal_unused_update_rev; try tauto.
      × size_auto.
  (* IF *)
  - (* non-speculative *)
    destruct (eval st be) eqn:Eqnbe; inversion H₁₀;
    inversion H₁; subst; clear H₁₀; clear H₁; simpl in ×.
    + apply IH in H₁₁; try tauto.
      × rewrite <- Eqnbe. apply Ideal_If. rewrite Eqnbe in ×.
        rewrite t_update_same in H₁₁. apply H₁₁.
      × size_auto.
      × rewrite t_update_eq. rewrite Eqnbe. assumption.
    + (* analog to false case *)
      apply IH in H₁₁; try tauto.
      × rewrite <- Eqnbe. apply Ideal_If. rewrite Eqnbe in ×.
        rewrite t_update_same in H₁₁. apply H₁₁.
      × size_auto.
      × rewrite t_update_eq. rewrite Eqnbe. assumption.
  - (* speculative *)
    destruct (eval st be) eqn:Eqnbe; inversion H₁₀; inversion H₁;
    subst; simpl in *; clear H₁₀; clear H₁; rewrite Eqnbe in H₁₁.
    + rewrite <- Eqnbe. apply Ideal_If_F. rewrite Eqnbe. apply IH in H₁₁; try tauto.
      × rewrite t_update_eq in H₁₁.
        apply ideal_unused_update in H₁₁; try tauto.
      × size_auto.
    + (* analog to false case *)
      rewrite <- Eqnbe. apply Ideal_If_F. rewrite Eqnbe. apply IH in H₁₁; try tauto.
      × rewrite t_update_eq in H₁₁.
        apply ideal_unused_update in H₁₁; try tauto.
      × size_auto.
  - (* While *)
    eapply Ideal_While.
    inversion H₁; subst; clear H₁.
    inversion H₁₁; subst; clear H₁₁; simpl in ×.
    + (* non-speculative *)
      assert(Lnil: os₂ = [] ∧ ds₂ = []).
      { inversion H₁₀; subst; eauto. }
      destruct Lnil; subst; simpl.
      apply Ideal_If.
      destruct (eval st be) eqn:Eqnbe.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁₀; subst; clear H₁₀; simpl in ×.
        rewrite Eqnbe. do 2 rewrite t_update_same.
        apply Ideal_Skip.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁; subst; clear H₁.
        inversion H₂; subst; clear H₂; simpl in ×.
        assert(Hwhile: <(st'1, ast'1, b'1, ds₂)>
          =[ sel_slh P <{{while be do c end }}> ]=> <(st', ast', b', os₂)> ).
        { simpl. replace ds₂ with (ds₂ ++ [])%list by (rewrite app_nil_r; reflexivity).
          replace os₂ with (os₂ ++ [])%list by (rewrite app_nil_r; reflexivity).
          eapply Spec_Seq; eassumption. }
        do 2 rewrite app_nil_r. eapply Ideal_Seq.
        { rewrite Eqnbe in H₁₃. rewrite t_update_same in H₁₃.
          apply IH in H₁₃; try tauto.
          - eassumption.
          - size_auto. }
        { apply IH in Hwhile; auto.
          - eapply ideal_unused_update_rev; eauto.
          - size_auto.
          - apply sel_slh_flag in H₁₃; try tauto.
            rewrite t_update_eq. rewrite Eqnbe. assumption. }
    + (* speculative; analog to non_speculative *)
      assert(Lnil: os₂ = [] ∧ ds₂ = []).
      { inversion H₁₀; subst; eauto. }
      destruct Lnil; subst; simpl.
      apply Ideal_If_F.
      destruct (eval st be) eqn:Eqnbe.
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁; subst; clear H₁.
        inversion H₂; subst; clear H₂; simpl in ×.
        assert(Hwhile: <(st'1, ast'1, b'1, ds₂)>
          =[ sel_slh P <{{while be do c end }}> ]=> <(st', ast', b', os₂)> ).
        { simpl. replace ds₂ with (ds₂ ++ [])%list by (rewrite app_nil_r; reflexivity).
          replace os₂ with (os₂ ++ [])%list by (rewrite app_nil_r; reflexivity).
          eapply Spec_Seq; eassumption. }
        do 2 rewrite app_nil_r. eapply Ideal_Seq.
        { rewrite Eqnbe in H₁₃.
          apply IH in H₁₃; try tauto.
          - rewrite t_update_eq in H₁₃.
            apply ideal_unused_update in H₁₃; [| tauto].
            eassumption.
          - size_auto. }
        { apply IH in Hwhile; auto.
          - rewrite Eqnbe in H₁₃.
            apply IH in H₁₃; try tauto.
            + apply ideal_unused_update_rev; eauto.
            + size_auto.
          - size_auto.
          - apply sel_slh_flag in H₁₃; try tauto.
            rewrite Eqnbe. rewrite t_update_eq. reflexivity. }
      × inversion H₁₂; subst; clear H₁₂.
        inversion H₁₀; subst; clear H₁₀; simpl in ×.
        rewrite Eqnbe. rewrite t_update_shadow. rewrite t_update_same.
        apply Ideal_Skip.
  (* ALoad *)
  - (* Spec_ALoad; public *)
    destruct (P x) eqn:Heq; try discriminate H.
    injection H; intros; subst; clear H.
    inversion H₁; clear H₁; subst. rewrite <- app_nil_r in ×.
    inversion H₀; clear H₀; subst; simpl in ×.
    × (* Ideal_ALoad *)
      rewrite t_update_neq; [| tauto]. rewrite Hstb.
      rewrite t_update_shadow. rewrite t_update_permute; [| tauto].
      rewrite t_update_eq. simpl.
      rewrite <- Hstb at 1. rewrite t_update_same.
      replace (not_zero (bool_to_nat (negb (not_zero
        (if ((if b' then 1 else 0) =? 0)%nat then 1 else 0)) || not_zero 0))) with (b' && (P x))
          by (rewrite Heq; destruct b'; simpl; reflexivity).
        eapply Ideal_ALoad; eauto.
    × (* Ideal_ALoad_U *)
      rewrite t_update_neq; [| tauto]. rewrite Hstb.
      rewrite t_update_shadow. rewrite t_update_permute; [| tauto].
      simpl. rewrite <- Hstb at 1. rewrite t_update_same.
      replace (x !-> 0; st) with (x !-> if P x then 0 else nth i' (ast' a') 0; st)
        by (rewrite Heq; reflexivity).
      eapply Ideal_ALoad_U; eauto.
  - (* Spec_ALoad; secret*)
    destruct (P x) eqn:Heq; try discriminate H. inversion H; clear H; subst.
    rewrite t_update_permute; [| tauto]. rewrite t_update_same.
    replace (x !-> nth (eval st i) (ast' a) 0; st)
      with (x !-> if b' && P x then 0 else nth (eval st i) (ast' a) 0; st)
        by (rewrite Heq; destruct b'; reflexivity).
    eapply Ideal_ALoad; eauto.
  - (* Spec_ALoad_U *)
    destruct (P x) eqn:Heq; try discriminate H. inversion H; clear H; subst.
    rewrite t_update_permute; [| tauto]. rewrite t_update_same.
    replace (x !-> nth i' (ast' a') 0; st)
      with (x !-> if P x then 0 else nth i' (ast' a') 0; st)
        by (rewrite Heq; reflexivity).
    eapply Ideal_ALoad_U; eauto.
  (* AStore *)
  - (* Spec_AStore *)
    rewrite t_update_same. apply Ideal_AStore; tauto.
  - (* Spec_AStore_U *)
    rewrite t_update_same. apply Ideal_AStore_U; tauto.
Qed.

Speculative constant-time security for Selective SLH

Finally, we use compiler correctness and spec_ct_secure for the ideal semantics to prove spec_ct_secure for sel_slh.

Theorem sel_slh_spec_ct_secure :
  ∀ P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds,
  P ;; PA ⊢ct - c →
  unused msf c →
  st₁ msf = 0 →
  st₂ msf = 0 →
  pub_equiv P st₁ st₂ →
  pub_equiv PA ast1 ast2 →
  <(st₁ , ast1 , false , ds )> =[ sel_slh P c ]=> <(st₁', ast1', b₁', os₁ )> →
  <(st₂ , ast2 , false , ds )> =[ sel_slh P c ]=> <(st₂', ast2', b₂', os₂ )> →
  os₁ = os₂.
Proof.
  intros P PA c st₁ st₂ ast1 ast2 st₁' st₂' ast1' ast2' b₁' b₂' os₁ os₂ ds
    Hwt Hunused Hs1b Hs2b Hequiv Haequiv Heval1 Heval2.
  eapply sel_slh_compiler_correctness in Heval1; try assumption.
  eapply sel_slh_compiler_correctness in Heval2; try assumption.
  eapply ideal_spec_ct_secure; eauto.
Qed.

Monadic interpreter for speculative semantics (optional)

Module SpecCTInterpreter.

Since manually constructing directions for the proofs of examples is very time consuming, we introduce a sound monadic interpreter, which can be used to simplify the proofs of the examples.

Definition prog_st : Type := state × astate × bool × dirs × obs.

Inductive output_st (A : Type): Type :=
| OST_Error : output_st A
| OST_OutOfFuel : output_st A
| OST_Finished : A → prog_st → output_st A.

Definition evaluator (A : Type): Type := prog_st → (output_st A ).
Definition interpreter : Type := evaluator unit.

Definition ret {A : Type} (value : A) : evaluator A :=
fun (pst: prog_st) ⇒ OST_Finished A value pst.

Definition bind {A : Type} {B : Type} (e : evaluator A) (f : A → evaluator B): evaluator B :=
  fun (pst: prog_st) ⇒
    match e pst with
    | OST_Finished _ value (st', ast', b', ds', os₁) ⇒
        match (f value) (st', ast', b', ds', os₁) with
        | OST_Finished _ value (st'', ast'', b'', ds'', os₂) ⇒
            OST_Finished B value (st'', ast'', b'', ds'', os₂)
        | ret ⇒ ret
        end
    | OST_Error _ ⇒ OST_Error B
    | OST_OutOfFuel _ ⇒ OST_OutOfFuel B
    end.

Notation "e >>= f" := (bind e f) (at level 58, left associativity).
Notation "e >> f" := (bind e (fun _ ⇒ f)) (at level 58, left associativity).

Helper functions for individual instructions

Definition finish : interpreter := ret tt.

Definition get_var (name : string): evaluator nat :=
  fun (pst : prog_st) ⇒
    let
      '(st, _, _, _, _) := pst
    in
      ret (st name) pst.

Definition set_var (name : string) (value : nat) : interpreter :=
  fun (pst: prog_st) ⇒
    let
      '(st, ast, b, ds, os) := pst
    in
      let
        new_st := (name !-> value; st)
      in
        finish (new_st , ast, b, ds, os).

Definition get_arr (name : string): evaluator (list nat) :=
  fun (pst: prog_st) ⇒
    let
      '(_, ast, _, _, _) := pst
    in
      ret (ast name) pst.

Definition set_arr (name : string) (value : list nat) : interpreter :=
  fun (pst : prog_st) ⇒
    let '(st, ast, b, ds, os) := pst in
    let new_ast := (name !-> value ; ast) in
    finish (st, new_ast , b, ds, os).

Definition start_speculating : interpreter :=
  fun (pst : prog_st) ⇒
    let '(st, ast, _, ds, os) := pst in
    finish (st, ast, true , ds, os).

Definition is_speculating : evaluator bool :=
  fun (pst : prog_st) ⇒
    let '(_, _, b, _, _) := pst in
    ret b pst.

Definition eval_exp (a : exp) : evaluator nat :=
  fun (pst: prog_st) ⇒
    let '(st, _, _, _, _) := pst in
    let v := eval st a in
    ret v pst.

Definition raise_error : interpreter :=
fun _ ⇒ OST_Error unit.

Definition observe (o : observation) : interpreter :=
  fun (pst : prog_st) ⇒
    let '(st, ast, b, ds, os) := pst in
    OST_Finished unit tt (st, ast, b, ds, (os ++ [o ])%list).

Definition fetch_direction : evaluator (option direction) :=
  fun (pst : prog_st) ⇒
    let '(st, ast, b, ds, os) := pst in
    match ds with
    | d::ds' ⇒
        ret (Some d) (st, ast, b, ds', os)
    | [] ⇒ ret None (st, ast, b, [], os)
    end.

The actual speculative interpreter

Fixpoint spec_eval_engine_aux (fuel : nat) (c : com) : interpreter :=
  match fuel with
  | O ⇒ fun _ ⇒ OST_OutOfFuel unit
  | S fuel ⇒
    match c with
    | <{ skip }> ⇒ finish
    | <{ x := e }> ⇒ eval_exp e >>= fun v ⇒ set_var x v
    | <{ c₁ ; c₂ }> ⇒
        spec_eval_engine_aux fuel c₁ >>
        spec_eval_engine_aux fuel c₂
    | <{ if be then ct else cf end }> ⇒
        eval_exp be >>= fun bool_value ⇒
          observe (OBranch (not_zero bool_value)) >> fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if not_zero bool_value then spec_eval_engine_aux fuel ct
              else spec_eval_engine_aux fuel cf
          | Some DForce ⇒
              start_speculating >>
              if not_zero bool_value then spec_eval_engine_aux fuel cf
              else spec_eval_engine_aux fuel ct
          | _ ⇒ raise_error
          end
    | <{ while be do c end }> ⇒
        spec_eval_engine_aux fuel <{if be then c ; while be do c end else skip end }>
    | <{ x <- a[[ie]] }> ⇒
        eval_exp ie >>= fun i ⇒ observe (OALoad a i) >> get_arr a >>=
        fun arr_a ⇒ is_speculating >>= fun b ⇒ fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if (i <? List.length arr_a)%nat then set_var x (nth i arr_a 0)
              else raise_error
          | Some (DLoad a' i') ⇒
              get_arr a' >>= fun arr_a' ⇒
                if negb (i <? List.length arr_a)%nat && (i' <? List.length arr_a')%nat && b then
                  set_var x (nth i' arr_a' 0)
                else raise_error
          | _ ⇒ raise_error
          end
    | <{ a[ie] <- e }> ⇒
        eval_exp ie >>= fun i ⇒ observe (OAStore a i) >> get_arr a >>=
        fun arr_a ⇒ eval_exp e >>= fun n ⇒ is_speculating >>= fun b ⇒ fetch_direction >>=
        fun dop ⇒
          match dop with
          | Some DStep ⇒
              if (i <? List.length arr_a)%nat then set_arr a (upd i arr_a n)
              else raise_error
          | Some (DStore a' i') ⇒
              get_arr a' >>= fun arr_a' ⇒
                if negb (i <? List.length arr_a)%nat && (i' <? List.length arr_a')%nat && b then
                  set_arr a' (upd i' arr_a' n)
                else raise_error
          | _ ⇒ raise_error
          end
    end
end.

Definition compute_fuel (c :com) (ds :dirs) : nat :=
  2 +
    match ds with
    | [] ⇒ com_size c
    | _ ⇒ length ds × com_size c
    end.

Definition spec_eval_engine (c : com) (st : state) (ast : astate) (b : bool) (ds : dirs)
      : option (state × astate × bool × obs) :=
    match spec_eval_engine_aux (compute_fuel c ds) c (st , ast , b , ds , []) with
    | OST_Finished _ _ (st', ast', b', ds', os) ⇒
        if ((length ds') =? 0)%nat then Some (st', ast', b', os)
        else None
    | _ ⇒ None
    end.

Soundness of the interpreter

Lemma ltb_reflect : ∀ n m :nat,
reflect (n < m) (n <? m)%nat.
Proof.
intros n m. apply iff_reflect. rewrite ltb_lt. reflexivity.
Qed.

Lemma eqb_reflect: ∀ n m :nat,
reflect (n = m ) (n =? m)%nat.
Proof.
intros n m. apply iff_reflect. rewrite eqb_eq. reflexivity.
Qed.

Lemma spec_eval_engine_aux_sound : ∀ n c st ast b ds os st' ast' b' ds' os' u,
  spec_eval_engine_aux n c (st , ast , b , ds , os )
    = OST_Finished unit u (st', ast', b', ds', os') →
  (∃ dsn osn ,
  (dsn ++ds')%list = ds ∧ (os ++osn)%list = os' ∧
      <(st , ast , b , dsn )> =[ c ]=> <(st', ast', b', osn )> ).
Proof.
  induction n as [| n' IH]; intros c st ast b ds os st' ast' b' ds' os' u Haux;
  simpl in Haux; [discriminate |].
  destruct c as [| X e | c₁ c₂ | be ct cf | be cw | X a ie | a ie e ] eqn:Eqnc;
  unfold ">>=" in Haux; simpl in Haux.
  - (* Skip *)
    inversion Haux; subst.
    ∃ []; ∃ []; split;[| split].
    + reflexivity.
    + rewrite app_nil_r. reflexivity.
    + apply Spec_Skip.
  - (* Asgn *)
    simpl in Haux. inversion Haux; subst.
    ∃ []; ∃ []; split;[| split].
    + reflexivity.
    + rewrite app_nil_r. reflexivity.
    + apply Spec_Asgn. reflexivity.
  - destruct (spec_eval_engine_aux _ c₁ _) eqn:Hc₁;
    try discriminate; simpl in Haux.
    destruct p as [ [ [ [stm astm] bm] dsm] osm]; simpl in Haux.
    destruct (spec_eval_engine_aux _ c₂ _) eqn:Hc₂;
    try discriminate; simpl in Haux.
    destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
    apply IH in Hc₁. destruct Hc₁ as [ds₁ [ os₁ [Hds1 [Hos1 Heval1] ] ] ].
    apply IH in Hc₂. destruct Hc₂ as [ds₂ [ os₂ [Hds2 [Hos2 Heval2] ] ] ].
    inversion Haux; subst. ∃ (ds₁++ds₂)%list; ∃ (os₁++os₂)%list;
    split; [| split].
    + rewrite <- app_assoc. reflexivity.
    + rewrite <- app_assoc. reflexivity.
    + eapply Spec_Seq; eauto.
  - (* IF *)
    destruct ds as [| d ds_tl] eqn:Eqnds; simpl in Haux; try discriminate.
    destruct d eqn:Eqnd; try discriminate; simpl in Haux.
    + (* DStep *)
      destruct (eval st be) eqn:Eqnbe.
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' cf (st, ast, b, ds_tl, (os ++ [OBranch false ])%list)) eqn:Hcf;
        try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hcf.
        destruct Hcf as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DStep :: dst); ∃ ([OBranch false ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_eval_O; [| eassumption].
          apply Spec_If. rewrite Eqnbe. apply Heval. }
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' ct (st, ast, b, ds_tl, (os ++ [OBranch true ])%list)) eqn:Hct;
        try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hct.
        destruct Hct as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DStep :: dst); ∃ ([OBranch true ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_eval_S; [| eassumption].
          apply Spec_If. rewrite Eqnbe. apply Heval. }
    + (* DForce *)
      destruct (eval st be) eqn:Eqnbe.
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' ct (st, ast, true , ds_tl, (os ++ [OBranch false ])%list)) eqn:Hcf;
        try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hcf.
        destruct Hcf as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DForce :: dst); ∃ ([OBranch false ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_eval_O; [| eassumption].
          apply Spec_If_F. rewrite Eqnbe. apply Heval. }
      × unfold obs, dirs, not_zero in Haux. simpl in Haux.
        destruct (spec_eval_engine_aux n' cf (st, ast, true , ds_tl, (os ++ [OBranch true ])%list)) eqn:Hct; try discriminate; simpl in Haux.
        destruct p as [ [ [ [stt astt] bt] dst] ost]; simpl in Haux.
        inversion Haux; subst. apply IH in Hct.
        destruct Hct as [dst [ ost [Hds [Hos Heval] ] ] ].
        ∃ (DForce :: dst); ∃ ([OBranch true ]++ost)%list; split;[| split].
        { simpl. rewrite Hds. reflexivity. }
        { rewrite app_assoc. rewrite Hos. reflexivity. }
        { erewrite <- not_zero_eval_S; [| eassumption].
          apply Spec_If_F. rewrite Eqnbe. apply Heval. }
  - (* While *)
    apply IH in Haux. destruct Haux as [dst [ ost [Hds [Hos Heval] ] ] ].
    ∃ dst; ∃ ost; split; [| split]; eauto.
  - (* ALoad *)
    destruct ds as [| d ds_tl] eqn:Eqnds; simpl in Haux; try discriminate.
    destruct d eqn:Eqnd; try discriminate; simpl in Haux.
    + (* DStep *)
      destruct (eval st ie <? Datatypes.length (ast a))%nat eqn:Eqnindex; try discriminate.
      destruct (observe (OALoad a (eval st ie)) (st, ast, b, ds_tl, os)) eqn:Eqbobs; try discriminate;
      simpl in Haux. inversion Haux; subst.
      eexists [DStep ]; eexists [OALoad a (eval st ie)]; split;[| split]; try reflexivity.
      eapply Spec_ALoad; eauto. destruct (ltb_reflect (eval st ie) (length (ast' a))) as [Hlt | Hgeq].
      × apply Hlt.
      × discriminate.
    + (* DForce *)
      destruct (negb (eval st ie <? Datatypes.length (ast a))%nat) eqn:Eqnindex1;
      destruct ((i <? Datatypes.length (ast a₀))%nat) eqn:Eqnindex2;
      destruct b eqn:Eqnb; try discriminate; simpl in Haux. inversion Haux; subst.
      eexists [DLoad a₀ i ]; eexists [OALoad a (eval st ie)]; split;[| split]; try reflexivity.
      eapply Spec_ALoad_U; eauto.
      × destruct (ltb_reflect (eval st ie) (length (ast' a))) as [Hlt | Hgeq].
        { discriminate. }
        { apply not_lt in Hgeq. apply Hgeq. }
      × destruct (ltb_reflect i (length (ast' a₀))) as [Hlt | Hgeq].
        { apply Hlt. }
        { discriminate. }
  - (* AStore *)
  destruct ds as [| d ds_tl] eqn:Eqnds; simpl in Haux; try discriminate.
  destruct d eqn:Eqnd; try discriminate; simpl in Haux.
  + (* DStep *)
    destruct ((eval st ie <? Datatypes.length (ast a))%nat) eqn:Eqnindex; try discriminate.
    destruct (observe (OAStore a (eval st ie)) (st, ast, b, ds_tl, os)) eqn:Eqbobs; try discriminate;
    simpl in Haux. inversion Haux; subst.
    eexists [DStep ]; eexists [OAStore a (eval st' ie)]; split;[| split]; try reflexivity.
    eapply Spec_AStore; eauto. destruct (ltb_reflect (eval st' ie) (length (ast a))) as [Hlt | Hgeq].
    × apply Hlt.
    × discriminate.
  + (* DForce *)
    destruct (negb (eval st ie <? Datatypes.length (ast a))%nat) eqn:Eqnindex1;
    destruct (i <? Datatypes.length (ast a₀))%nat eqn:Eqnindex2;
    destruct b eqn:Eqnb; try discriminate; simpl in Haux. inversion Haux; subst.
    eexists [DStore a₀ i]; eexists [OAStore a (eval st' ie)]; split;[| split]; try reflexivity.
    eapply Spec_AStore_U; eauto.
    × destruct (ltb_reflect (eval st' ie) (length (ast a))) as [Hlt | Hgeq].
      { discriminate. }
      { apply not_lt in Hgeq. apply Hgeq. }
    × destruct (ltb_reflect i (length (ast a₀))) as [Hlt | Hgeq].
      { apply Hlt. }
      { discriminate. }
Qed.

Theorem spec_eval_engine_sound: ∀ c st ast b ds st' ast' b' os',
  spec_eval_engine c st ast b ds = Some (st', ast', b', os') →
  <(st , ast , b , ds )> =[ c ]=> <(st', ast', b', os')> .
Proof.
  intros c st ast b ds st' ast' b' os' Hengine.
  unfold spec_eval_engine in Hengine.
  destruct (spec_eval_engine_aux _ c _) eqn:Eqnaux;
  try discriminate. destruct p as [ [ [ [stt astt] bt] dst] ost].
  destruct ((Datatypes.length dst =? 0)%nat) eqn:Eqnds; try discriminate.
  apply spec_eval_engine_aux_sound in Eqnaux.
  destruct Eqnaux as [dsn [osn [Hdsn [Hosn Heval] ] ] ].
  inversion Hengine; subst. rewrite app_nil_l.
  destruct (eqb_reflect (length dst) 0) as [Heq | Hneq].
  + apply length_zero_iff_nil in Heq. rewrite Heq. rewrite app_nil_r. apply Heval.
  + discriminate.
Qed.

Back to showing that our example is not speculative constant-time

Example spec_insecure_prog_2_is_ct_and_spec_insecure :
  XYZpub ;; APpub ⊢ct - spec_insecure_prog_2 ∧
  ¬ (spec_ct_secure XYZpub APpub spec_insecure_prog_2 ) .
Proof.
  split; unfold spec_insecure_prog_2.
  (* program satisfies cct_well_typed. *)
  - apply CCT_Seq.
    + eapply CCT_Asgn; auto.
    + apply CCT_Seq.
      × eapply CCT_Asgn; auto.
      × eapply CCT_Seq.
        { apply CCT_While.
          - rewrite <- join_public_l. apply T_Bin; auto.
            + rewrite <- join_public_l. apply T_Bin; auto.
            + unfold BFalse. auto.
          - eapply CCT_Seq.
            + eapply CCT_ALoad; auto.
            + eapply CCT_Seq.
              × eapply CCT_Asgn with (l:= public).
                { rewrite <- join_public_l.
                  eapply T_Bin; auto. }
                { reflexivity. }
              × eapply CCT_Asgn with (l:= public).
                { rewrite <- join_public_l.
                  eapply T_Bin; auto. }
                { reflexivity. } }
        { apply CCT_If; auto.
          - rewrite <- join_public_l.
            eapply T_Bin; auto.
          - eapply CCT_Asgn; auto. }
  (* program is insecure under speculative execution. *)
  - remember (_ !-> 0) as st.
    remember (AP!-> [0;1;2]; AS !-> [0;0;0;0]; _ !-> []) as ast1.
    remember (AP!-> [0;1;2]; AS !-> [4;5;6;7]; _ !-> []) as ast2.
    remember ([DStep ; DStep ; DStep ; DStep ; DStep ; DStep ; DForce ; DLoad AS 3; DStep ; DStep ]) as ds.
    intros Hsecure.
    assert (L: ∃ stt1 astt1 bt₁ os₁ stt2 astt2 bt₂ os₂ ,
      <(st, ast1, false , ds )> =[ spec_insecure_prog_2 ]=> <( stt1 , astt1 , bt₁ , os₁ )> ∧
      <(st, ast2, false , ds )> =[ spec_insecure_prog_2 ]=> <( stt2 , astt2 , bt₂ , os₂ )> ∧
      os₁ ≠ os₂ ).
    { eexists; eexists; eexists; eexists; eexists; eexists; eexists; eexists.
      split; [| split].
      - apply spec_eval_engine_sound. unfold spec_insecure_prog_2, spec_eval_engine;
        subst; simpl; reflexivity.
      - apply spec_eval_engine_sound. unfold spec_insecure_prog_2, spec_eval_engine;
        subst; simpl; reflexivity.
      - intros Contra; inversion Contra. }
    destruct L as [stt1 [astt1 [bt₁ [os₁ [stt2 [astt2 [bt₂ [os₂ [Heval1 [Heval2 Hneq] ] ] ] ] ] ] ] ] ].
    eapply Hsecure in Heval1; eauto.
    + apply pub_equiv_refl.
    + subst. apply pub_equiv_update_public; auto.
      apply pub_equiv_update_secret; auto.
      apply pub_equiv_refl.
Qed.

End SpecCTInterpreter.

(* 2025-07-17 19:00 *)