474 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>" |
474 | "procs_of_shm (e # \<tau>) = procs_of_shm \<tau>" |
475 |
475 |
476 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
476 definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool" |
477 where |
477 where |
478 "info_flow_shm \<tau> from to \<equiv> (from = to) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. |
478 "info_flow_shm \<tau> from to \<equiv> (from = to) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. |
479 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
479 (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))" |
480 |
480 |
481 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
481 fun current_msgqs :: "t_state \<Rightarrow> t_msg set" |
482 where |
482 where |
483 "current_msgqs [] = init_msgqs" |
483 "current_msgqs [] = init_msgqs" |
484 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |
484 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)" |
1426 t_init: "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []" |
1426 t_init: "obj \<in> seeds \<Longrightarrow> obj \<in> tainted []" |
1427 | t_clone: "\<lbrakk>O_proc p \<in> tainted s; valid (Clone p p' fds shms # s)\<rbrakk> |
1427 | t_clone: "\<lbrakk>O_proc p \<in> tainted s; valid (Clone p p' fds shms # s)\<rbrakk> |
1428 \<Longrightarrow> O_proc p' \<in> tainted (Clone p p' fds shms # s)" |
1428 \<Longrightarrow> O_proc p' \<in> tainted (Clone p p' fds shms # s)" |
1429 | t_execve: "\<lbrakk>O_file f \<in> tainted s; valid (Execve p f fds # s)\<rbrakk> |
1429 | t_execve: "\<lbrakk>O_file f \<in> tainted s; valid (Execve p f fds # s)\<rbrakk> |
1430 \<Longrightarrow> O_proc p \<in> tainted (Execve p f fds # s)" |
1430 \<Longrightarrow> O_proc p \<in> tainted (Execve p f fds # s)" |
1431 | t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''\<rbrakk> |
1431 | t_ptrace: "\<lbrakk>O_proc p \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p' p''; p'' \<in> current_procs s\<rbrakk> |
1432 \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)" |
1432 \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)" |
1433 | t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''\<rbrakk> |
1433 | t_ptrace':"\<lbrakk>O_proc p' \<in> tainted s; valid (Ptrace p p' # s); info_flow_shm s p p''; p'' \<in> current_procs s\<rbrakk> |
1434 \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)" |
1434 \<Longrightarrow> O_proc p'' \<in> tainted (Ptrace p p' # s)" |
1435 | t_cfile: "\<lbrakk>O_proc p \<in> tainted s; valid (Open p f flags fd (Some inum) # s)\<rbrakk> |
1435 | t_cfile: "\<lbrakk>O_proc p \<in> tainted s; valid (Open p f flags fd (Some inum) # s)\<rbrakk> |
1436 \<Longrightarrow> O_file f \<in> tainted (Open p f flags fd (Some inum) # s)" |
1436 \<Longrightarrow> O_file f \<in> tainted (Open p f flags fd (Some inum) # s)" |
1437 | t_read: "\<lbrakk>O_file f \<in> tainted s; valid (ReadFile p fd # s); |
1437 | t_read: "\<lbrakk>O_file f \<in> tainted s; valid (ReadFile p fd # s); |
1438 file_of_proc_fd s p fd = Some f; info_flow_shm s p p'\<rbrakk> |
1438 file_of_proc_fd s p fd = Some f; info_flow_shm s p p'; p' \<in> current_procs s\<rbrakk> |
1439 \<Longrightarrow> O_proc p' \<in> tainted (ReadFile p fd # s)" |
1439 \<Longrightarrow> O_proc p' \<in> tainted (ReadFile p fd # s)" |
1440 | t_write: "\<lbrakk>O_proc p \<in> tainted s; valid (WriteFile p fd # s); |
1440 | t_write: "\<lbrakk>O_proc p \<in> tainted s; valid (WriteFile p fd # s); |
1441 file_of_proc_fd s p fd = Some f; has_same_inode s f f'\<rbrakk> |
1441 file_of_proc_fd s p fd = Some f; has_same_inode s f f'\<rbrakk> |
1442 \<Longrightarrow> O_file f' \<in> tainted (WriteFile p fd # s)" |
1442 \<Longrightarrow> O_file f' \<in> tainted (WriteFile p fd # s)" |
1443 (* directory is not tainted |
1443 (* directory is not tainted |
1454 | t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> |
1454 | t_rename':"\<lbrakk>O_dir f'' \<in> tainted s; valid (Rename p f f' # s);f \<preceq> f''\<rbrakk> |
1455 \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)" |
1455 \<Longrightarrow> O_dir (file_after_rename f f' f'') \<in> tainted (Rename p f f' # s)" |
1456 *) |
1456 *) |
1457 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk> |
1457 | t_sendmsg:"\<lbrakk>O_proc p \<in> tainted s; valid (SendMsg p q m # s)\<rbrakk> |
1458 \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)" |
1458 \<Longrightarrow> O_msg q m \<in> tainted (SendMsg p q m # s)" |
1459 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\<rbrakk> |
1459 | t_recvmsg:"\<lbrakk>O_msg q m \<in> tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'; p' \<in> current_procs s\<rbrakk> |
1460 \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)" |
1460 \<Longrightarrow> O_proc p' \<in> tainted (RecvMsg p q m # s)" |
1461 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> |
1461 | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> |
1462 \<Longrightarrow> obj \<in> tainted (e # s)" |
1462 \<Longrightarrow> obj \<in> tainted (e # s)" |
1463 |
1463 |
1464 definition taintable:: "t_object \<Rightarrow> bool" |
1464 definition taintable:: "t_object \<Rightarrow> bool" |