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 (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 dest:info_shm_flow_in_procs)

done

lemma has_inode_Tainted_aux:

apply (auto intro:tainted.intros simp:has_same_inode_def)

(*?? need simpset for tainted *)

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"

  case Nil

apply simp defer

apply (frule vd_cons, frule vt_grant_os, case_tac a)

apply (auto simp:info_flow_shm_def elim!:disjE)

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