1 theory Tainted_prop 

     2 imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop

     3 begin

     4 

     5 ML {*quick_and_dirty := true*}

     6 

     7 context tainting begin

     8 

     9 lemma valid_tainted_obj:

    10   "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> p fd. obj \<noteq> O_fd p fd) \<and> (\<forall> s. obj \<noteq> O_tcp_sock s) \<and> (\<forall> s. obj \<noteq> O_udp_sock s)" (*(\<forall> h. obj \<noteq> O_shm h) \<and>*)

    11 apply (induct s, simp)

    12 apply (drule seeds_appropriate, case_tac obj, simp+)

    13 apply (frule vd_cons, frule vt_grant_os, case_tac a)

    14 apply (auto split:if_splits option.splits)

    15 done

    16 

    17 lemma dir_not_tainted: "\<lbrakk>O_dir f \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> False"

    18 by (auto dest!:valid_tainted_obj)

    19 

    20 lemma msgq_not_tainted: "\<lbrakk>O_msgq q \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> False"

    21 by (auto dest:valid_tainted_obj)

    22 

    23 lemma tainted_in_current:

    24   "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"

    25 apply (induct s, simp)

    26 apply (drule seeds_appropriate, case_tac obj, simp_all add:is_file_nil)

    27 apply (frule vd_cons, frule valid_tainted_obj, simp, frule vt_grant_os, case_tac a)

    28 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits

    29            intro:same_inode_files_prop1 (*procs_of_shm_prop2 

    30             dest:info_shm_flow_in_procs *))

    31 apply (auto simp:same_inode_files_def is_file_def split:if_splits)

    32 done 

    33 

    34 lemma tainted_proc_in_current:

    35   "\<lbrakk>O_proc p \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

    36 by (drule tainted_in_current, simp+)

    37 

    38 (*

    39 lemma info_flow_shm_tainted:

    40   "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s"

    41 proof (induct s arbitrary:p p')

    42   case Nil

    43   thus ?case by (simp add:flow_shm_in_seeds)

    44 next

    45   case (Cons e s)

    46   hence p1: "O_proc p \<in> tainted (e # s)" and p2: "info_flow_shm (e # s) p p'" and p3: "valid (e # s)"  

    47     and p4: "\<And> p p'. \<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s" 

    48     and p5: "valid s" and p6: "os_grant s e"

    49     by (auto dest:vd_cons intro:vd_cons vt_grant_os)

    50   have p4': 

    51     "\<And> p p' h flag. \<lbrakk>O_proc p \<in> tainted s; (p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h\<rbrakk> 

    52                 \<Longrightarrow> O_proc p' \<in> tainted s"

    53     by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2 p5)    

    54   from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" 

    55     by (auto dest:info_shm_flow_in_procs) 

    56   show ?case

    57   proof (cases "self_shm s p p'")

    58     case True with p1 show ?thesis by simp

    59   next

    60     case False

    61     with p1 p2 p5 p6 p7 p8 p3 show ?thesis

    62     apply (case_tac e)(*

    63     prefer 7

    64     apply (simp add:info_flow_shm_simps split:if_splits option.splits)

    65     apply (rule allI|rule impI|rule conjI)+

    66     apply simp

    67     apply (case_tac "O_proc p \<in> tainted s", drule_tac p'=p' in p4, simp+)

    68     apply simp

    69 

    70 

    71 

    72 

    73     apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:tainted_in_current 

    74   intro:p4 p4' split:if_splits option.splits)

    75     apply (auto simp:info_flow_shm_def one_flow_shm_def)

    76 

    77 

    78 

    79     apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits)

    80 

    81 

    82 

    83     prefer 7

    84     apply (simp split:if_splits option.splits)

    85     apply (rule allI|rule impI|rule conjI)+

    86 

    87 

    88     apply (auto dest:p4'   procs_of_shm_prop2 tainted_in_current split:if_splits option.splits)[1]

    89 

    90     apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+)

    91     apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp)

    92     apply ((erule exE|erule conjE)+)

    93     

    94 

    95     apply (auto simp:info_flow_shm_def dest:p4'

    96            procs_of_shm_prop2 tainted_in_current split:if_splits option.splits)[1]

    97     apply (drule_tac p = p and p' = p' in p4')

    98     apply (erule_tac x = ha in allE, simp)

    99     apply (drule_tac p = "nat1" and p' = p' in p4')

   100     apply (auto dest:p4'[where p = nat1 and p' = p'])

   101     

   102 apply (induct s) 

   103 apply simp defer

   104 apply (frule vd_cons, frule vt_grant_os, case_tac a)

   105 apply (auto simp:info_flow_shm_def elim!:disjE)

   106 sorry *)

   107   sorry

   108 qed

   109 qed

   110 *)

   111 

   112 lemma has_same_inode_comm:

   113   "has_same_inode s f f' = has_same_inode s f' f"

   114 by (auto simp add:has_same_inode_def same_inode_files_def is_file_def)

   115 

   116 (*

   117 lemma info_flow_shm_tainted:

   118   "\<lbrakk>O_proc p \<in> tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> tainted s"

   119 by (simp only:tainted_eq_tainted info_flow_shm_tainted)

   120 *)

   121 

   122 lemma same_inode_files_tainted:

   123   "\<lbrakk>O_file f \<in> tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"

   124 apply (induct s arbitrary:f f', simp add:same_inode_in_seeds has_same_inode_def)

   125 apply (frule vt_grant_os, frule vd_cons, case_tac a)

   126 prefer 6

   127 apply (simp split:if_splits option.splits add:same_inode_files_open current_files_simps)

   128 prefer 8

   129 apply (frule tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)

   130 apply (auto simp add:same_inode_files_closefd split:option.splits if_splits)[1]

   131 prefer 8

   132 apply (frule tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)

   133 apply (auto simp add:same_inode_files_unlink split:option.splits if_splits)[1]

   134 prefer 10

   135 apply (auto split:if_splits option.splits simp:same_inode_files_linkhard current_files_simps)[1]

   136 apply (drule tainted_in_current, simp, simp add:alive.simps is_file_in_current)

   137 apply (drule same_inode_files_prop5, simp)

   138 apply (drule same_inode_files_prop5, drule_tac f' = list1 and f'' = f' in same_inode_files_prop4, simp, simp)

   139 

   140 apply (auto simp:same_inode_files_other split:if_splits)

   141 apply (drule_tac f'' = f' and f' = f and f = fa in same_inode_files_prop4, simp+)

   142 apply (drule_tac f'' = f' and f' = f and f = list in same_inode_files_prop4, simp+)

   143 done

   144 

   145 lemma has_same_inode_tainted:

   146   "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s"

   147 by (simp add:has_same_inode_def same_inode_files_tainted)

   148 

   149 lemma same_inodes_tainted:

   150   "\<lbrakk>f \<in> same_inode_files s f'; valid s\<rbrakk> \<Longrightarrow> (O_file f \<in> tainted s) = (O_file f' \<in> tainted s)"

   151 apply (frule same_inode_files_prop8, frule same_inode_files_prop7)

   152 apply (auto intro:has_same_inode_tainted)

   153 done

   154 

   155 lemma t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> 

   156              \<Longrightarrow> obj \<in> tainted (e # s)"

   157 apply (frule vd_cons, frule vt_grant_os, case_tac e)

   158 apply (auto simp:alive_simps split:option.splits if_splits)

   159 done

   160 

   161 lemma not_exited_cons:

   162   "\<not> exited obj (e # s) \<Longrightarrow> \<not> exited obj s"

   163 apply (case_tac e, case_tac [!] obj)

   164 by (auto)

   165 

   166 lemma t_remain_app:

   167   "\<lbrakk>obj \<in> tainted s; \<not> died obj (s' @ s); valid (s' @ s)\<rbrakk> 

   168   \<Longrightarrow> obj \<in> tainted (s' @ s)"

   169 apply (induct s', simp)

   170 apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)

   171 apply (simp_all add:not_died_cons_D vd_cons) 

   172 apply (frule tainted_in_current)

   173 apply (simp add:vd_cons)

   174 apply (drule valid_tainted_obj, simp add:vd_cons) 

   175 apply (case_tac a, auto simp:alive_simps split:t_object.splits option.splits)

   176 done

   177 

   178 lemma t_remain_app_deleted:

   179   "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); appropriate obj; \<not> exited obj (s' @ s); valid (s' @ s)\<rbrakk>

   180    \<Longrightarrow> obj \<in> tainted (s' @ s)"

   181 apply (rule t_remain_app, simp_all add:deleted_died)

   182 done

   183 

   184 end

   185 

   186 end