theory Final_theorem
imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 Dynamic_static
begin
context tainting_s begin
lemma t2ts:
"obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
apply (frule tainted_in_current, frule tainted_is_valid)
apply (frule s2ss_included_sobj, simp)
apply (case_tac sobj, simp_all)
apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits)
apply (drule dir_not_tainted, simp)
apply (drule msgq_not_tainted, simp)
apply (drule shm_not_tainted, simp)
done
lemma delq_imp_delqm:
"deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"
apply (induct s, simp)
by (case_tac a, auto)
lemma tainted_s_subset_prop:
"\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj"
apply (case_tac sobj)
apply auto
done
theorem static_complete:
assumes undel: "undeletable obj" and tbl: "taintable obj"
shows "taintable_s obj"
proof-
from tbl obtain s where tainted: "obj \<in> tainted s"
by (auto simp:taintable_def)
hence vs: "valid s" by (simp add:tainted_is_valid)
hence static: "s2ss s \<propto> static" using d2s_main by auto
from tainted tbl vs obtain sobj where sobj: "co2sobj s obj = Some sobj"
apply (clarsimp simp add:taintable_def)
apply (frule tainted_in_current)
apply (case_tac obj, simp_all add:co2sobj.simps)
apply (frule current_proc_has_sp, simp, auto)
done
from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj"
by (auto simp:undeletable_def)
with vs sobj have "init_obj_related sobj obj"
apply (case_tac obj, case_tac [!] sobj)
apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
apply (frule not_deleted_init_file, simp+)
apply (drule is_file_has_sfile', simp, erule exE)
apply (rule_tac x = sf in bexI)
apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1]
apply (drule root_is_init_dir', simp)
apply (frule not_deleted_init_file, simp, simp)
apply (simp add:cf2sfile_def split:option.splits if_splits)
apply (simp add:cf2sfiles_def)
apply (rule_tac x = list in bexI, simp, simp add:same_inode_files_def not_deleted_init_file)
apply (frule not_deleted_init_dir, simp+)
apply (simp add:cf2sfile_def split:option.splits if_splits)
apply (case_tac list, simp add:sroot_def, simp)
apply (drule file_dir_conflict, simp+)
done
with tainted t2ts init_alive sobj static
show ?thesis unfolding taintable_s_def
apply (simp add:init_ss_in_def)
apply (erule bexE)
apply (simp add:init_ss_eq_def)
apply (rule_tac x = "ss'" in bexI)
apply (rule_tac x = "sobj" in exI)
thm tainted_s_subset_prop
by (auto intro:tainted_s_subset_prop)
qed
lemma cp2sproc_pi:
"\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs"
by (simp add:cp2sproc_def split:option.splits if_splits)
lemma cq2smsgq_qi:
"\<lbrakk>cq2smsgq s q = Some (Init q', sec, sms); valid s\<rbrakk> \<Longrightarrow> q = q' \<and> \<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs"
by (simp add:cq2smsgq_def split:option.splits if_splits)
lemma cm2smsg_mi:
"\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk>
\<Longrightarrow> m = m' \<and> \<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs"
by (clarsimp simp add:cm2smsg_def split:if_splits option.splits)
lemma ch2sshm_hi:
"\<lbrakk>ch2sshm s h = Some (Init h', sec); valid s\<rbrakk> \<Longrightarrow> h = h' \<and> \<not> deleted (O_shm h) s \<and> h \<in> init_shms"
by (clarsimp simp:ch2sshm_def split:if_splits option.splits)
lemma root_not_deleted:
"\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False"
apply (induct s, simp)
apply (frule vd_cons, frule vt_grant_os, case_tac a, auto)
done
lemma cf2sfile_fi:
"\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and>
(if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f
else \<not> deleted (O_dir f) s \<and> is_init_dir f)"
apply (case_tac f)
by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted
split:if_splits option.splits)
lemma init_deled_imp_deled_s:
"\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj"
apply (rule notI)
apply (clarsimp simp:s2ss_def)
apply (case_tac obj, case_tac [!] obja, case_tac sobj)
apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps)
apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps
split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
done
lemma deleted_imp_deletable_s:
"\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"
apply (simp add:deletable_s_def)
apply (frule d2s_main)
apply (simp add:init_ss_in_def)
apply (erule bexE)
apply (rule_tac x = ss' in bexI)
apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s)
apply (case_tac obj, case_tac [!] sobj)
apply auto
apply (erule set_mp)
apply (simp)
apply auto
apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI)
apply auto
done
lemma init_related_imp_init_sobj:
"init_obj_related sobj obj \<Longrightarrow> is_init_sobj sobj"
apply (case_tac sobj, case_tac [!] obj, auto)
apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI, auto)
done
theorem undeletable_s_complete:
assumes undel_s: "undeletable_s obj"
shows "undeletable obj"
proof-
from undel_s have init_alive: "init_alive obj"
and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj"
using undeletable_s_def by auto
have "\<not> (\<exists> s. valid s \<and> deleted obj s)"
proof
assume "\<exists> s. valid s \<and> deleted obj s"
then obtain s where vs: "valid s" and del: "deleted obj s" by auto
from vs have vss: "s2ss s \<propto> static" by (rule d2s_main)
with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)"
and related: "init_obj_related sobj obj"
apply (simp add:init_ss_in_def init_ss_eq_def)
apply (erule bexE, erule_tac x= ss' in ballE)
apply (auto dest:init_related_imp_init_sobj)
done
from init_alive del vs have "deletable_s obj"
by (auto elim:deleted_imp_deletable_s)
with alive_s
show False by (auto simp:deletable_s_def)
qed
with init_alive show ?thesis
by (simp add:undeletable_def)
qed
theorem final_offer:
"\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"
apply (erule swap)
by (simp add:static_complete undeletable_s_complete)
(************** static \<rightarrow> dynamic ***************)
lemma set_eq_D:
"\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"
by auto
lemma cqm2sms_prop1:
"\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
apply (induct queue arbitrary:sms)
apply (auto simp:cqm2sms.simps split:option.splits)
done
lemma sq_sm_prop:
"\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk>
\<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)
declare co2sobj.simps [simp add]
lemma subseteq_D:
"\<lbrakk> S \<subseteq> {x. P x}; x \<in> S\<rbrakk> \<Longrightarrow> P x"
by auto
lemma "\<lbrakk>tainted_s ss sobj; ss \<in> static; is_init_sobj sobj\<rbrakk>
\<Longrightarrow> \<exists> s. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
apply (drule s2d_main')
apply (erule exE, erule conjE, simp add:s2ss_def init_ss_eq_def, erule conjE)
apply (rule_tac x = s in exI, simp)
apply (case_tac sobj, simp_all only:tainted_s.simps)
thm set_eq_D
apply (simp split:option.splits)
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
apply (rule_tac x = obj in exI, simp)
apply (case_tac obj, (simp split:option.splits if_splits)+)
lemma tainted_s_imp_tainted:
"\<lbrakk>tainted_s ss sobj; ss \<in> static; init_obj_related sobj obj\<rbrakk>
\<Longrightarrow> \<exists> s. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
apply (drule s2d_main')
apply (erule exE, erule conjE, simp add:s2ss_def init_ss_eq_def, erule conjE)
apply (rule_tac x = s in exI, simp)
apply (case_tac sobj, simp_all)
apply (case_tac[!] obj, simp_all del:co2sobj.simps)
apply (simp split:option.splits)
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
apply (rule_tac x = obj in exI, simp)
apply (case_tac obj, (simp split:option.splits if_splits)+)
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
apply (rule_tac x = obj in exI, simp)
apply (case_tac obj, (simp split:option.splits if_splits)+)
sorry
lemma tainted_s_imp_tainted:
"\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
apply (drule s2d_main)
apply (erule exE, erule conjE, simp add:s2ss_def)
apply (rule_tac x = s in exI, simp)
apply (case_tac sobj, simp_all)
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
apply (rule_tac x = obj in exI, simp)
apply (case_tac obj, (simp split:option.splits if_splits)+)
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
apply (rule_tac x = obj in exI, simp)
apply (case_tac obj, (simp split:option.splits if_splits)+)
done
lemma has_same_inode_prop3:
"has_same_inode s f f' \<Longrightarrow> has_same_inode s f' f"
by (auto simp:has_same_inode_def)
theorem static_sound:
assumes tbl_s: "taintable_s obj"
shows "taintable obj"
proof-
from tbl_s obtain ss sobj where static: "ss \<in> static"
and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj"
and init_alive: "init_alive obj" by (auto simp:taintable_s_def)
from static sobj tainted_s_imp_tainted
obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj"
and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast
from co2sobj related vs
have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')"
apply (case_tac obj', case_tac [!] obj)
apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def
split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
done
with tainted' vs have tainted: "obj \<in> tainted s"
by (auto dest:has_same_inode_prop3 intro:has_same_inode_tainted)
from sobj related init_alive have "appropriate obj"
by (case_tac obj, case_tac [!] sobj, auto)
with vs init_alive tainted
show ?thesis by (auto simp:taintable_def)
qed
end
end