420 lines
15 KiB
Plaintext
420 lines
15 KiB
Plaintext
(*
|
|
* Copyright 2014, NICTA
|
|
*
|
|
* This software may be distributed and modified according to the terms of
|
|
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
|
* See "LICENSE_GPLv2.txt" for details.
|
|
*
|
|
* @TAG(NICTA_GPL)
|
|
*)
|
|
|
|
theory Noninterference_Refinement
|
|
imports "Noninterference" "ADT_IF_Refine_C" "Noninterference_Base_Refinement"
|
|
begin
|
|
|
|
(* FIXME: fp is currently ignored by ADT_C_if *)
|
|
consts fp :: bool
|
|
|
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
|
|
|
lemma internal_R_ADT_A_if:
|
|
"internal_R (ADT_A_if uop) R = R"
|
|
apply (rule ext, rule ext)
|
|
apply (simp add: internal_R_def ADT_A_if_def)
|
|
done
|
|
|
|
lemma LI_trans:
|
|
"\<lbrakk>LI A H R (Ia \<times> Ih); LI H C S (Ih \<times> Ic); H \<Turnstile> Ih\<rbrakk>
|
|
\<Longrightarrow> LI A C (R O (S \<inter> {(h, c). h \<in> Ih})) (Ia \<times> Ic)"
|
|
apply (clarsimp simp: LI_def)
|
|
apply safe
|
|
apply (clarsimp simp: Image_def)
|
|
apply (erule_tac x=s in allE)+
|
|
apply (drule(1) set_mp)
|
|
apply clarsimp
|
|
apply (drule(1) set_mp)
|
|
apply (clarsimp simp: invariant_holds_def)
|
|
apply blast
|
|
apply (clarsimp simp: rel_semi_def)
|
|
apply (erule_tac x=j in allE)+
|
|
apply (drule_tac x="(ya, z)" in set_mp)
|
|
apply blast
|
|
apply (clarsimp simp: invariant_holds_def)
|
|
apply blast
|
|
apply (erule_tac x=x in allE)
|
|
apply (erule_tac x=y in allE)+
|
|
apply (erule_tac x=z in allE)
|
|
apply simp
|
|
done
|
|
|
|
end
|
|
|
|
context kernel_m begin
|
|
|
|
definition big_step_ADT_C_if where
|
|
"big_step_ADT_C_if utf \<equiv> big_step_adt (ADT_C_if fp utf) (internal_R (ADT_C_if fp utf) big_step_R) big_step_evmap"
|
|
|
|
(*Note: Might be able to generalise big_step_adt_refines for fw_sim*)
|
|
lemma big_step_ADT_C_if_big_step_ADT_A_if_refines:
|
|
"uop_nonempty utf \<Longrightarrow> refines (big_step_ADT_C_if utf) (big_step_ADT_A_if utf) "
|
|
apply (simp add: big_step_ADT_A_if_def big_step_ADT_C_if_def)
|
|
apply (rule big_step_adt_refines[where A="ADT_A_if utf", simplified internal_R_ADT_A_if])
|
|
apply (rule LI_trans)
|
|
apply (erule global_automata_refine.fw_sim_abs_conc[OF haskell_to_abs])
|
|
apply (erule global_automata_refine.fw_sim_abs_conc[OF c_to_haskell])
|
|
apply (rule global_automaton_invs.ADT_invs[OF haskell_invs])
|
|
apply (rule global_automaton_invs.ADT_invs[OF abstract_invs])
|
|
apply simp
|
|
done
|
|
|
|
end
|
|
|
|
context begin interpretation Arch . (*FIXME: arch_split*)
|
|
|
|
lemma LI_sub_big_steps':
|
|
"\<lbrakk>(s',as) \<in> sub_big_steps C (internal_R C R) s;
|
|
LI A C S (Ia \<times> Ic); A [> Ia; C [> Ic;
|
|
(t, s) \<in> S; s \<in> Ic; t \<in> Ia\<rbrakk>
|
|
\<Longrightarrow> \<exists>t'. (t',as) \<in> sub_big_steps A (internal_R A R) t \<and> (t', s') \<in> S \<and> t' \<in> Ia"
|
|
apply (induct rule: sub_big_steps.induct)
|
|
apply(clarsimp simp: LI_def)
|
|
apply (rule_tac x=t in exI)
|
|
apply clarsimp
|
|
apply (rule sub_big_steps.nil, simp_all)[1]
|
|
apply (force simp: internal_R_def)
|
|
apply (clarsimp simp: LI_def)
|
|
apply (erule_tac x=e in allE)
|
|
apply (clarsimp simp: rel_semi_def)
|
|
apply (drule_tac x="(t', ta)" in set_mp)
|
|
apply (rule_tac b=s' in relcompI)
|
|
apply simp
|
|
apply (rule sub_big_steps_I_holds)
|
|
apply assumption+
|
|
apply clarsimp
|
|
apply (rule_tac x=y in exI)
|
|
apply clarsimp
|
|
apply (subst conj_commute)
|
|
apply (rule context_conjI)
|
|
apply (erule inv_holdsE)
|
|
apply assumption+
|
|
apply (rule sub_big_steps.step[OF refl])
|
|
apply assumption+
|
|
apply (subgoal_tac "z \<in> Ic")
|
|
prefer 2
|
|
apply (rule_tac I=Ic in inv_holdsE)
|
|
apply assumption+
|
|
apply (erule sub_big_steps_I_holds)
|
|
apply assumption+
|
|
apply (force simp: internal_R_def)
|
|
done
|
|
|
|
lemma LI_rel_terminate:
|
|
assumes ex_abs: "\<And>s'. s' \<in> Ic \<Longrightarrow> (\<exists>s. s \<in> Ia \<and> (s, s') \<in> S)"
|
|
assumes rel_correct: "\<And>s s' s0''. \<lbrakk>(internal_R C R)\<^sup>+\<^sup>+ s0'' s'; s0''\<in>Init C s0; (s, s') \<in> S\<rbrakk> \<Longrightarrow> \<exists>s0'\<in>Init A s0. (internal_R A R)\<^sup>+\<^sup>+ s0' s"
|
|
assumes init_rel_correct: "\<And>s0''. s0'' \<in> Init C s0 \<Longrightarrow> \<exists>s0' \<in> Init A s0. (s0', s0'') \<in> S"
|
|
assumes Ia_inv: "A [> Ia"
|
|
assumes s0_Ia: "Init A s0 \<subseteq> Ia"
|
|
assumes Ic_inv: "C [> Ic"
|
|
assumes s0_Ic: "Init C s0 \<subseteq> Ic"
|
|
assumes li: "LI A C S (Ia \<times> Ic)"
|
|
shows "\<lbrakk>rel_terminate A s0 (internal_R A R) Ia (internal_R A measuref)\<rbrakk>
|
|
\<Longrightarrow> rel_terminate C s0 (internal_R C R) Ic (internal_R C measuref)"
|
|
apply (simp add: rel_terminate_def)
|
|
apply (clarsimp simp: rtranclp_def2)
|
|
apply (erule disjE)
|
|
apply (cut_tac s'=s in ex_abs, assumption)
|
|
apply clarsimp
|
|
apply (cut_tac s=sa and s'=s in rel_correct, assumption+)
|
|
apply (erule_tac x="sa" in allE)
|
|
apply simp
|
|
apply (erule impE)
|
|
apply blast
|
|
apply (erule_tac x=as in allE)
|
|
apply (frule(3) LI_sub_big_steps'[OF _ li Ia_inv Ic_inv])
|
|
apply clarsimp
|
|
apply (erule_tac x=t' in allE)
|
|
apply simp
|
|
using li
|
|
apply (clarsimp simp: LI_def)
|
|
apply (erule_tac x=a in allE)
|
|
apply (clarsimp simp: rel_semi_def)
|
|
apply (frule(1) sub_big_steps_I_holds[OF Ic_inv])
|
|
apply (drule_tac x="(t', s'')" in set_mp)
|
|
apply blast
|
|
apply clarsimp
|
|
apply (erule_tac x=y in allE)
|
|
apply (erule impE)
|
|
apply blast
|
|
apply (simp add: internal_R_def)
|
|
apply (frule_tac x=sa in spec, drule_tac x=s in spec)
|
|
apply (frule_tac x=y in spec, drule_tac x=z in spec)
|
|
apply (drule_tac x=x in spec, drule_tac x=s' in spec)
|
|
apply simp
|
|
using Ia_inv Ic_inv
|
|
apply (clarsimp simp: invariant_holds_def inv_holds_def)
|
|
apply (erule_tac x=a in allE)+
|
|
apply (drule_tac x=y in set_mp, blast)
|
|
apply (drule_tac x=z in set_mp, blast)
|
|
apply simp
|
|
apply clarsimp
|
|
apply (cut_tac s0''=s0' in init_rel_correct, assumption+)
|
|
apply clarsimp
|
|
apply (erule_tac x="s0'a" in allE)
|
|
apply (frule set_mp[OF s0_Ia])
|
|
apply (erule impE)
|
|
apply blast
|
|
apply (erule_tac x=as in allE)
|
|
apply (frule(3) LI_sub_big_steps'[OF _ li Ia_inv Ic_inv])
|
|
apply clarsimp
|
|
apply (erule_tac x=t' in allE)
|
|
apply simp
|
|
using li
|
|
apply (clarsimp simp: LI_def)
|
|
apply (erule_tac x=a in allE)+
|
|
apply (clarsimp simp: rel_semi_def)
|
|
apply (frule(1) sub_big_steps_I_holds[OF Ic_inv])
|
|
apply (drule_tac x="(t', s'')" in set_mp)
|
|
apply blast
|
|
apply clarsimp
|
|
apply (erule_tac x=y in allE)
|
|
apply (erule impE)
|
|
apply blast
|
|
apply (simp add: internal_R_def)
|
|
apply (frule_tac x=s0'a in spec, drule_tac x=s0' in spec)
|
|
apply (frule_tac x=y in spec, drule_tac x=z in spec)
|
|
apply (drule_tac x=x in spec, drule_tac x=s' in spec)
|
|
apply simp
|
|
using Ia_inv Ic_inv
|
|
apply (clarsimp simp: invariant_holds_def inv_holds_def)
|
|
apply (erule_tac x=a in allE)+
|
|
apply (drule_tac x=y in set_mp, blast)
|
|
apply (drule_tac x=z in set_mp, blast)
|
|
apply simp
|
|
done
|
|
|
|
end
|
|
|
|
locale valid_initial_state_C = valid_initial_state + kernel_m +
|
|
assumes ADT_C_if_serial:
|
|
"\<forall>s' a. (\<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if')
|
|
\<longrightarrow> (\<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a)"
|
|
|
|
lemma internal_R_tranclp:
|
|
"(internal_R A R)\<^sup>+\<^sup>+ s s' \<Longrightarrow> R\<^sup>+\<^sup>+ (Fin A s) (Fin A s')"
|
|
apply (induct rule: tranclp.induct)
|
|
apply (simp add: internal_R_def)
|
|
apply (simp add: internal_R_def)
|
|
done
|
|
|
|
lemma inv_holds_transport:
|
|
"\<lbrakk> A [> Ia; C [> Ic; LI A C R (Ia \<times> Ic) \<rbrakk> \<Longrightarrow> C [> {s'. \<exists>s. (s,s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic}"
|
|
apply (clarsimp simp: LI_def inv_holds_def)
|
|
apply (erule_tac x=j in allE)+
|
|
apply (clarsimp simp: rel_semi_def)
|
|
apply (subgoal_tac "(s,x) \<in> Step A j O R")
|
|
prefer 2
|
|
apply blast
|
|
apply blast
|
|
done
|
|
|
|
lemma inv_holds_T: "A [> UNIV"
|
|
by (simp add: inv_holds_def)
|
|
|
|
context valid_initial_state_C begin
|
|
|
|
lemma LI_abs_to_c:
|
|
"LI (ADT_A_if utf) (ADT_C_if fp utf)
|
|
(((lift_fst_rel (lift_snd_rel state_relation)))
|
|
O ((lift_fst_rel (lift_snd_rel rf_sr)) \<inter> {(h, c). h \<in> full_invs_if'}))
|
|
(full_invs_if \<times> UNIV)"
|
|
apply (rule LI_trans)
|
|
apply (rule global_automata_refine.fw_sim_abs_conc[OF haskell_to_abs])
|
|
apply (rule uop_nonempty)
|
|
apply (rule global_automata_refine.fw_sim_abs_conc[OF c_to_haskell])
|
|
apply (rule uop_nonempty)
|
|
apply (rule global_automaton_invs.ADT_invs[OF haskell_invs])
|
|
done
|
|
|
|
lemma ADT_C_if_Init_Fin_serial:
|
|
"Init_Fin_serial (ADT_C_if fp utf) s {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}"
|
|
apply (unfold_locales)
|
|
apply (subgoal_tac "ADT_C_if fp utf \<Turnstile> P" for P)
|
|
prefer 2
|
|
apply (rule fw_inv_transport)
|
|
apply (rule global_automaton_invs.ADT_invs)
|
|
apply (rule haskell_invs)
|
|
apply (rule invariant_T)
|
|
apply (rule global_automata_refine.fw_sim_abs_conc)
|
|
apply (rule c_to_haskell)
|
|
apply (rule uop_nonempty)
|
|
apply simp
|
|
apply (rule ADT_C_if_serial[rule_format])
|
|
apply simp
|
|
apply (clarsimp simp: ADT_C_if_def lift_fst_rel_def lift_snd_rel_def)
|
|
apply blast
|
|
apply (clarsimp simp: lift_fst_rel_def lift_snd_rel_def ADT_C_if_def)
|
|
apply (rule_tac x=bb in exI)
|
|
apply (clarsimp simp: full_invs_if'_def)
|
|
apply (case_tac "sys_mode_of s", simp_all)
|
|
done
|
|
|
|
lemma ADT_C_if_Init_Fin_serial_weak:
|
|
"Init_Fin_serial_weak (ADT_C_if fp utf) s {s'.
|
|
\<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}"
|
|
apply (rule Init_Fin_serial.serial_to_weak)
|
|
apply (rule ADT_C_if_Init_Fin_serial)
|
|
done
|
|
|
|
lemma Fin_ADT_C_if:
|
|
"Fin (ADT_C_if fp utf) ((uc, s), m) = ((uc, cstate_to_A s), m)"
|
|
by (simp add: ADT_C_if_def)
|
|
|
|
lemma Fin_Init_s0_ADT_C_if:
|
|
"s0' \<in> Init (ADT_C_if fp utf) s0 \<Longrightarrow> Fin (ADT_C_if fp utf) s0' = s0"
|
|
by (clarsimp simp: ADT_C_if_def s0_def)
|
|
|
|
lemma big_step_R_tranclp_abs':
|
|
"\<lbrakk>(s, s')
|
|
\<in> lift_fst_rel (lift_snd_rel state_relation) O
|
|
lift_fst_rel (lift_snd_rel rf_sr);
|
|
big_step_R\<^sup>+\<^sup>+ s0 s''\<rbrakk> \<Longrightarrow> s'' = (Fin (ADT_C_if fp utf) s')
|
|
\<longrightarrow> big_step_R\<^sup>+\<^sup>+ s0 s"
|
|
apply (erule tranclp_induct)
|
|
apply (clarsimp simp: Fin_ADT_C_if lift_fst_rel_def)
|
|
apply (rule tranclp.r_into_trancl)
|
|
apply (simp add: big_step_R_def)
|
|
apply (clarsimp simp: Fin_ADT_C_if lift_fst_rel_def)
|
|
apply (rule tranclp.trancl_into_trancl)
|
|
apply assumption
|
|
apply (simp add: big_step_R_def)
|
|
done
|
|
|
|
lemmas big_step_R_tranclp_abs = big_step_R_tranclp_abs'[rule_format]
|
|
|
|
lemma ADT_C_if_inv_holds_transport:
|
|
"ADT_C_if fp utf [>
|
|
{s'.
|
|
\<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and>
|
|
hs \<in> full_invs_if' \<and>
|
|
(\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and>
|
|
invs_if as)}"
|
|
apply (subst arg_cong[where f="\<lambda>S. ADT_C_if fp utf [> S"])
|
|
prefer 2
|
|
apply (rule_tac A="ADT_A_if utf" in inv_holds_transport)
|
|
prefer 3
|
|
apply (rule weaken_LI)
|
|
apply (rule LI_abs_to_c)
|
|
prefer 2
|
|
apply (rule invs_if_inv_holds_ADT_A_if)
|
|
prefer 2
|
|
apply (rule inv_holds_T)
|
|
apply (clarsimp simp: invs_if_full_invs_if)
|
|
apply force
|
|
done
|
|
|
|
lemma ADT_C_if_Init_transport:
|
|
"Init (ADT_C_if fp utf) s0
|
|
\<subseteq> {s'.
|
|
\<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and>
|
|
hs \<in> full_invs_if' \<and>
|
|
(\<exists>as. (as, hs) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and>
|
|
invs_if as)}"
|
|
apply clarsimp
|
|
apply (frule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_nonempty]]])
|
|
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
|
apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_nonempty]]])
|
|
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
|
apply (rule_tac x=bb in exI)
|
|
apply simp
|
|
apply (rule conjI)
|
|
apply (force simp: ADT_H_if_def)
|
|
apply (rule_tac x=ba in exI)
|
|
apply (clarsimp simp: ADT_A_if_def)
|
|
done
|
|
|
|
lemma ADT_C_if_big_step_R_terminate:
|
|
"rel_terminate (ADT_C_if fp utf) s0
|
|
(internal_R (ADT_C_if fp utf) big_step_R)
|
|
{s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and>
|
|
hs \<in> full_invs_if' \<and> (\<exists>as. (as, hs) \<in>
|
|
lift_fst_rel (lift_snd_rel state_relation) \<and> invs_if as)}
|
|
(\<lambda>s s'. internal_R (ADT_C_if fp utf) measuref_if s s')"
|
|
apply (rule_tac S="lift_fst_rel (lift_snd_rel state_relation) O
|
|
(lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})"
|
|
and Ia="Collect invs_if" and A="ADT_A_if utf" in LI_rel_terminate)
|
|
apply blast
|
|
prefer 8
|
|
apply (simp add: internal_R_ADT_A_if)
|
|
apply (rule ADT_A_if_big_step_R_terminate)
|
|
apply (simp add: internal_R_ADT_A_if, simp add: ADT_A_if_def)
|
|
apply (rule_tac x="s0" in bexI)
|
|
apply (drule internal_R_tranclp)
|
|
apply (simp add: Fin_Init_s0_ADT_C_if)
|
|
apply clarsimp
|
|
apply (rule big_step_R_tranclp_abs)
|
|
apply force
|
|
apply assumption
|
|
apply simp
|
|
apply (clarsimp simp: invs_if_full_invs_if extras_s0)
|
|
apply (drule set_mp[OF global_automata_refine.init_refinement[OF c_to_haskell[OF uop_nonempty]]])
|
|
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
|
apply (frule set_mp[OF global_automata_refine.init_refinement[OF haskell_to_abs[OF uop_nonempty]]])
|
|
apply (clarsimp simp: Image_def lift_fst_rel_def lift_snd_rel_def)
|
|
apply (rule_tac x="((aa, bc), bd)" in bexI)
|
|
apply (rule_tac b="((aa, bb), bd)" in relcompI)
|
|
apply simp
|
|
apply (force simp: ADT_H_if_def)
|
|
apply simp
|
|
apply (rule invs_if_inv_holds_ADT_A_if)
|
|
apply (simp add: ADT_A_if_def invs_if_full_invs_if extras_s0)
|
|
apply (rule ADT_C_if_inv_holds_transport)
|
|
apply (rule ADT_C_if_Init_transport)
|
|
apply (rule weaken_LI[OF LI_abs_to_c])
|
|
apply (clarsimp simp: invs_if_full_invs_if)
|
|
done
|
|
|
|
lemma big_step_ADT_C_if_enabled_system:
|
|
"enabled_system (big_step_ADT_C_if utf) s0"
|
|
apply (simp add: big_step_ADT_C_if_def)
|
|
apply (rule_tac measuref="internal_R (ADT_C_if fp utf) measuref_if" in big_step_adt_enabled_system)
|
|
apply simp
|
|
apply (force simp: big_step_R_def internal_R_def)
|
|
apply (rule Init_Fin_serial_weak_strengthen)
|
|
apply (rule ADT_C_if_Init_Fin_serial_weak)
|
|
apply (rule ADT_C_if_inv_holds_transport)
|
|
apply force
|
|
apply (rule ADT_C_if_Init_transport)
|
|
apply (rule ADT_C_if_big_step_R_terminate)
|
|
done
|
|
|
|
end
|
|
|
|
sublocale valid_initial_state_C \<subseteq>
|
|
abstract_to_C: noninterference_refinement
|
|
"big_step_ADT_A_if utf" (* the ADT that we prove infoflow for *)
|
|
s0 (* initial state *)
|
|
"\<lambda>e s. part s" (* dom function *)
|
|
"uwr" (* uwr *)
|
|
"policyFlows (pasPolicy initial_aag)" (* policy *)
|
|
"undefined" (* out -- unused *)
|
|
PSched (* scheduler partition name *)
|
|
"big_step_ADT_C_if utf"
|
|
apply(unfold_locales)
|
|
apply(insert big_step_ADT_C_if_enabled_system)[1]
|
|
apply(fastforce simp: enabled_system_def)
|
|
apply(rule big_step_ADT_C_if_big_step_ADT_A_if_refines)
|
|
apply (rule uop_nonempty)
|
|
done
|
|
|
|
context valid_initial_state_C begin
|
|
|
|
lemma xnonleakage_C:
|
|
"abstract_to_C.conc.xNonleakage_gen"
|
|
apply(rule abstract_to_C.xNonleakage_gen_refinement_closed)
|
|
apply(rule xnonleakage)
|
|
done
|
|
|
|
end
|
|
|
|
end
|