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 Alive_prop

begin

ML {*quick_and_dirty := true*}

context tainting begin

lemma valid_tainted_obj:

  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and>  (\<forall> p fd. obj \<noteq> O_fd p fd) \<and> (\<forall> s. obj \<noteq> O_tcp_sock s) \<and> (\<forall> s. obj \<noteq> O_udp_sock s)"

apply (induct s, simp)

apply (drule seeds_in_init, case_tac obj, simp+)

apply (frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto split:if_splits option.splits)

done

lemma dir_not_tainted: "\<lbrakk>O_dir f \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> False"

by (auto dest!:valid_tainted_obj)

lemma msgq_not_tainted: "\<lbrakk>O_msgq q \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> False"

by (auto dest:valid_tainted_obj)

lemma tainted_in_current:

  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"

apply (induct s, simp)

apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)

apply (frule vd_cons, frule valid_tainted_obj, simp, frule vt_grant_os, case_tac a)

apply (auto simp:alive_simps split:if_splits option.splits t_object.splits intro:file_of_pfd_is_file)

done

lemma tainted_proc_in_current:

  "\<lbrakk>O_proc p \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

by (drule tainted_in_current, simp+)

lemma t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 

             \<Longrightarrow> obj \<in> tainted (e # s)"

apply (frule vd_cons, frule vt_grant_os, case_tac e)

apply (auto simp:alive_simps split:option.splits if_splits)

done

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)

apply (simp add:vd_cons)

apply (simp add:not_deleted_imp_alive_cons)

done

end

end