Theory Instance_Common

section ‹Relative Security instantiation - Common Aspects›

text ‹ This theory sets up a generic instantiaton infrastructure for all our running examples. For a detailed explanation of each example and it's (dis)proof of Relative Security see the work by Dongol et al. \cite{RS}›


theory Instance_Common
imports "../IMP/Step_Normal" "../IMP/Step_Spec" 
begin



no_notation bot (‹⊥›)
(* This will be used for non-informative entities, e.g., a noninformative output: *)
abbreviation noninform (‹⊥›) where "⊥ ≡ undefined"


(* Avoid splitting the quantifiers over product types into two quantifiers *)
declare split_paired_All[simp del]
declare split_paired_Ex[simp del]

(*  *)
(*mis-speculation cases*)
definition noMisSpec where "noMisSpec (cfgs::config list) ≡ (cfgs = [])"
lemma noMisSpec_ext[simp]:"map x cfgs = map x cfgs' ⟹ noMisSpec cfgs ⟷ noMisSpec cfgs'"
  by (auto simp: noMisSpec_def)
(* mis-speculation of nestedness level 1: *)
definition misSpecL1 where "misSpecL1 (cfgs::config list) ≡ (length cfgs = Suc 0)"
lemma misSpecL1_len[simp]:"misSpecL1 cfgs ⟷ length cfgs = 1" by (simp add: misSpecL1_def)
(*level 2*)
definition misSpecL2 where "misSpecL2 (cfgs::config list) ≡ (length cfgs = 2)"





(* *)
fun tuple::"'a × 'b × 'c ⇒ 'a × 'b"
  where "tuple (a,b,c) = (a,b)"

fun tuple_sel::"'a × 'b × 'c × 'd × 'e  ⇒ 'b × 'd"
  where "tuple_sel (a,b,c,d,e) = (b,d)"

fun cfgsOf::"'a × 'b × 'c × 'd × 'e  ⇒ 'c"
  where "cfgsOf (a,b,c,d,e) = c"

fun pstateOf::"'a × 'b × 'c × 'd × 'e  ⇒ 'a"
  where "pstateOf (a,b,c,d,e) = a"

fun stateOfs::"'a × 'b × 'c × 'd × 'e  ⇒ 'b"
  where "stateOfs (a,b,c,d,e) = b"

(*  *)

context Prog_Mispred
begin
text ‹The "vanilla-semantics" transitions are the normal executions (featuring no speculation):›

text ‹Vanilla-semantics system model: given by the normal semantics›
type_synonym stateV = "config × val llist × val llist × loc set"
fun validTransV where "validTransV (cfg_ib_ls,cfg_ib_ls') = cfg_ib_ls →N cfg_ib_ls'"

text ‹Vanilla-semantics observation infrastructure (part of the vanilla-semantics state-wise attacker model): ›
text ‹The attacker observes the output value, the program counter history and the set of accessed locations so far:›
type_synonym obsV = "val × loc set"
text ‹The attacker-action is just a value (used as input to the function):›
type_synonym actV = "val"
text ‹The attacker's interaction›
fun isIntV :: "stateV ⇒ bool" where 
"isIntV ss = (¬ finalN ss)"
text ‹The attacker interacts with the system by passing input to the function and 
reading the outputs (standard channel) and the accessed locations (side channel) ›
fun getIntV :: "stateV ⇒ actV × obsV" where 
"getIntV (cfg,ibT,ibUT,ls) = 
 (case prog!(pcOf cfg) of 
    Input T _ ⇒ (lhd ibT, ⊥)
   |Input U _ ⇒ (lhd ibUT, ⊥)
   |Output U _ ⇒ (⊥, (outOf (prog!(pcOf cfg)) (stateOf cfg), ls))
   |_ ⇒ (⊥,⊥)
 )"

lemma validTransV_iff_nextN: "validTransV (s1, s2) = (¬ finalN s1 ∧ nextN s1 = s2)"
  by (simp add: stepN_iff_nextN)+
(* *)

text ‹The optimization-enhanced semantics system model: given by the speculative semantics›
type_synonym stateO = configS
fun validTransO where "validTransO (cfgS,cfgS') = cfgS →S cfgS'"

text ‹Optimization-enhanced semantics observation infrastructure (part of the optimization-enhanced semantics state-wise attacker model):
similar to that of the vanilla semantics, in that the standard-channel inputs and outputs are those produced by the normal execution.  
However, the side-channel outputs (the sets of read locations) are also collected.›
type_synonym obsO = "val × loc set"
type_synonym actO = "val"
fun isIntO :: "stateO ⇒ bool" where 
"isIntO ss = (¬ finalS ss)"
fun getIntO :: "stateO ⇒ actO × obsO" where 
"getIntO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (case (cfgs, prog!(pcOf cfg)) of 
    ([],Input T _) ⇒ (lhd ibT, ⊥)
   |([],Input U _) ⇒ (lhd ibUT, ⊥)
   |([],Output U _) ⇒ 
      (⊥, (outOf (prog!(pcOf cfg)) (stateOf cfg), ls))
   |_ ⇒ (⊥,⊥)
 )"

end (* context Prog_Mispred *)


locale Prog_Mispred_Init = 
Prog_Mispred prog mispred resolve update 
for prog :: "com list"
and mispred :: "predState ⇒ pcounter list ⇒ bool"
and resolve :: "predState ⇒ pcounter list ⇒ bool"
and update :: "predState ⇒ pcounter list ⇒ predState"
+ 
fixes initPstate :: predState
  and istate :: "state ⇒ bool"
  and input :: "nat"
begin

