40 | "Tainted (CloseFd p fd # s) = |
40 | "Tainted (CloseFd p fd # s) = |
41 (case (file_of_proc_fd s p fd) of |
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)) |
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 ) |
43 then Tainted s - {O_file f} else Tainted s ) |
44 | _ \<Rightarrow> Tainted s)" |
44 | _ \<Rightarrow> Tainted s)" |
45 | "Tainted (UnLink p f # s) = Tainted s - {O_file f}" |
45 | "Tainted (UnLink p f # s) = |
|
46 (if (proc_fd_of_file s f = {}) then Tainted s - {O_file f} else Tainted s)" |
46 | "Tainted (LinkHard p f f' # s) = |
47 | "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 (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 | "Tainted (Truncate p f len # s) = |
49 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
50 (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 then Tainted s \<union> {O_file f' | f'. has_same_inode s f f'} |
51 else Tainted s)" |
52 else Tainted s)" |
52 | "Tainted (SendMsg p q m # s) = |
53 | "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 (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 | "Tainted (RecvMsg p q m # s) = |
55 (if (O_msg q m \<in> Tainted s) |
56 (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 then (Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}) - {O_msg q m} |
57 else Tainted s)" |
58 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 (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 | "Tainted (e # s) = Tainted s" |
60 |
61 |
61 lemma valid_Tainted_obj: |
62 lemma valid_Tainted_obj: |
68 lemma Tainted_in_current: |
69 lemma Tainted_in_current: |
69 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
70 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
70 apply (induct s, simp) |
71 apply (induct s, simp) |
71 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
72 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 (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 simp:alive_simps split:if_splits option.splits t_object.splits |
74 apply (auto intro:has_same_inode_prop2 has_same_inode_prop1) |
75 intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs) |
75 apply |
76 done |
|
77 |
|
78 |
|
79 lemma has_inode_Tainted_aux: |
|
80 "\<lbrakk>O_file f \<in> tainted s; has_same_inode s f f'\<rbrakk> \<Longrightarrow> O_file f' \<in> tainted s" |
|
81 apply (erule tainted.induct) |
|
82 apply (auto intro:tainted.intros simp:has_same_inode_def) |
|
83 (*?? need simpset for tainted *) |
|
84 sorry |
|
85 |
|
86 lemma info_flow_shm_Tainted: |
|
87 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
|
88 proof (induct s) |
|
89 case Nil |
|
90 thus ?case |
|
91 apply simp |
|
92 apply (induct s) |
|
93 apply simp defer |
|
94 apply (frule vd_cons, frule vt_grant_os, case_tac a) |
|
95 apply (auto simp:info_flow_shm_def elim!:disjE) |
|
96 sorry |
|
97 |
|
98 lemma tainted_imp_Tainted: |
|
99 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
|
100 apply (induct rule:tainted.induct) |
|
101 apply (auto intro:info_flow_shm_Tainted dest:vd_cons) |
|
102 apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) |
|
103 done |
76 |
104 |
77 lemma Tainted_imp_tainted: |
105 lemma Tainted_imp_tainted: |
78 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s" |
106 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> obj \<in> tainted s" |
79 apply (induct s arbitrary:obj, rule t_init, simp) |
107 proof (induct s arbitrary:obj) |
80 apply (frule vd_cons, frule vt_grant_os) |
108 case Nil |
|
109 thus ?case by (auto intro:t_init) |
|
110 next |
|
111 case (Cons e s) |
|
112 hence p1: "\<And> obj. obj \<in> Tainted s \<Longrightarrow> obj \<in> tainted s" |
|
113 and p2: "obj \<in> Tainted (e # s)" and p3: "valid (e # s)" |
|
114 and p4: "valid s" and p5: "os_grant s e" |
|
115 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
|
116 from p1 have p6: "" |
|
117 apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp) |
81 apply (case_tac a) |
118 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 |
119 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) |
120 intro:t_remain |
|
121 split:if_splits option.splits dest:Tainted_in_current) |
84 pr 25 |
122 pr 25 |
85 |
123 |
86 lemma tainted_imp_Tainted: |
124 lemma tainted_imp_Tainted: |
87 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
125 "obj \<in> tainted s \<Longrightarrow> obj \<in> Tainted s" |
88 |
126 |