theory Tainted_prop 

imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop

begin

context tainting begin

lemma tainted_in_current:

  "obj \<in> tainted s \<Longrightarrow> alive s obj"

apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)

apply (drule seeds_in_init, simp add:tobj_in_alive)

apply (erule has_same_inode_prop2, simp, simp add:vd_cons)

apply (frule vt_grant_os, simp)

apply (erule has_same_inode_prop1, simp, simp add:vd_cons)

done

lemma tainted_is_valid:

  "obj \<in> tainted s \<Longrightarrow> valid s"

by (erule tainted.induct, auto intro:valid.intros)

lemma t_remain_app:

  "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); valid (s' @ s)\<rbrakk> 

  \<Longrightarrow> obj \<in> tainted (s' @ s)"

apply (induct s', simp)

apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)

apply (simp_all add:not_deleted_cons_D vd_cons)

apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons)

done

lemma valid_tainted_obj:

  "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h)"

apply (erule tainted.induct)

apply (drule seeds_in_init)

by auto

lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False"

by (auto dest:valid_tainted_obj)

lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False"

by (auto dest:valid_tainted_obj)

lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False"

by (auto dest:valid_tainted_obj)

end

end