theory Tainted_prop +
−
imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop +
−
begin+
−
+
−
context tainting begin+
−
+
−
fun Tainted :: "t_state \<Rightarrow> t_object set"+
−
where+
−
  "Tainted [] = seeds"+
−
| "Tainted (Clone p p' fds shms # s) = +
−
     (if (O_proc p) \<in> Tainted s then Tainted s \<union> {O_proc p'} else Tainted s)"+
−
| "Tainted (Execve p f fds # s) = +
−
     (if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)"+
−
| "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}"+
−
| "Tainted (Ptrace p p' # s) = +
−
     (if (O_proc p) \<in> Tainted s +
−
      then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}+
−
      else if (O_proc p') \<in> Tainted s +
−
           then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}+
−
                else Tainted s)"+
−
| "Tainted (Exit p # s) = Tainted s - {O_proc p}"+
−
| "Tainted (Open p f flags fd opt # s) = +
−
     (case opt of+
−
        Some inum \<Rightarrow> (if (O_proc p) \<in> Tainted s+
−
                      then Tainted s \<union> {O_file f}+
−
                      else Tainted s)+
−
      | _         \<Rightarrow> Tainted s)" +
−
| "Tainted (ReadFile p fd # s) = +
−
     (case (file_of_proc_fd s p fd) of+
−
        Some f \<Rightarrow> if (O_file f) \<in> Tainted s+
−
                  then Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}+
−
                  else Tainted s+
−
      | None   \<Rightarrow> Tainted s)"+
−
| "Tainted (WriteFile p fd # s) = +
−
     (case (file_of_proc_fd s p fd) of +
−
        Some f \<Rightarrow> if (O_proc p) \<in> Tainted s+
−
                  then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}+
−
                  else Tainted s+
−
      | None   \<Rightarrow> Tainted s)"+
−
| "Tainted (CloseFd p fd # s) = +
−
     (case (file_of_proc_fd s p fd) of+
−
        Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p,fd)}) \<and> (f \<in> files_hung_by_del s))+
−
                    then Tainted s - {O_file f} else Tainted s )+
−
      | _      \<Rightarrow> Tainted s)"+
−
| "Tainted (UnLink p f # s) = +
−
     (if (proc_fd_of_file s f = {}) then Tainted s - {O_file f} else Tainted s)"+
−
| "Tainted (LinkHard p f f' # s) = +
−
     (if (O_file f \<in> Tainted s) then Tainted s \<union> {O_file f'} else Tainted s)"+
−
| "Tainted (Truncate p f len # s) = +
−
     (if (len > 0 \<and> O_proc p \<in> Tainted s)+
−
      then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}+
−
      else Tainted s)"+
−
| "Tainted (Attach p h flag # s) = +
−
     (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) +
−
      then Tainted s \<union> {O_proc p' | p' flag'. (p', flag') \<in> procs_of_shm s h}+
−
      else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h)+
−
           then Tainted s \<union> {O_proc p}+
−
           else Tainted s)"+
−
| "Tainted (SendMsg p q m # s) = +
−
     (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)"+
−
| "Tainted (RecvMsg p q m # s) = +
−
     (if (O_msg q m \<in> Tainted s) +
−
      then (Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}) - {O_msg q m}+
−
      else Tainted s)"+
−
| "Tainted (RemoveMsgq p q # s) = Tainted s - {O_msg q m| m. O_msg q m \<in> Tainted s}"+
−
| "Tainted (e # s) = Tainted s"+
−
+
−
lemma valid_Tainted_obj:+
−
  "\<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)"+
−
apply (induct s, simp, drule seeds_in_init, case_tac obj, simp+)+
−
apply (frule vd_cons, frule vt_grant_os, case_tac a)+
−
apply (auto split:if_splits option.splits)+
−
done+
−
+
−
lemma Tainted_in_current:+
−
  "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"+
−
apply (induct s, simp)+
−
apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil)+
−
apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a)+
−
apply (auto simp:alive_simps split:if_splits option.splits t_object.splits+
−
           intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 +
−
            dest:info_shm_flow_in_procs)+
−
done +
−
+
−
lemma Tainted_proc_in_current:+
−
  "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"+
−
by (drule Tainted_in_current, simp+)+
−
+
−
lemma has_inode_tainted_aux:+
−
  "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"+
−
apply (erule tainted.induct)+
−
apply (auto intro:tainted.intros simp:has_same_inode_def)+
−
(*?? need simpset for tainted *)+
−
+
−
+
−
sorry+
−
+
−
lemma has_inode_Tainted_aux:+
−
  "\<lbrakk>O_file f \<in> Tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> Tainted s"+
−
apply (induct s, auto)+
−
apply (auto intro:tainted.intros simp:has_same_inode_def)+
−
(*?? need simpset for tainted *)+
−
sorry+
−
+
−
lemma "\<lbrakk>info_flow_shm s pa pb; info_flow_shm s pb pc; valid s\<rbrakk> \<Longrightarrow> info_flow_shm s pa pc"+
−
apply (auto simp add:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2)+
−
apply (erule_tac x = h in allE, simp)+
−
apply (case_tac "h = ha", simp+)+
−
sorry+
−
+
−
lemma info_flow_shm_Tainted:+
−
  "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s"+
