# HG changeset patch # User chunhan # Date 1368603766 -28800 # Node ID f2788297625144067ade592ab318ca91b4ad37b0 # Parent 8779d321cc2e9a21d59dc71f6bc04887c7a99d2a finally get cf2sfile path property done diff -r 8779d321cc2e -r f27882976251 Co2sobj_prop.thy --- a/Co2sobj_prop.thy Wed May 15 11:21:39 2013 +0800 +++ b/Co2sobj_prop.thy Wed May 15 15:42:46 2013 +0800 @@ -8,8 +8,6 @@ (************ simpset for cf2sfile ***************) -declare get_parentfs_ctxts.simps [simp del] - lemma sroot_only: "cf2sfile s [] = Some sroot" by (simp add:cf2sfile_def) @@ -71,6 +69,49 @@ apply (auto simp:cf2sfile_def split:if_splits option.splits) done +lemma sroot_set: + "valid s \ \ sec. sroot = (Init [], sec, None, {}) \ sectxt_of_obj s (O_dir []) = Some sec" +apply (frule root_is_dir) +apply (drule is_dir_has_sec, simp) +apply (auto simp:sroot_def sec_of_root_def sectxt_of_obj_def type_of_obj.simps + root_type_remains root_user_remains + dest!:root_has_type' root_has_user' root_has_init_type' root_has_init_user' + split:option.splits) +done + +lemma cf2sfile_path_file: + "\is_file s (f # pf); valid s\ + \ cf2sfile s (f # pf) = ( + case (cf2sfile s pf) of + Some (pfi, pfsec, psec, asecs) \ + (case (sectxt_of_obj s (O_file (f # pf))) of + Some fsec \ Some (if (\ deleted (O_file (f # pf)) s \ is_init_file (f # pf)) then Init (f # pf) + else Created, fsec, Some pfsec, asecs \ {pfsec}) + | None \ None) + | _ \ None)" +apply (frule is_file_in_current, drule parentf_is_dir'', simp) +apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp) +apply (frule sroot_set) +apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) +done + +lemma cf2sfile_path_dir: + "\is_dir s (f # pf); valid s\ + \ cf2sfile s (f # pf) = ( + case (cf2sfile s pf) of + Some (pfi, pfsec, psec, asecs) \ + (case (sectxt_of_obj s (O_dir (f # pf))) of + Some fsec \ Some (if (\ deleted (O_dir (f # pf)) s \ is_init_dir (f # pf)) then Init (f # pf) + else Created, fsec, Some pfsec, asecs \ {pfsec}) + | None \ None) + | _ \ None)" +apply (frule is_dir_in_current, drule parentf_is_dir'', simp) +apply (frule_tac f = "f # pf" in is_dir_has_sfile, simp) +apply (frule_tac f = "pf" in is_dir_has_sfile, simp) +apply (frule sroot_set) +apply (case_tac pf, (clarsimp simp:get_parentfs_ctxts'_def sectxt_of_pf_def)+) +done + lemma cf2sfile_path: "\f # pf \ current_files s; valid s\ \ cf2sfile s (f # pf) = ( case (cf2sfile s pf) of @@ -80,16 +121,38 @@ else Created, fsec, Some pfsec, asecs \ {pfsec}) | None \ None) else (case (sectxt_of_obj s (O_dir (f # pf))) of - Some fsec \ Some (if (\ deleted (O_dir (f # pf)) s \ is_init_file (f # pf)) then Init (f # pf) + Some fsec \ Some (if (\ deleted (O_dir (f # pf)) s \ is_init_dir (f # pf)) then Init (f # pf) else Created, fsec, Some pfsec, asecs \ {pfsec}) | None \ None) ) | None \ None)" +apply (drule is_file_or_dir, simp) +apply (erule disjE) +apply (frule cf2sfile_path_file, simp) defer +apply (frule cf2sfile_path_dir, simp, drule is_dir_not_file) +apply (auto split:option.splits) +done + + + +apply simp + +thm cf2sfile_def +apply (simp (no_asm_simp)) +apply simp +apply (frule cf2sfile_path_file, simp) +apply (simp add: cf2sfile_path_file) +apply auto +apply (simp only:cf2sfile_path_file) +by (simp add:cf2sfile_path_file cf2sfile_path_dir) apply (frule parentf_is_dir'', simp) -apply (frule parentf_in_current', simp) apply (frule is_file_or_dir, simp) -apply (frule_tac f = pf in current_file_has_sfile, simp, erule exE) -apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop - simp:cf2sfile_def split:option.splits if_splits) +apply (frule sroot_set, erule disjE) +apply (frule is_dir_has_sfile, simp, frule is_file_has_sfile, simp) +apply (case_tac pf, clarsimp) +apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop simp:cf2sfile_def get_parentfs_ctxts.simps + simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1] +apply (auto dest!:is_file_has_sec' is_dir_has_sec' get_pfs_secs_prop + simp:get_parentfs_ctxts'_def sectxt_of_pf_def split:option.splits if_splits)[1] apply (case_tac "is_file s (f # pf)") apply (frule is_file_has_sec, simp) apply (frule is_dir_has_sec, simp) diff -r 8779d321cc2e -r f27882976251 Current_files_prop.thy --- a/Current_files_prop.thy Wed May 15 11:21:39 2013 +0800 +++ b/Current_files_prop.thy Wed May 15 15:42:46 2013 +0800 @@ -215,25 +215,27 @@ have "\ f. f \ files_hung_by_del (a # \) \ inum_of_file (a # \) f \ None" apply (clarify, case_tac a) using os fin - apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def + apply (auto simp:files_hung_by_del.simps inum_of_file.simps os_grant.simps current_files_def is_file_def split:if_splits option.splits) done moreover have "\f pf im. parent f = Some pf \ inum_of_file (a # \) f = Some im \ inum_of_file (a # \) pf \ None" apply (clarify, case_tac a) using vt os pin' - apply (auto simp:os_grant.simps current_files_def inum_of_file.simps split:if_splits option.splits) + apply (auto simp:os_grant.simps current_files_def inum_of_file.simps is_file_def is_dir_def + split:if_splits option.splits t_inode_tag.splits) apply (drule_tac f = pf and f' = f in hns', simp, simp, simp) - apply (drule_tac f = list and f' = f in fns', simp, simp, simp) - apply (drule_tac f = list and f' = f in dns', simp, simp, simp) + apply (rule_tac f = list and f' = f in fns', simp add:is_file_def, simp, simp) + apply (rule_tac f = list and f' = f in dns', simp add:is_dir_def, simp, simp) done moreover have "\f f' im. is_file (a # \) f \ parent f' = Some f \ inum_of_file (a # \) f' = Some im \ False" apply (clarify, case_tac a) - using vt os fns'' + using vt os fns'' cons apply (auto simp:os_grant.simps current_files_def inum_of_file.simps itag_of_inum.simps is_file_def is_dir_def dest:ios's_im_in_cim iof's_im_in_cim - split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) + split:if_splits option.splits t_inode_tag.splits t_socket_type.splits) + apply (rule_tac im = a and f = f and f' = f' in fns'', simp+) apply (drule_tac f = f' and pf = list in pin', simp, simp) apply (drule_tac f = f' and pf = list2 in pin', simp, simp) done @@ -370,7 +372,7 @@ apply (induct \) apply (clarsimp simp add:file_of_proc_fd.simps inum_of_file.simps init_filefd_prop1 init_file_has_inum) apply ((rule_tac allI|rule_tac impI|erule_tac conjE)+, frule vd_cons, frule vt_grant_os, case_tac a) -apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def +apply (auto simp:inum_of_file.simps file_of_proc_fd.simps os_grant.simps current_files_def is_file_def split:if_splits option.splits) apply (simp add:pfdof_simp3)+ apply (simp add:proc_fd_of_file_def)+ @@ -496,7 +498,7 @@ lemma current_files_linkhard: "valid (LinkHard p f\<^isub>1 f\<^isub>2 # \) \ current_files (LinkHard p f\<^isub>1 f\<^isub>2 # \) = insert f\<^isub>2 (current_files \)" apply (frule vt_grant_os, frule vd_cons) -by (auto simp:current_files_def inum_of_file.simps os_grant.simps split:option.splits) +by (auto simp:current_files_def inum_of_file.simps os_grant.simps is_file_def split:option.splits) (* lemma rename_renaming_decom: diff -r 8779d321cc2e -r f27882976251 Delete_prop.thy --- a/Delete_prop.thy Wed May 15 11:21:39 2013 +0800 +++ b/Delete_prop.thy Wed May 15 15:42:46 2013 +0800 @@ -25,7 +25,7 @@ lemma not_deleted_init_file: "\\ deleted (O_file f) s; valid s; is_init_file f\ \ is_file s f" -apply (induct s, simp add:is_init_file_prop1) +apply (induct s, simp add:is_file_nil) apply (frule vd_cons, frule vt_grant_os) apply (case_tac a) prefer 6 apply (case_tac option) apply (auto simp:is_file_simps split:option.splits) @@ -33,7 +33,7 @@ lemma not_deleted_init_dir: "\\ deleted (O_dir f) s; valid s; is_init_dir f\ \ is_dir s f" -apply (induct s, simp add:is_init_dir_prop1) +apply (induct s, simp add:is_dir_nil) apply (frule vd_cons, frule vt_grant_os) apply (case_tac a) prefer 6 apply (case_tac option) apply (auto simp:is_dir_simps split:option.splits) @@ -71,7 +71,7 @@ lemma not_deleted_init_tcp_aux: "\\ deleted (O_tcp_sock (p,fd)) s; valid s; is_init_tcp_sock (p,fd)\ \ is_tcp_sock s (p,fd) \ \ deleted (O_proc p) s" -apply (induct s arbitrary:p, simp add:is_init_tcp_sock_prop1) +apply (induct s arbitrary:p, simp add:is_tcp_sock_nil) apply (frule vd_cons, frule vt_grant_os) apply (case_tac a) prefer 6 apply (case_tac option) by (auto simp:is_tcp_sock_simps split:option.splits t_socket_type.splits @@ -90,7 +90,7 @@ lemma not_deleted_init_udp_aux: "\\ deleted (O_udp_sock (p,fd)) s; valid s; is_init_udp_sock (p,fd)\ \ is_udp_sock s (p,fd) \ \ deleted (O_proc p) s" -apply (induct s arbitrary:p, simp add:is_init_udp_sock_prop1) +apply (induct s arbitrary:p, simp add:is_udp_sock_nil) apply (frule vd_cons, frule vt_grant_os) apply (case_tac a) prefer 6 apply (case_tac option) by (auto simp:is_udp_sock_simps split:option.splits t_socket_type.splits diff -r 8779d321cc2e -r f27882976251 Flask.thy --- a/Flask.thy Wed May 15 11:21:39 2013 +0800 +++ b/Flask.thy Wed May 15 15:42:46 2013 +0800 @@ -1017,6 +1017,23 @@ (Some u, Some r, Some t) \ Some (u, r, t) | _ \ None)" +fun init_role_of_obj :: "t_object \ role_t option" +where + "init_role_of_obj (O_proc p) = init_role_of_proc p" +| "init_role_of_obj _ = Some R_object" + +definition init_sectxt_of_obj :: "t_object \ security_context_t option" +where + "init_sectxt_of_obj obj \ + (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of + (Some u, Some r, Some t) \ Some (u,r,t) + | _ \ None)" + +definition sec_of_root :: "security_context_t" +where + "sec_of_root \ (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of + (Some u, Some t) \ (u, R_object, t))" + (******* flask granting ******** * involves three kinds of rules: * 1. allow rule of types, allowed_rule_list_t, main diff -r 8779d321cc2e -r f27882976251 Init_prop.thy --- a/Init_prop.thy Wed May 15 11:21:39 2013 +0800 +++ b/Init_prop.thy Wed May 15 15:42:46 2013 +0800 @@ -68,19 +68,19 @@ lemmas init_sockets_props = init_sockets_prop1 init_sockets_prop2 init_sockets_prop3 init_sockets_prop4 init_sockets_prop5 -lemma is_init_file_prop1: "is_init_file f = (f \ init_files \ is_file [] f)" -by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits) +lemma is_init_file_prop1: "is_init_file f \ f \ init_files" +by (auto simp add:is_init_file_def init_inum_of_file_props split:option.splits) -lemma is_init_file_prop2: "is_init_file f = (init_alive (O_file f))" -by (auto simp add:is_init_file_def is_file_def init_inum_of_file_props split:option.splits) +lemma is_init_file_prop2: "is_init_file f \ \ is_init_dir f" +by (auto simp add:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits) lemmas is_init_file_props = is_init_file_prop1 is_init_file_prop2 -lemma is_init_dir_prop1: "is_init_dir f = (f \ init_files \ is_dir [] f)" +lemma is_init_dir_prop1: "is_init_dir f \ f \ init_files" by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) -lemma is_init_dir_prop2: "is_init_dir f = (init_alive (O_dir f))" -by (auto simp add:is_init_dir_def is_dir_def init_inum_of_file_props split:option.splits) +lemma is_init_dir_prop2: "is_init_dir f \ \ is_init_file f" +by (auto simp add:is_init_dir_def is_init_file_def split:option.splits t_inode_tag.splits) lemmas is_init_dir_props = is_init_dir_prop1 is_init_dir_prop2 @@ -94,14 +94,14 @@ "is_udp_sock [] k = is_init_udp_sock k" by (auto simp:is_udp_sock_def is_init_udp_sock_def split:option.splits) -lemma is_init_udp_sock_prop1: "is_init_udp_sock s = (s \ init_sockets \ is_udp_sock [] s)" +lemma is_init_udp_sock_prop1: "is_init_udp_sock s \ s \ init_sockets" apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props dest:init_socket_has_inode split:option.splits) done -lemma is_init_udp_sock_prop2: "is_init_udp_sock s = (init_alive (O_udp_sock s))" -apply (auto simp add:is_init_udp_sock_def is_udp_sock_def init_inum_of_socket_props - dest:init_socket_has_inode split:option.splits) +lemma is_init_udp_sock_prop2: "is_init_udp_sock s \ \ is_init_tcp_sock s" +apply (auto simp add:is_init_udp_sock_def is_init_tcp_sock_def + dest:init_socket_has_inode split:option.splits t_inode_tag.splits) done lemma is_init_udp_sock_prop3: @@ -121,14 +121,14 @@ "is_tcp_sock [] k = is_init_tcp_sock k" by (auto simp:is_tcp_sock_def is_init_tcp_sock_def split:option.splits) -lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s = (s \ init_sockets \ is_tcp_sock [] s)" +lemma is_init_tcp_sock_prop1: "is_init_tcp_sock s \ s \ init_sockets" apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props dest:init_socket_has_inode split:option.splits) done -lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s = (init_alive (O_tcp_sock s))" -apply (auto simp add:is_init_tcp_sock_def is_tcp_sock_def init_inum_of_socket_props - dest:init_socket_has_inode split:option.splits) +lemma is_init_tcp_sock_prop2: "is_init_tcp_sock s \ \ is_init_udp_sock s" +apply (auto simp add:is_init_tcp_sock_def is_init_udp_sock_def + dest:init_socket_has_inode split:option.splits t_inode_tag.splits) done lemma is_init_tcp_sock_prop3: @@ -301,7 +301,8 @@ lemma init_alive_prop: "init_alive obj = alive [] obj" apply (case_tac obj, simp_all add:is_init_file_props is_init_dir_props is_init_tcp_sock_props - is_init_udp_sock_props init_files_props init_sockets_props) + is_init_udp_sock_props init_files_props init_sockets_props is_file_nil is_dir_nil + is_tcp_sock_nil is_udp_sock_nil) done lemma init_alive_proc: "p \ init_procs \ init_alive (O_proc p)" by simp @@ -369,7 +370,7 @@ lemmas init_role_of_proc_props = init_procrole_prop1 init_procrole_prop2 init_procrole_prop3 lemma init_file_user_prop1: "is_init_file f \ \ t. init_user_of_obj (O_file f) = Some t" -apply (simp only: is_init_file_prop2) +apply (drule init_alive_file) by (drule init_obj_has_user, auto) lemma init_file_user_prop2: "is_init_file f \ init_user_of_obj (O_file f) \ None" @@ -389,7 +390,7 @@ lemmas init_file_users_props = init_file_user_prop1 init_file_user_prop2 init_file_user_prop3 init_file_user_prop4 init_file_user_prop5 lemma init_dir_user_prop1: "is_init_dir f \ \ t. init_user_of_obj (O_dir f) = Some t" -apply (simp only: is_init_dir_prop2) +apply (drule init_alive_dir) by (drule init_obj_has_user, auto) lemma init_dir_user_prop2: "is_init_dir f \ init_user_of_obj (O_dir f) \ None" @@ -765,8 +766,7 @@ dest:init_same_inode_prop1 split:option.splits) apply (rule_tac x = list in exI, simp add:init_same_inode_files_def) -apply (simp add:init_files_props) -apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict) +apply (drule is_init_file_prop1, simp add:init_files_props) done lemma s2ss_nil_prop: diff -r 8779d321cc2e -r f27882976251 Sectxt_prop.thy --- a/Sectxt_prop.thy Wed May 15 11:21:39 2013 +0800 +++ b/Sectxt_prop.thy Wed May 15 15:42:46 2013 +0800 @@ -373,6 +373,58 @@ is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec'' current_msgq_has_sec'' current_msg_has_sec'' +(************ root sec remains ************) + +lemma root_type_remains: + "valid s \ type_of_obj s (O_dir []) = init_type_of_obj (O_dir [])" +apply (induct s) +apply (simp) +apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 +by (case_tac option, auto) + +lemma root_user_remains: + "valid s \ user_of_obj s (O_dir []) = init_user_of_obj (O_dir [])" +apply (induct s) +apply (simp) +apply (frule vd_cons, frule vt_grant_os, case_tac a) prefer 6 +by (case_tac option, auto) + +lemma root_has_type': + "\type_of_obj s (O_dir []) = None; valid s\ \ False" +apply (drule alive_obj_has_type', simp) +by (drule root_is_dir, simp) + +lemma root_has_user': + "\user_of_obj s (O_dir []) = None; valid s\ \ False" +apply (drule alive_obj_has_user', simp) +by (drule root_is_dir, simp) + +lemma root_has_init_type': + "init_type_of_obj (O_dir []) = None \ False" +using init_obj_has_type[where obj = "O_dir []"] root_is_init_dir +by auto + +lemma root_has_init_user': + "init_user_of_obj (O_dir []) = None \ False" +using init_obj_has_user[where obj = "O_dir []"] root_is_init_dir +by auto + +lemma root_sec_remains: + "valid s \ sectxt_of_obj s (O_dir []) = init_sectxt_of_obj (O_dir [])" +by (auto simp:root_user_remains root_type_remains sectxt_of_obj_def init_sectxt_of_obj_def + split:option.splits) + +lemma root_sec_set: + "\ u t. sec_of_root = (u, R_object, t)" +by (auto simp:sec_of_root_def split:option.splits + dest!: root_has_init_type' root_has_init_user') + +lemma sec_of_root_set: + "init_sectxt_of_obj (O_dir []) = Some sec_of_root" +using root_has_init_type' root_has_init_user' +apply (auto simp:init_sectxt_of_obj_def sec_of_root_def split:option.splits) +done + (*************** sectxt_of_obj simpset ****************) lemma sec_execve: diff -r 8779d321cc2e -r f27882976251 Static.thy --- a/Static.thy Wed May 15 11:21:39 2013 +0800 +++ b/Static.thy Wed May 15 15:42:46 2013 +0800 @@ -6,18 +6,6 @@ begin -fun init_role_of_obj :: "t_object \ role_t option" -where - "init_role_of_obj (O_proc p) = init_role_of_proc p" -| "init_role_of_obj _ = Some R_object" - -definition init_sectxt_of_obj :: "t_object \ security_context_t option" -where - "init_sectxt_of_obj obj \ - (case (init_user_of_obj obj, init_role_of_obj obj, init_type_of_obj obj) of - (Some u, Some r, Some t) \ Some (u,r,t) - | _ \ None)" - (* definition init_sectxt_of_file:: "t_file \ security_context_t option" where @@ -27,11 +15,6 @@ else None" *) -definition sec_of_root :: "security_context_t" -where - "sec_of_root \ (case (init_user_of_obj (O_dir []), init_type_of_obj (O_dir [])) of - (Some u, Some t) \ (u, R_object, t))" - definition sroot :: "t_sfile" where "sroot \ (Init [], sec_of_root, None, {})"