# HG changeset patch # User chunhan # Date 1387334676 -28800 # Node ID 030643fab8a10c7b5675e4f50f4ea0cf91405c8e # Parent 6f7b9039715f1669a6f49bb43a4f5e99a2283197 Enrich diff -r 6f7b9039715f -r 030643fab8a1 Flask.thy --- a/Flask.thy Tue Dec 17 13:30:21 2013 +0800 +++ b/Flask.thy Wed Dec 18 10:44:36 2013 +0800 @@ -1316,7 +1316,7 @@ Some pf \ (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of (Some (pu,pr,pt), Some (du,dr,dt)) \ - (search_check s (pu,pr,pt) f \ + (search_check s (pu,pr,pt) pf \ permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \ permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) | _ \ False) diff -r 6f7b9039715f -r 030643fab8a1 no_shm_selinux/Enrich.thy --- a/no_shm_selinux/Enrich.thy Tue Dec 17 13:30:21 2013 +0800 +++ b/no_shm_selinux/Enrich.thy Wed Dec 18 10:44:36 2013 +0800 @@ -3,6 +3,14 @@ Temp begin +datatype t_enrich_obj = + E_proc "t_process" +| E_file "t_file" +| E_fd "t_process" "t_fd" +| E_inum "nat" +| E_msgq "t_msgq" +| E_msg "t_msgq" "t_msg" + context tainting_s begin (* enrich s target_proc duplicated_pro *) @@ -78,6 +86,44 @@ by (case_tac a, simp) qed +lemma enrich_search_check': + assumes grant: "search_check s (up, rp, tp) f" + and cf2sf: "\ f. f \ current_files s \ cf2sfile s' f = cf2sfile s f" + and vd: "valid s" and vd': "valid s'" and f_in: "is_dir s f" and f_in': "is_dir s' f" + and sec: "sectxt_of_obj s' (O_dir f) = sectxt_of_obj s (O_dir f)" + shows "search_check s' (up, rp, tp) f" +proof (cases f) + case Nil + have "sectxt_of_obj s' (O_dir []) = sectxt_of_obj s (O_dir [])" + using cf2sf + apply (erule_tac x = "[]" in allE) + by (auto simp:cf2sfile_def root_sec_remains vd vd') + thus ?thesis using grant Nil + by auto +next + case (Cons n pf) + from vd f_in obtain sf where sf: "cf2sfile s f = Some sf" + apply (drule_tac is_dir_in_current, drule_tac current_file_has_sfile, simp) + apply (erule exE, simp) + done + then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons + by (auto simp:cf2sfile_def split:option.splits if_splits) + from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_dir_in_current) + then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons + by (auto simp:cf2sfile_def split:option.splits if_splits) + with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in' + apply (drule_tac is_dir_not_file) + apply (drule is_dir_not_file) + apply (simp add:cf2sfile_def split:option.splits) + apply (case_tac sf, simp) + done + show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec + apply (drule_tac is_dir_not_file) + apply (drule_tac is_dir_not_file) + apply (simp add:Cons split:option.splits) + by (case_tac a, simp) +qed + lemma proc_filefd_has_sfd: "\fd \ proc_file_fds s p; valid s\ \ \ sfd. cfd2sfd s p fd = Some sfd" apply (simp add:proc_file_fds_def) apply (auto dest: current_filefd_has_sfd) @@ -132,24 +178,34 @@ apply (case_tac a, auto) done -fun enrich_not_alive :: "t_state \ t_object \ bool" +fun enrich_not_alive :: "t_state \ t_enrich_obj \ bool" where - "enrich_not_alive s (O_file f) = (f \ current_files s)" -| "enrich_not_alive s (O_dir f) = (f \ current_files s)" -| "enrich_not_alive s (O_proc p) = (p \ current_procs s)" -| "enrich_not_alive s (O_fd p fd) = (fd \ current_proc_fds s p)" -| "enrich_not_alive s (O_msgq q) = (q \ current_msgqs s)" -| "enrich_not_alive s (O_msg q m) = (m \ set (msgs_of_queue s q) \ q \ current_msgqs s)" -| "enrich_not_alive s _ = True" + "enrich_not_alive s (E_file f) = (f \ current_files s)" +| "enrich_not_alive s (E_proc p) = (p \ current_procs s)" +| "enrich_not_alive s (E_fd p fd) = (p \ current_procs s \ fd \ current_proc_fds s p)" +| "enrich_not_alive s (E_msgq q) = (q \ current_msgqs s)" +| "enrich_not_alive s (E_inum i) = (i \ current_inode_nums s)" +| "enrich_not_alive s (E_msg q m) = (q \ current_msgqs s \ m \ set (msgs_of_queue s q))" + +lemma file_has_parent: "\is_file s f; valid s\ \ \ pf. is_dir s pf \ parent f = Some pf" +apply (case_tac f) +apply (simp, drule root_is_dir', simp+) +apply (simp add:parentf_is_dir_prop2) +done lemma enrich_valid_intro_cons: assumes vs': "valid s'" and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" and alive: "\ obj. alive s obj \ alive s' obj" and alive': "\ obj. enrich_not_alive s obj \ enrich_not_alive s' obj" + and hungs: "files_hung_by_del s' = files_hung_by_del s" and cp2sp: "\ p. p \ current_procs s \ cp2sproc s' p = cp2sproc s p" and cf2sf: "\ f. f \ current_files s \ cf2sfile s' f = cf2sfile s f" + and cq2sq: "\ q. q \ current_msgqs s \ cq2smsgq s' q = cq2smsgq s q" and ffd_remain: "\ p fd f. file_of_proc_fd s p fd = Some f \ file_of_proc_fd s' p fd = Some f" + and fflags_remain: "\ p fd flags. flags_of_proc_fd s p fd = Some flags \ flags_of_proc_fd s' p fd = Some flags" + and sms_remain: "\ q. msgs_of_queue s' q = msgs_of_queue s q" + (* 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" shows "valid (e # s')" proof (cases e) @@ -209,7 +265,7 @@ apply (erule_tac x = "O_proc p" in allE) by (auto simp:Clone) have p'_not_in: "p' \ current_procs s'" using os alive' - apply (erule_tac x = "O_proc p'" in allE) + apply (erule_tac x = "E_proc p'" in allE) by (auto simp:Clone) have fd_in: "fds \ proc_file_fds s' p" using os alive ffd_remain by (auto simp:Clone proc_file_fds_def) @@ -238,8 +294,764 @@ ultimately show ?thesis using vs' by (erule_tac valid.intros(2), simp+) next + case (Kill p p') + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:Kill) + have p'_in: "p' \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p'" in allE) + by (auto simp:Kill) + have "os_grant s' e" using p_in p'_in by (simp add:Kill) + moreover have "grant s' e" + proof- + from grant obtain up rp tp up' rp' tp' + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p'1: "sectxt_of_obj s (O_proc p') = Some (up', rp', tp')" + apply (simp add:Kill split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Kill co2sobj.simps cp2sproc_def split:option.splits) + from p'1 have p'1': "sectxt_of_obj s' (O_proc p') = Some (up', rp', tp')" + using os cp2sp + apply (erule_tac x = p' in allE) + by (auto simp:Kill co2sobj.simps cp2sproc_def split:option.splits) + show ?thesis using p1 p'1 p1' p'1' grant + by (simp add:Kill) + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (Ptrace p p') + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:Ptrace) + have p'_in: "p' \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p'" in allE) + by (auto simp:Ptrace) + have "os_grant s' e" using p_in p'_in by (simp add:Ptrace) + moreover have "grant s' e" + proof- + from grant obtain up rp tp up' rp' tp' + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p'1: "sectxt_of_obj s (O_proc p') = Some (up', rp', tp')" + apply (simp add:Ptrace split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Ptrace co2sobj.simps cp2sproc_def split:option.splits) + from p'1 have p'1': "sectxt_of_obj s' (O_proc p') = Some (up', rp', tp')" + using os cp2sp + apply (erule_tac x = p' in allE) + by (auto simp:Ptrace co2sobj.simps cp2sproc_def split:option.splits) + show ?thesis using p1 p'1 p1' p'1' grant + by (simp add:Ptrace) + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (Exit p) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:Exit) + have "os_grant s' e" using p_in by (simp add:Exit) + moreover have "grant s' e" + by (simp add:Exit) + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (Open p f flags fd opt) + show ?thesis + proof (cases opt) + case None + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:Open None) + have f_in: "is_file s' f" using os alive + 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 + apply (erule_tac x = "E_fd p fd" in allE) + by (simp add:Open None) + have "os_grant s' e" using p_in f_in fd_not_in os + by (simp add:Open None) + moreover have "grant s' e" + proof- + from grant obtain up rp tp uf rf tf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" + apply (simp add:Open None split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Open None co2sobj.simps cp2sproc_def split:option.splits) + from os have f_in': "is_file s f" by (simp add:Open None) + from vd os have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_file_in_current current_file_has_sfile simp:Open None) + hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf + apply (erule_tac x = f in allE) + apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) + apply (case_tac f, simp) + apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) + done + have "search_check s' (up, rp, tp) f" + using p1 p2 p2' vd cf2sf f_in' grant Open None f_in + apply (rule_tac s = s in enrich_search_check) + by (simp_all split:option.splits) + thus ?thesis using p1' p2' + apply (simp add:Open None split:option.splits) + using grant Open None p1 p2 + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) + next + case (Some inum) + from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf" + by (auto simp:Open Some) + have pf_in: "is_dir s' pf" using pf_in_s alive + apply (erule_tac x = "O_dir pf" in allE) + by simp + 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' + apply (erule_tac x = "E_file f" in allE) + by (auto simp:Open Some) + have fd_not_in: "fd \ current_proc_fds s' p" + using os alive' p_in + apply (erule_tac x = "E_fd p fd" in allE) + by (simp add:Open Some) + have inum_not_in: "inum \ current_inode_nums s'" + using os alive' + apply (erule_tac x = "E_inum inum" in allE) + by (simp add:Open Some) + 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" + proof- + from grant parent obtain up rp tp uf rf tf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_dir pf) = Some (uf, rf, tf)" + apply (simp add:Open Some split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Open Some co2sobj.simps cp2sproc_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s pf = Some sf" + by (auto dest!:is_dir_in_current current_file_has_sfile simp:Open Some) + hence p2': "sectxt_of_obj s' (O_dir pf) = Some (uf, rf, tf)" using p2 cf2sf pf_in pf_in_s + apply (erule_tac x = pf in allE) + apply (erule exE, frule_tac s = s in is_dir_in_current, simp) + apply (drule is_dir_not_file, drule is_dir_not_file) + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac pf, simp_all) + by (simp add:sroot_def root_sec_remains vd vs') + have "search_check s' (up, rp, tp) pf" + using p1 p2 p2' vd cf2sf pf_in grant Open Some pf_in_s parent vs' + apply (rule_tac s = s in enrich_search_check') + by (simp_all split:option.splits) + thus ?thesis using p1' p2' parent + apply (simp add:Open Some split:option.splits) + using grant Open Some p1 p2 + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) + qed +next + case (ReadFile p fd) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:ReadFile) + have fd_in: "fd \ current_proc_fds s' p" using os alive + apply (erule_tac x = "O_fd p fd" in allE) + by (auto simp:ReadFile) + obtain f where ffd: "file_of_proc_fd s p fd = Some f" + using os ReadFile by auto + hence f_in_s: "is_file s f" using vd + by (auto intro:file_of_pfd_is_file) + obtain flags where fflag: "flags_of_proc_fd s p fd = Some flags" + using os ReadFile by auto + have ffd_in: "file_of_proc_fd s' p fd = Some f" + using ffd_remain ffd by auto + hence f_in: "is_file s' f" using vs' + by (auto intro:file_of_pfd_is_file) + have flags_in: "flags_of_proc_fd s' p fd = Some flags" + using fflags_remain fflag by auto + have "os_grant s' e" using p_in fd_in ffd_in flags_in fflag os f_in + by (auto simp add:ReadFile is_file_in_current) + moreover have "grant s' e" + proof- + from grant ffd obtain up rp tp uf rf tf ufd rfd tfd + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" + and p3: "sectxt_of_obj s (O_fd p fd) = Some (ufd, rfd, tfd)" + apply (simp add:ReadFile split:option.splits) + by (case_tac a, case_tac aa, case_tac ab, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:ReadFile co2sobj.simps cp2sproc_def split:option.splits) + from vd f_in_s have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_file_in_current current_file_has_sfile) + hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in_s p2 cf2sf + apply (erule_tac x = f in allE) + apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) + apply (case_tac f, simp) + apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) + done + have p3': "sectxt_of_obj s' (O_fd p fd) = Some (ufd, rfd, tfd)" + using cfd2sfd ffd_in ffd p3 f_in f_in_s vd + apply (erule_tac x = p in allE) + apply (erule_tac x = fd in allE) + apply (simp add:proc_file_fds_def) + apply (auto simp:cfd2sfd_def fflag flags_in p3 split:option.splits + dest!:current_file_has_sfile' simp:is_file_in_current) + done + show ?thesis using p1' p2' p3' ffd_in ffd + apply (simp add:ReadFile split:option.splits) + using grant p1 p2 p3 ReadFile + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (WriteFile p fd) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:WriteFile) + have fd_in: "fd \ current_proc_fds s' p" using os alive + apply (erule_tac x = "O_fd p fd" in allE) + by (auto simp:WriteFile) + obtain f where ffd: "file_of_proc_fd s p fd = Some f" + using os WriteFile by auto + hence f_in_s: "is_file s f" using vd + by (auto intro:file_of_pfd_is_file) + obtain flags where fflag: "flags_of_proc_fd s p fd = Some flags" + using os WriteFile by auto + have ffd_in: "file_of_proc_fd s' p fd = Some f" + using ffd_remain ffd by auto + hence f_in: "is_file s' f" using vs' + by (auto intro:file_of_pfd_is_file) + have flags_in: "flags_of_proc_fd s' p fd = Some flags" + using fflags_remain fflag by auto + have "os_grant s' e" using p_in fd_in ffd_in flags_in fflag os f_in + by (auto simp add:WriteFile is_file_in_current) + moreover have "grant s' e" + proof- + from grant ffd obtain up rp tp uf rf tf ufd rfd tfd + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" + and p3: "sectxt_of_obj s (O_fd p fd) = Some (ufd, rfd, tfd)" + apply (simp add:WriteFile split:option.splits) + by (case_tac a, case_tac aa, case_tac ab, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:WriteFile co2sobj.simps cp2sproc_def split:option.splits) + from vd f_in_s have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_file_in_current current_file_has_sfile) + hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in_s p2 cf2sf + apply (erule_tac x = f in allE) + apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) + apply (case_tac f, simp) + apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) + done + have p3': "sectxt_of_obj s' (O_fd p fd) = Some (ufd, rfd, tfd)" + using cfd2sfd ffd_in ffd p3 f_in f_in_s vd + apply (erule_tac x = p in allE) + apply (erule_tac x = fd in allE) + apply (simp add:proc_file_fds_def) + apply (auto simp:cfd2sfd_def fflag flags_in p3 split:option.splits + dest!:current_file_has_sfile' simp:is_file_in_current) + done + show ?thesis using p1' p2' p3' ffd_in ffd + apply (simp add:WriteFile split:option.splits) + using grant p1 p2 p3 WriteFile + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (CloseFd p fd) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:CloseFd) + have fd_in: "fd \ current_proc_fds s' p" using os alive + apply (erule_tac x = "O_fd p fd" in allE) + by (auto simp:CloseFd) + have "os_grant s' e" using p_in fd_in + by (auto simp add:CloseFd) + moreover have "grant s' e" + by(simp add:CloseFd) + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (UnLink p f) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:UnLink) + have f_in: "is_file s' f" using os alive + apply (erule_tac x = "O_file f" in allE) + by (auto simp:UnLink) + from os vd obtain pf where pf_in_s: "is_dir s pf" + and parent: "parent f = Some pf" + by (auto simp:UnLink dest!:file_has_parent) + from pf_in_s alive have pf_in: "is_dir s' pf" + apply (erule_tac x = "O_dir pf" in allE) + by (auto simp:UnLink) + have "os_grant s' e" using p_in f_in os + by (simp add:UnLink hungs) + moreover have "grant s' e" + proof- + from grant parent obtain up rp tp uf rf tf upf rpf tpf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" + and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" + apply (simp add:UnLink split:option.splits) + by (case_tac a, case_tac aa, case_tac ab, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:UnLink co2sobj.simps cp2sproc_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_file_in_current current_file_has_sfile simp:UnLink) + hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" + using p2 cf2sf f_in os parent + apply (erule_tac x = f in allE) + apply (erule exE, clarsimp simp:UnLink) + apply (frule_tac s = s in is_file_in_current, simp) + by (auto simp:cf2sfile_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s pf = Some sf" + by (auto dest!:is_dir_in_current current_file_has_sfile simp:UnLink) + hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s + apply (erule_tac x = pf in allE) + apply (erule exE, frule_tac s = s in is_dir_in_current, simp) + apply (drule is_dir_not_file, drule is_dir_not_file) + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac pf, simp_all) + by (simp add:sroot_def root_sec_remains vd vs') + have "search_check s' (up, rp, tp) f" + using p1 p2 p2' vd cf2sf f_in grant UnLink os parent vs' + apply (rule_tac s = s in enrich_search_check) + by (simp_all split:option.splits) + thus ?thesis using p1' p2' p3' parent + apply (simp add:UnLink split:option.splits) + using grant UnLink p1 p2 p3 + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (Rmdir p f) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:Rmdir) + have f_in: "is_dir s' f" using os alive + apply (erule_tac x = "O_dir f" in allE) + by (auto simp:Rmdir dir_is_empty_def) + have not_root: "f \ []" using os + by (auto simp:Rmdir) + from os vd obtain pf where pf_in_s: "is_dir s pf" + and parent: "parent f = Some pf" + apply (auto simp:Rmdir dir_is_empty_def) + apply (case_tac f, simp+) + apply (drule parentf_is_dir_prop1, auto) + done + 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 + apply (simp add:dir_is_empty_def f_in) + apply auto using alive' + apply (erule_tac x = "E_file f'" in allE) + by (simp add:Rmdir dir_is_empty_def) + have "os_grant s' e" using p_in f_in os empty_in + by (simp add:Rmdir hungs) + moreover have "grant s' e" + proof- + from grant parent obtain up rp tp uf rf tf upf rpf tpf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_dir f) = Some (uf, rf, tf)" + and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" + apply (simp add:Rmdir split:option.splits) + by (case_tac a, case_tac aa, case_tac ab, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Rmdir co2sobj.simps cp2sproc_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_dir_in_current current_file_has_sfile simp:dir_is_empty_def Rmdir) + hence p2': "sectxt_of_obj s' (O_dir f) = Some (uf, rf, tf)" + using p2 cf2sf f_in os parent + apply (erule_tac x = f in allE) + apply (erule exE, clarsimp simp:Rmdir dir_is_empty_def) + apply (frule_tac s = s in is_dir_in_current, simp) + apply (drule is_dir_not_file, drule is_dir_not_file) + by (auto simp:cf2sfile_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s pf = Some sf" + by (auto dest!:is_dir_in_current current_file_has_sfile simp:Rmdir) + hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s + apply (erule_tac x = pf in allE) + apply (erule exE, frule_tac s = s in is_dir_in_current, simp) + apply (drule is_dir_not_file, drule is_dir_not_file) + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac pf, simp_all) + by (simp add:sroot_def root_sec_remains vd vs') + have "search_check s' (up, rp, tp) f" + using p1 p2 p2' vd cf2sf f_in grant Rmdir os parent vs' + apply (rule_tac s = s in enrich_search_check') + by (simp_all add:dir_is_empty_def split:option.splits) + thus ?thesis using p1' p2' p3' parent + apply (simp add:Rmdir split:option.splits) + using grant Rmdir p1 p2 p3 + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (Mkdir p f inum) + from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f = Some pf" + by (auto simp:Mkdir) + have pf_in: "is_dir s' pf" using pf_in_s alive + apply (erule_tac x = "O_dir pf" in allE) + by simp + 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' + apply (erule_tac x = "E_file f" in allE) + by (auto simp:Mkdir) + have inum_not_in: "inum \ current_inode_nums s'" + using os alive' + apply (erule_tac x = "E_inum inum" in allE) + by (simp add:Mkdir) + 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" + proof- + from grant parent obtain up rp tp uf rf tf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_dir pf) = Some (uf, rf, tf)" + apply (simp add:Mkdir split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Mkdir co2sobj.simps cp2sproc_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s pf = Some sf" + by (auto dest!:is_dir_in_current current_file_has_sfile simp:Mkdir) + hence p2': "sectxt_of_obj s' (O_dir pf) = Some (uf, rf, tf)" using p2 cf2sf pf_in pf_in_s + apply (erule_tac x = pf in allE) + apply (erule exE, frule_tac s = s in is_dir_in_current, simp) + apply (drule is_dir_not_file, drule is_dir_not_file) + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac pf, simp_all) + by (simp add:sroot_def root_sec_remains vd vs') + have "search_check s' (up, rp, tp) pf" + using p1 p2 p2' vd cf2sf pf_in grant Mkdir pf_in_s parent vs' + apply (rule_tac s = s in enrich_search_check') + apply (simp_all split:option.splits) + done + thus ?thesis using p1' p2' parent + apply (simp add:Mkdir split:option.splits) + using grant Mkdir p1 p2 + apply simp + done + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (LinkHard p f f') + from os obtain pf where pf_in_s: "is_dir s pf" and parent: "parent f' = Some pf" + by (auto simp:LinkHard) + have pf_in: "is_dir s' pf" using pf_in_s alive + apply (erule_tac x = "O_dir pf" in allE) + by simp + 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' + apply (erule_tac x = "E_file f'" in allE) + by (auto simp:LinkHard) + have f_in: "is_file s' f" using os alive + apply (erule_tac x = "O_file f" in allE) + by (auto simp:LinkHard) + have "os_grant s' e" using p_in pf_in parent os f_in f'_not_in + by (simp add:LinkHard hungs) + moreover have "grant s' e" + proof- + from grant parent obtain up rp tp uf rf tf upf rpf tpf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" + and p3: "sectxt_of_obj s (O_dir pf) = Some (upf, rpf, tpf)" + apply (simp add:LinkHard split:option.splits) + by (case_tac a, case_tac aa, case_tac ab, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:LinkHard co2sobj.simps cp2sproc_def split:option.splits) + from vd os pf_in_s have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_file_in_current current_file_has_sfile simp:LinkHard) + hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" + using p2 cf2sf f_in os parent + apply (erule_tac x = f in allE) + apply (erule exE, clarsimp simp:LinkHard) + apply (frule_tac s = s in is_file_in_current, simp) + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac f, simp) + by (drule_tac s = s in root_is_dir', simp add:vd, simp+) + from vd os pf_in_s have "\ sf. cf2sfile s pf = Some sf" + by (auto dest!:is_dir_in_current current_file_has_sfile simp:LinkHard) + hence p3': "sectxt_of_obj s' (O_dir pf) = Some (upf, rpf, tpf)" using p3 cf2sf pf_in pf_in_s + apply (erule_tac x = pf in allE) + apply (erule exE, frule_tac s = s in is_dir_in_current, simp) + apply (drule is_dir_not_file, drule is_dir_not_file) + apply (auto simp:cf2sfile_def split:option.splits) + apply (case_tac pf, simp_all) + by (simp add:sroot_def root_sec_remains vd vs') + have "search_check s' (up, rp, tp) f" + using p1 p2 p2' vd cf2sf f_in grant LinkHard os parent vs' + apply (rule_tac s = s in enrich_search_check) + by (simp_all split:option.splits) + moreover have "search_check s' (up, rp, tp) pf" + using p1 p3 p3' vd cf2sf pf_in grant LinkHard os parent vs' + apply (rule_tac s = s in enrich_search_check') + apply (simp_all split:option.splits) + done + ultimately show ?thesis using p1' p2' p3' parent + apply (simp add:LinkHard split:option.splits) + using grant LinkHard p1 p2 p3 + apply simp + done + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (Truncate p f len) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:Truncate) + have f_in: "is_file s' f" using os alive + apply (erule_tac x = "O_file f" in allE) + by (auto simp:Truncate) + have "os_grant s' e" using p_in f_in by (simp add:Truncate) + moreover have "grant s' e" + proof- + from grant obtain up rp tp uf rf tf + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" + apply (simp add:Truncate split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:Truncate co2sobj.simps cp2sproc_def split:option.splits) + from os have f_in': "is_file s f" by (simp add:Truncate) + from vd os have "\ sf. cf2sfile s f = Some sf" + by (auto dest!:is_file_in_current current_file_has_sfile simp:Truncate) + hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf + apply (erule_tac x = f in allE) + apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) + apply (case_tac f, simp) + apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) + done + have "search_check s' (up, rp, tp) f" + using p1 p2 p2' vd cf2sf f_in' grant Truncate f_in + apply (rule_tac s = s in enrich_search_check) + by (simp_all split:option.splits) + thus ?thesis using p1' p2' + apply (simp add:Truncate split:option.splits) + using grant Truncate p1 p2 + by (simp add:Truncate grant p1 p2) + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (CreateMsgq p q) + 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' + apply (erule_tac x = "E_msgq q" in allE) + by (simp add:CreateMsgq) + have "os_grant s' e" using p_in q_not_in by (simp add:CreateMsgq) + moreover have "grant s' e" + proof- + from grant obtain up rp tp + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + apply (simp add:CreateMsgq split:option.splits) + by (case_tac a, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:CreateMsgq co2sobj.simps cp2sproc_def split:option.splits) + show ?thesis using p1' + apply (simp add:CreateMsgq split:option.splits) + using grant CreateMsgq p1 + by simp + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (RemoveMsgq p q) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:RemoveMsgq) + have q_in: "q \ current_msgqs s'" using os alive + apply (erule_tac x = "O_msgq q" in allE) + by (simp add:RemoveMsgq) + have "os_grant s' e" using p_in q_in by (simp add:RemoveMsgq) + moreover have "grant s' e" + proof- + from grant obtain up rp tp uq rq tq + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)" + apply (simp add:RemoveMsgq split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:RemoveMsgq co2sobj.simps cp2sproc_def split:option.splits) + from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)" + using os cq2sq vd + apply (erule_tac x = q in allE) + by (auto simp:RemoveMsgq co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits) + show ?thesis using p1' p2' grant p1 p2 + by (simp add:RemoveMsgq) + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (SendMsg p q m) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:SendMsg) + 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' + apply (erule_tac x = "E_msg q m" in allE) + by (simp add:SendMsg q_in) + have "os_grant s' e" using p_in q_in m_not_in + by (simp add:SendMsg) + moreover have "grant s' e" + proof- + from grant obtain up rp tp uq rq tq + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)" + apply (simp add:SendMsg split:option.splits) + by (case_tac a, case_tac aa, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:SendMsg co2sobj.simps cp2sproc_def split:option.splits) + from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)" + using os cq2sq vd + apply (erule_tac x = q in allE) + by (auto simp:SendMsg co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits) + show ?thesis using p1' p2' grant p1 p2 + by (simp add:SendMsg) + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (RecvMsg p q m) + have p_in: "p \ current_procs s'" using os alive + apply (erule_tac x = "O_proc p" in allE) + by (auto simp:RecvMsg) + have q_in: "q \ current_msgqs s'" using os alive + apply (erule_tac x = "O_msgq q" in allE) + by (simp add:RecvMsg) + have m_in: "m = hd (msgs_of_queue s' q)" + and sms_not_empty: "msgs_of_queue s' q \ []" + using os sms_remain + by (auto simp:RecvMsg) + have "os_grant s' e" using p_in q_in m_in sms_not_empty os + by (simp add:RecvMsg) + moreover have "grant s' e" + proof- + from grant obtain up rp tp uq rq tq um rm tm + where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" + and p2: "sectxt_of_obj s (O_msgq q) = Some (uq, rq, tq)" + and p3: "sectxt_of_obj s (O_msg q m) = Some (um, rm, tm)" + apply (simp add:RecvMsg split:option.splits) + by (case_tac a, case_tac aa, case_tac ab, blast) + from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" + using os cp2sp + apply (erule_tac x = p in allE) + by (auto simp:RecvMsg co2sobj.simps cp2sproc_def split:option.splits) + from p2 have p2': "sectxt_of_obj s' (O_msgq q) = Some (uq, rq, tq)" + using os cq2sq vd + apply (erule_tac x = q in allE) + by (auto simp:RecvMsg co2sobj.simps cq2smsgq_def dest!:current_has_sms' split:option.splits) + from p3 have p3': "sectxt_of_obj s' (O_msg q m) = Some (um, rm, tm)" + using sms_remain cq2sq vd os p2 p2' p3 + apply (erule_tac x = q in allE) + apply (erule_tac x = q in allE) + apply (clarsimp simp:RecvMsg) + apply (simp add:cq2smsgq_def split:option.splits if_splits) + apply (drule current_has_sms', simp, simp) + apply (case_tac "msgs_of_queue s q", simp) + apply (simp add:cqm2sms.simps split:option.splits) + apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1] + apply (case_tac "msgs_of_queue s q", simp) + apply (simp add:cqm2sms.simps split:option.splits) + apply (auto simp add:cm2smsg_def split:option.splits if_splits)[1] + done + show ?thesis using p1' p2' p3' grant p1 p2 p3 + by (simp add:RecvMsg) + qed + ultimately show ?thesis using vs' + by (erule_tac valid.intros(2), simp+) +next + case (CreateSock p af st fd inum) + show ?thesis using grant + by (simp add:CreateSock) +next + case (Bind p fd addr) + show ?thesis using grant + by (simp add:Bind) +next + case (Connect p fd addr) + show ?thesis using grant + by (simp add:Connect) +next + case (Listen p fd) + show ?thesis using grant + by (simp add:Listen) +next + case (Accept p fd addr port fd' inum) + show ?thesis using grant + by (simp add:Accept) +next + case (SendSock p fd) + show ?thesis using grant + by (simp add:SendSock) +next + case (RecvSock p fd) + show ?thesis using grant + by (simp add:RecvSock) +next + case (Shutdown p fd how) + show ?thesis using grant + by (simp add:Shutdown) +qed - + + + + + + + + diff -r 6f7b9039715f -r 030643fab8a1 no_shm_selinux/Flask.thy --- a/no_shm_selinux/Flask.thy Tue Dec 17 13:30:21 2013 +0800 +++ b/no_shm_selinux/Flask.thy Wed Dec 18 10:44:36 2013 +0800 @@ -1378,7 +1378,7 @@ Some pf \ (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of (Some (pu,pr,pt), Some (du,dr,dt)) \ - (search_check s (pu,pr,pt) f \ + (search_check s (pu,pr,pt) pf \ permission_check (pu,pr,pt) (nfctxt_create (pu,pr,pt) (du,dr,dt) C_dir) C_dir P_create \ permission_check (pu,pr,pt) (du,dr,dt) C_dir P_add_name) | _ \ False)