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