equal
deleted
inserted
replaced
13 (if (O_proc p) \<in> Tainted s then Tainted s \<union> {O_proc p'} else Tainted s)" |
13 (if (O_proc p) \<in> Tainted s then Tainted s \<union> {O_proc p'} else Tainted s)" |
14 | "Tainted (Execve p f fds # s) = |
14 | "Tainted (Execve p f fds # s) = |
15 (if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)" |
15 (if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)" |
16 | "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}" |
16 | "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}" |
17 | "Tainted (Ptrace p p' # s) = |
17 | "Tainted (Ptrace p p' # s) = |
18 (if (O_proc p) \<in> Tainted s |
18 (if (O_proc p \<in> Tainted s) |
19 then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''} |
19 then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''} |
20 else if (O_proc p') \<in> Tainted s |
20 else if (O_proc p' \<in> Tainted s) |
21 then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''} |
21 then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''} |
22 else Tainted s)" |
22 else Tainted s)" |
23 | "Tainted (Exit p # s) = Tainted s - {O_proc p}" |
23 | "Tainted (Exit p # s) = Tainted s - {O_proc p}" |
24 | "Tainted (Open p f flags fd opt # s) = |
24 | "Tainted (Open p f flags fd opt # s) = |
25 (case opt of |
25 (case opt of |