equal
deleted
inserted
replaced
52 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
52 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
53 then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'} |
53 then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'} |
54 else Tainted s)" |
54 else Tainted s)" |
55 | "Tainted (Attach p h flag # s) = |
55 | "Tainted (Attach p h flag # s) = |
56 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
56 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
57 then Tainted s \<union> {O_proc p' | p' flag'. (p', flag') \<in> procs_of_shm s h} |
57 then Tainted s \<union> {O_proc p'' | p' flag' p''. (p', flag') \<in> procs_of_shm s h \<and> info_flow_shm s p' p''} |
58 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
58 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
59 then Tainted s \<union> {O_proc p} |
59 then Tainted s \<union> {O_proc p'| p'. info_flow_shm s p p'} |
60 else Tainted s)" |
60 else Tainted s)" |
61 | "Tainted (SendMsg p q m # s) = |
61 | "Tainted (SendMsg p q m # s) = |
62 (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)" |
62 (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)" |
63 | "Tainted (RecvMsg p q m # s) = |
63 | "Tainted (RecvMsg p q m # s) = |
64 (if (O_msg q m \<in> Tainted s) |
64 (if (O_msg q m \<in> Tainted s) |