equal
deleted
inserted
replaced
703 | "os_grant \<tau> (CreateMsgq p q) = |
703 | "os_grant \<tau> (CreateMsgq p q) = |
704 (p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))" |
704 (p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))" |
705 | "os_grant \<tau> (SendMsg p q m) = |
705 | "os_grant \<tau> (SendMsg p q m) = |
706 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))" |
706 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))" |
707 | "os_grant \<tau> (RecvMsg p q m) = |
707 | "os_grant \<tau> (RecvMsg p q m) = |
708 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q))" |
708 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q) \<and> msgs_of_queue \<tau> q \<noteq> [])" |
709 | "os_grant \<tau> (RemoveMsgq p q) = |
709 | "os_grant \<tau> (RemoveMsgq p q) = |
710 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)" |
710 (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau>)" |
711 | "os_grant \<tau> (CreateShM p h) = |
711 | "os_grant \<tau> (CreateShM p h) = |
712 (p \<in> current_procs \<tau> \<and> h \<notin> (current_shms \<tau>))" |
712 (p \<in> current_procs \<tau> \<and> h \<notin> (current_shms \<tau>))" |
713 | "os_grant \<tau> (Attach p h flag) = |
713 | "os_grant \<tau> (Attach p h flag) = |
1473 \<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)" |
1474 *) |
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> |
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)" |
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> |
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)" |
1478 \<Longrightarrow> O_proc p \<in> tainted (Attach p h flag # s)" |
1479 | 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> |
1480 \<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)" |
1481 | 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> |
1482 \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)" |
1482 \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)" |
1483 | 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> |