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.
Flask.thy
changeset 23 25e55731ed01
parent 22 f20a798cdf7d
child 25 259a50be4381 
--- a/Flask.thy	Sat Jun 08 09:59:33 2013 +0800
+++ b/Flask.thy	Sun Jun 09 14:28:58 2013 +0800
@@ -475,7 +475,7 @@
 
 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"
 where
-  "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs s) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. 
+  "info_flow_shm \<tau> from to \<equiv> (from = to \<and> from \<in> current_procs \<tau>) \<or> (\<exists> h toflag. 
     (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" 
 
 fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
@@ -1417,7 +1417,9 @@
 
 fixes seeds :: "t_object set"
 assumes 
-  seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj"
+      seeds_in_init: "\<And> obj. obj \<in> seeds \<Longrightarrow> tobj_in_init obj"
+  and same_inode_in_seeds: "\<And> f f'. \<lbrakk>O_file f \<in> seeds; has_same_inode [] f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> seeds"
+  and flow_shm_in_seeds: "\<And> p p'. \<lbrakk>O_proc p \<in> seeds; info_flow_shm [] p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> seeds"
 
 begin
selinux