−
proof (induct s arbitrary:p p')+
−
  case Nil+
−
  thus ?case by (simp add:flow_shm_in_seeds)+
−
next+
−
  case (Cons e s)+
−
  hence p1: "O_proc p \<in> Tainted (e # s)" and p2: "info_flow_shm (e # s) p p'" and p3: "valid (e # s)"  +
−
    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" +
−
    and p5: "valid s" and p6: "os_grant s e"+
−
    by (auto dest:vd_cons intro:vd_cons vt_grant_os)+
−
  have p4': +
−
    "\<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> +
−
                \<Longrightarrow> O_proc p' \<in> Tainted s"+
−
    apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *)    +
−
    sorry+
−
  from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" (*+
−
    by (auto dest:info_shm_flow_in_procs) *) sorry+
−
  show ?case+
−
  proof (cases "self_shm s p p'")+
−
    case True with p1 show ?thesis by simp+
−
  next+
−
    case False+
−
    with p1 p2 p5 p6 p7 p8 p3 show ?thesis+
−
    apply (case_tac e)+
−
    prefer 7+
−
    apply (simp add:info_flow_shm_simps split:if_splits option.splits)+
−
    apply (rule allI|rule impI|rule conjI)++
−
    apply simp+
−
    apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+)+
−
    apply simp+
−
+
−
+
−
+
−
+
−
    apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current +
−
  intro:p4 p4' split:if_splits option.splits)+
−
    apply (auto simp:info_flow_shm_def one_flow_shm_def)+
−
+
−
+
−
+
−
    apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits)+
−
+
−
+
−
+
−
+
−
+
−
+
−
    prefer 7+
−
    apply (simp split:if_splits option.splits)+
−
    apply (rule allI|rule impI|rule conjI)++
−
+
−
+
−
    apply (auto dest:p4'   procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]+
−
+
−
    apply (erule disjE, drule_tac p = p and p' = p' in p4', simp+)+
−
    apply (erule disjE, rule disjI2, rule disjI2, rule_tac x = h in exI, simp, rule_tac x= toflag in exI, simp)+
−
    apply ((erule exE|erule conjE)+)+
−
    +
−
+
−
    apply (auto simp:info_flow_shm_def dest:p4'+
−
           procs_of_shm_prop2 Tainted_in_current split:if_splits option.splits)[1]+
−
    apply (drule_tac p = p and p' = p' in p4')+
−
    apply (erule_tac x = ha in allE, simp)+
−
    apply (drule_tac p = "nat1" and p' = p' in p4')+
−
    apply (auto dest:p4'[where p = nat1 and p' = p'])+
−
    +
−
apply (induct s) (*+
−
apply simp defer+
−
apply (frule vd_cons, frule vt_grant_os, case_tac a)+
−
apply (auto simp:info_flow_shm_def elim!:disjE)+
−
sorry *)+
−
  sorry+
−
next +
−
  case (Cons e s)+
−
  show ?case +
−
    sorry+
−
qed+
−
+
−
lemma tainted_imp_Tainted:+
−
  "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"+
−
apply (induct rule:tainted.induct)+
−
apply (auto intro:info_flow_shm_Tainted dest:vd_cons)+
−
apply (case_tac e, auto split:option.splits if_splits simp:alive_simps)+
−
done+
−
+
−
lemma Tainted_imp_tainted:+
−
  "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s"+
−
proof (induct s arbitrary:obj)+
−
  case Nil+
−
  thus ?case by (auto intro:t_init)+
−
next+
−
  case (Cons e s)+
−
  hence p1: "\<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s"+
−
    and p2: "obj \<in> Tainted (e # s)" and p3: "valid (e # s)" +
−
    and p4: "valid s" and p5: "os_grant s e"+
−
    by (auto dest:vd_cons intro:vd_cons vt_grant_os)+
−
  from p1 have p6: ""+
−
apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp)+
−
apply (case_tac a)+
−
apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg+
−
            intro:t_remain+
−
             split:if_splits option.splits dest:Tainted_in_current)+
−
pr 25+
−
+
−
lemma tainted_imp_Tainted:+
−
  "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s"+
−
+
−
+
−
+
−
+
−
+
−
+
−
lemma tainted_in_current:+
−
  "obj \<in> tainted s \<Longrightarrow> alive s obj"+
−
apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)+
−
apply (drule seeds_in_init, simp add:tobj_in_alive)+
−
apply (erule has_same_inode_prop2, simp, simp add:vd_cons)+
−
apply (frule vt_grant_os, simp)+
−
apply (erule has_same_inode_prop1, simp, simp add:vd_cons)+
−
done+
−
+
−
lemma tainted_is_valid:+
−
  "obj \<in> tainted s \<Longrightarrow> valid s"+
−
by (erule tainted.induct, auto intro:valid.intros)+
−
+
−
lemma t_remain_app:+
−
  "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); valid (s' @ s)\<rbrakk> +
−
  \<Longrightarrow> obj \<in> tainted (s' @ s)"+
−
apply (induct s', simp)+
−
apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)+
−
apply (simp_all add:not_deleted_cons_D vd_cons)+
−
apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons)+
−
done+
−
+
−
lemma valid_tainted_obj:+
−
  "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)"+
−
apply (erule tainted.induct)+
−
apply (drule seeds_in_init)+
−
by auto+
−
+
−
lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False"+
−
by (auto dest:valid_tainted_obj)+
−
+
−
lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False"+
−
by (auto dest:valid_tainted_obj)+
−
+
−
lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False"+
−
by (auto dest:valid_tainted_obj)+
−
+
−
end+
−
+
−
end+
−