# HG changeset patch # User chunhan # Date 1369207370 -28800 # Node ID 47a4b2ae0556de499e2ce9db5f9e3a5c7e178ea5 # Parent 3e7617baa6a372bbed321cf54b572c6cf0b97993 Modify definitions of cpfd2sfds diff -r 3e7617baa6a3 -r 47a4b2ae0556 Co2sobj_prop.thy --- a/Co2sobj_prop.thy Tue May 21 10:19:51 2013 +0800 +++ b/Co2sobj_prop.thy Wed May 22 15:22:50 2013 +0800 @@ -603,23 +603,10 @@ "\cfd2sfd s p fd = None; valid s\ \ file_of_proc_fd s p fd = None" by (case_tac "file_of_proc_fd s p fd", auto dest:current_filefd_has_sfd) -definition cpfd2sfds' :: "t_state \ t_process \ t_sfd set" -where - "cpfd2sfds' s p \ {sfd. \ fd f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}" - -definition cph2spshs' :: "t_state \ t_process \ t_sproc_sshm set" -where - "cph2spshs' s p \ {(sh, flag). \ h. (p, flag) \ procs_of_shm s h \ ch2sshm s h = Some sh}" - -lemma "x \ cph2spshs' s p \ False" -apply (simp add:cph2spshs'_def) -apply (case_tac x, simp) - - -lemma cpfd2sfds_open_some1: - "valid (Open p f flags fd (Some inum) # s) \ - cpfd2sfds (Open p f flags fd (Some inum) # s) p = ( - case (cfd2sfd (Open p f flags fd (Some inum) # s) p fd) of +lemma cpfd2sfds_open1: + "valid (Open p f flags fd opt # s) \ + cpfd2sfds (Open p f flags fd opt # s) p = ( + case (cfd2sfd (Open p f flags fd opt # s) p fd) of Some sfd \ (cpfd2sfds s p) \ {sfd} | _ \ cpfd2sfds s p)" apply (frule vd_cons, frule vt_grant_os) @@ -627,32 +614,43 @@ apply (rule conjI, rule impI, drule current_filefd_has_sfd', simp, simp) apply (rule allI, rule impI) apply (rule set_eqI, rule iffI) +apply (case_tac "x = a", simp) unfolding cpfd2sfds_def -thm CollectE -apply (erule CollectE) apply (erule CollectE, (erule conjE|erule exE)+) -apply (simp only:file_of_proc_fd.simps split:if_splits) -apply (simp add:cpfd2sfds_def) +apply (simp split:if_splits) +apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2) +apply (case_tac "x = a", simp) +apply (rule_tac x = fd in exI, simp+) +apply (erule conjE|erule exE)+ +apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2) +apply (rule impI, drule proc_fd_in_fds, simp) +apply (simp split:option.splits) +done -apply (auto simp:cpfd2sfds_def split:option.splits if_splits dest:file_of_proc_fd_in_curf proc_fd_in_fds proc_fd_in_procs) - -lemma cpfd2sfds_open1: +lemma cpfd2sfds_open1': "valid (Open p f flags fd opt # s) \ cpfd2sfds (Open p f flags fd opt # s) p = ( case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of (Some sec, Some sf) \ (cpfd2sfds s p) \ {(sec, flags, sf)} | _ \ cpfd2sfds s p)" -apply (frule vd_cons, frule vt_grant_os) -apply (case_tac opt) -apply (auto simp:sectxt_of_obj_simps current_files_simps dest!:current_has_sec' current_file_has_sfile' - split:option.splits) -apply (auto simp:cpfd2sfds_def split:if_splits) -apply (auto simp:cfd2sfd_open cf2sfile_open sectxt_of_obj_simps current_files_simps split:option.splits if_splits dest!:current_has_sec' current_file_has_sfile') apply (frule cfd2sfd_open1) -apply ( -apply (simp add:cpfd2sfds_def) -apply (auto simp add:cpfd2sfds_def split:option.splits) -apply (auto dest!:current_has_sec') +apply (auto dest:cpfd2sfds_open1 split:option.splits) +done + +lemma cpfd2sfds_open2: + "\valid (Open p f flags fd opt # s); p' \ p\ \ cpfd2sfds (Open p f flags fd opt # s) p' = cpfd2sfds s p'" +apply (frule vt_grant_os, frule vd_cons) +unfolding cpfd2sfds_def +apply (rule set_eqI, rule iffI) +apply (erule CollectE, (erule exE|erule conjE)+) +apply (simp only:file_of_proc_fd.simps cfd2sfd_open2 split:if_splits) +apply (rule CollectI) +apply (rule_tac x = fda in exI, rule_tac x = fa in exI, simp) +apply (erule CollectE, (erule exE|erule conjE)+) +apply (simp only:file_of_proc_fd.simps split:if_splits) +apply (rule CollectI) +apply (rule_tac x = fda in exI, simp add:cfd2sfd_open2) +done lemma cpfd2sfds_open: "valid (Open p f flags fd opt # s) @@ -660,12 +658,21 @@ case (sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), cf2sfile (Open p f flags fd opt # s) f) of (Some sec, Some sf) \ (cpfd2sfds s p) \ {(sec, flags, sf)} | _ \ cpfd2sfds s p))" -apply (frule cfd2sfd_open1) apply (rule ext) -apply (simp add:cpfd2sfds_def) -apply (auto simp add:cpfd2sfds_def split:option.splits) +apply (case_tac "x \ p") +apply (simp add:cpfd2sfds_open2) +apply (simp add:cpfd2sfds_open1') +done -lemma cpfd2sfds_simps = +lemma cpfd2sfds_execve: + "valid (Execve p fds # s) + \ cpfd2sfds (Execve p fds # s) = (cpfd2sfds s) (p := " + +lemma cpfd2sfds_other: + "\valid (e # s); + \ + +lemma cpfd2sfds_simps = cpfd2sfds_open cpfd2sfds_other (******** cp2sproc simpset *********) diff -r 3e7617baa6a3 -r 47a4b2ae0556 Flask.thy --- a/Flask.thy Tue May 21 10:19:51 2013 +0800 +++ b/Flask.thy Wed May 22 15:22:50 2013 +0800 @@ -759,6 +759,14 @@ | "deleted obj (_ # s) = deleted obj s" +definition proc_file_fds :: "t_state \ t_process \ t_fd set" +where + "proc_file_fds s p \ {fd. \ f. file_of_proc_fd s p fd = Some f}" + + +definition init_proc_file_fds:: "t_process \ t_fd set" + "init_proc_file_fds p \ {fd. \ f. init_file_of_proc_fd p fd = Some f}" + end diff -r 3e7617baa6a3 -r 47a4b2ae0556 Static.thy --- a/Static.thy Tue May 21 10:19:51 2013 +0800 +++ b/Static.thy Wed May 22 15:22:50 2013 +0800 @@ -47,7 +47,7 @@ definition init_cfds2sfds :: "t_process \ (security_context_t \ t_open_flags \ t_sfile) set" where - "init_cfds2sfds p \ { sfd. \ fd f. init_file_of_proc_fd p fd = Some f \ init_cfd2sfd p fd = Some sfd}" + "init_cfds2sfds p \ { sfd. \ fd \ init_proc_file_fds p. init_cfd2sfd p fd = Some sfd}" definition init_ch2sshm :: "t_shm \ t_sshm option" where @@ -712,7 +712,7 @@ definition cpfd2sfds :: "t_state \ t_process \ t_sfd set" where - "cpfd2sfds s p \ {sfd. \ fd f. file_of_proc_fd s p fd = Some f \ cfd2sfd s p fd = Some sfd}" + "cpfd2sfds s p \ {sfd. \ fd \ proc_file_fds s p. cfd2sfd s p fd = Some sfd}" definition ch2sshm :: "t_state \ t_shm \ t_sshm option" where