Mercurial Mercurial > hg > selinux / diff
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.
Tainted_prop.thy
changeset 56 ced9becf9eeb
parent 43 137358bd4921
child 65 6f9a588bcfc4 
--- a/Tainted_prop.thy	Tue Oct 08 16:37:39 2013 +0800
+++ b/Tainted_prop.thy	Thu Oct 10 12:00:49 2013 +0800
@@ -54,9 +54,9 @@
       else Tainted s)"
 | "Tainted (Attach p h flag # s) = 
      (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) 
-      then Tainted s \<union> {O_proc p' | p' flag'. (p', flag') \<in> procs_of_shm s h}
+      then Tainted s \<union> {O_proc p'' | p' flag' p''. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p''}
       else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)
-           then Tainted s \<union> {O_proc p}
+           then Tainted s \<union> {O_proc p'| p'. info_flow_shm s p p'}
            else Tainted s)"
 | "Tainted (SendMsg p q m # s) = 
      (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)"
selinux