diff -r e832378a2ff2 -r ded3f83f6cb9 no_shm_selinux/Enrich.thy --- a/no_shm_selinux/Enrich.thy Wed Jan 01 23:00:24 2014 +0800 +++ b/no_shm_selinux/Enrich.thy Mon Jan 06 23:07:51 2014 +0800 @@ -3,14 +3,28 @@ Temp begin -(* objects that need dynamic indexing, all nature-numbers *) +(* enriched objects, closely related to static objects, so are only 3 kinds *) datatype t_enrich_obj = - E_proc "t_process" -| E_file "t_file" -| E_fd "t_process" "t_fd" -| E_inum "nat" + E_proc "t_process" "t_msgq" "t_msgq" +| E_file_link "t_file" +| E_file "t_file" "nat" + (* +| E_fd "t_process" "t_fd" +| E_inum "nat" *) | E_msgq "t_msgq" +(* | E_msg "t_msgq" "t_msg" +*) + + +(* objects that need dynamic indexing, all nature-numbers *) +datatype t_index_obj = + I_proc "t_process" +| I_file "t_file" +| I_fd "t_process" "t_fd" +| I_inum "nat" +| I_msgq "t_msgq" +| I_msg "t_msgq" "t_msg" context tainting_s begin @@ -73,6 +87,7 @@ | "all_files (LinkHard p f f' # s) = all_files s \ {f'}" | "all_files (e # s) = all_files s" +(* fun notin_all:: "t_state \ t_enrich_obj \ bool" where "notin_all s (E_proc p) = (p \ all_procs s)" @@ -81,6 +96,37 @@ | "notin_all s (E_inum i) = (i \ all_inums s)" | "notin_all s (E_msgq q) = (q \ all_msgqs s)" | "notin_all s (E_msg q m) = (m \ all_msgs s q)" +*) + +fun nums_of_recvmsg:: "t_state \ t_process \ nat" +where + "nums_of_recvmsg [] p' = 0" +| "nums_of_recvmsg (RecvMsg p q m # s) p' = + (if p' = p then Suc (nums_of_recvmsg s p) else nums_of_recvmsg s p')" +| "nums_of_recvmsg (e # s) p' = nums_of_recvmsg s p'" + +lemma nums_of_recv_0: + "\p \ current_procs s; no_del_event s; valid s\ \ nums_of_recvmsg s p = 0" +apply (induct s, simp) +apply (frule vt_grant_os, frule vd_cons, case_tac a) +apply (auto) +done + +lemma new_msgq_1: + "\new_msgq s \ q; q \ new_msgq s - Suc 0\ \ False" +apply (subgoal_tac "new_msgq s \ 0") +apply (simp, simp add:new_msgq_def next_nat_def) +done + +fun notin_cur:: "t_state \ t_enrich_obj \ bool" +where + "notin_cur s (E_proc p qmin qmax) = + (p \ current_procs s \ qmin = new_msgq s \ qmax = new_msgq s + (nums_of_recvmsg s p) - 1)" +| "notin_cur s (E_file f inum) = + (f \ current_files s \ (\ pf. parent f = Some pf \ is_dir s pf) \ inum \ current_inode_nums s)" +| "notin_cur s (E_file_link f) = + (f \ current_files s \ (\ pf. parent f = Some pf \ is_dir s pf))" +| "notin_cur s (E_msgq q) = (q \ current_msgqs s)" lemma not_all_procs_cons: "p \ all_procs (e # s) \ p \ all_procs s" @@ -118,17 +164,24 @@ "p' \ all_msgqs s \ p' \ current_msgqs s" apply (induct s, simp) by (case_tac a, auto) - -fun enrich_not_alive :: "t_state \ t_enrich_obj \ t_enrich_obj \ bool" + +fun enrich_not_alive :: "t_state \ t_enrich_obj \ t_index_obj \ bool" where - "enrich_not_alive s obj (E_file f) = (f \ current_files s \ obj \ E_file f)" -| "enrich_not_alive s obj (E_proc p) = (p \ current_procs s \ obj \ E_proc p)" -| "enrich_not_alive s obj (E_fd p fd) = - ((p \ current_procs s \ fd \ current_proc_fds s p) \ obj \ E_fd p fd \ obj \ E_proc p)" -| "enrich_not_alive s obj (E_msgq q) = (q \ current_msgqs s \ obj \ E_msgq q)" -| "enrich_not_alive s obj (E_inum i) = (i \ current_inode_nums s \ obj \ E_inum i)" -| "enrich_not_alive s obj (E_msg q m) = - ((q \ current_msgqs s \ m \ set (msgs_of_queue s q)) \ obj \ E_msg q m \ obj \ E_msgq q)" + "enrich_not_alive s obj (I_file f) = + (f \ current_files s \ (\ inum. obj \ E_file f inum) \ obj \ E_file_link f)" +| "enrich_not_alive s obj (I_proc p) = (p \ current_procs s \ (\ qmin qmax. obj \ E_proc p qmin qmax))" +| "enrich_not_alive s obj (I_fd p fd) = + ((p \ current_procs s \ fd \ current_proc_fds s p) \ (\ qmin qmax. obj \ E_proc p qmin qmax))" +| "enrich_not_alive s obj (I_msgq q) = (q \ current_msgqs s \ obj \ E_msgq q \ + (case obj of + E_proc p qmin qmax \ \ (q \ qmin \ q \ qmax) + | _ \ True) )" +| "enrich_not_alive s obj (I_inum i) = (i \ current_inode_nums s \ (\ f. obj \ E_file f i))" +| "enrich_not_alive s obj (I_msg q m) = + ((q \ current_msgqs s \ m \ set (msgs_of_queue s q)) \ obj \ E_msgq q \ + (case obj of + E_proc p qmin qmax \ \ (q \ qmin \ q \ qmax) + | _ \ True) )" lemma file_has_parent: "\is_file s f; valid s\ \ \ pf. is_dir s pf \ parent f = Some pf" apply (case_tac f) @@ -310,7 +363,7 @@ (* and empty_remain: "\ f. dir_is_empty s f \ dir_is_empty s' f" *) and cfd2sfd: "\ p fd. fd \ proc_file_fds s p \ cfd2sfd s' p fd = cfd2sfd s p fd" and nodel: "no_del_event (e # s)" - and notin_all: "notin_all (e # s) obj'" + and notin_cur: "notin_cur (e # s) obj'" shows "valid (e # s')" proof- from vd' have os: "os_grant s e" and grant: "grant s e" and vd: "valid s" @@ -372,9 +425,9 @@ have p_in: "p \ current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Clone) - have p'_not_in: "p' \ current_procs s'" using alive' notin_all os Clone - apply (erule_tac x = "E_proc p'" in allE) - apply (auto dest:not_all_procs_prop3) + have p'_not_in: "p' \ current_procs s'" using alive' notin_cur os Clone + apply (erule_tac x = "I_proc p'" in allE) + apply (auto dest:not_all_procs_prop3 simp del:nums_of_recvmsg.simps) done have fd_in: "fds \ proc_file_fds s' p" using os alive ffd_remain by (auto simp:Clone proc_file_fds_def) @@ -482,8 +535,8 @@ apply (erule_tac x = "O_file f" in allE) by (auto simp:Open None) have fd_not_in: "fd \ current_proc_fds s' p" - using os alive' p_in notin_all Open None - apply (erule_tac x = "E_fd p fd" in allE) + using os alive' p_in notin_cur Open None + apply (erule_tac x = "I_fd p fd" in allE) apply (case_tac obj') apply (auto dest:not_all_procs_prop3) done @@ -530,19 +583,20 @@ have p_in: "p \ current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Open Some) - have f_not_in: "f \ current_files s'" using os alive' Open Some notin_all - apply (erule_tac x = "E_file f" in allE) - apply (case_tac obj') - by auto + have f_not_in: "f \ current_files s'" using os alive' Open Some notin_cur nodel + apply (erule_tac x = "I_file f" in allE) + by (case_tac obj', auto simp:current_files_simps) have fd_not_in: "fd \ current_proc_fds s' p" - using os alive' p_in Open Some notin_all - apply (erule_tac x = "E_fd p fd" in allE) + using os alive' p_in Open Some notin_cur + apply (erule_tac x = "I_fd p fd" in allE) apply (case_tac obj', auto dest:not_all_procs_prop3) done have inum_not_in: "inum \ current_inode_nums s'" - using os alive' Open Some notin_all - apply (erule_tac x = "E_inum inum" in allE) - by (case_tac obj', auto) + using os alive' Open Some notin_cur nodel + apply (erule_tac x = "I_inum inum" in allE) + apply (case_tac obj', auto) + apply (auto simp add:current_inode_nums_def current_file_inums_def split:if_splits) + done have "os_grant s' e" using p_in pf_in parent f_not_in fd_not_in inum_not_in os by (simp add:Open Some hungs) moreover have "grant s' e" @@ -780,10 +834,10 @@ from pf_in_s alive have pf_in: "is_dir s' pf" apply (erule_tac x = "O_dir pf" in allE) by (auto simp:Rmdir) - have empty_in: "dir_is_empty s' f" using os Rmdir notin_all + have empty_in: "dir_is_empty s' f" using os Rmdir notin_cur apply (clarsimp simp add:dir_is_empty_def f_in) using alive' - apply (erule_tac x = "E_file f'" in allE) + apply (erule_tac x = "I_file f'" in allE) apply simp apply (erule disjE) apply (erule_tac x = f' in allE, simp) @@ -797,6 +851,16 @@ apply (erule_tac x = pf in allE) apply (drule_tac f = pf in is_dir_in_current) apply (simp add:noJ_Anc) + + apply (clarsimp) + apply (drule_tac f' = f in parent_ancen) + apply (simp, rule notI, simp add:noJ_Anc) + apply (case_tac "f = pf") + using vd' Rmdir + apply (simp_all add:is_dir_rmdir) + apply (erule_tac x = pf in allE) + apply (drule_tac f = pf in is_dir_in_current) + apply (simp add:noJ_Anc) done have "os_grant s' e" using p_in f_in os empty_in by (simp add:Rmdir hungs) @@ -851,13 +915,15 @@ have p_in: "p \ current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:Mkdir) - have f_not_in: "f \ current_files s'" using os alive' Mkdir notin_all - apply (erule_tac x = "E_file f" in allE) - by (auto) + have f_not_in: "f \ current_files s'" + using os alive' Mkdir notin_cur + apply (erule_tac x = "I_file f" in allE) + by (auto simp:current_files_simps) have inum_not_in: "inum \ current_inode_nums s'" - using os alive' Mkdir notin_all - apply (erule_tac x = "E_inum inum" in allE) - by (auto) + using os alive' Mkdir notin_cur + apply (erule_tac x = "I_inum inum" in allE) + apply (auto simp:current_inode_nums_def current_file_inums_def split:if_splits) + done have "os_grant s' e" using p_in pf_in parent f_not_in os inum_not_in by (simp add:Mkdir hungs) moreover have "grant s' e" @@ -903,9 +969,11 @@ have p_in: "p \ current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:LinkHard) - have f'_not_in: "f' \ current_files s'" using os alive' LinkHard notin_all - apply (erule_tac x = "E_file f'" in allE) - by (auto simp:LinkHard) + have f'_not_in: "f' \ current_files s'" + using os alive' LinkHard notin_cur vd' + apply (erule_tac x = "I_file f'" in allE) + apply (auto simp:LinkHard current_files_simps) + done have f_in: "is_file s' f" using os alive apply (erule_tac x = "O_file f" in allE) by (auto simp:LinkHard) @@ -1004,9 +1072,13 @@ have p_in: "p \ current_procs s'" using os alive apply (erule_tac x = "O_proc p" in allE) by (auto simp:CreateMsgq) - have q_not_in: "q \ current_msgqs s'" using os alive' CreateMsgq notin_all - apply (erule_tac x = "E_msgq q" in allE) - by auto + have q_not_in: "q \ current_msgqs s'" + using os alive' CreateMsgq notin_cur nodel vd + apply (erule_tac x = "I_msgq q" in allE) + apply (auto split:t_enrich_obj.splits) + apply (drule nums_of_recv_0, simp+) + apply (drule new_msgq_1, simp+) + done have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq) moreover have "grant s' e" proof- @@ -1062,9 +1134,12 @@ have q_in: "q \ current_msgqs s'" using os alive apply (erule_tac x = "O_msgq q" in allE) by (simp add:SendMsg) - have m_not_in: "m \ set (msgs_of_queue s' q)" using os alive' notin_all SendMsg q_in - apply (erule_tac x = "E_msg q m" in allE) + have m_not_in: "m \ set (msgs_of_queue s' q)" + using os alive' notin_cur SendMsg q_in nodel vd + apply (erule_tac x = "I_msg q m" in allE) apply (case_tac obj', auto dest:not_all_msgqs_prop3) + apply (drule nums_of_recv_0, simp+) + apply (drule new_msgq_1, simp+) done have "os_grant s' e" using p_in q_in m_not_in sms_remain os by (simp add:SendMsg)