6 

     7 fun Tainted :: "t_state \<Rightarrow> t_object set"

     8 where

     9   "Tainted [] = seeds"

    10 | "Tainted (Clone p p' fds shms # s) = 

    11      (if (O_proc p) \<in> Tainted s then Tainted s \<union> {O_proc p'} else Tainted s)"

    12 | "Tainted (Execve p f fds # s) = 

    13      (if (O_file f) \<in> Tainted s then Tainted s \<union> {O_proc p} else Tainted s)"

    14 | "Tainted (Kill p p' # s) = Tainted s - {O_proc p'}"

    15 | "Tainted (Ptrace p p' # s) = 

    16      (if (O_proc p) \<in> Tainted s 

    17       then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p' p''}

    18       else if (O_proc p') \<in> Tainted s 

    19            then Tainted s \<union> {O_proc p'' | p''. info_flow_shm s p p''}

    20                 else Tainted s)"

    21 | "Tainted (Exit p # s) = Tainted s - {O_proc p}"

    22 | "Tainted (Open p f flags fd opt # s) = 

    23      (case opt of

    24         Some inum \<Rightarrow> (if (O_proc p) \<in> Tainted s

    25                       then Tainted s \<union> {O_file f}

    26                       else Tainted s)

    27       | _         \<Rightarrow> Tainted s)" 

    28 | "Tainted (ReadFile p fd # s) = 

    29      (case (file_of_proc_fd s p fd) of

    30         Some f \<Rightarrow> if (O_file f) \<in> Tainted s

    31                   then Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}

    32                   else Tainted s

    33       | None   \<Rightarrow> Tainted s)"

    34 | "Tainted (WriteFile p fd # s) = 

    35      (case (file_of_proc_fd s p fd) of 

    36         Some f \<Rightarrow> if (O_proc p) \<in> Tainted s

    37                   then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}

    38                   else Tainted s

    39       | None   \<Rightarrow> Tainted s)"

    40 | "Tainted (CloseFd p fd # s) = 

    41      (case (file_of_proc_fd s p fd) of

    42         Some f \<Rightarrow> ( if ((proc_fd_of_file s f = {(p,fd)}) \<and> (f \<in> files_hung_by_del s))

    43                     then Tainted s - {O_file f} else Tainted s )

    44       | _      \<Rightarrow> Tainted s)"

    45 | "Tainted (UnLink p f # s) = Tainted s - {O_file f}"

    46 | "Tainted (LinkHard p f f' # s) = 

    47      (if (O_file f \<in> Tainted s) then Tainted s \<union> {O_file f'} else Tainted s)"

    48 | "Tainted (Truncate p f len # s) = 

    49      (if (len > 0 \<and> O_proc p \<in> Tainted s)

    50       then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'}

    51       else Tainted s)"

    52 | "Tainted (SendMsg p q m # s) = 

    53      (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)"

    54 | "Tainted (RecvMsg p q m # s) = 

    55      (if (O_msg q m \<in> Tainted s) 

    56       then Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'} - {O_msg q m}

    57       else Tainted s)"

    58 | "Tainted (RemoveMsgq p q # s) = Tainted s - {O_msg q m| m. O_msg q m \<in> Tainted s}"

    59 | "Tainted (e # s) = Tainted s"

    60 

    61 lemma valid_Tainted_obj:

    62   "\<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)"

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

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

    65 apply (auto split:if_splits option.splits)

    66 done

    67 

    68 lemma Tainted_in_current:

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

    70 apply (induct s, simp)

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

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

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

    74 apply (auto intro:has_same_inode_prop2 has_same_inode_prop1)

    75 apply 

    76 

    77 lemma Tainted_imp_tainted:

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

    79 apply (induct s arbitrary:obj, rule t_init, simp)

    80 apply (frule vd_cons, frule vt_grant_os)

    81 apply (case_tac a)

    82 apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg

    83              split:if_splits option.splits)

    84 pr 25

    85 

    86 lemma tainted_imp_Tainted:

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

    88 

    89 

    90 

    91 

    92