HypreSpectre.Leak

Leakage models

From HypreSpectre Require Import Lang.
From Coq Require Import EquivDec.

Low Equivalence

Note that this only serves to illustrate how our definitions relate to the established notion of noninterference. We never use low equivalence in this development, as we never prove noninterference.
Definition low_eq (h1 h2: heap) := forall a, (a > 0)%Z -> alist_find decZ a h1 = alist_find decZ a h2.

Observations

Across our leakage models, here are all the various observations that can be produced.
Inductive observation : Type :=
  | BranchTrue
  | BranchFalse
  | WhileHeader
  | ReadAddress (a : Z)
  | WritePublicAddress (a v : Z)
  | WriteSecretAddress (a : Z)
  | Termination.

Equality of observations is decidable.
Lemma eqDec_obs:
EquivDec.EqDec observation eq.
Proof.
  unfold EquivDec.EqDec, equiv, complement. destruct x, y; try (now left); try now right.
  - destruct (Z.eq_dec a a0). left. now rewrite e. right. inversion 1. contradiction.
  - destruct (Z.eq_dec v v0), (Z.eq_dec a a0); try (right; inversion 1; contradiction). left. now rewrite e, e0.
  - destruct (Z.eq_dec a a0). left. now rewrite e. right. inversion 1. contradiction.
Qed.

Constant-Time Leakage Model

Definition leak_ct (s : state) : option observation
  := match s with
     | (V, H, s) => match s with
                    | nil => Some Termination
                    | s :: l => match s with
                                | Read x a => Some (ReadAddress (eval_expr_fun a V))
                                | Write x a => let a' := eval_expr_fun a V in
                                    match (Z_lt_dec a' 0) with
                                    | left _ => Some (WriteSecretAddress a')
                                    | right _ => match (alist_find _ x V) with
                                                 | Some v => Some (WritePublicAddress a' v)
                                                 | None => Some (WritePublicAddress a' 0)
                                                 end
                                    end
                                | If i t e => let i' := eval_expr_fun i V in
                                    match (Z.eq_dec i' 0) with
                                    | left _ => Some BranchFalse
                                    | right _ => Some BranchTrue
                                    end
                                | _ => None
                                end
                    end
     end.

Definition leak_ct' (sl : list specstate) : option observation
  := match sl with
     | nil => Some Termination
     | s :: l => match s with
                 | (Some 0, _, _, _) => None
                 | (Some _, _, _, nil) => None
                 | (None, V, H, nil) => Some Termination
                 | (_, V, H, s :: l) => match s with
                                        | Read x a => Some (ReadAddress (eval_expr_fun a V))
                                        | Write x a => let a' := eval_expr_fun a V in
                                            match (Z_lt_dec a' 0) with
                                            | left _ => Some (WriteSecretAddress a')
                                            | right _ => match (alist_find _ x V) with
                                                         | Some v => Some (WritePublicAddress a' v)
                                                         | None => Some (WritePublicAddress a' 0)
                                                         end
                                            end
                                        | If i t e => let i' := eval_expr_fun i V in
                                            match (Z.eq_dec i' 0) with
                                            | left _ => Some BranchFalse
                                            | right _ => Some BranchTrue
                                            end
                                        | _ => None
                                        end
                 end
     end.

Loops + Memory Leakage Model

Definition leak_lm (s : state) : option observation
  := match s with
     | (V, H, s) => match s with
                    | nil => Some Termination
                    | s :: l => match s with
                                | Read x a => Some (ReadAddress (eval_expr_fun a V))
                                | Write x a => let a' := eval_expr_fun a V in
                                    match (Z_lt_dec a' 0) with
                                    | left _ => Some (WriteSecretAddress a')
                                    | right _ => match (alist_find _ x V) with
                                                 | Some v => Some (WritePublicAddress a' v)
                                                 | None => Some (WritePublicAddress a' 0)
                                                 end
                                    end
                                | While _ _ _ => Some WhileHeader
                                | _ => None
                                end
                    end
     end.

Definition leak_lm' (sl : list specstate) : option observation
  := match sl with
     | nil => Some Termination
     | s :: l => match s with
                 | (Some 0, _, _, _) => None
                 | (Some _, _, _, nil) => None
                 | (None, V, H, nil) => Some Termination
                 | (_, V, H, s :: l) => match s with
                                        | Read x a => Some (ReadAddress (eval_expr_fun a V))
                                        | Write x a => let a' := eval_expr_fun a V in
                                            match (Z_lt_dec a' 0) with
                                            | left _ => Some (WriteSecretAddress a')
                                            | right _ => match (alist_find _ x V) with
                                                         | Some v => Some (WritePublicAddress a' v)
                                                         | None => Some (WritePublicAddress a' 0)
                                                         end
                                            end
                                        | While _ _ _ => Some WhileHeader
                                        | _ => None
                                        end
                 end
     end.

Memory-only Leakage Model

Definition leak_mem (s : state) : option observation
  := match s with
     | (V, H, s) => match s with
                    | nil => Some Termination
                    | s :: l => match s with
                                | Read x a => Some (ReadAddress (eval_expr_fun a V))
                                | Write x a => let a' := eval_expr_fun a V in
                                    match (Z_lt_dec a' 0) with
                                    | left _ => Some (WriteSecretAddress a')
                                    | right _ => match (alist_find _ x V) with
                                                 | Some v => Some (WritePublicAddress a' v)
                                                 | None => Some (WritePublicAddress a' 0)
                                                 end
                                    end
                                | _ => None
                                end
                    end
     end.

Definition leak_mem' (sl : list specstate) : option observation
  := match sl with
     | nil => Some Termination
     | s :: l => match s with
                 | (Some 0, _, _, _) => None
                 | (Some _, _, _, nil) => None
                 | (None, V, H, nil) => Some Termination
                 | (_, V, H, s :: l) => match s with
                                        | Read x a => Some (ReadAddress (eval_expr_fun a V))
                                        | Write x a => let a' := eval_expr_fun a V in
                                            match (Z_lt_dec a' 0) with
                                            | left _ => Some (WriteSecretAddress a')
                                            | right _ => match (alist_find _ x V) with
                                                         | Some v => Some (WritePublicAddress a' v)
                                                         | None => Some (WritePublicAddress a' 0)
                                                         end
                                            end
                                        | _ => None
                                        end
                 end
     end.