Mercurial Mercurial > hg > selinux / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Current_prop.thy
changeset 26 b6333712cb02
parent 25 259a50be4381
child 27 fc749f19b894
equal deleted inserted replaced
25:259a50be4381 26:b6333712cb02 
    18 apply (simp, drule init_procs_has_shm, simp)
 
    18 apply (simp, drule init_procs_has_shm, simp)
 
    19 apply (frule vd_cons, frule vt_grant_os)
 
    19 apply (frule vd_cons, frule vt_grant_os)
 
    20 apply (case_tac a, auto split:if_splits option.splits)
 
    20 apply (case_tac a, auto split:if_splits option.splits)
 
    21 done
 
    21 done
 
    22 
    22 
       
    23 lemma procs_of_shm_prop2':
 
       
    24   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<forall> flag h. (p, flag) \<notin> procs_of_shm s h"
 
       
    25 by (auto dest:procs_of_shm_prop2)
 
       
    26 
    23 lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
 
    27 lemma procs_of_shm_prop3: "\<lbrakk>(p, flag) \<in> procs_of_shm s h; (p, flag') \<in> procs_of_shm s h; valid s\<rbrakk>
 
    24   \<Longrightarrow> flag = flag'"
 
    28   \<Longrightarrow> flag = flag'"
 
    25 apply (induct s arbitrary:p flag flag')
 
    29 apply (induct s arbitrary:p flag flag')
 
    26 apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
 
    30 apply (simp, drule_tac flag = flag in init_procs_has_shm, drule_tac flag = flag' in init_procs_has_shm, simp)
 
    27 apply (frule vd_cons, frule vt_grant_os)
 
    31 apply (frule vd_cons, frule vt_grant_os)
 
    47   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
 
    51   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
 
    48 using not_deleted_init_proc by auto
 
    52 using not_deleted_init_proc by auto
 
    49 
    53 
    50 lemma info_shm_flow_in_procs:
 
    54 lemma info_shm_flow_in_procs:
 
    51   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
 
    55   "\<lbrakk>info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s \<and> p' \<in> current_procs s"
 
    52 apply (induct rule:info_flow_shm.induct )
 
    56 by (auto intro:procs_of_shm_prop2 simp:info_flow_shm_def one_flow_shm_def)
 
    53 by (auto intro:procs_of_shm_prop2)
 
       
    54 
    57 
    55 (*********** simpset for info_flow_shm **************)
 
    58 (*********** simpset for info_flow_shm **************)
 
    56 
    59 
       
    60 lemma info_flow_shm_attach:
 
       
    61   "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. 
       
    62      (pa = p \<and> flag = SHM_RDWR \<and> (\<exists> flagb. (pb, flagb) \<in> procs_of_shm s h)) \<or>
 
       
    63      (pb = p \<and> (pa, SHM_RDWR) \<in> procs_of_shm s h) \<or>
 
       
    64      (info_flow_shm s pa pb)                       )"
 
       
    65 apply (rule ext, rule ext, frule vt_grant_os)
 
       
    66 by (auto simp add:info_flow_shm_def one_flow_shm_def)
 
       
    67 
       
    68 lemma info_flow_shm_detach:
 
       
    69   "valid (Detach p h # s) \<Longrightarrow> info_flow_shm (Detach p h # s) = (\<lambda> pa pb. 
       
    70      self_shm s pa pb \<or> ((p = pa \<or> p = pb) \<and> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)) \<or>
 
       
    71      (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb) )"
 
       
    72 apply (rule ext, rule ext, frule vt_grant_os)
 
       
    73 by (auto simp:info_flow_shm_def one_flow_shm_def)
 
       
    74 
       
    75 lemma info_flow_shm_deleteshm:
 
       
    76   "valid (DeleteShM p h # s) \<Longrightarrow> info_flow_shm (DeleteShM p h # s) = (\<lambda> pa pb. 
       
    77      self_shm s pa pb \<or> (\<exists> h'. h' \<noteq> h \<and> one_flow_shm s h' pa pb)     )"
 
       
    78 apply (rule ext, rule ext, frule vt_grant_os)
 
       
    79 by (auto simp:info_flow_shm_def one_flow_shm_def)
 
       
    80 
       
    81 lemma info_flow_shm_clone:
 
       
    82   "valid (Clone p p' fds shms # s) \<Longrightarrow> info_flow_shm (Clone p p' fds shms # s) = (\<lambda> pa pb. 
       
    83      (pa = p' \<and> pb = p') \<or> (pa = p' \<and> pb \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h p pb)) \<or> 
       
    84      (pb = p' \<and> pa \<noteq> p' \<and> (\<exists> h \<in> shms. one_flow_shm s h pa p)) \<or> 
       
    85      (pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb))"
 
       
    86 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons, clarsimp)
 
       
    87 apply (frule_tac p = p' in procs_of_shm_prop2', simp)
 
       
    88 apply (auto simp:info_flow_shm_def one_flow_shm_def)
 
       
    89 done
 
       
    90 
       
    91 lemma info_flow_shm_execve:
 
       
    92   "valid (Execve p f fds # s) \<Longrightarrow> info_flow_shm (Execve p f fds # s) = (\<lambda> pa pb. 
       
    93      (pa = p \<and> pb = p) \<or> (pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb)    )"
 
       
    94 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
 
       
    95 by (auto simp:info_flow_shm_def one_flow_shm_def)
 
       
    96 
       
    97 lemma info_flow_shm_kill:
 
       
    98   "valid (Kill p p' # s) \<Longrightarrow> info_flow_shm (Kill p p' # s) = (\<lambda> pa pb. 
       
    99      pa \<noteq> p' \<and> pb \<noteq> p' \<and> info_flow_shm s pa pb                 )"
 
       
   100 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
 
       
   101 by (auto simp:info_flow_shm_def one_flow_shm_def)
 
       
   102 
       
   103 lemma info_flow_shm_exit:
 
       
   104   "valid (Exit p # s) \<Longrightarrow> info_flow_shm (Exit p # s) = (\<lambda> pa pb. 
       
   105      pa \<noteq> p \<and> pb \<noteq> p \<and> info_flow_shm s pa pb                          )"
 
       
   106 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
 
       
   107 by (auto simp:info_flow_shm_def one_flow_shm_def)
 
       
   108 
       
   109 lemma info_flow_shm_other:
 
       
   110   "\<lbrakk>valid (e # s); 
       
   111     \<forall> p h flag. e \<noteq> Attach p h flag;
 
       
   112     \<forall> p h. e \<noteq> Detach p h;
 
       
   113     \<forall> p h. e \<noteq> DeleteShM p h;
 
       
   114     \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
 
       
   115     \<forall> p f fds. e \<noteq> Execve p f fds;
 
       
   116     \<forall> p p'. e \<noteq> Kill p p';
 
       
   117     \<forall> p. e \<noteq> Exit p
 
       
   118    \<rbrakk> \<Longrightarrow> info_flow_shm (e # s) = info_flow_shm s"
 
       
   119 apply (rule ext, rule ext, frule vt_grant_os, frule vd_cons)
 
       
   120 apply (case_tac e, auto simp:info_flow_shm_def one_flow_shm_def dest:procs_of_shm_prop2)
 
       
   121 apply (erule_tac x = h in allE, simp)
 
       
   122 apply (drule procs_of_shm_prop1, auto)
 
       
   123 done
 
       
   124 
       
   125 
       
   126 (*
 
    57 lemma info_flow_shm_prop1: 
   127 lemma info_flow_shm_prop1: 
    58   "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 
   128   "\<lbrakk>info_flow_shm s p p'; p \<noteq> p'; valid s\<rbrakk> 
    59    \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
 
   129    \<Longrightarrow> \<exists> h h' flag. (p, SHM_RDWR) \<in> procs_of_shm s h \<and> (p', flag) \<in> procs_of_shm s h'"
 
    60 by (induct rule: info_flow_shm.induct, auto)
 
   130 by (induct rule: info_flow_shm.induct, auto)
 
    61 
   131 
    81 
   151 
    82 definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
 
   152 definition flowed_procs:: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process set"
 
    83 where
 
   153 where
 
    84   "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"
 
   154   "flowed_procs s h \<equiv> {p'. \<exists> p \<in> attached_procs s h. flows_shm s p p'}"
 
    85 
   155 
       
   156 inductive flowed_shm:: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm set"
 
       
   157 
    86 fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
 
   158 fun Info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process set"
 
    87 where
 
   159 where
 
    88   "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
 
   160   "Info_flow_shm [] = (\<lambda> p. {p'. flows_shm [] p p'})"
 
    89 | "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. if (p' = p) then {p''. \<exists> }"
 
   161 | "Info_flow_shm (Attach p h flag # s) = (\<lambda> p'. 
       
   162      if (p' = p) then flowed_procs s h 
       
   163      else if ()
 
       
   164     "
 
    90 
   165 
    91 
   166 
    92 lemma info_flow_shm_attach:
 
   167 lemma info_flow_shm_attach:
 
    93   "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> 
   168   "valid (Attach p h flag # s) \<Longrightarrow> info_flow_shm (Attach p h flag # s) = (\<lambda> pa pb. (info_flow_shm s pa pb) \<or> 
    94      (if (pa = p) 
   169      (if (pa = p) 
   105 apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)
 
   180 apply (auto split:if_splits intro:info_flow_shm.intros elim:info_flow_shm_cases)
 
   106 apply (erule info_flow_shm_cases, simp, simp split:if_splits)
 
   181 apply (erule info_flow_shm_cases, simp, simp split:if_splits)
 
   107 apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
 
   182 apply (rule_tac p = pa and p' = p' in info_flow_shm.intros(2), simp+)
 
   108 apply (rule notI, erule info_flow_shm.cases, simp+)
 
   183 apply (rule notI, erule info_flow_shm.cases, simp+)
 
   109 pr 5
 
   184 pr 5
 
   110 
   185 *)
 
   111 lemmas info_flow_shm_simps = info_flow_shm_other
 
   186 lemmas info_flow_shm_simps = info_flow_shm_other info_flow_shm_attach info_flow_shm_detach info_flow_shm_deleteshm
 
       
   187   info_flow_shm_clone info_flow_shm_execve info_flow_shm_kill info_flow_shm_exit
 
   112 
   188 
   113 lemma has_same_inode_in_current:
 
   189 lemma has_same_inode_in_current:
 
   114   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
 
   190   "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
 
   115 by (auto simp add:has_same_inode_def current_files_def)
 
   191 by (auto simp add:has_same_inode_def current_files_def)
 
   116 
   192
selinux