--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/simple_selinux/Alive_prop.thy Mon Dec 02 10:52:40 2013 +0800
@@ -0,0 +1,335 @@
+theory Alive_prop
+imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop Proc_fd_of_file_prop
+begin
+
+context flask begin
+
+lemma distinct_queue_msgs:
+ "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> distinct (msgs_of_queue s q)"
+apply (induct s)
+apply (simp add:init_msgs_distinct)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply auto
+apply (case_tac "msgs_of_queue s q", simp+)
+done
+
+lemma received_msg_notin:
+ "\<lbrakk>hd (msgs_of_queue s q) \<in> set (tl (msgs_of_queue s q)); q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> False"
+apply (drule distinct_queue_msgs, simp)
+apply (case_tac "msgs_of_queue s q", auto)
+done
+
+lemma other_msg_remains:
+ "\<lbrakk>m \<noteq> hd (msgs_of_queue s q); q \<in> current_msgqs s; valid s\<rbrakk>
+ \<Longrightarrow> (m \<in> set (tl (msgs_of_queue s q))) = (m \<in> set (msgs_of_queue s q))"
+apply (drule distinct_queue_msgs, simp)
+apply (case_tac "msgs_of_queue s q", auto)
+done
+
+lemma is_tcp_in_current:
+ "is_tcp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>"
+by (auto simp:is_tcp_sock_def current_sockets_def split:option.splits)
+
+lemma is_udp_in_current:
+ "is_udp_sock \<tau> s \<Longrightarrow> s \<in> current_sockets \<tau>"
+by (auto simp:is_udp_sock_def current_sockets_def split:option.splits)
+
+(************ alive simpset **************)
+
+lemma alive_open:
+ "valid (Open p f flag fd opt # s) \<Longrightarrow> alive (Open p f flag fd opt # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then True
+ else alive s obj
+ | O_file f' \<Rightarrow> (if (opt = None) then alive s obj
+ else if (f = f') then True
+ else alive s obj)
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ dest:is_dir_in_current split:if_splits option.splits)
+done
+
+(* sock is not inherited on Execve, Clone cases, cause I simplified it with os_grant.
+ * chunhan, 2013-11-20
+lemma alive_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd)
+ else if (p = p') then False
+ else alive s (O_fd p' fd))
+ | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
+ else if (p = p') then False
+ else alive s (O_tcp_sock (p', fd)))
+ | O_udp_sock (p', fd) \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
+ else if (p = p') then False
+ else alive s (O_udp_sock (p', fd)))
+ | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ dest:is_dir_in_current split:if_splits option.splits)
+
+done
+
+lemma alive_clone:
+ "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = (
+ \<lambda> obj. case obj of
+ O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj
+ | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
+ else if (p'' = p') then False
+ else alive s obj
+ | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
+ else if (p'' = p') then False
+ else alive s (O_tcp_sock (p'', fd)))
+ | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
+ else if (p'' = p') then False
+ else alive s (O_udp_sock (p'', fd)))
+ | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current split:if_splits option.splits)
+done
+*)
+
+lemma alive_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd)
+ else if (p = p') then False
+ else alive s (O_fd p' fd))
+ | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+ else alive s (O_tcp_sock (p', fd)))
+ | O_udp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+ else alive s (O_udp_sock (p', fd)))
+ | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ dest:is_dir_in_current split:if_splits option.splits
+ dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
+done
+
+lemma alive_clone:
+ "valid (Clone p p' fds # s) \<Longrightarrow> alive (Clone p p' fds # s) = (
+ \<lambda> obj. case obj of
+ O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj
+ | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
+ else if (p'' = p') then False
+ else alive s obj
+ | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False
+ else alive s (O_tcp_sock (p'', fd)))
+ | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p') then False
+ else alive s (O_udp_sock (p'', fd)))
+ | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current split:if_splits option.splits
+ dest:file_fds_subset_pfds[where s = s] udp_notin_file_fds tcp_notin_file_fds)
+done
+
+lemma alive_kill:
+ "valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (
+ \<lambda> obj. case obj of
+ O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj
+ | O_fd p'' fd \<Rightarrow> if (p'' = p') then False else alive s obj
+ | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj
+ | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current split:if_splits option.splits)
+done
+
+lemma alive_exit:
+ "valid (Exit p' # s) \<Longrightarrow> alive (Exit p' # s) = (
+ \<lambda> obj. case obj of
+ O_proc p'' \<Rightarrow> if (p'' = p') then False else alive s obj
+ | O_fd p'' fd \<Rightarrow> if (p'' = p') then False else alive s obj
+ | O_tcp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj
+ | O_udp_sock (p'', fd) \<Rightarrow> if (p'' = p') then False else alive s obj
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current split:if_splits option.splits)
+done
+
+lemma alive_closefd:
+ "valid (CloseFd p fd # s) \<Longrightarrow> alive (CloseFd p fd # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then False else alive s obj
+ | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd) then False else alive s obj
+ | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd) then False else alive s obj
+ | O_file f \<Rightarrow> (case (file_of_proc_fd s p fd) of
+ Some f' \<Rightarrow> (if (f = f' \<and> proc_fd_of_file s f = {(p, fd)} \<and> f \<in> files_hung_by_del s)
+ then False else alive s obj)
+ | _ \<Rightarrow> alive s obj)
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current file_of_pfd_is_file' split:if_splits option.splits)
+done
+
+lemma alive_unlink:
+ "valid (UnLink p f # s) \<Longrightarrow> alive (UnLink p f # s) = (
+ \<lambda> obj. case obj of
+ O_file f' \<Rightarrow> if (f' = f \<and> proc_fd_of_file s f = {}) then False else alive s obj
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict
+ split:if_splits option.splits)
+done
+
+lemma alive_rmdir:
+ "valid (Rmdir p d # s) \<Longrightarrow> alive (Rmdir p d # s) = (alive s) (O_dir d := False)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current file_of_pfd_is_file' file_dir_conflict
+ split:if_splits option.splits)
+done
+
+lemma alive_mkdir:
+ "valid (Mkdir p d inum # s) \<Longrightarrow> alive (Mkdir p d inum # s) = (alive s) (O_dir d := True)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current
+ split:if_splits option.splits)
+done
+
+(*
+lemma alive_linkhard:
+ "valid (LinkHard p f f' # s) \<Longrightarrow> alive (LinkHard p f f' # s) = (alive s) (O_file f' := True)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current file_of_pfd_is_file' is_file_in_current
+ split:if_splits option.splits)
+done
+*)
+
+lemma alive_createmsgq:
+ "valid (CreateMsgq p q # s) \<Longrightarrow> alive (CreateMsgq p q # s) = (alive s) (O_msgq q := True)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)
+done
+
+lemma alive_sendmsg:
+ "valid (SendMsg p q m # s) \<Longrightarrow> alive (SendMsg p q m # s) = (alive s) (O_msg q m := True)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)
+done
+
+lemma alive_recvmsg:
+ "valid (RecvMsg p q m # s) \<Longrightarrow> alive (RecvMsg p q m # s) = (alive s) (O_msg q m := False)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def other_msg_remains
+ dest:received_msg_notin)
+done
+
+lemma alive_removemsgq:
+ "valid (RemoveMsgq p q # s) \<Longrightarrow> alive (RemoveMsgq p q # s) = (
+ \<lambda> obj. case obj of
+ O_msgq q' \<Rightarrow> if (q' = q) then False else alive s obj
+ | O_msg q' m \<Rightarrow> if (q' = q) then False else alive s obj
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)
+done
+
+(*
+lemma alive_createshm:
+ "valid (CreateShM p h # s) \<Longrightarrow> alive (CreateShM p h # s) = (alive s) (O_shm h := True)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)
+done
+
+lemma alive_deleteshm:
+ "valid (DeleteShM p h # s) \<Longrightarrow> alive (DeleteShM p h # s) = (alive s) (O_shm h := False)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def)
+done
+*)
+
+lemma alive_createsock:
+ "valid (CreateSock p af st fd inum # s) \<Longrightarrow> alive (CreateSock p af st fd inum # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd' \<Rightarrow> if (p' = p \<and> fd' = fd) then True else alive s obj
+ | O_tcp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = STREAM) then True else alive s obj
+ | O_udp_sock (p', fd') \<Rightarrow> if (p' = p \<and> fd' = fd \<and> st = DGRAM) then True else alive s obj
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def
+ intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)
+done
+
+lemma alive_accept:
+ "valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> alive (Accept p fd addr port fd' inum # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd'' \<Rightarrow> if (p' = p \<and> fd'' = fd') then True else alive s obj
+ | O_tcp_sock (p', fd'') \<Rightarrow> if (p' = p \<and> fd'' = fd') then True else alive s obj
+ | _ \<Rightarrow> alive s obj)"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def
+ intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)
+done
+
+lemma alive_other:
+ "\<lbrakk>valid (e # s);
+ \<forall> p f flag fd opt. e \<noteq> Open p f flag fd opt;
+ \<forall> p f fds. e \<noteq> Execve p f fds;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
+ \<forall> p p'. e \<noteq> Kill p p';
+ \<forall> p. e \<noteq> Exit p;
+ \<forall> p fd. e \<noteq> CloseFd p fd;
+ \<forall> p f. e \<noteq> UnLink p f;
+ \<forall> p d. e \<noteq> Rmdir p d;
+ \<forall> p d inum. e \<noteq> Mkdir p d inum;
+ \<forall> p f f'. e \<noteq> LinkHard p f f';
+ \<forall> p q. e \<noteq> CreateMsgq p q;
+ \<forall> p q m. e \<noteq> SendMsg p q m;
+ \<forall> p q m. e \<noteq> RecvMsg p q m;
+ \<forall> p q. e \<noteq> RemoveMsgq p q;
+ \<forall> p af st fd inum. e \<noteq> CreateSock p af st fd inum;
+ \<forall> p fd addr port fd' inum. e \<noteq> Accept p fd addr port fd' inum\<rbrakk>
+ \<Longrightarrow> alive (e # s) = alive s"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac x, case_tac [!] e)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps dir_is_empty_def
+ intro:is_tcp_in_current is_udp_in_current split:t_socket_type.splits)
+done
+
+lemmas alive_simps = alive_open alive_execve alive_clone alive_kill alive_exit alive_closefd alive_unlink
+ alive_rmdir alive_mkdir alive_createmsgq alive_removemsgq
+ alive_createsock alive_accept alive_other alive_sendmsg alive_recvmsg
+
+
+end
+
+end
\ No newline at end of file