fun istateV :: "stateV ⇒ bool" where 
"istateV (cfg, ibT, ibUT, ls) ⟷ 
  pcOf cfg = 0 ∧ istate (stateOf cfg) ∧
  llength ibT = ∞ ∧ llength ibUT = ∞ ∧
  ls = {}"

fun istateO :: "stateO ⇒ bool" where 
"istateO (pstate, cfg, cfgs, ibT,ibUT, ls) ⟷ 
  pstate = initPstate ∧ 
  pcOf cfg = 0 ∧ ls = {} ∧  
  istate (stateOf cfg) ∧ 
  cfgs = [] ∧ llength ibT = ∞ ∧ llength ibUT = ∞"

(* Some auxiliary definitions and facts: *)

lemma istateV_config_imp:
"istateV (cfg, ibT,ibUT, ls) ⟹ pcOf cfg = 0 ∧ ls = {} ∧ ibT ≠ LNil"
  by force

lemma istateO_config_imp:
"istateO (pstate,cfg,cfgs,ibT,ibUT,ls) ⟹
 cfgs = [] ∧ pcOf cfg = 0 ∧ ls = {} ∧ ibT ≠ LNil"
  unfolding istateO.simps
  by auto

(* *)

(*same variable for all cfgs*)
definition "same_var_all x cfg1 cfg2 cfg3 cfgs3 cfg4 cfgs4 ≡ 
 vstore (getVstore (stateOf cfg1)) x = vstore (getVstore (stateOf cfg4)) x ∧
 vstore (getVstore (stateOf cfg2)) x = vstore (getVstore (stateOf cfg4)) x ∧
 vstore (getVstore (stateOf cfg3)) x = vstore (getVstore (stateOf cfg4)) x ∧
 (∀cfg3'∈set cfgs3. vstore (getVstore (stateOf cfg3')) x = vstore (getVstore (stateOf cfg3)) x) ∧ 
 (∀cfg4'∈set cfgs4. vstore (getVstore (stateOf cfg4')) x = vstore (getVstore (stateOf cfg4)) x)"

(*same variable for cfg1 and cfg2*)
definition "same_var x cfg cfg' ≡ 
  vstore (getVstore (stateOf cfg)) x = vstore (getVstore (stateOf cfg')) x"

(*same variable for cfg1 and cfg2, value provided*)
definition "same_var_val x (val::int) cfg cfg' ≡ 
  vstore (getVstore (stateOf cfg)) x = vstore (getVstore (stateOf cfg')) x ∧
  vstore (getVstore (stateOf cfg)) x = val"


(*We want the originals to have the same action, but making sure i ≥ N*)
definition "same_var_o ii cfg3 cfgs3 cfg4 cfgs4 ≡ 
 vstore (getVstore (stateOf cfg3)) ii = vstore (getVstore (stateOf cfg4)) ii ∧
 (∀cfg3'∈set cfgs3. vstore (getVstore (stateOf cfg3')) ii = vstore (getVstore (stateOf cfg3)) ii) ∧ 
 (∀cfg4'∈set cfgs4. vstore (getVstore (stateOf cfg4')) ii = vstore (getVstore (stateOf cfg4)) ii)"


lemma set_var_shrink:"∀cfg3'∈set cfgs.
           vstore (getVstore (stateOf cfg3')) var =
           vstore (getVstore (stateOf cfg)) var 
       ⟹       
       ∀cfg3'∈set (butlast cfgs).
           vstore (getVstore (stateOf cfg3')) var =
           vstore (getVstore (stateOf cfg)) var"
  by (meson in_set_butlastD)


lemma heapSimp:"(∀cfg''∈set cfgs''. getHheap (stateOf cfg') = getHheap (stateOf cfg'')) ∧ cfgs'' ≠ []
⟹ getHheap (stateOf cfg') = getHheap (stateOf (last cfgs''))"
  by simp

lemma heapSimp2:"(∀cfg''∈set cfgs''. getHheap (stateOf cfg') = getHheap (stateOf cfg'')) ∧ cfgs'' ≠ []

⟹ getHheap (stateOf cfg') = getHheap (stateOf (hd cfgs''))"
  by simp

lemma array_baseSimp:"array_base aa1 (getAvstore (stateOf cfg)) =
 array_base aa1 (getAvstore (stateOf cfg')) ∧ 
 (∀cfg'∈set cfgs. array_base aa1 (getAvstore (stateOf cfg')) =
   array_base aa1 (getAvstore (stateOf cfg)))
∧ cfgs ≠ []
⟹ 
 array_base aa1 (getAvstore (stateOf cfg)) =
 array_base aa1 (getAvstore (stateOf (last cfgs)))
"
  by simp

lemma finalB_imp_finalS:"finalB (cfg, ibT,ibUT) ⟹ (∀pstate cfgs ls. finalS (pstate, cfg, [], ibT,ibUT, ls))"
  unfolding finalB_def finalS_def final_def apply clarsimp
    subgoal for pstate ls pstate' cfg' cfgs' ibT ibUT' ls'
      apply(erule allE[of _ "(cfg', ibT,ibUT')"])
      subgoal premises step 
        using step(1) apply (cases rule: stepS_cases)
        using finalB_imp_finalM step(2) nextB_stepB by (simp_all, blast) . .

lemma cfgs_Suc_zero[simp]:"length cfgs = Suc 0 ⟹ cfgs = [last cfgs]"
  by (metis Suc_length_conv last_ConsL length_0_conv)

lemma cfgs_map[simp]:"length cfgs = Suc 0 ⟹ map pcOf cfgs = [pcOf (last cfgs)]"
  apply(frule cfgs_Suc_zero[of cfgs])
  apply(rule ssubst[of "map pcOf cfgs" "map pcOf [last cfgs]"]) 
  by (presburger,metis list.simps(8,9))

end (* context Prog_Mispred_Init *)


end