50 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state" |
50 fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state" |
51 where |
51 where |
52 "enrich_proc [] tp dp = []" |
52 "enrich_proc [] tp dp = []" |
53 | "enrich_proc (Execve p f fds # s) tp dp = ( |
53 | "enrich_proc (Execve p f fds # s) tp dp = ( |
54 if (tp = p) |
54 if (tp = p) |
55 then Execve dp f fds # Execve p f fds # (enrich_proc s tp dp) |
55 then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp) |
56 else Execve p f fds # (enrich_proc s tp dp))" |
56 else Execve p f fds # (enrich_proc s tp dp))" |
57 | "enrich_proc (Clone p p' fds shms # s) tp dp = ( |
57 | "enrich_proc (Clone p p' fds shms # s) tp dp = ( |
58 if (tp = p') |
58 if (tp = p') |
59 then Clone p dp fds shms # Clone p p' fds shms # s |
59 then Clone p dp (fds \<inter> proc_file_fds s p) shms # Clone p p' fds shms # s |
60 else Clone p dp fds shms # (enrich_proc s tp dp))" |
60 else Clone p p' fds shms # (enrich_proc s tp dp))" |
61 | "enrich_proc (Open p f flags fd opt # s) tp dp = ( |
61 | "enrich_proc (Open p f flags fd opt # s) tp dp = ( |
62 if (tp = p) |
62 if (tp = p) |
63 then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp) |
63 then Open dp f (remove_create_flag flags) fd opt # Open p f flags fd opt # (enrich_proc s tp dp) |
64 else Open p f flags fd opt # (enrich_proc s tp dp))" |
64 else Open p f flags fd opt # (enrich_proc s tp dp))" |
65 | "enrich_proc (CloseFd p fd # s) tp dp = ( |
65 | "enrich_proc (CloseFd p fd # s) tp dp = ( |
84 |
84 |
85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
86 where |
86 where |
87 "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s" |
87 "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s" |
88 |
88 |
|
89 lemma enrich_search_check: |
|
90 assumes grant: "search_check s (up, rp, tp) f" |
|
91 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
|
92 and vd: "valid s" and f_in: "is_file s f" and f_in': "is_file s' f" |
|
93 and sec: "sectxt_of_obj s' (O_file f) = sectxt_of_obj s (O_file f)" |
|
94 shows "search_check s' (up, rp, tp) f" |
|
95 proof (cases f) |
|
96 case Nil |
|
97 with f_in vd have "False" |
|
98 by (auto dest:root_is_dir') |
|
99 thus ?thesis by simp |
|
100 next |
|
101 case (Cons n pf) |
|
102 from vd f_in obtain sf where sf: "cf2sfile s f = Some sf" |
|
103 apply (drule_tac is_file_in_current, drule_tac current_file_has_sfile, simp) |
|
104 apply (erule exE, simp) |
|
105 done |
|
106 then obtain psfs where psfs: "get_parentfs_ctxts s pf = Some psfs" using Cons |
|
107 by (auto simp:cf2sfile_def split:option.splits if_splits) |
|
108 from sf cf2sf f_in have sf': "cf2sfile s' f = Some sf" by (auto dest:is_file_in_current) |
|
109 then obtain psfs' where psfs': "get_parentfs_ctxts s' pf = Some psfs'"using Cons |
|
110 by (auto simp:cf2sfile_def split:option.splits if_splits) |
|
111 with sf sf' psfs have psfs_eq: "set psfs' = set psfs" using Cons f_in f_in' |
|
112 apply (simp add:cf2sfile_def split:option.splits) |
|
113 apply (case_tac sf, simp) |
|
114 done |
|
115 show ?thesis using grant f_in f_in' psfs psfs' psfs_eq sec |
|
116 apply (simp add:Cons split:option.splits) |
|
117 by (case_tac a, simp) |
|
118 qed |
|
119 |
|
120 lemma enrich_inherit_fds_check: |
|
121 assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s" |
|
122 and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
|
123 and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'" |
|
124 and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p" |
|
125 shows "inherit_fds_check s' (up, nr, nt) p fds" |
|
126 proof- |
|
127 have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
|
128 proof- |
|
129 fix fd |
|
130 assume fd_in_fds: "fd \<in> fds" |
|
131 hence fd_in_cfds: "fd \<in> current_proc_fds s p" |
|
132 and fd_in_cfds': "fd \<in> current_proc_fds s' p" |
|
133 using fd_in fd_in' by auto |
|
134 from p_in vd obtain sp where csp: "cp2sproc s p = Some sp" |
|
135 by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp) |
|
136 with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p" |
|
137 apply (erule_tac x = p in allE) |
|
138 by (auto simp:cp2sproc_def split:option.splits simp:p_in) |
|
139 hence "cfd2sfd s p fd = cfd2sfd s' p fd" |
|
140 apply (simp add:cpfd2sfds_def) |
|
141 thm inherit_fds_check_def |
|
142 thm sectxts_of_fds_def |
|
143 thm cpfd2sfds_def |
|
144 apply ( |
|
145 |
|
146 show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)" |
|
147 sorry |
|
148 qed |
|
149 hence "sectxts_of_fds s' p fds = sectxts_of_fds s p fds" |
|
150 by (simp add:sectxts_of_fds_def) |
|
151 thus ?thesis using grant |
|
152 by (simp add:inherit_fds_check_def) |
|
153 qed |
|
154 |
|
155 |
89 lemma enrich_proc_aux1: |
156 lemma enrich_proc_aux1: |
90 assumes vs': "valid s'" |
157 assumes vs': "valid s'" |
91 and os: "os_grant s e" and grant: "grant s e" |
158 and os: "os_grant s e" and grant: "grant s e" and vd: "valid s" |
92 and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" |
159 and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" |
93 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
160 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
94 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
161 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
95 shows "valid (e # s')" |
162 shows "valid (e # s')" |
96 proof (cases e) |
163 proof (cases e) |
103 by (auto simp:Execve) |
170 by (auto simp:Execve) |
104 have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive |
171 have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive |
105 apply (auto simp:Execve) |
172 apply (auto simp:Execve) |
106 by (erule_tac x = "O_fd p x" in allE, auto) |
173 by (erule_tac x = "O_fd p x" in allE, auto) |
107 have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve) |
174 have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve) |
108 moreover have "grant s' e" |
175 moreover have "grant s' e" apply (simp add:Execve) |
109 proof- |
176 proof- |
110 from grant obtain up rp tp uf rf tf |
177 from grant obtain up rp tp uf rf tf |
111 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
178 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
112 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
179 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
113 by (simp add:Execve split:option.splits, blast) |
180 by (simp add:Execve split:option.splits, blast) |
115 by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast) |
182 by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast) |
116 from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" |
183 from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" |
117 using os cp2sp |
184 using os cp2sp |
118 apply (erule_tac x = p in allE) |
185 apply (erule_tac x = p in allE) |
119 by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits) |
186 by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits) |
120 from p2 have p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" |
187 from os have f_in': "is_file s f" by (simp add:Execve) |
121 using os cf2sf |
188 from vd os have "\<exists> sf. cf2sfile s f = Some sf" |
122 apply (erule_tac x = "f" in allE) |
189 by (auto dest!:is_file_in_current current_file_has_sfile simp:Execve) |
123 apply (auto simp:Execve dest:is_file_in_current) |
190 hence p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" using f_in f_in' p2 cf2sf |
124 thm cf2sfile_def |
191 apply (erule_tac x = f in allE) |
125 apply (auto simp:cf2sfile_def split:option.splits) |
192 apply (auto dest:is_file_in_current simp:cf2sfile_def split:option.splits) |
126 apply (auto simp:Execve co2sobj.simps cf2sfile_simps split:option.splits) |
193 apply (case_tac f, simp) |
127 apply (simp add:cf2sfiles_def) |
194 apply (drule_tac s = s in root_is_dir', simp add:vd, simp+) |
128 apply (auto)[1] |
195 done |
129 using os pre |
196 show ? |
130 show ?thesis |
|
131 proof- |
197 proof- |
132 have |
198 have |
133 |
199 |
134 |
200 |
135 |
201 |
136 |
202 |
137 lemma enrich_proc_prop: |
203 lemma enrich_proc_prop: |
138 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
204 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
139 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
205 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
140 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
206 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
141 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
207 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and> |
|
208 (\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and> |
|
209 (\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and> |
|
210 (Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))" |
142 proof (induct s) |
211 proof (induct s) |
143 case Nil |
212 case Nil |
144 thus ?case by (auto simp:is_created_proc_def) |
213 thus ?case by (auto simp:is_created_proc_def) |
145 next |
214 next |
146 case (Cons e s) |
215 case (Cons e s) |