Theory Security

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
section ‹Definition of the SIFUM-Security Property›

theory Security
imports Main Preliminaries
begin

context sifum_security begin

subsection ‹Evaluation of Concurrent Programs›

abbreviation eval_abv :: "('Com, 'Var, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl "↝" 70)
  where
  "x ↝ y ≡ (x, y) ∈ eval"

abbreviation conf_abv :: "'Com ⇒ 'Var Mds ⇒ ('Var, 'Val) Mem ⇒ (_,_,_) LocalConf"
  ("⟨_, _, _⟩" [0, 0, 0] 1000)
  where
  "⟨ c, mds, mem ⟩ ≡ ((c, mds), mem)"

(* Evaluation of global configurations: *)
inductive_set meval :: "(_,_,_) GlobalConf rel"
  and meval_abv :: "_ ⇒ _ ⇒ bool" (infixl "→" 70)
  where
  "conf → conf' ≡ (conf, conf') ∈ meval" |
  meval_intro [iff]: "⟦ (cms ! n, mem) ↝ (cm', mem'); n < length cms ⟧ ⟹
  ((cms, mem), (cms [n := cm'], mem')) ∈ meval"

inductive_cases meval_elim [elim!]: "((cms, mem), (cms', mem')) ∈ meval"

(* Syntactic sugar for the reflexive-transitive closure of meval: *)
abbreviation meval_clos :: "_ ⇒ _ ⇒ bool" (infixl "→*" 70)
  where
  "conf →* conf' ≡ (conf, conf') ∈ meval*"

fun lc_set_var :: "(_, _, _) LocalConf ⇒ 'Var ⇒ 'Val ⇒ (_, _, _) LocalConf"
  where
  "lc_set_var (c, mem) x v = (c, mem (x := v))"

fun meval_k :: "nat ⇒ ('Com, 'Var, 'Val) GlobalConf ⇒ (_, _, _) GlobalConf ⇒ bool"
  where
  "meval_k 0 c c' = (c = c')" |
  "meval_k (Suc n) c c' = (∃ c''. meval_k n c c'' ∧ c'' → c')"

(* k steps of evaluation (for global configurations: *)
abbreviation meval_k_abv :: "nat ⇒ (_, _, _) GlobalConf ⇒ (_, _, _) GlobalConf ⇒ bool"
  ("_ →ı _" [100, 100] 80)
  where
  "gc →⇘k ⇙gc' ≡ meval_k k gc gc'"

subsection ‹Low-equivalence and Strong Low Bisimulations›

(* Low-equality between memory states: *)
definition low_eq :: "('Var, 'Val) Mem ⇒ (_, _) Mem ⇒ bool" (infixl "=l" 80)
  where
  "mem1 =l mem2 ≡ (∀ x. dma x = Low ⟶ mem1 x = mem2 x)"

(* Low-equality modulo a given mode state: *)
definition low_mds_eq :: "'Var Mds ⇒ ('Var, 'Val) Mem ⇒ (_, _) Mem ⇒ bool"
  ("_ =ıl _" [100, 100] 80)
  where
  "(mem1 =⇘mds⇙l mem2) ≡ (∀ x. dma x = Low ∧ x ∉ mds AsmNoRead ⟶ mem1 x = mem2 x)"

(* Initial mode state: *)
definition "mdss" :: "'Var Mds" where
  "mdss x = {}"

lemma [simp]: "mem =l mem' ⟹ mem =⇘mds⇙l mem'"
  by (simp add: low_mds_eq_def low_eq_def)

lemma [simp]: "(∀ mds. mem =⇘mds⇙l mem') ⟹ mem =l mem'"
  by (auto simp: low_mds_eq_def low_eq_def)

(* Closedness under globally consistent changes: *)
definition closed_glob_consistent :: "(('Com, 'Var, 'Val) LocalConf) rel ⇒ bool"
  where
  "closed_glob_consistent ℛ =
  (∀ c1 mds mem1 c2 mem2. (⟨ c1, mds, mem1 ⟩, ⟨ c2, mds, mem2 ⟩) ∈ ℛ ⟶
   (∀ x. ((dma x = High ∧ x ∉ mds AsmNoWrite) ⟶
           (∀ v1 v2. (⟨ c1, mds, mem1 (x := v1) ⟩, ⟨ c2, mds, mem2 (x := v2) ⟩) ∈ ℛ)) ∧
         ((dma x = Low ∧ x ∉ mds AsmNoWrite) ⟶
           (∀ v. (⟨ c1, mds, mem1 (x := v) ⟩, ⟨ c2, mds, mem2 (x := v) ⟩) ∈ ℛ))))"

(* Strong low bisimulations modulo modes: *)
definition strong_low_bisim_mm :: "(('Com, 'Var, 'Val) LocalConf) rel ⇒ bool"
  where
  "strong_low_bisim_mm ℛ ≡
  sym ℛ ∧
  closed_glob_consistent ℛ ∧
  (∀ c1 mds mem1 c2 mem2. (⟨ c1, mds, mem1 ⟩, ⟨ c2, mds, mem2 ⟩) ∈ ℛ ⟶
   (mem1 =⇘mds⇙l mem2) ∧
   (∀ c1' mds' mem1'. ⟨ c1, mds, mem1 ⟩ ↝ ⟨ c1', mds', mem1' ⟩ ⟶
    (∃ c2' mem2'. ⟨ c2, mds, mem2 ⟩ ↝ ⟨ c2', mds', mem2' ⟩ ∧
                  (⟨ c1', mds', mem1' ⟩, ⟨ c2', mds', mem2' ⟩) ∈ ℛ)))"

inductive_set mm_equiv :: "(('Com, 'Var, 'Val) LocalConf) rel"
  and mm_equiv_abv :: "('Com, 'Var, 'Val) LocalConf ⇒ 
  ('Com, 'Var, 'Val) LocalConf ⇒ bool" (infix "≈" 60)
  where
  "mm_equiv_abv x y ≡ (x, y) ∈ mm_equiv" |
  mm_equiv_intro [iff]: "⟦ strong_low_bisim_mm ℛ ; (lc1, lc2) ∈ ℛ ⟧ ⟹ (lc1, lc2) ∈ mm_equiv"

inductive_cases mm_equiv_elim [elim]: "⟨ c1, mds, mem1 ⟩ ≈ ⟨ c2, mds, mem2 ⟩"

definition low_indistinguishable :: "'Var Mds ⇒ 'Com ⇒ 'Com ⇒ bool"
  ("_ ∼ı _" [100, 100] 80)
  where "c1 ∼⇘mds⇙ c2 = (∀ mem1 mem2. mem1 =⇘mds⇙l mem2 ⟶
    ⟨ c1, mds, mem1 ⟩ ≈ ⟨ c2, mds, mem2 ⟩)"

subsection ‹SIFUM-Security›

(* SIFUM-security for commands: *)
definition com_sifum_secure :: "'Com ⇒ bool"
  where "com_sifum_secure c = c ∼⇘mdss⇙ c"

definition add_initial_modes :: "'Com list ⇒ ('Com × 'Var Mds) list"
  where "add_initial_modes cmds = zip cmds (replicate (length cmds) mdss)"

definition no_assumptions_on_termination :: "'Com list ⇒ bool"
  where "no_assumptions_on_termination cmds =
  (∀ mem mem' cms'.
    (add_initial_modes cmds, mem) →* (cms', mem') ∧
    list_all (λ c. c = stop) (map fst cms') ⟶
      (∀ mds' ∈ set (map snd cms'). mds' AsmNoRead = {} ∧ mds' AsmNoWrite = {}))"

(* SIFUM-security for programs: *)
definition prog_sifum_secure :: "'Com list ⇒ bool"
  where "prog_sifum_secure cmds =
  (no_assumptions_on_termination cmds ∧
   (∀ mem1 mem2. mem1 =l mem2 ⟶
    (∀ k cms1' mem1'.
     (add_initial_modes cmds, mem1) →⇘k⇙ (cms1', mem1') ⟶
      (∃ cms2' mem2'. (add_initial_modes cmds, mem2) →⇘k⇙ (cms2', mem2') ∧
                      map snd cms1' = map snd cms2' ∧
                      length cms2' = length cms1' ∧
                      (∀ x. dma x = Low ∧ (∀ i < length cms1'.
                        x ∉ snd (cms1' ! i) AsmNoRead) ⟶ mem1' x = mem2' x)))))"

subsection ‹Sound Mode Use›

definition doesnt_read :: "'Com ⇒ 'Var ⇒ bool"
  where
  "doesnt_read c x = (∀ mds mem c' mds' mem'.
  ⟨ c, mds, mem ⟩ ↝ ⟨ c', mds', mem' ⟩ ⟶
  ((∀ v. ⟨ c, mds, mem (x := v) ⟩ ↝ ⟨ c', mds', mem' (x := v) ⟩) ∨
   (∀ v. ⟨ c, mds, mem (x := v) ⟩ ↝ ⟨ c', mds', mem' ⟩)))"

definition doesnt_modify :: "'Com ⇒ 'Var ⇒ bool"
  where
  "doesnt_modify c x = (∀ mds mem c' mds' mem'. (⟨ c, mds, mem ⟩ ↝ ⟨ c', mds', mem' ⟩) ⟶
                        mem x = mem' x)"

(* Local reachability of local configurations: *)
inductive_set loc_reach :: "('Com, 'Var, 'Val) LocalConf ⇒ ('Com, 'Var, 'Val) LocalConf set"
  for lc :: "(_, _, _) LocalConf"
  where
  refl : "⟨fst (fst lc), snd (fst lc), snd lc⟩ ∈ loc_reach lc" |
  step : "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach lc;
            ⟨c', mds', mem'⟩ ↝ ⟨c'', mds'', mem''⟩ ⟧ ⟹
          ⟨c'', mds'', mem''⟩ ∈ loc_reach lc" |
  mem_diff : "⟦ ⟨ c', mds', mem' ⟩ ∈ loc_reach lc;
                (∀ x ∈ mds' AsmNoWrite. mem' x = mem'' x) ⟧ ⟹
              ⟨ c', mds', mem'' ⟩ ∈ loc_reach lc"

definition locally_sound_mode_use :: "(_, _, _) LocalConf ⇒ bool"
  where
  "locally_sound_mode_use lc =
  (∀ c' mds' mem'. ⟨ c', mds', mem' ⟩ ∈ loc_reach lc ⟶
    (∀ x. (x ∈ mds' GuarNoRead ⟶ doesnt_read c' x) ∧
          (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)))"

definition compatible_modes :: "('Var Mds) list ⇒ bool"
  where
  "compatible_modes mdss = (∀ (i :: nat) x. i < length mdss ⟶
    (x ∈ (mdss ! i) AsmNoRead ⟶
     (∀ j < length mdss. j ≠ i ⟶ x ∈ (mdss ! j) GuarNoRead)) ∧
    (x ∈ (mdss ! i) AsmNoWrite ⟶
     (∀ j < length mdss. j ≠ i ⟶ x ∈ (mdss ! j) GuarNoWrite)))"

definition reachable_mode_states :: "('Com, 'Var, 'Val) GlobalConf ⇒ (('Var Mds) list) set"
  where "reachable_mode_states gc =
  {mdss. (∃ cms' mem'. gc →* (cms', mem') ∧ map snd cms' = mdss)}"

definition globally_sound_mode_use :: "('Com, 'Var, 'Val) GlobalConf ⇒ bool"
  where "globally_sound_mode_use gc =
  (∀ mdss. mdss ∈ reachable_mode_states gc ⟶ compatible_modes mdss)"

primrec sound_mode_use :: "(_, _, _) GlobalConf ⇒ bool"
  where
  "sound_mode_use (cms, mem) =
     (list_all (λ cm. locally_sound_mode_use (cm, mem)) cms ∧
      globally_sound_mode_use (cms, mem))"

(* We now show that mm_equiv itself forms a strong low bisimulation modulo modes: *)
lemma mm_equiv_sym:
  assumes equivalent: "⟨c1, mds1, mem1⟩ ≈ ⟨c2, mds2, mem2⟩"
  shows "⟨c2, mds2, mem2⟩ ≈ ⟨c1, mds1, mem1⟩"
proof -
  from equivalent obtain ℛ
    where ℛ_bisim: "strong_low_bisim_mm ℛ ∧ (⟨c1, mds1, mem1⟩, ⟨c2, mds2, mem2⟩) ∈ ℛ"
    by (metis mm_equiv.simps)
  hence "sym ℛ"
    by (auto simp: strong_low_bisim_mm_def)
  hence "(⟨c2, mds2, mem2⟩, ⟨c1, mds1, mem1⟩) ∈ ℛ"
    by (metis ℛ_bisim symE)
  thus ?thesis
    by (metis ℛ_bisim mm_equiv.intros)
qed

lemma low_indistinguishable_sym: "lc ∼⇘mds⇙ lc' ⟹ lc' ∼⇘mds⇙ lc"
  by (auto simp: mm_equiv_sym low_indistinguishable_def low_mds_eq_def)

lemma mm_equiv_glob_consistent: "closed_glob_consistent mm_equiv"
  unfolding closed_glob_consistent_def
  apply clarify
  apply (erule mm_equiv_elim)
  by (auto simp: strong_low_bisim_mm_def closed_glob_consistent_def)

lemma mm_equiv_strong_low_bisim: "strong_low_bisim_mm mm_equiv"
  unfolding strong_low_bisim_mm_def
proof (auto)
  show "closed_glob_consistent mm_equiv" by (rule mm_equiv_glob_consistent)
next
  fix c1 mds mem1 c2 mem2 x
  assume "⟨ c1, mds, mem1 ⟩ ≈ ⟨ c2, mds, mem2 ⟩"
  then obtain ℛ where
    "strong_low_bisim_mm ℛ ∧ (⟨ c1, mds, mem1 ⟩, ⟨ c2, mds, mem2 ⟩) ∈ ℛ"
    by blast
  thus "mem1 =⇘mds⇙l mem2" by (auto simp: strong_low_bisim_mm_def)
next
  fix c1 :: 'Com
  fix mds mem1 c2 mem2 c1' mds' mem1'
  let ?lc1 = "⟨ c1, mds, mem1 ⟩" and
      ?lc1' = "⟨ c1', mds', mem1' ⟩" and
      ?lc2 = "⟨ c2, mds, mem2 ⟩"
  assume "?lc1 ≈ ?lc2"
  then obtain ℛ where "strong_low_bisim_mm ℛ ∧ (?lc1, ?lc2) ∈ ℛ"
    by (rule mm_equiv_elim, blast)
  moreover assume "?lc1 ↝ ?lc1'"
  ultimately show "∃ c2' mem2'. ?lc2 ↝ ⟨ c2', mds', mem2' ⟩ ∧ ?lc1' ≈ ⟨ c2', mds', mem2' ⟩"
    by (simp add: strong_low_bisim_mm_def mm_equiv_sym, blast)
next
  show "sym mm_equiv"
    by (auto simp: sym_def mm_equiv_sym)
qed

end

end