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> h. obj \<noteq> O_shm h) \<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)"

    11 apply (induct s, simp, drule seeds_in_init, case_tac obj, simp+)

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

    13 apply (auto split:if_splits option.splits)

    14 done

    15 

    16 lemma Tainted_in_current:

    17   "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"

    18 apply (induct s, simp)

    19 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)

    20 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a)

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

    22            intro:same_inode_files_prop1 procs_of_shm_prop2 

    23             dest:info_shm_flow_in_procs)

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

    25 done 

    26 

    27 lemma Tainted_proc_in_current:

    28   "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"

    29 by (drule Tainted_in_current, simp+)

    30 

    31 

    32 lemma info_flow_shm_Tainted:

    33   "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"

    34 proof (induct s arbitrary:p p')

    35   case Nil

    36   thus ?case by (simp add:flow_shm_in_seeds)

    37 next

    38   case (Cons e s)

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

    40     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" 

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

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

    43   have p4': 

    44     "\<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> 

    45                 \<Longrightarrow> O_proc p' \<in> Tainted s"

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

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

    48     by (auto dest:info_shm_flow_in_procs) 

    49   show ?case

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

    51     case True with p1 show ?thesis by simp

    52   next

    53     case False

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

    55     apply (case_tac e)(*

    56     prefer 7

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

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

    59     apply simp

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

    61     apply simp

    62 

    63 

    64 

    65 

    66     apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current 

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

    68     apply (auto simp:info_flow_shm_def one_flow_shm_def)

    69 

    70 

    71 

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

    73 

    74 

    75 

    76     prefer 7

    77     apply (simp split:if_splits option.splits)

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

    79 

    80 

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

    82 

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

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

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

    86     

    87 

    88     apply (auto simp:info_flow_shm_def dest:p4'

    89            procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]

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

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

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

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

    94     

    95 apply (induct s) 

    96 apply simp defer

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

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

    99 sorry *)

   100   sorry

   101 qed

   102 qed

   103 

   104 lemma has_same_inode_comm:

   105   "has_same_inode s f f' = has_same_inode s f' f"

   106 by (auto simp add:has_same_inode_def same_inode_files_def is_file_def)

   107 

   108 lemma tainted_imp_Tainted:

   109   "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"

   110 apply (induct rule:tainted.induct)  (*

   111 apply (simp_all add:vd_cons) 

   112 apply (rule impI)

   113 

   114 apply (rule disjI2, rule_tac x = flag' in exI, simp)

   115 apply ((rule impI)+, erule_tac x = p' in allE, simp)

   116 *)

   117 apply (auto intro:info_flow_shm_Tainted simp:has_same_inode_def dest:vd_cons)

   118 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps)

   119 done

   120 

   121 lemma Tainted_imp_tainted_aux_remain:

   122   "\<lbrakk>obj \<in> Tainted s; valid (e # s); alive (e # s) obj; \<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s\<rbrakk>

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

   124 by (rule t_remain, auto)

   125 

   126 lemma Tainted_imp_tainted:

   127   "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s"

   128 apply (induct s arbitrary:obj, simp add:t_init)

   129 apply (frule Tainted_in_current, simp+)

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

   131 apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros

   132   simp:has_same_inode_def)

   133 done

   134 

   135 lemma tainted_eq_Tainted:

   136   "valid s \<Longrightarrow> (obj \<in> tainted s) = (obj \<in> Tainted s)"

   137 by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted)

   138 

   139 lemma info_flow_shm_tainted:

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

   141 by (simp only:tainted_eq_Tainted info_flow_shm_Tainted)

   142 

   143 

   144 lemma same_inode_files_Tainted:

   145   "\<lbrakk>O_file f \<in> Tainted s; f' \<in> same_inode_files s f; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"

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

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

   148 prefer 6

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

   150 prefer 8

   151 apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)

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

   153 prefer 8

   154 apply (frule Tainted_in_current, simp, simp add:alive.simps, drule is_file_in_current)

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

   156 prefer 10

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

   158 apply (drule Tainted_in_current, simp, simp add:alive.simps is_file_in_current)

   159 apply (drule same_inode_files_prop5, simp)

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

   161 

   162 apply (auto simp:same_inode_files_other split:if_splits)

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

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

   165 done

   166 

   167 lemma has_same_inode_Tainted:

   168   "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"

   169 by (simp add:has_same_inode_def same_inode_files_Tainted)

   170 

   171 lemma has_same_inode_tainted:

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

   173 by (simp add:has_same_inode_Tainted tainted_eq_Tainted)

   174 

   175 lemma same_inodes_Tainted:

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

   177 apply (frule same_inode_files_prop8, frule same_inode_files_prop7)

   178 apply (auto intro:has_same_inode_Tainted)

   179 done

   180 

   181 

   182 

   183 lemma tainted_in_current:

   184   "obj \<in> tainted s \<Longrightarrow> alive s obj"

   185 apply (erule tainted.induct)

   186 apply (auto dest:vt_grant_os vd_cons info_shm_flow_in_procs procs_of_shm_prop2 simp:is_file_simps)

   187 apply (drule seeds_in_init, simp add:tobj_in_alive)

   188 apply (erule has_same_inode_prop2, simp, simp add:vd_cons)

   189 apply (frule vt_grant_os, simp)

   190 apply (erule has_same_inode_prop1, simp, simp add:vd_cons)

   191 done

   192 

   193 lemma tainted_is_valid:

   194   "obj \<in> tainted s \<Longrightarrow> valid s"

   195 by (erule tainted.induct, auto intro:valid.intros)

   196 

   197 lemma t_remain_app:

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

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

   200 apply (induct s', simp)

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

   202 apply (simp_all add:not_deleted_cons_D vd_cons)

   203 apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons)

   204 done

   205 

   206 lemma valid_tainted_obj:

   207   "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h) \<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)"

   208 apply (erule tainted.induct)

   209 apply (drule seeds_in_init)

   210 by auto

   211 

   212 lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False"

   213 by (auto dest:valid_tainted_obj)

   214 

   215 lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False"

   216 by (auto dest:valid_tainted_obj)

   217 

   218 lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False"

   219 by (auto dest:valid_tainted_obj)

   220 

   221 end

   222 

   223 end