diff -r 924ab7a4e7fa -r 271e9818b6f6 simple_selinux/Alive_prop.thy
--- /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