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> |
1484 \<Longrightarrow> obj \<in> tainted (e # s)" |
1484 \<Longrightarrow> obj \<in> tainted (e # s)" |
1485 |
1485 |
|
1486 (* reasonable tainted object, fd and sock and msgq and msg is excluded |
|
1487 * this is different from tainted, which already excluded some of them, |
|
1488 * tainted not excluded msg, which does not have the meaning of "tainteable", but |
|
1489 * but acting as a media to "pass" the virus. We normally will not say that |
|
1490 * a message is tableable or not. |
|
1491 *) |
|
1492 fun appropriate :: "t_object \<Rightarrow> bool" |
|
1493 where |
|
1494 "appropriate (O_proc p) = (p \<in> init_procs)" |
|
1495 | "appropriate (O_file f) = (is_init_file f)" |
|
1496 | "appropriate (O_dir f) = False" |
|
1497 | "appropriate (O_fd p fd) = False" |
|
1498 | "appropriate (O_node n) = False" (* cause socket is temperary not considered *) |
|
1499 | "appropriate (O_tcp_sock k) = False" |
|
1500 | "appropriate (O_udp_sock k) = False" |
|
1501 | "appropriate (O_shm h) = False" |
|
1502 | "appropriate (O_msgq q) = False" |
|
1503 | "appropriate (O_msg q m) = False" |
|
1504 |
1486 definition taintable:: "t_object \<Rightarrow> bool" |
1505 definition taintable:: "t_object \<Rightarrow> bool" |
1487 where |
1506 where |
1488 "taintable obj \<equiv> init_alive obj \<and> (\<exists> s. obj \<in> tainted s)" |
1507 "taintable obj \<equiv> init_alive obj \<and> appropriate obj \<and> (\<exists> s. obj \<in> tainted s)" |
1489 |
1508 |
1490 definition undeletable :: "t_object \<Rightarrow> bool" |
1509 definition undeletable :: "t_object \<Rightarrow> bool" |
1491 where |
1510 where |
1492 "undeletable obj \<equiv> init_alive obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)" |
1511 "undeletable obj \<equiv> init_alive obj \<and> \<not> (\<exists> s. valid s \<and> deleted obj s)" |
1493 |
1512 |