Theory Security

theory Security
imports Preliminaries
(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
header {* 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 "\<leadsto>" 70)
  where
  "x \<leadsto> 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) \<leadsto> (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"
  ("_ ->\<index> _" [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"
  ("_ =\<index>l _" [100, 100] 80)
  where
  "(mem1 =mdsl 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 =mdsl mem'"
  by (simp add: low_mds_eq_def low_eq_def)

lemma [simp]: "(∀ mds. mem =mdsl 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 \<R> =
  (∀ c1 mds mem1 c2 mem2. (⟨ c1, mds, mem1 ⟩, ⟨ c2, mds, mem2 ⟩) ∈ \<R> -->
   (∀ x. ((dma x = High ∧ x ∉ mds AsmNoWrite) -->
           (∀ v1 v2. (⟨ c1, mds, mem1 (x := v1) ⟩, ⟨ c2, mds, mem2 (x := v2) ⟩) ∈ \<R>)) ∧
         ((dma x = Low ∧ x ∉ mds AsmNoWrite) -->
           (∀ v. (⟨ c1, mds, mem1 (x := v) ⟩, ⟨ c2, mds, mem2 (x := v) ⟩) ∈ \<R>))))"

(* Strong low bisimulations modulo modes: *)
definition strong_low_bisim_mm :: "(('Com, 'Var, 'Val) LocalConf) rel => bool"
  where
  "strong_low_bisim_mm \<R> ≡
  sym \<R> ∧
  closed_glob_consistent \<R> ∧
  (∀ c1 mds mem1 c2 mem2. (⟨ c1, mds, mem1 ⟩, ⟨ c2, mds, mem2 ⟩) ∈ \<R> -->
   (mem1 =mdsl mem2) ∧
   (∀ c1' mds' mem1'. ⟨ c1, mds, mem1 ⟩ \<leadsto> ⟨ c1', mds', mem1' ⟩ -->
    (∃ c2' mem2'. ⟨ c2, mds, mem2 ⟩ \<leadsto> ⟨ c2', mds', mem2' ⟩ ∧
                  (⟨ c1', mds', mem1' ⟩, ⟨ c2', mds', mem2' ⟩) ∈ \<R>)))"

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 \<R> ; (lc1, lc2) ∈ \<R> |] ==> (lc1, lc2) ∈ mm_equiv"

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

definition low_indistinguishable :: "'Var Mds => 'Com => 'Com => bool"
  ("_ ∼\<index> _" [100, 100] 80)
  where "c1 ∼mds c2 = (∀ mem1 mem2. mem1 =mdsl 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 ⟩ \<leadsto> ⟨ c', mds', mem' ⟩ -->
  ((∀ v. ⟨ c, mds, mem (x := v) ⟩ \<leadsto> ⟨ c', mds', mem' (x := v) ⟩) ∨
   (∀ v. ⟨ c, mds, mem (x := v) ⟩ \<leadsto> ⟨ c', mds', mem' ⟩)))"

definition doesnt_modify :: "'Com => 'Var => bool"
  where
  "doesnt_modify c x = (∀ mds mem c' mds' mem'. (⟨ c, mds, mem ⟩ \<leadsto> ⟨ 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'⟩ \<leadsto> ⟨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 \<R>
    where \<R>_bisim: "strong_low_bisim_mm \<R> ∧ (⟨c1, mds1, mem1⟩, ⟨c2, mds2, mem2⟩) ∈ \<R>"
    by (metis mm_equiv.simps)
  hence "sym \<R>"
    by (auto simp: strong_low_bisim_mm_def)
  hence "(⟨c2, mds2, mem2⟩, ⟨c1, mds1, mem1⟩) ∈ \<R>"
    by (metis \<R>_bisim symE)
  thus ?thesis
    by (metis \<R>_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 \<R> where
    "strong_low_bisim_mm \<R> ∧ (⟨ c1, mds, mem1 ⟩, ⟨ c2, mds, mem2 ⟩) ∈ \<R>"
    by blast
  thus "mem1 =mdsl 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 \<R> where "strong_low_bisim_mm \<R> ∧ (?lc1, ?lc2) ∈ \<R>"
    by (rule mm_equiv_elim, blast)
  moreover assume "?lc1 \<leadsto> ?lc1'"
  ultimately show "∃ c2' mem2'. ?lc2 \<leadsto> ⟨ 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