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 53 e3ad1b294fd9
parent 52 ec73b98d4a64
child 54 e934f9a697f5
equal deleted inserted replaced
52:ec73b98d4a64 53:e3ad1b294fd9 
   772   "update_s2ss_obj s ss obj sobj sobj' = 
   772   "update_s2ss_obj s ss obj sobj sobj' = 
   773      (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
 
   773      (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj)
 
   774       then ss \<union> {sobj'}
 
   774       then ss \<union> {sobj'}
 
   775       else ss - {sobj} \<union> {sobj'})"
 
   775       else ss - {sobj} \<union> {sobj'})"
 
   776 
   776 
   777 definition update_s2ss_sfile :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 
   777 definition update_s2ss_sfile_del :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 
   778 where 
   778 where 
   779   "update_s2ss_sfile s ss f sf \<equiv> 
   779   "update_s2ss_sfile_del s ss f sf \<equiv> 
   780      if (same_inode_files s f = {f})
 
   780      if (same_inode_files s f = {f})
 
   781      then ss
 
   781      then ss
 
   782      else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"
 
   782      else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}"
 
   783 
   783 
   784 definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 
   784 definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 
   785 where
 
   785 where
 
   786   "del_s2ss_file s ss f sf = 
   786   "del_s2ss_file s ss f sf = 
   787      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
 
   787      (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf)
 
   788       then ss
 
   788       then ss
 
   789       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
 
   789       else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
 
   790            then update_s2ss_sfile s ss f sf
 
   790            then update_s2ss_sfile_del s ss f sf
 
   791            else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
 
   791            else update_s2ss_sfile_del s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf)"
 
   792 
   792 
   793 lemma alive_co2sobj_closefd1:
 
   793 lemma alive_co2sobj_closefd1:
 
   794   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
   794   "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; 
   795     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
 
   795     file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk>
 
   796    \<Longrightarrow> alive (CloseFd p fd # s) obj"
 
   796    \<Longrightarrow> alive (CloseFd p fd # s) obj"
 
   972 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
   972 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+)
 
   973 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
   973 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
   974 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
   974 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
   975 
   975 
   976 apply (rule impI, tactic {*my_seteq_tac 1*})
 
   976 apply (rule impI, tactic {*my_seteq_tac 1*})
 
   977 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
 
   977 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 
   978 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
   978 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
   979 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
   979 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
   980 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
   980 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
   981 apply (rule disjI2, rule_tac x = obj in exI)
 
   981 apply (rule disjI2, rule_tac x = obj in exI)
 
   982 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
   982 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1053 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 
  1053 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps)
 
  1054 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1054 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1055 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1055 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1056 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
  1056 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp)
 
  1057 
  1057 
  1058 apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
 
  1058 apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
 
  1059 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
  1059 apply (erule disjE, rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
  1060 apply (erule exE, erule conjE)
 
  1060 apply (erule exE, erule conjE)
 
  1061 apply (case_tac "obj = O_proc p")
 
  1061 apply (case_tac "obj = O_proc p")
 
  1062 apply (rule_tac x = obj' in exI)
 
  1062 apply (rule_tac x = obj' in exI)
 
  1063 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 
  1063 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd)
 
  1147 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
 
  1147 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd is_dir_simps)
 
  1148 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
  1148 apply (rule_tac x = obj in exI, simp add:co2sobj_closefd)
 
  1149 
  1149 
  1150 apply (rule impI, rule conjI, rule impI)
 
  1150 apply (rule impI, rule conjI, rule impI)
 
  1151 apply (tactic {*my_seteq_tac 1*})
 
  1151 apply (tactic {*my_seteq_tac 1*})
 
  1152 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
 
  1152 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 
  1153 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
  1153 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
  1154 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
  1154 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
  1155 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1155 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1156 apply (rule disjI2, rule_tac x = obj in exI)
 
  1156 apply (rule disjI2, rule_tac x = obj in exI)
 
  1157 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1157 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1229 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
  1229 apply (frule_tac obj = obj in co2sobj_closefd, simp)
 
  1230 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
  1230 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1]
 
  1231 
  1231 
  1232 apply (rule impI)
 
  1232 apply (rule impI)
 
  1233 apply (tactic {*my_seteq_tac 1*})
 
  1233 apply (tactic {*my_seteq_tac 1*})
 
  1234 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_def)
 
  1234 apply (simp add:update_s2ss_obj_def update_s2ss_sfile_del_def)
 
  1235 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
  1235 apply (rule conjI| rule impI|erule exE|erule conjE)+
 
  1236 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
  1236 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
  1237 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1237 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1238 apply (rule disjI2, rule_tac x = obj in exI)
 
  1238 apply (rule disjI2, rule_tac x = obj in exI)
 
  1239 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1239 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1332 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
  1332 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
  1333 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1333 apply (rule disjI2, rule conjI, rule disjI2, rule conjI, rule_tac x = obj in exI)
 
  1334 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1334 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps)
 
  1335 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
  1335 apply (rule notI, simp add:co2sobj.simps split:option.splits)+
 
  1336 
  1336 
  1337 apply (simp add:update_s2ss_sfile_def update_s2ss_obj_def split:if_splits)
 
  1337 apply (simp add:update_s2ss_sfile_del_def update_s2ss_obj_def split:if_splits)
 
  1338 apply (erule conjE, erule disjE)
 
  1338 apply (erule conjE, erule disjE)
 
  1339 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
  1339 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted)
 
  1340 apply (erule exE, erule conjE)
 
  1340 apply (erule exE, erule conjE)
 
  1341 apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1341 apply (case_tac "obj = O_file a", simp add:co2sobj.simps tainted_eq_Tainted)
 
  1342 apply (case_tac "obj = O_proc p")
 
  1342 apply (case_tac "obj = O_proc p")
 
  1469            | _       \<Rightarrow> {})
 
  1469            | _       \<Rightarrow> {})
 
  1470      else s2ss s)"
 
  1470      else s2ss s)"
 
  1471 apply (frule vd_cons, frule vt_grant_os, clarsimp split:if_splits)
 
  1471 apply (frule vd_cons, frule vt_grant_os, clarsimp split:if_splits)
 
  1472 apply (frule is_file_has_sfile', simp, erule exE, simp)
 
  1472 apply (frule is_file_has_sfile', simp, erule exE, simp)
 
  1473 apply (rule conjI, rule impI)
 
  1473 apply (rule conjI, rule impI)
 
  1474 apply (simp add:update_s2ss_sfile_def del_s2ss_file_def)
 
  1474 apply (simp add:update_s2ss_sfile_del_def del_s2ss_file_def)
 
  1475 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer
 
  1475 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ defer
 
  1476 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
  1476 apply (rule impI|erule conjE|erule exE|rule conjI|erule bexE)+ 
  1477 
  1477 
  1478 apply (simp add:s2ss_def)
 
  1478 apply (simp add:s2ss_def)
 
  1479 apply (tactic {*my_seteq_tac 1*})
 
  1479 apply (tactic {*my_seteq_tac 1*})
 
  1738 apply (tactic {*my_setiff_tac 1*})
 
  1738 apply (tactic {*my_setiff_tac 1*})
 
  1739 apply (case_tac "obj = O_dir f", simp add:is_dir_in_current)
 
  1739 apply (case_tac "obj = O_dir f", simp add:is_dir_in_current)
 
  1740 apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)
 
  1740 apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)
 
  1741 done
 
  1741 done
 
  1742 
  1742 
  1743 definition update_s2ss_sfile_link:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 
  1743 definition update_s2ss_sfile:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"
 
  1744 where
 
  1744 where
 
  1745  "update_s2ss_sfile_link s ss f sf \<equiv>
 
  1745  "update_s2ss_sfile s ss f sf \<equiv>
 
  1746     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
 
  1746     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))
 
  1747        then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}
 
  1747        then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}
 
  1748        else ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)} 
  1748        else ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)} 
  1749                \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}"
 
  1749                \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}"
 
  1750 
  1750 
  1751 lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (
 
  1751 lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (
 
  1752   case (cf2sfile (LinkHard p f f' # s) f') of
 
  1752   case (cf2sfile (LinkHard p f f' # s) f') of
 
  1753     Some sf \<Rightarrow> update_s2ss_sfile_link s (s2ss s) f sf
 
  1753     Some sf \<Rightarrow> update_s2ss_sfile s (s2ss s) f sf
 
  1754   | _       \<Rightarrow> {})"
 
  1754   | _       \<Rightarrow> {})"
 
  1755 apply (frule vt_grant_os, frule vd_cons, clarsimp)
 
  1755 apply (frule vt_grant_os, frule vd_cons, clarsimp)
 
  1756 apply (split option.splits)
 
  1756 apply (split option.splits)
 
  1757 apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)
 
  1757 apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)
 
  1758 apply (rule allI, rule impI)
 
  1758 apply (rule allI, rule impI)
 
  1759 
  1759 
  1760 apply (simp add:update_s2ss_sfile_link_def)
 
  1760 apply (simp add:update_s2ss_sfile_def)
 
  1761 apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
 
  1761 apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)
 
  1762 apply (simp add:s2ss_def)
 
  1762 apply (simp add:s2ss_def)
 
  1763 apply (tactic {*my_seteq_tac 1*})
 
  1763 apply (tactic {*my_seteq_tac 1*})
 
  1764 apply (case_tac "obj = O_file f'")
 
  1764 apply (case_tac "obj = O_file f'")
 
  1765 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
 
  1765 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted
 
  1834 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
  1834 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
  1835 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
  1835 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
  1836 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
  1836 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)
 
  1837 done
 
  1837 done
 
  1838 
  1838 
       
  1839 lemma has_same_inode_prop3:
 
       
  1840   "is_file s f \<Longrightarrow> has_same_inode s f f"
 
       
  1841 by (auto simp:is_file_def has_same_inode_def split:option.splits)
 
       
  1842 
       
  1843 definition update_s2ss_sfile_tainted:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> bool \<Rightarrow> t_static_state"
 
       
  1844 where
 
       
  1845  "update_s2ss_sfile_tainted s ss f tag \<equiv>
 
       
  1846     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> 
       
  1847               co2sobj s (O_file f') = Some (S_file (cf2sfiles s f) False))
 
       
  1848        then ss \<union> {S_file (cf2sfiles s f) True}
 
       
  1849        else ss - {S_file (cf2sfiles s f) False} 
       
  1850                \<union> {S_file (cf2sfiles s f) True}"
 
       
  1851 
       
  1852 lemma s2ss_truncate: "valid (Truncate p f len # s) \<Longrightarrow> s2ss (Truncate p f len # s) = (
 
       
  1853   if (O_file f \<notin> Tainted s \<and> O_proc p \<in> Tainted s \<and> len > 0)
 
       
  1854   then update_s2ss_sfile_tainted s (s2ss s) f True
 
       
  1855   else s2ss s)"
 
       
  1856 apply (frule vt_grant_os, frule vd_cons, simp split:if_splits)
 
       
  1857 apply (rule conjI, rule impI, (erule conjE)+)
 
       
  1858 
       
  1859 apply (simp add:update_s2ss_sfile_tainted_def)
 
       
  1860 apply (rule conjI|rule impI|erule exE|erule conjE)+
 
       
  1861 apply (simp add:s2ss_def)
 
       
  1862 apply (tactic {*my_seteq_tac 1*})
 
       
  1863 apply (case_tac "obj = O_file f")
 
       
  1864 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
 
       
  1865 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1866 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
 
       
  1867 apply (case_tac "fa \<in> same_inode_files s f")
 
       
  1868 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
 
       
  1869 apply (simp add:same_inode_files_prop7)
 
       
  1870 apply (rule disjI2, simp, rule_tac x = obj in exI)
 
       
  1871 apply (simp add:co2sobj_truncate is_file_simps)
 
       
  1872 apply (rule disjI2, simp, rule_tac x = obj in exI)
 
       
  1873 apply (simp add:co2sobj_truncate)
 
       
  1874 apply (rule disjI2, simp, rule_tac x = obj in exI)
 
       
  1875 apply (simp add:co2sobj_truncate is_dir_simps)
 
       
  1876 apply (rule disjI2, simp, rule_tac x = obj in exI)
 
       
  1877 apply (simp add:co2sobj_truncate)
 
       
  1878 apply (tactic {*my_setiff_tac 1*})
 
       
  1879 apply (rule_tac x = "O_file f" in exI)
 
       
  1880 apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
 
       
  1881 apply (tactic {*my_setiff_tac 1*})
 
       
  1882 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1883 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
 
       
  1884 apply (case_tac "fa \<in> same_inode_files s f")
 
       
  1885 apply (rule_tac x = "O_file f'" in exI)
 
       
  1886 apply (auto simp:co2sobj_truncate is_file_simps is_dir_simps split:t_object.splits)[1]
 
       
  1887 apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop)
 
       
  1888 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
 
       
  1889 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
 
       
  1890 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
 
       
  1891 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
 
       
  1892 
       
  1893 apply (rule conjI|rule impI|erule exE|erule conjE)+
 
       
  1894 apply (simp add:s2ss_def)
 
       
  1895 apply (tactic {*my_seteq_tac 1*})
 
       
  1896 apply (case_tac "obj = O_file f")
 
       
  1897 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted has_same_inode_prop3 cf2sfiles_other)
 
       
  1898 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1899 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_truncate alive_simps)
 
       
  1900 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1901 apply (case_tac "fa \<in> same_inode_files s f")
 
       
  1902 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted cf2sfiles_prop cf2sfiles_other)
 
       
  1903 apply (simp add:same_inode_files_prop7)
 
       
  1904 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 
       
  1905 apply (simp add:co2sobj_truncate is_file_simps)
 
       
  1906 apply (rule notI, simp add:co2sobj_truncate is_file_simps)
 
       
  1907 apply (erule_tac x = fa in allE)
 
       
  1908 apply (simp add:co2sobj.simps)
 
       
  1909 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 
       
  1910 apply (simp add:co2sobj_truncate)
 
       
  1911 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1912 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 
       
  1913 apply (simp add:co2sobj_truncate is_dir_simps)
 
       
  1914 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1915 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI)
 
       
  1916 apply (simp add:co2sobj_truncate)
 
       
  1917 apply (rule notI, simp add:co2sobj.simps split:option.splits)
 
       
  1918 apply (tactic {*my_setiff_tac 1*})
 
       
  1919 apply (rule_tac x = "O_file f" in exI)
 
       
  1920 apply (simp add:co2sobj.simps is_file_simps tainted_eq_Tainted cf2sfiles_other has_same_inode_prop3)
 
       
  1921 apply (tactic {*my_setiff_tac 1*})
 
       
  1922 apply (erule_tac obj = obj in co2sobj_some_caseD)
 
       
  1923 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
 
       
  1924 apply (case_tac "fa \<in> same_inode_files s f")
 
       
  1925 apply (simp add:co2sobj.simps same_inodes_Tainted tainted_eq_Tainted cf2sfiles_prop)
 
       
  1926 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_file_simps)
 
       
  1927 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
 
       
  1928 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate is_dir_simps)
 
       
  1929 apply (rule_tac x = obj in exI, simp add:co2sobj_truncate)
 
       
  1930 
       
  1931 apply (rule impI, simp add:s2ss_def)
 
       
  1932 apply (tactic {*my_seteq_tac 1*})
 
       
  1933 apply (rule_tac x = obj in exI)
 
       
  1934 apply (simp add:alive_simps co2sobj_truncate)
 
       
  1935 apply (simp split:t_object.splits if_splits add:co2sobj.simps tainted_eq_Tainted)
 
       
  1936 apply (case_tac "O_proc p \<in> Tainted s", simp add:same_inodes_Tainted)
 
       
  1937 apply simp
 
       
  1938 apply (tactic {*my_setiff_tac 1*})
 
       
  1939 apply (rule_tac x = obj in exI)
 
       
  1940 apply (simp add:alive_simps co2sobj_truncate)
 
       
  1941 apply (auto split:t_object.splits if_splits simp:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted)
 
       
  1942 done
 
       
  1943 
       
  1944 lemma s2ss_createmsgq: "valid (CreateMsgq p q # s) \<Longrightarrow> s2ss (CreateMsgq p q # s) = 
       
  1945   (case (cq2smsgq (CreateMsgq p q # s) q) of 
       
  1946      Some sq \<Rightarrow> s2ss s \<union> {S_msgq sq}
 
       
  1947    | _       \<Rightarrow> {})"
 
       
  1948 apply (frule vd_cons, frule vt_grant_os, clarsimp)
 
       
  1949 apply (case_tac "cq2smsgq (CreateMsgq p q # s) q")
 
       
  1950 apply (drule current_has_smsgq', simp+)
 
       
  1951 apply (simp add:s2ss_def)
 
       
  1952 apply (tactic {*my_seteq_tac 1*})
 
       
  1953 apply (case_tac "obj = O_msgq q")
 
       
  1954 apply (rule disjI1, simp add:co2sobj.simps)
 
       
  1955 apply (rule disjI2, simp, rule_tac x = obj in exI)
 
       
  1956 apply (simp add:co2sobj_createmsgq is_file_simps is_dir_simps split:t_object.splits if_splits)
 
       
  1957 apply (simp add:co2sobj.simps)
 
       
  1958 apply (simp add:co2sobj.simps)
 
       
  1959 apply (tactic {*my_setiff_tac 1*})
 
       
  1960 apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps)
 
       
  1961 apply (tactic {*my_setiff_tac 1*})
 
       
  1962 apply (case_tac "obj = O_msgq q")
 
       
  1963 apply simp
 
       
  1964 apply (rule_tac x = obj in exI)
 
       
  1965 apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits)
 
       
  1966 done
 
       
  1967 
       
  1968 lemma s2ss_sendmsg:
 
       
  1969 
       
  1970 lemma s2ss_recvmsg:
 
       
  1971 
       
  1972 lemma s2ss_removemsgq:
 
  1839 
  1973 
  1840 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
 
  1974 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open
 
  1841   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
 
  1975   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard
 
  1842   s2ss
 
  1976   s2ss_truncate s2ss_createmsgq 
  1843 
  1977
selinux