--- a/simple_selinux/Tainted_prop.thy Mon Dec 02 10:52:40 2013 +0800
+++ b/simple_selinux/Tainted_prop.thy Tue Dec 03 22:42:48 2013 +0800
@@ -6,217 +6,50 @@
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> h. obj \<noteq> O_shm h) \<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, drule seeds_in_init, case_tac obj, simp+)
+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 Tainted_in_current:
- "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
+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:same_inode_files_prop1 procs_of_shm_prop2
- dest:info_shm_flow_in_procs)
-apply (auto simp:same_inode_files_def is_file_def split:if_splits)
-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 info_flow_shm_Tainted:
- "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
-proof (induct s arbitrary:p p')
- case Nil
- thus ?case by (simp add:flow_shm_in_seeds)
-next
- case (Cons e s)
- hence p1: "O_proc p \<in> Tainted (e # s)" and p2: "info_flow_shm (e # s) p p'" and p3: "valid (e # s)"
- and p4: "\<And> p p'. \<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"
- and p5: "valid s" and p6: "os_grant s e"
- by (auto dest:vd_cons intro:vd_cons vt_grant_os)
- have p4':
- "\<And> p p' h flag. \<lbrakk>O_proc p \<in> Tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk>
- \<Longrightarrow> O_proc p' \<in> Tainted s"
- by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2 p5)
- from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)"
- by (auto dest:info_shm_flow_in_procs)
- show ?case
- proof (cases "self_shm s p p'")
- case True with p1 show ?thesis by simp
- next
- case False
- with p1 p2 p5 p6 p7 p8 p3 show ?thesis
- apply (case_tac e)(*
- prefer 7
- apply (simp add:info_flow_shm_simps split:if_splits option.splits)
- apply (rule allI|rule impI|rule conjI)+
- apply simp
- apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+)
- apply simp
-
-
-
-
- apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current
- intro:p4 p4' split:if_splits option.splits)
- apply (auto simp:info_flow_shm_def one_flow_shm_def)
-
-
-
- apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits)
-
-
-
- prefer 7
- apply (simp split:if_splits option.splits)
- apply (rule allI|rule impI|rule conjI)+
-
-
- apply (auto dest:p4' procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]
-
- apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+)
- apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp)
- apply ((erule exE|erule conjE)+)
-
-
- apply (auto simp:info_flow_shm_def dest:p4'
- procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]
- apply (drule_tac p = p and p' = p' in p4')
- apply (erule_tac x = ha in allE, simp)
- apply (drule_tac p = "nat1" and p' = p' in p4')
- apply (auto dest:p4'[where p = nat1 and p' = p'])
-
-apply (induct s)
-apply simp defer
-apply (frule vd_cons, frule vt_grant_os, case_tac a)
-apply (auto simp:info_flow_shm_def elim!:disjE)
-sorry *)
- sorry
-qed
-qed
-
-lemma has_same_inode_comm:
- "has_same_inode s f f' = has_same_inode s f' f"
-by (auto simp add:has_same_inode_def same_inode_files_def is_file_def)
-
-lemma tainted_imp_Tainted:
- "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"
-apply (induct rule:tainted.induct) (*
-apply (simp_all add:vd_cons)
-apply (rule impI)
-
-apply (rule disjI2, rule_tac x = flag' in exI, simp)
-apply ((rule impI)+, erule_tac x = p' in allE, simp)
-*)
-apply (auto intro:info_flow_shm_Tainted simp:has_same_inode_def dest:vd_cons)
-apply (case_tac e, auto split:option.splits if_splits simp:alive_simps)
+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_imp_tainted_aux_remain:
- "\<lbrakk>obj \<in> Tainted s; valid (e # s); alive (e # s) obj; \<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s\<rbrakk>
- \<Longrightarrow> obj \<in> tainted (e # s)"
-by (rule t_remain, auto)
-
-lemma Tainted_imp_tainted:
- "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s"
-apply (induct s arbitrary:obj, simp add:t_init)
-apply (frule Tainted_in_current, simp+)
-apply (frule vt_grant_os, frule vd_cons, case_tac a)
-apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros
- simp:has_same_inode_def)
-done
-
-lemma tainted_eq_Tainted:
- "valid s \<Longrightarrow> (obj \<in> tainted s) = (obj \<in> Tainted s)"
-by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted)
-
-lemma info_flow_shm_tainted:
- "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s"
-by (simp only:tainted_eq_Tainted info_flow_shm_Tainted)
-
+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 same_inode_files_Tainted:
- "\<lbrakk>O_file f \<in> Tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
-apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def)
-apply (frule vt_grant_os, frule vd_cons, case_tac a)
-prefer 6
-apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps)
-prefer 8
-apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
-apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1]
-prefer 8
-apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)
-apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1]
-prefer 10
-apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1]
-apply (drule Tainted_in_current, simp, simp add:alive.simps is_file_in_current)
-apply (drule same_inode_files_prop5, simp)
-apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp)
-
-apply (auto simp:same_inode_files_other split:if_splits)
-apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+)
-apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, 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 has_same_inode_Tainted:
- "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"
-by (simp add:has_same_inode_def same_inode_files_Tainted)
-
-lemma has_same_inode_tainted:
- "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"
-by (simp add:has_same_inode_Tainted tainted_eq_Tainted)
-
-lemma same_inodes_Tainted:
- "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> Tainted s) = (O_file f' \<in> Tainted s)"
-apply (frule same_inode_files_prop8, frule same_inode_files_prop7)
-apply (auto intro:has_same_inode_Tainted)
-done
-
-
-
-lemma tainted_in_current:
- "obj \<in> tainted s \<Longrightarrow> alive s obj"
-apply (erule tainted.induct)
-apply (auto dest:vt_grant_os vd_cons info_shm_flow_in_procs procs_of_shm_prop2 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)
+apply (drule tainted_in_current)
+apply (simp add:vd_cons)
+apply (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) \<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 (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