48 (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)" |
49 | "Tainted (Truncate p f len # s) = |
49 | "Tainted (Truncate p f len # s) = |
50 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
50 (if (len > 0 \<and> O_proc p \<in> Tainted s) |
51 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'} |
52 else Tainted s)" |
52 else Tainted s)" |
|
53 | "Tainted (Attach p h flag # s) = |
|
54 (if (O_proc p \<in> Tainted s \<and> flag = SHM_RDWR) |
|
55 then Tainted s \<union> {O_proc p' | p' flag'. (p', flag') \<in> procs_of_shm s h} |
|
56 else if (\<exists> p'. O_proc p' \<in> Tainted s \<and> (p', SHM_RDWR) \<in> procs_of_shm s h) |
|
57 then Tainted s \<union> {O_proc p} |
|
58 else Tainted s)" |
53 | "Tainted (SendMsg p q m # s) = |
59 | "Tainted (SendMsg p q m # s) = |
54 (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)" |
60 (if (O_proc p \<in> Tainted s) then Tainted s \<union> {O_msg q m} else Tainted s)" |
55 | "Tainted (RecvMsg p q m # s) = |
61 | "Tainted (RecvMsg p q m # s) = |
56 (if (O_msg q m \<in> Tainted s) |
62 (if (O_msg q m \<in> Tainted s) |
57 then (Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}) - {O_msg q m} |
63 then (Tainted s \<union> {O_proc p' | p'. info_flow_shm s p p'}) - {O_msg q m} |
70 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
76 "\<lbrakk>obj \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj" |
71 apply (induct s, simp) |
77 apply (induct s, simp) |
72 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
78 apply (drule seeds_in_init, case_tac obj, simp_all add:is_file_nil) |
73 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
79 apply (frule vd_cons, frule valid_Tainted_obj, simp, frule vt_grant_os, case_tac a) |
74 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
80 apply (auto simp:alive_simps split:if_splits option.splits t_object.splits |
75 intro:has_same_inode_prop2 has_same_inode_prop1 dest:info_shm_flow_in_procs) |
81 intro:has_same_inode_prop2 has_same_inode_prop1 procs_of_shm_prop2 |
|
82 dest:info_shm_flow_in_procs) |
76 done |
83 done |
77 |
84 |
78 lemma Tainted_proc_in_current: |
85 lemma Tainted_proc_in_current: |
79 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
86 "\<lbrakk>O_proc p \<in> Tainted s; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s" |
80 by (drule Tainted_in_current, simp+) |
87 by (drule Tainted_in_current, simp+) |
93 apply (induct s, auto) |
100 apply (induct s, auto) |
94 apply (auto intro:tainted.intros simp:has_same_inode_def) |
101 apply (auto intro:tainted.intros simp:has_same_inode_def) |
95 (*?? need simpset for tainted *) |
102 (*?? need simpset for tainted *) |
96 sorry |
103 sorry |
97 |
104 |
98 lemma info_flow_shm_intro: |
|
99 "\<lbrakk>(p, SHM_RDWR) \<in> procs_of_shm s h; (p', flag) \<in> procs_of_shm s h; valid s\<rbrakk> |
|
100 \<Longrightarrow> info_flow_shm s p p'" |
|
101 apply (rule_tac p = p and p' = p in info_flow_shm.intros(2)) |
|
102 apply (auto intro!:info_flow_shm.intros(1) procs_of_shm_prop2) |
|
103 done |
|
104 |
105 |
105 lemma info_flow_shm_Tainted: |
106 lemma info_flow_shm_Tainted: |
106 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
107 "\<lbrakk>O_proc p \<in> Tainted s; info_flow_shm s p p'; valid s\<rbrakk> \<Longrightarrow> O_proc p' \<in> Tainted s" |
107 proof (induct s arbitrary:p p') |
108 proof (induct s arbitrary:p p') |
108 case Nil |
109 case Nil |
114 and p5: "valid s" and p6: "os_grant s e" |
115 and p5: "valid s" and p6: "os_grant s e" |
115 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
116 by (auto dest:vd_cons intro:vd_cons vt_grant_os) |
116 have p4': |
117 have p4': |
117 "\<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> |
118 "\<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> |
118 \<Longrightarrow> O_proc p' \<in> Tainted s" |
119 \<Longrightarrow> O_proc p' \<in> Tainted s" |
119 by (rule p4, auto intro!:info_flow_shm_intro p5) |
120 by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def) |
120 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" |
121 from p2 p3 have p7: "p \<in> current_procs (e # s)" and p8: "p' \<in> current_procs (e # s)" |
121 by (auto dest:info_shm_flow_in_procs) |
122 by (auto dest:info_shm_flow_in_procs) |
122 show ?case |
123 show ?case |
123 proof (cases "p = p'") |
124 proof (cases "self_shm s p p'") |
124 case True with p1 show ?thesis by simp |
125 case True with p1 show ?thesis by simp |
125 next |
126 next |
126 case False |
127 case False |
127 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
128 with p1 p2 p5 p6 p7 p8 p3 show ?thesis |
128 apply (case_tac e) |
129 apply (case_tac e) |
|
130 prefer 7 |
|
131 apply (simp add:info_flow_shm_simps split:if_splits option.splits) |
|
132 apply (rule allI|rule impI|rule conjI)+ |
|
133 apply simp |
|
134 apply (case_tac "O_proc p \<in> Tainted s", drule_tac p'=p' in p4, simp+) |
|
135 apply simp |
|
136 |
|
137 |
|
138 |
|
139 |
|
140 apply (auto simp:info_flow_shm_simps one_flow_shm_def dest:Tainted_in_current |
|
141 intro:p4 p4' split:if_splits option.splits) |
|
142 apply (auto simp:info_flow_shm_def one_flow_shm_def) |
|
143 |
|
144 |
|
145 |
|
146 apply (auto simp:one_flow_shm_def intro:p4 p4' split:if_splits option.splits) |
|
147 |
|
148 |
|
149 |
|
150 |
|
151 |
|
152 |
129 prefer 7 |
153 prefer 7 |
130 apply (simp split:if_splits option.splits) |
154 apply (simp split:if_splits option.splits) |
131 apply (rule allI|rule impI|rule conjI)+ |
155 apply (rule allI|rule impI|rule conjI)+ |
132 |
156 |
133 |
157 |