(*<*)
theory Current_prop
imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
begin
(*>*)
context flask begin
lemma procs_of_shm_prop1: "\<lbrakk> p_flag \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> h \<in> current_shms s"
apply (induct s arbitrary:p_flag)
apply (case_tac p_flag, simp, drule init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits)
done
lemma procs_of_shm_prop2: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
apply (induct s arbitrary:p flag)
apply (simp, drule init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits)
done
lemma procs_of_shm_prop2':
"\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<forall> flag h. (p, flag) \<notin> procs_of_shm s h"
by (auto dest:procs_of_shm_prop2)
lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
\<Longrightarrow> flag = flag'"
apply (induct s arbitrary:p flag flag')
apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
done
lemma procs_of_shm_prop4: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> flag_of_proc_shm s p h = Some flag"
apply (induct s arbitrary:p flag)
apply (simp, drule init_procs_has_shm, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
done
lemma procs_of_shm_prop4':
"\<lbrakk>flag_of_proc_shm s p h = None; valid s\<rbrakk> \<Longrightarrow> \<forall> flag. (p, flag) \<notin> procs_of_shm s h"
by (auto dest:procs_of_shm_prop4)
lemma not_init_intro_proc:
"\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs"
using not_deleted_init_proc by auto
lemma not_init_intro_proc':
"\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
using not_deleted_init_proc by auto
lemma info_shm_flow_in_procs:
"\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)
lemma flag_of_proc_shm_prop1:
"\<lbrakk>flag_of_proc_shm s p h = Some flag; valid s\<rbrakk> \<Longrightarrow> (p, flag) \<in> procs_of_shm s h"
apply (induct s arbitrary:p flag)
apply (simp, drule init_shmflag_has_proc, simp)
apply (frule vd_cons, frule vt_grant_os)
apply (case_tac a, auto split:if_splits option.splits dest:procs_of_shm_prop2)
done
(*********** simpset for one_flow_shm **************)
lemma one_flow_not_self:
"one_flow_shm s h p p \<Longrightarrow> False"
by (simp add:one_flow_shm_def)
lemma one_flow_shm_attach:
"valid (Attach p h flag # s) \<Longrightarrow> one_flow_shm (Attach p h flag # s) = (\<lambda> h' pa pb.
if (h' = h)
then (pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
(pb = p \<and> pa \<noteq> p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
(one_flow_shm s h pa pb)
else one_flow_shm s h' pa pb )"
apply (rule ext, rule ext, rule ext, frule vd_cons, frule vt_grant_os)
by (auto simp add: one_flow_shm_def)
lemma one_flow_shm_detach:
"valid (Detach p h # s) \<Longrightarrow> one_flow_shm (Detach p h # s) = (\<lambda> h' pa pb.
if (h' = h)
then (pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h' pa pb)
else one_flow_shm s h' pa pb)"
apply (rule ext, rule ext, rule ext, frule vt_grant_os)
by (auto simp:one_flow_shm_def)
lemma one_flow_shm_deleteshm:
"valid (DeleteShM p h # s) \<Longrightarrow> one_flow_shm (DeleteShM p h # s) = (\<lambda> h' pa pb.
if (h' = h)
then False
else one_flow_shm s h' pa pb)"
apply (rule ext, rule ext, rule ext, frule vt_grant_os)
by (auto simp: one_flow_shm_def)
lemma one_flow_shm_clone:
"valid (Clone p p' fds shms # s) \<Longrightarrow> one_flow_shm (Clone p p' fds shms # s) = (\<lambda> h pa pb.
if (pa = p' \<and> pb \<noteq> p' \<and> h \<in> shms)
then (if (pb = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h p pb)
else if (pb = p' \<and> pa \<noteq> p' \<and> h \<in> shms)
then (if (pa = p) then (flag_of_proc_shm s p h = Some SHM_RDWR) else one_flow_shm s h pa p)
else one_flow_shm s h pa pb)"
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
apply (frule_tac p = p' in procs_of_shm_prop2', simp)
apply (auto simp:one_flow_shm_def intro:procs_of_shm_prop4 flag_of_proc_shm_prop1)
done
lemma one_flow_shm_execve:
"valid (Execve p f fds # s) \<Longrightarrow> one_flow_shm (Execve p f fds # s) = (\<lambda> h pa pb.
pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:one_flow_shm_def)
lemma one_flow_shm_kill:
"valid (Kill p p' # s) \<Longrightarrow> one_flow_shm (Kill p p' # s) = (\<lambda> h pa pb.
pa \<noteq> p' \<and> pb \<noteq> p' \<and> one_flow_shm s h pa pb )"
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:one_flow_shm_def)
lemma one_flow_shm_exit:
"valid (Exit p # s) \<Longrightarrow> one_flow_shm (Exit p # s) = (\<lambda> h pa pb.
pa \<noteq> p \<and> pb \<noteq> p \<and> one_flow_shm s h pa pb )"
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:one_flow_shm_def)
lemma one_flow_shm_other:
"\<lbrakk>valid (e # s);
\<forall> p h flag. e \<noteq> Attach p h flag;
\<forall> p h. e \<noteq> Detach p h;
\<forall> p h. e \<noteq> DeleteShM p h;
\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
\<forall> p f fds. e \<noteq> Execve p f fds;
\<forall> p p'. e \<noteq> Kill p p';
\<forall> p. e \<noteq> Exit p
\<rbrakk> \<Longrightarrow> one_flow_shm (e # s) = one_flow_shm s"
apply (rule ext, rule ext, rule ext, frule vt_grant_os, frule vd_cons)
apply (case_tac e, auto simp:one_flow_shm_def dest:procs_of_shm_prop2)
apply (drule procs_of_shm_prop1, auto)
done
lemmas one_flow_shm_simps = one_flow_shm_other one_flow_shm_attach one_flow_shm_detach one_flow_shm_deleteshm
one_flow_shm_clone one_flow_shm_execve one_flow_shm_kill one_flow_shm_exit
inductive Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
where
ifs_self: "p \<in> current_procs s \<Longrightarrow> Info_flow_shm s p p"
| ifs_flow:"\<lbrakk>Info_flow_shm s p p'; one_flow_shm s h p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
lemma Info_flow_trans_aux:
"Info_flow_shm s p' p'' \<Longrightarrow> \<forall>p. Info_flow_shm s p p' \<longrightarrow> Info_flow_shm s p p''"
apply (erule Info_flow_shm.induct)
by (auto intro:Info_flow_shm.intros)
lemma Info_flow_trans:
"\<lbrakk>Info_flow_shm s p p'; Info_flow_shm s p' p''\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
by (auto dest:Info_flow_trans_aux)
lemma one_flow_flows:
"\<lbrakk>one_flow_shm s h p p'; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p'"
apply (rule Info_flow_shm.intros(2), simp_all)
apply (rule Info_flow_shm.intros(1))
apply (auto intro:procs_of_shm_prop2 simp:one_flow_shm_def)
done
lemma ifs_flow': "\<lbrakk>one_flow_shm s h p p'; Info_flow_shm s p' p''; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p''"
apply (drule one_flow_flows, simp+)
apply (erule Info_flow_trans, simp+)
done
lemma Info_flow_shm_cases1:
"\<lbrakk>Info_flow_shm s pa pb;
\<And>p \<tau>. \<lbrakk>\<tau> = s; pa = p; pb = p; p \<in> current_procs \<tau>\<rbrakk> \<Longrightarrow> P;
\<And>\<tau> p p' h p''. \<lbrakk>\<tau> = s; pa = p; pb = p''; Info_flow_shm \<tau> p p'; one_flow_shm \<tau> h p' p''\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (erule Info_flow_shm.cases, auto)
lemma Info_flow_shm_prop1:
"\<not> Info_flow_shm s p p \<Longrightarrow> p \<notin> current_procs s"
by (rule notI, drule Info_flow_shm.intros(1), simp)
lemma Info_flow_shm_intro4:
"\<lbrakk>(p, flagb) \<in> procs_of_shm s h; valid s\<rbrakk> \<Longrightarrow> Info_flow_shm s p p"
by (drule procs_of_shm_prop2, simp, simp add:Info_flow_shm.intros)
(********* simpset for inductive Info_flow_shm **********)
lemma Info_flow_shm_attach1:
"Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
((Info_flow_shm s pa pb) \<or>
(\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and>
(\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
(\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and>
(\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')))"
proof (induct rule:Info_flow_shm.induct)
case (ifs_self proc \<tau>)
show ?case
proof (rule impI)
assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
from ifs_self pre have "proc \<in> current_procs s" by simp
hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
show "Info_flow_shm s proc proc \<or>
(\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and> flag = SHM_RDWR \<and>
(\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc)) \<or>
(\<not> Info_flow_shm s proc proc \<and> proc = p \<and> proc \<noteq> p \<and>
(\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'))"
using p4 p3 by auto
qed
next
case (ifs_flow \<tau> pa pb h' pc)
thus ?case
proof (rule_tac impI)
assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> (\<tau> = Attach p h flag # s) \<longrightarrow> Info_flow_shm s pa pb \<or>
\<not> Info_flow_shm s pa pb \<and> pa = p \<and>
pb \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and> (\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')"
and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
from p2 and p4 have p2': "Info_flow_shm s pa pb \<or>
(\<not> Info_flow_shm s pa pb \<and> pa = p \<and> pb \<noteq> p \<and> flag = SHM_RDWR \<and>
(\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
(\<not> Info_flow_shm s pa pb \<and> pb = p \<and> pa \<noteq> p \<and>
(\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
by (erule_tac impE, simp)
from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
from p3 p4 have p8: "if (h' = h)
then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
(pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
(one_flow_shm s h pb pc)
else one_flow_shm s h' pb pc " by (auto simp add:one_flow_shm_attach)
have "\<lbrakk>pa = p; pc = p\<rbrakk> \<Longrightarrow> Info_flow_shm s pa pc " using p7 by simp
moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag = SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
\<Longrightarrow> \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
sorry
moreover have "\<lbrakk>pa = p; pc \<noteq> p; flag \<noteq> SHM_RDWR; \<not> Info_flow_shm s pa pc\<rbrakk>
\<Longrightarrow> Info_flow_shm s pa pc"
sorry
moreover have "\<lbrakk>pc = p; pa \<noteq> p; \<not> Info_flow_shm s pa pc\<rbrakk>
\<Longrightarrow> \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'"
sorry
ultimately
show "Info_flow_shm s pa pc \<or>
(\<not> Info_flow_shm s pa pc \<and> pa = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and>
(\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc)) \<or>
(\<not> Info_flow_shm s pa pc \<and> pc = p \<and> pa \<noteq> p \<and>
(\<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'))"
apply auto
sorry
qed
qed
lemma Info_flow_shm_intro3:
"\<lbrakk>Info_flow_shm s p from; (from, SHM_RDWR) \<in> procs_of_shm s h; (to, flag) \<in> procs_of_shm s h\<rbrakk>
\<Longrightarrow> Info_flow_shm s p to"
apply (case_tac "from = to", simp)
apply (erule_tac h = h in Info_flow_shm.intros(2), simp add:one_flow_shm_def)
by (rule_tac x = flag in exI, simp)
lemma Info_flow_shm_attach1:
"Info_flow_shm s' pa pb \<Longrightarrow> valid s' \<and> (s' = Attach p h flag # s) \<longrightarrow>
(if Info_flow_shm s pa pb then True else
(if (pa = p \<and> flag = SHM_RDWR)
then (\<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)
else if (pb = p)
then (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
else (\<exists> p' flag'. Info_flow_shm s pa p \<and> flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and>
Info_flow_shm s p' pb) \<or>
(\<exists> p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb)
) )"
proof (induct rule:Info_flow_shm.induct)
case (ifs_self proc \<tau>)
show ?case
proof (rule impI)
assume pre: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
hence p1: "p \<in> current_procs s" and p2: "valid s" by (auto intro:vd_cons dest:vt_grant_os)
hence p3: "Info_flow_shm s p p" by (auto intro:Info_flow_shm.intros)
from ifs_self pre have "proc \<in> current_procs s" by simp
hence p4: "Info_flow_shm s proc proc" by (auto intro:Info_flow_shm.intros)
show "if Info_flow_shm s proc proc then True
else if proc = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc
else if proc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s proc p'
else (\<exists>p' flag'. Info_flow_shm s proc p \<and>
flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' proc) \<or>
(\<exists>p'. Info_flow_shm s proc p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p proc)" using p4 p3 by auto
qed
next
case (ifs_flow \<tau> pa pb h' pc)
thus ?case
proof (rule_tac impI)
assume p1:"Info_flow_shm \<tau> pa pb" and p2: "valid \<tau> \<and> \<tau> = Attach p h flag # s \<longrightarrow>
(if Info_flow_shm s pa pb then True
else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
(\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
and p3: "one_flow_shm \<tau> h' pb pc" and p4: "valid \<tau> \<and> \<tau> = Attach p h flag # s"
from p2 and p4 have p2': "(if Info_flow_shm s pa pb then True
else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb
else if pb = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb) \<or>
(\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pb))"
by (erule_tac impE, simp)
from p4 have p5: "valid s" and p6: "os_grant s (Attach p h flag)" by (auto intro:vd_cons dest:vt_grant_os)
from p6 have "p \<in> current_procs s" by simp hence p7:"Info_flow_shm s p p" by (erule_tac Info_flow_shm.intros)
from p3 p4 have p8: "if (h' = h)
then (pb = p \<and> pc \<noteq> p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pc, flagb) \<in> procs_of_shm s h)) \<or>
(pc = p \<and> pb \<noteq> p \<and> (pb, SHM_RDWR) \<in> procs_of_shm s h) \<or>
(one_flow_shm s h pb pc)
else one_flow_shm s h' pb pc " by (auto simp add:one_flow_shm_attach)
have "\<And> flagb. (pc, flagb) \<in> procs_of_shm s h
\<Longrightarrow> \<exists> p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc"
apply (rule_tac x= pc in exI, rule_tac x = flagb in exI, frule procs_of_shm_prop2)
by (simp add:p5, simp add:Info_flow_shm.intros(1))
hence p10: "\<not> Info_flow_shm s p pc \<Longrightarrow> (\<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
Info_flow_shm s pa pc"
using p2' p7 p8 p5
by (auto split:if_splits dest:Info_flow_shm.intros(2))
(* apply (rule_tac x = pb in exI, simp add:one_flow_flows, rule_tac x = flagb in exI, simp)+ *)
moreover have "pc = p \<Longrightarrow> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p')
\<or> Info_flow_shm s pa pc"
using p2' p7 p8 p5
by (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
moreover have "\<lbrakk>pc \<noteq> p; pa \<noteq> p \<or> flag \<noteq> SHM_RDWR\<rbrakk> \<Longrightarrow> (\<exists>p' flag'. Info_flow_shm s pa p \<and>
flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
(\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc) \<or>
Info_flow_shm s pa pc"
using p2' p7 p8 p5
apply (auto split:if_splits intro:Info_flow_shm_intro3 simp:one_flow_shm_def)
apply (rule_tac x = pc in exI, simp add:Info_flow_shm_intro4)
apply (rule_tac x = flagb in exI, simp)
done
ultimately show "if Info_flow_shm s pa pc then True
else if pa = p \<and> flag = SHM_RDWR then \<exists>p' flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc
else if pc = p then \<exists>p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s pa p'
else (\<exists>p' flag'. Info_flow_shm s pa p \<and>
flag = SHM_RDWR \<and> (p', flag') \<in> procs_of_shm s h \<and> Info_flow_shm s p' pc) \<or>
(\<exists>p'. Info_flow_shm s pa p' \<and> (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p pc)"
using p7 by auto
qed
qed
lemma Info_flow_shm_attach:
"valid (Attach p h flag # s) \<Longrightarrow> Info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb.
(Info_flow_shm s pa pb) \<or>
(pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)) \<or>
(pb = p \<and> (\<exists> p'. (p', SHM_RDWR) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pa)) )"
apply (rule ext, rule ext, rule iffI)
apply (case_tac "Info_flow_shm s pa pb", simp)
apply (case_tac "pa = p \<and> flag = SHM_RDWR \<and> (\<exists>flagb. (p', flagb) \<in> procs_of_shm s h \<and> Info_flow_shm s p' pb)", simp)
apply (erule Info_flow_shm_cases1, simp, drule_tac p = pc in Info_flow_shm.intros(1), simp)
apply (simp add:one_flow_shm_simps split:if_splits, erule disjE, simp)
apply (simp split:if_splits, (rule impI|rule allI|rule conjI|erule conjE|erule exE)+, simp)
apply (simp)
apply (simp, erule Info_flow_shm_cases', simp, simp)
apply (rule_tac x =
apply (auto dest:Info_flow_shm.cases)
apply (auto simp add:one_flow_shm_simps)
lemma info_flow_shm_detach:
"valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb.
self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>
(pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
apply (rule ext, rule ext, frule vt_grant_os)
by (auto simp:info_flow_shm_def one_flow_shm_def)
lemma info_flow_shm_deleteshm:
"valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb.
self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb) )"
apply (rule ext, rule ext, frule vt_grant_os)
by (auto simp:info_flow_shm_def one_flow_shm_def)
lemma info_flow_shm_clone:
"valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb.
(pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or>
(pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or>
(pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
apply (frule_tac p = p' in procs_of_shm_prop2', simp)
apply (auto simp:info_flow_shm_def one_flow_shm_def)
done
lemma info_flow_shm_execve:
"valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb.
(pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:info_flow_shm_def one_flow_shm_def)
lemma info_flow_shm_kill:
"valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb.
pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb )"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:info_flow_shm_def one_flow_shm_def)
lemma info_flow_shm_exit:
"valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb.
pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb )"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
by (auto simp:info_flow_shm_def one_flow_shm_def)
lemma info_flow_shm_other:
"\<lbrakk>valid (e # s);
\<forall> p h flag. e \<noteq> Attach p h flag;
\<forall> p h. e \<noteq> Detach p h;
\<forall> p h. e \<noteq> DeleteShM p h;
\<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
\<forall> p f fds. e \<noteq> Execve p f fds;
\<forall> p p'. e \<noteq> Kill p p';
\<forall> p. e \<noteq> Exit p
\<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"
apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)
apply (erule_tac x = h in allE, simp)
apply (drule procs_of_shm_prop1, auto)
done
(*
lemma info_flow_shm_prop1:
"\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk>
\<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
by (induct rule: info_flow_shm.induct, auto)
lemma info_flow_shm_cases:
"\<lbrakk>info_flow_shm \<tau> pa pb; \<And>p s. \<lbrakk>s = \<tau> ; pa = p; pb = p; p \<in> current_procs s\<rbrakk> \<Longrightarrow> P;
\<And>s p p' h p'' flag. \<lbrakk>s = \<tau>; pa = p; pb = p''; info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h;
(p'', flag) \<in> procs_of_shm s h\<rbrakk>\<Longrightarrow> P\<rbrakk>
\<Longrightarrow> P"
by (erule info_flow_shm.cases, auto)
definition one_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
where
"one_flow_shm s p p' \<equiv> p \<noteq> p' \<and> (\<exists> h flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h)"
inductive flows_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
where
"p \<in> current_procs s \<Longrightarrow> flows_shm s p p"
| "\<lbrakk>flows_shm s p p'; one_flow_shm s p' p''\<rbrakk> \<Longrightarrow> flows_shm s p p''"
definition attached_procs :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
where
"attached_procs s h \<equiv> {p. \<exists> flag. (p, flag) \<in> procs_of_shm s h}"
definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
where
"flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"
inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"
fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
where
"Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
| "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'.
if (p' = p) then flowed_procs s h
else if ()
"
lemma info_flow_shm_attach:
"valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or>
(if (pa = p)
then (if (flag = SHM_RDWR)
then (\<exists> flag. (pb, flag) \<in> procs_of_shm s h)
else (pb = p))
else (if (pb = p)
then (pa, SHM_RDWR) \<in> procs_of_shm s h
else info_flow_shm s pa pb)) )"
apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext)
apply (case_tac "info_flow_shm s pa pb", simp)
thm info_flow_shm.cases
apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)
apply (erule info_flow_shm_cases, simp, simp split:if_splits)
apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
apply (rule notI, erule info_flow_shm.cases, simp+)
pr 5
*)
lemmas info_flow_shm_simps = info_flow_shm_other info_flow_shm_attach info_flow_shm_detach info_flow_shm_deleteshm
info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit
lemma has_same_inode_in_current:
"\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
by (auto simp add:has_same_inode_def current_files_def)
lemma has_same_inode_prop1:
"\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
by (auto simp:has_same_inode_def is_file_def)
lemma has_same_inode_prop1':
"\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
by (auto simp:has_same_inode_def is_file_def)
lemma has_same_inode_prop2:
"\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
apply (drule has_same_inode_prop1)
apply (simp add:file_of_pfd_is_file, simp+)
done
lemma has_same_inode_prop2':
"\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
apply (drule has_same_inode_prop1')
apply (simp add:file_of_pfd_is_file, simp+)
done
lemma tobj_in_init_alive:
"tobj_in_init obj \<Longrightarrow> init_alive obj"
by (case_tac obj, auto)
lemma tobj_in_alive:
"tobj_in_init obj \<Longrightarrow> alive [] obj"
by (case_tac obj, auto simp:is_file_nil)
end
end