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.
bug in tainted
authorchunhan
Tue, 08 Oct 2013 16:37:39 +0800
changeset 55 6f3ac2861978
parent 54 e934f9a697f5
child 56 ced9becf9eeb
bug in tainted
Flask.thy file | annotate | diff | comparison | revisions 
--- a/Flask.thy	Tue Oct 08 16:21:23 2013 +0800
+++ b/Flask.thy	Tue Oct 08 16:37:39 2013 +0800
@@ -1472,10 +1472,10 @@
 | t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk>
              \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)"
 *)
-| t_attach1:"\<lbrakk>O_proc p \<in> tainted s; valid (Attach p h SHM_RDWR # s); (p', flag') \<in> procs_of_shm s h\<rbrakk>
-             \<Longrightarrow> O_proc p' \<in> tainted (Attach p h SHM_RDWR # s)"
-| t_attach2:"\<lbrakk>O_proc p' \<in> tainted s; valid (Attach p h flag # s); (p', SHM_RDWR) \<in> procs_of_shm s h\<rbrakk>
-             \<Longrightarrow> O_proc p \<in> tainted (Attach p h flag # s)"
+| t_attach1:"\<lbrakk>O_proc p \<in> tainted s; valid (Attach p h SHM_RDWR # s); (p', flag') \<in> procs_of_shm s h; info_flow_shm s p' p''\<rbrakk>
+             \<Longrightarrow> O_proc p'' \<in> tainted (Attach p h SHM_RDWR # s)"
+| t_attach2:"\<lbrakk>O_proc p' \<in> tainted s; valid (Attach p h flag # s); (p', SHM_RDWR) \<in> procs_of_shm s h; info_flow_shm s p p''\<rbrakk>
+             \<Longrightarrow> O_proc p'' \<in> tainted (Attach p h flag # s)"
 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk>
              \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)"
 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk>
selinux