480 | "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk> |
480 | "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk> |
481 \<Longrightarrow> info_flow_shm s p p''" |
481 \<Longrightarrow> info_flow_shm s p p''" |
482 *) |
482 *) |
483 definition one_flow_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
483 definition one_flow_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
484 where |
484 where |
485 "one_flow_shm s h from to \<equiv> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> (\<exists> flag. (to, flag) \<in> procs_of_shm s h)" |
485 "one_flow_shm s h from to \<equiv> from \<noteq> to \<and> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> |
|
486 (\<exists> flag. (to, flag) \<in> procs_of_shm s h)" |
486 |
487 |
487 fun self_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
488 fun self_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
488 where |
489 where |
489 "self_shm s p p' = (p = p' \<and> p' \<in> current_procs s)" |
490 "self_shm s p p' = (p = p' \<and> p' \<in> current_procs s)" |
490 |
491 |
1469 | t_rename: "\<lbrakk>O_file f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> |
1470 | t_rename: "\<lbrakk>O_file f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> |
1470 \<Longrightarrow> O_file (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)" |
1471 \<Longrightarrow> O_file (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)" |
1471 | t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> |
1472 | t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> |
1472 \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)" |
1473 \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)" |
1473 *) |
1474 *) |
|
1475 | 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> |
|
1476 \<Longrightarrow> O_proc p' \<in> tainted (Attach p h SHM_RDWR # s)" |
|
1477 | 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> |
|
1478 \<Longrightarrow> O_proc p \<in> tainted (Attach p h SHM_RDWR # s)" |
1474 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk> |
1479 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk> |
1475 \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)" |
1480 \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)" |
1476 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk> |
1481 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk> |
1477 \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)" |
1482 \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)" |
1478 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> |
1483 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> |