Mercurial Mercurial > hg > selinux / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
600 loc to finish s2ss_closefd
authorchunhan
Wed, 25 Sep 2013 11:29:13 +0800
changeset 49 68649272054c
parent 48 bf8c09ec1186
child 50 ed90f7d5e6d7
600 loc to finish s2ss_closefd
S2ss_prop.thy file | annotate | diff | comparison | revisions 
--- a/S2ss_prop.thy	Tue Sep 24 23:39:03 2013 +0800
+++ b/S2ss_prop.thy	Wed Sep 25 11:29:13 2013 +0800
@@ -1258,72 +1258,161 @@
 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 apply (case_tac "f = a", simp add:alive_simps)
-apply (case_tac "f \<in> same_inode_files s a", rule disjI2)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop)
-
-
 apply (erule bexE, erule conjE)
-apply (rule conjI, rule_tac x = "O_file f''" in exI)
-apply (simp add:same_inode_files_prop11 co2sobj.simps tainted_eq_Tainted cf2sfiles_prop same_inodes_Tainted)
-apply (rule notI, simp)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (erule_tac x = f'' in ballE, simp, simp)
+apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
+apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted)
+apply (rule notI, simp add:co2sobj_closefd)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted) 
+apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
-apply (rule notI, simp add:co2sobj.simps)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (rule disjI2, rule conjI, rule disjI2, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (rule impI, rule conjI, rule impI)
+
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule notI, simp)
+apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule conjI, rule disjI2, rule conjI)
+apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
-apply (rule notI, simp add:co2sobj.simps split:option.splits)
-apply (rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)+
+apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)+
+apply (rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)+
+apply (rule impI)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule notI, simp)
+apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule_tac x = obj in allE, simp add:co2sobj_closefd)
 apply (rule notI, simp add:co2sobj.simps split:option.splits)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a", rule disjI1)
+apply (simp add:co2sobj_closefd split:if_splits option.splits t_sobject.splits)
+apply (simp add:co2sobj.simps cf2sfiles_prop same_inodes_Tainted tainted_eq_Tainted)
+apply (erule bexE, erule conjE, erule_tac x = "f''" in ballE, simp, simp)
+apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (simp add:is_file_simps co2sobj_closefd tainted_eq_Tainted)
+apply (rule notI, simp add:co2sobj.simps)
+apply (rule notI, simp add:co2sobj_closefd tainted_eq_Tainted)
+apply (erule_tac x = f in allE, simp add:is_file_simps co2sobj.simps tainted_eq_Tainted)
+apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)+
+apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)+
+apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
+apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
+apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
-apply (erule bexE, erule conjE)
-apply (simp add:update_s2ss_obj_def split:if_splits)
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
+apply (erule conjE, erule disjE)
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule exE, erule conjE)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_proc p")
+apply (rule_tac x = obj' in exI, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
+apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
+apply (simp add:co2sobj_closefd)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule conjE|erule exE|erule disjE)+
+apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_proc p")
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
+apply (erule conjE|erule exE|erule disjE)+
+apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule same_inode_files_prop11)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
+apply (simp add:alive_simps)+
+apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule conjE, erule disjE)
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
 apply (erule exE, erule conjE)
 apply (case_tac "obj = O_proc p")
-apply (rule_tac x = obj' in exI)
-apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
-apply (simp add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
-apply (rule conjI)
-apply (rule impI)
-apply (rule_tac x = f' in ballE, simp, simp, simp)
-apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
-apply (rule_tac x = obj in exI)
-apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
-apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
-apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
-apply (erule conjE, erule exE, erule conjE)
-apply (case_tac "obj = O_proc p")
+apply (rule_tac x = "obj'" in exI, simp, frule_tac obj = obj' in co2sobj_sproc_imp, erule exE)
+apply (frule_tac obj = obj' in alive_co2sobj_closefd3, simp+)
+apply (simp add:co2sobj_closefd tainted_eq_Tainted)
 apply (simp add:co2sobj.simps tainted_eq_Tainted)
-apply (case_tac "obj = O_file a")
-apply (rule_tac x = "O_file f'" in exI)
-apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps same_inode_files_prop11)
-apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)
-apply (rule conjI)
-apply (rule impI)
-apply (rule_tac x = f' in ballE, simp, simp, simp)
-apply (simp add:same_inode_files_prop11 co2sobj.simps cf2sfiles_prop same_inodes_Tainted)
-apply (rule_tac x = obj in exI)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
-apply (frule_tac obj = obj in co2sobj_closefd, simp)
-apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
-
-
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_closefd)
+apply (case_tac "f = a", simp add:alive_simps)
+apply (case_tac "f \<in> same_inode_files s a")
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (erule disjE)
+apply (drule same_inode_files_prop10, simp add:file_of_pfd_is_file, erule exE, erule conjE)
+apply (rule_tac x = "O_file f'" in exI)
+apply (frule same_inode_files_prop11)
+apply (frule_tac obj = "O_file f'" in co2sobj_closefd)
+apply (simp add:alive_simps)+
+apply (frule_tac f = "f'" in is_file_has_sfile', simp, erule exE)
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted split:if_splits)
+apply (rule impI, erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule bexE, erule conjE, erule_tac x = f'' in ballE, simp, simp)
+apply (erule conjE, erule disjE)
+apply (rule_tac x = "O_proc p" in exI)
+apply (simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule conjE, erule exE, erule conjE)
+apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
+apply (erule_tac obj = obj in co2sobj_some_caseD)
+apply (rule_tac x = obj in exI)
+apply (simp add:co2sobj_closefd)
+apply (case_tac "f \<in> same_inode_files s a")
+apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_file_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
+apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
-
-
-apply 
-
-defer
 apply (rule impI)
 apply (simp add:update_s2ss_obj_def)
 apply (rule conjI, rule impI, erule exE, erule conjE)
selinux