Mercurial Mercurial > hg > selinux / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
S2ss_prop.thy
changeset 36 1397b2a763ab
parent 35 f2e620d799cf
child 37 029cccce84b4
equal deleted inserted replaced
35:f2e620d799cf 36:1397b2a763ab 
   126   "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"
 
   126   "\<lbrakk>f \<in> same_inode_files s f'; is_dir s f''\<rbrakk> \<Longrightarrow> f \<noteq> f''"
 
   127 apply (rule notI)
 
   127 apply (rule notI)
 
   128 apply (simp add:same_inode_files_def is_file_def is_dir_def 
   128 apply (simp add:same_inode_files_def is_file_def is_dir_def 
   129           split:if_splits option.splits t_inode_tag.splits)
 
   129           split:if_splits option.splits t_inode_tag.splits)
 
   130 done
 
   130 done
 
       
   131 
       
   132 lemma same_inode_files_prop4:
 
       
   133   "\<lbrakk>f' \<in> same_inode_files s f; f'' \<in> same_inode_files s f'\<rbrakk> \<Longrightarrow> f'' \<in> same_inode_files s f"
 
       
   134 by (auto simp:same_inode_files_def split:if_splits)
 
       
   135 
       
   136 lemma same_inode_files_prop5:
 
       
   137   "f' \<in> same_inode_files s f \<Longrightarrow> f \<in> same_inode_files s f'"
 
       
   138 by (auto simp:same_inode_files_def is_file_def split:if_splits)
 
   131 
   139 
   132 (* simpset for cf2sfiles *)
 
   140 (* simpset for cf2sfiles *)
 
   133 
   141 
   134 lemma cf2sfiles_open:
 
   142 lemma cf2sfiles_open:
 
   135   "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
 
   143   "\<lbrakk>valid (Open p f flag fd opt # s); f' \<in> current_files (Open p f flag fd opt # s)\<rbrakk>
 
   165   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
 
   173   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1 cf2sfile_other')
 
   166 apply (drule_tac f' = f' in cf2sfile_rmdir)
 
   174 apply (drule_tac f' = f' in cf2sfile_rmdir)
 
   167 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
 
   175 apply (simp add:current_files_simps same_inode_files_prop1 same_inode_files_prop3 dir_is_empty_def)+
 
   168 done
 
   176 done
 
   169 
   177 
       
   178 lemma cf2sfile_linkhard1':
 
       
   179   "\<lbrakk>valid (LinkHard p oldf f # s); f' \<in> same_inode_files s f''\<rbrakk>
 
       
   180    \<Longrightarrow> cf2sfile (LinkHard p oldf f# s) f' = cf2sfile s f'"
 
       
   181 apply (drule same_inode_files_prop1)
 
       
   182 by (simp add:cf2sfile_linkhard1)
 
       
   183 
   170 lemma cf2sfiles_linkhard:
 
   184 lemma cf2sfiles_linkhard:
 
   171   "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. 
   185   "valid (LinkHard p oldf f # s) \<Longrightarrow> cf2sfiles (LinkHard p oldf f # s) = (\<lambda> f'. 
   172      if (f' = f \<or> f' \<in> same_inode_files s oldf)
 
   186      if (f' = f \<or> f' \<in> same_inode_files s oldf)
 
   173      then (case (cf2sfile (LinkHard p oldf f # s) f) of
 
   187      then (case (cf2sfile (LinkHard p oldf f # s) f) of
 
   174              Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}
 
   188              Some sf \<Rightarrow> cf2sfiles s oldf \<union> {sf}
 
   175            | _       \<Rightarrow> {})
 
   189            | _       \<Rightarrow> {})
 
   176      else cf2sfiles s f')"
 
   190      else cf2sfiles s f')"
 
   177 apply (frule vt_grant_os, frule vd_cons, rule ext)
 
   191 apply (frule vt_grant_os, frule vd_cons, rule ext)
 
   178 apply (auto simp:cf2sfiles_def cf2sfile_simps same_inode_files_simps current_files_simps
 
   192 apply (auto simp:cf2sfiles_def cf2sfile_linkhard1' same_inode_files_linkhard current_files_linkhard 
   179   split:if_splits option.splits dest!:current_file_has_sfile' dest:same_inode_files_prop1)
 
   193   split:if_splits option.splits dest!:current_file_has_sfile' current_has_sec' dest:same_inode_files_prop1)
 
   180 apply (simp add:cf2sfiles_def)
 
   194 done
 
       
   195 
       
   196 lemma cf2sfile_unlink':
 
       
   197   "\<lbrakk>valid (UnLink p f # s); f' \<in> same_inode_files (UnLink p f # s) f''\<rbrakk>
 
       
   198    \<Longrightarrow> cf2sfile (UnLink p f # s) f' = cf2sfile s f'"
 
       
   199 apply (drule same_inode_files_prop1)
 
       
   200 by (simp add:cf2sfile_unlink)
 
   181 
   201 
   182 lemma cf2sfiles_unlink:
 
   202 lemma cf2sfiles_unlink:
 
       
   203   "\<lbrakk>valid (UnLink p f # s); f' \<in> current_files (UnLink p f # s)\<rbrakk> \<Longrightarrow> cf2sfiles (UnLink p f # s) f' = ( 
       
   204      if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and> 
       
   205          (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) then 
       
   206         (case (cf2sfile s f) of 
       
   207            Some sf \<Rightarrow> cf2sfiles s f' - {sf}
 
       
   208          | _       \<Rightarrow> {})
 
       
   209      else cf2sfiles s f')"
 
       
   210 apply (frule vt_grant_os, frule vd_cons, simp add:current_files_simps split:if_splits)
 
       
   211 apply (rule conjI, clarify, frule is_file_has_sfile', simp, erule exE, simp)
 
       
   212 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   213 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
 
       
   214 apply (simp add:current_files_unlink, simp, erule conjE)
 
       
   215 apply (erule_tac x = f'a in ballE, frule_tac f' = "f'a" in cf2sfile_unlink)
 
       
   216 apply (simp add:current_files_unlink same_inode_files_prop1, simp)
 
       
   217 apply (rule_tac x = f'a in bexI, simp, simp)
 
       
   218 apply (drule_tac f = f and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
 
       
   219 apply (erule conjE|erule exE|erule bexE)+
 
       
   220 apply (case_tac "f'a = f", simp)
 
       
   221 apply (frule_tac f' = f' in same_inode_files_unlink, simp add:current_files_unlink)
 
       
   222 apply (frule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
 
       
   223 apply (rule_tac x = f'a in bexI, simp, simp)
 
       
   224 
       
   225 apply (rule impI)+
 
       
   226 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   227 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
 
       
   228 apply (simp add:current_files_unlink, simp, (erule conjE)+)
 
       
   229 apply (rule_tac x = f'a in bexI, frule_tac f' = "f'a" in cf2sfile_unlink)
 
       
   230 apply (simp add:current_files_unlink same_inode_files_prop1, simp, simp)
 
       
   231 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
 
       
   232 apply (simp add:current_files_unlink, simp)
 
       
   233 apply (case_tac "f'a = f", simp)
 
       
   234 apply (frule_tac f = f' and f' = f in same_inode_files_prop5, simp)
 
       
   235 apply (erule bexE, erule conjE)
 
       
   236 apply (rule_tac x = f'' in bexI)
 
       
   237 apply (drule_tac f' = f'' in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
 
       
   238 apply (simp, simp, erule same_inode_files_prop4, simp)
 
       
   239 apply (rule_tac x = f'a in bexI)
 
       
   240 apply (drule_tac f' = f'a in cf2sfile_unlink, simp add:current_files_unlink same_inode_files_prop1)
 
       
   241 apply (simp, simp)
 
       
   242 
       
   243 
       
   244 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   245 apply (erule bexE, frule_tac f' = f' in same_inode_files_unlink)
 
       
   246 apply (simp add:current_files_unlink, simp)
 
       
   247 apply (rule_tac x = f'a in bexI)
 
       
   248 apply (frule_tac f' = f'a in cf2sfile_unlink)
 
       
   249 apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
 
       
   250 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_unlink)
 
       
   251 apply (simp add:current_files_unlink, simp)
 
       
   252 apply (rule_tac x = f'a in bexI)
 
       
   253 apply (frule_tac f' = f'a in cf2sfile_unlink)
 
       
   254 apply (simp add:same_inode_files_prop1 current_files_unlink, simp, simp)
 
       
   255 done
 
   183 
   256 
   184 lemma cf2sfiles_closefd:
 
   257 lemma cf2sfiles_closefd:
 
       
   258   "\<lbrakk>valid (CloseFd p fd # s); f' \<in> current_files (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> cf2sfiles (CloseFd p fd # s) f' = (
 
       
   259      case (file_of_proc_fd s p fd) of
 
       
   260        Some f \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s \<and> 
       
   261                     (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f)) 
       
   262                  then (case (cf2sfile s f) of 
       
   263                          Some sf \<Rightarrow> cf2sfiles s f' - {sf}
 
       
   264                        | _       \<Rightarrow> {})
 
       
   265                  else cf2sfiles s f'
 
       
   266      | _       \<Rightarrow> cf2sfiles s f')"
 
       
   267 
       
   268 apply (frule vt_grant_os, frule vd_cons, case_tac "file_of_proc_fd s p fd")
 
       
   269 apply (simp_all add:current_files_simps split:if_splits)
 
       
   270 
       
   271 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   272 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   273 apply (simp add:current_files_closefd, simp)
 
       
   274 apply (rule_tac x = f'a in bexI)
 
       
   275 apply (frule_tac f = f'a in cf2sfile_closefd)
 
       
   276 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
 
       
   277 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   278 apply (simp add:current_files_closefd, simp)
 
       
   279 apply (rule_tac x = f'a in bexI)
 
       
   280 apply (frule_tac f = f'a in cf2sfile_closefd)
 
       
   281 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
 
       
   282 
       
   283 apply (rule conjI, clarify, frule file_of_pfd_is_file, simp)
 
       
   284 apply (frule is_file_has_sfile', simp, erule exE, simp)
 
       
   285 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   286 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   287 apply (simp add:current_files_closefd, simp, erule conjE)
 
       
   288 apply (erule_tac x = f'a in ballE, frule_tac f = "f'a" in cf2sfile_closefd)
 
       
   289 apply (simp add:current_files_closefd same_inode_files_prop1, simp)
 
       
   290 apply (rule_tac x = f'a in bexI, simp, simp)
 
       
   291 apply (drule_tac f = a and f' = f' and f'' = f'a in same_inode_files_prop4, simp+)
 
       
   292 apply (erule conjE|erule exE|erule bexE)+
 
       
   293 apply (case_tac "f'a = a", simp)
 
       
   294 apply (frule_tac f' = f' in same_inode_files_closefd, simp add:current_files_closefd, simp)
 
       
   295 apply (frule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
 
       
   296 apply (rule_tac x = f'a in bexI, simp, simp)
 
       
   297 
       
   298 apply (rule impI)+
 
       
   299 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   300 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   301 apply (simp add:current_files_closefd, simp, (erule conjE)+)
 
       
   302 apply (rule_tac x = f'a in bexI, frule_tac f = f'a in cf2sfile_closefd)
 
       
   303 apply (simp add:current_files_closefd same_inode_files_prop1, simp, simp)
 
       
   304 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   305 apply (simp add:current_files_closefd, simp)
 
       
   306 apply (case_tac "f'a = a", simp)
 
       
   307 apply (frule_tac f = f' and f' = a in same_inode_files_prop5, simp)
 
       
   308 apply (erule bexE, erule conjE)
 
       
   309 apply (rule_tac x = f'' in bexI)
 
       
   310 apply (drule_tac f = f'' in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
 
       
   311 apply (simp, simp, erule same_inode_files_prop4, simp)
 
       
   312 apply (rule_tac x = f'a in bexI)
 
       
   313 apply (drule_tac f = f'a in cf2sfile_closefd, simp add:current_files_closefd same_inode_files_prop1)
 
       
   314 apply (simp, simp)
 
       
   315 
       
   316 apply (rule conjI, clarify)
 
       
   317 
       
   318 apply (rule impI)
 
       
   319 apply (case_tac "a \<in> files_hung_by_del s", simp_all)
 
       
   320 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   321 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   322 apply (simp add:current_files_closefd, simp)
 
       
   323 apply (rule_tac x = f'a in bexI)
 
       
   324 apply (frule_tac f = f'a in cf2sfile_closefd)
 
       
   325 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
 
       
   326 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   327 apply (simp add:current_files_closefd, simp)
 
       
   328 apply (rule_tac x = f'a in bexI)
 
       
   329 apply (frule_tac f = f'a in cf2sfile_closefd)
 
       
   330 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
 
       
   331 apply (simp add:cf2sfiles_def, rule set_eqI, rule iffI, drule CollectD)
 
       
   332 apply (erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   333 apply (simp add:current_files_closefd, simp)
 
       
   334 apply (rule_tac x = f'a in bexI)
 
       
   335 apply (frule_tac f = f'a in cf2sfile_closefd)
 
       
   336 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
 
       
   337 apply (drule CollectD, erule bexE, frule_tac f' = f' in same_inode_files_closefd)
 
       
   338 apply (simp add:current_files_closefd, simp)
 
       
   339 apply (rule_tac x = f'a in bexI)
 
       
   340 apply (frule_tac f = f'a in cf2sfile_closefd)
 
       
   341 apply (simp add:same_inode_files_prop1 current_files_closefd, simp, simp)
 
       
   342 done
 
   185 
   343 
   186 lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other
 
   344 lemmas cf2sfiles_simps = cf2sfiles_open cf2sfiles_linkhard cf2sfiles_other
 
   187   cf2sfiles_unlink cf2sfiles_closefd
 
   345   cf2sfiles_unlink cf2sfiles_closefd
 
   188   
   346   
   189 
   347 
   199 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 
   357 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 
   200 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 
   358 apply (simp_all add:current_files_simps ch2sshm_other cq2smsgq_other tainted_eq_Tainted)
 
   201 apply (case_tac "cp2sproc (Execve p f fds # s) p")
 
   359 apply (case_tac "cp2sproc (Execve p f fds # s) p")
 
   202 apply (drule current_proc_has_sp', simp, simp)
 
   360 apply (drule current_proc_has_sp', simp, simp)
 
   203 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
 
   361 apply (simp (no_asm_simp) add:cp2sproc_execve tainted_eq_Tainted split:option.splits)
 
   204 
   362 apply (rule impI, simp add:cf2sfiles_other) 
   205 apply (rule impI, simp add:cf2sfiles_def) defer
 
       
   206 
       
   207 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 
   363 apply (frule_tac s = s in is_dir_has_sdir', simp, erule exE, simp)
 
   208 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 
   364 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 
   209 apply (simp add:is_dir_in_current)
 
   365 apply (simp add:is_dir_in_current)
 
   210 done
 
   366 done
 
       
   367 
       
   368 lemma co2sobj_
 
       
   369 
   211 
   370 
   212 end
 
   371 end
 
   213 
   372 
   214 (* simpset for s2ss*)
 
   373 (* simpset for s2ss*)
 
   215 
   374
selinux