1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7theory ADT_AC
8imports Syscall_AC
9begin
10
11context begin interpretation Arch . (*FIXME: arch_split*)
12
13lemma pd_of_thread_same_agent:
14  "\<lbrakk> pas_refined aag s; is_subject aag tcb_ptr;
15     get_pd_of_thread (kheap s) (arch_state s) tcb_ptr = pd;
16     pd \<noteq> arm_global_pd (arch_state s) \<rbrakk>
17   \<Longrightarrow> pasObjectAbs aag tcb_ptr = pasObjectAbs aag pd"
18  apply (rule_tac aag="pasPolicy aag" in aag_wellformed_Control[rotated])
19   apply (fastforce simp: pas_refined_def)
20  apply (rule pas_refined_mem[rotated], simp)
21  apply (clarsimp simp: get_pd_of_thread_eq)
22  apply (cut_tac ptr="(tcb_ptr, tcb_cnode_index 1)" in sbta_caps)
23     prefer 4
24     apply (simp add: state_objs_to_policy_def)
25    apply (subst caps_of_state_tcb_cap_cases)
26      apply (simp add: get_tcb_def)
27     apply (simp add: dom_tcb_cap_cases[simplified])
28    apply simp
29   apply (simp add: obj_refs_def)
30  apply (simp add: cap_auth_conferred_def is_page_cap_def)
31  done
32
33lemma invs_valid_global_pd_mappings:
34  "invs s \<Longrightarrow> valid_global_vspace_mappings s"
35  apply (simp add: invs_def valid_state_def)
36  done
37
38lemma objs_valid_tcb_vtable:
39  "\<lbrakk>valid_objs s; get_tcb t s = Some tcb\<rbrakk> \<Longrightarrow> s \<turnstile> tcb_vtable tcb"
40  apply (clarsimp simp: get_tcb_def split: option.splits Structures_A.kernel_object.splits)
41  apply (erule cte_wp_valid_cap[rotated])
42  apply (rule cte_wp_at_tcbI[where t="(a, b)" for a b, where b3="tcb_cnode_index 1"])
43    apply fastforce+
44  done
45
46lemma pd_of_thread_page_directory_at:
47  "\<lbrakk> invs s; get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s) \<rbrakk>
48    \<Longrightarrow> page_directory_at ((get_pd_of_thread (kheap s) (arch_state s) tcb)) s"
49  apply (clarsimp simp: get_pd_of_thread_def
50                 split: option.splits kernel_object.splits cap.splits arch_cap.splits if_splits)
51  apply (frule_tac t=tcb in objs_valid_tcb_vtable[OF invs_valid_objs])
52   apply (simp add: get_tcb_def)
53  apply (fastforce simp: valid_cap_def2 valid_cap_ref_def valid_arch_cap_ref_simps)
54  done
55
56lemma ptr_offset_in_ptr_range:
57  "\<lbrakk> invs s; get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
58           (get_pd_of_thread (kheap s) (arch_state s) tcb) x =
59          Some (base, sz, attr, r); x \<notin> kernel_mappings;
60     get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s) \<rbrakk>
61   \<Longrightarrow> ptrFromPAddr base + (x && mask sz) \<in> ptr_range (ptrFromPAddr base) sz"
62  apply (simp add: ptr_range_def mask_def)
63  apply (rule conjI)
64   apply (rule_tac b="2 ^ sz - 1" in word_plus_mono_right2)
65    apply (frule some_get_page_info_umapsD)
66          apply (clarsimp simp: get_pd_of_thread_reachable invs_vspace_objs
67                                invs_psp_aligned invs_valid_asid_table invs_valid_objs)+
68    apply (drule is_aligned_ptrFromPAddr_n)
69     apply (simp add: pageBitsForSize_def split: vmpage_size.splits)
70    apply (clarsimp simp: is_aligned_no_overflow' word_and_le1)+
71
72  apply (subst p_assoc_help)
73  apply (rule word_plus_mono_right)
74   apply (rule word_and_le1)
75  apply (frule some_get_page_info_umapsD)
76        apply (clarsimp simp: get_pd_of_thread_reachable invs_vspace_objs
77                              invs_psp_aligned invs_valid_asid_table invs_valid_objs)+
78  apply (drule is_aligned_ptrFromPAddr_n)
79   apply (simp add: pageBitsForSize_def split: vmpage_size.splits)
80  apply (clarsimp simp: is_aligned_no_overflow')
81  done
82
83lemma kernel_mappings_kernel_mapping_slots:
84  "x \<notin> kernel_mappings \<Longrightarrow> ucast (x >> 20) \<notin> kernel_mapping_slots"
85  apply (rule kernel_base_kernel_mapping_slots)
86  apply (simp add: kernel_mappings_def)
87  done
88
89lemmas kernel_mappings_kernel_mapping_slots' =
90       kernel_mappings_kernel_mapping_slots[simplified kernel_mapping_slots_def, simplified]
91
92lemma ptable_state_objs_to_policy:
93  "\<lbrakk> invs s; ptable_lift tcb s x = Some ptr;
94     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x);
95     get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s);
96     \<forall>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
97        (get_pd_of_thread (kheap s) (arch_state s) tcb) x \<noteq>
98        Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk>
99  \<Longrightarrow> (get_pd_of_thread (kheap s) (arch_state s) tcb, auth, ptrFromPAddr ptr)
100          \<in> state_objs_to_policy s"
101  apply (simp add: state_objs_to_policy_def)
102  apply (rule sbta_vref)
103  apply (clarsimp simp: ptable_lift_def ptable_rights_def state_vrefs_def
104                  split: option.splits)
105  apply (frule pd_of_thread_page_directory_at, simp)
106  apply (clarsimp simp: typ_at_eq_kheap_obj)
107
108  apply (clarsimp simp: vs_refs_no_global_pts_def)
109  apply (rule_tac x="(ucast (x >> 20), ptrFromPAddr a, aa,
110                      vspace_cap_rights_to_auth b)" in bexI)
111   apply clarsimp
112   apply (rule_tac x="(ptrFromPAddr a + (x && mask aa), auth)" in image_eqI)
113    apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
114   apply (simp add: ptr_offset_in_ptr_range)
115
116  apply (simp add: kernel_mappings_kernel_mapping_slots')
117  apply (clarsimp simp: graph_of_def)
118  apply (clarsimp simp: get_page_info_def get_pd_entry_def pde_ref2_def
119                  split: option.splits pde.splits arch_kernel_obj.splits)
120   apply (clarsimp simp: get_arch_obj_def
121                   split: option.splits kernel_object.splits arch_kernel_obj.splits)+
122  done
123
124lemma pt_in_pd_same_agent:
125  "\<lbrakk> pas_refined aag s; is_subject aag pd_ptr; vptr \<notin> kernel_mappings;
126     get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr vptr = Some (PageTablePDE p x xa) \<rbrakk>
127   \<Longrightarrow> pasObjectAbs aag pd_ptr = pasObjectAbs aag (ptrFromPAddr p)"
128  apply (rule_tac aag="pasPolicy aag" in aag_wellformed_Control[rotated])
129   apply (fastforce simp: pas_refined_def)
130  apply (rule pas_refined_mem[rotated], simp)
131  apply (clarsimp simp: get_pd_entry_def get_arch_obj_def
132                  split: option.splits kernel_object.splits arch_kernel_obj.splits)
133  apply (simp add: state_objs_to_policy_def)
134  apply (rule sbta_vref)
135  apply (simp add: state_vrefs_def split: option.splits)
136
137  apply (clarsimp simp: vs_refs_no_global_pts_def)
138  apply (rule_tac x="(ucast (vptr >> 20), ptrFromPAddr p, 0, {Control})" in bexI)
139   apply simp
140
141  apply (simp add: kernel_mappings_kernel_mapping_slots' graph_of_def pde_ref2_def)
142  done
143
144lemma pt_in_pd_page_table_at:
145  "\<lbrakk> invs s; get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ptr x =
146     Some (PageTablePDE word1 set1 word2); (\<exists>\<rhd> pd_ptr) s; x \<notin> kernel_mappings \<rbrakk>
147    \<Longrightarrow> page_table_at (ptrFromPAddr word1) s"
148  apply (clarsimp simp: get_pd_entry_def get_arch_obj_def
149                  split: option.splits kernel_object.splits arch_kernel_obj.splits)
150  apply (rename_tac "fun")
151  apply (subgoal_tac "valid_vspace_obj (PageDirectory fun) s")
152   apply (simp add: kernel_mappings_slots_eq)
153   apply (drule bspec)
154    apply simp+
155  apply (drule invs_vspace_objs)
156  apply (auto simp: obj_at_def invs_vspace_objs valid_vspace_objs_def)
157  done
158
159lemma get_page_info_state_objs_to_policy:
160  "\<lbrakk> invs s; auth \<in> vspace_cap_rights_to_auth r;
161     get_page_info (\<lambda>obj. get_arch_obj (kheap s obj))
162           (get_pd_of_thread (kheap s) (arch_state s) tcb) x = Some (base, sz, attr, r);
163     get_pd_of_thread (kheap s) (arch_state s) tcb \<noteq> arm_global_pd (arch_state s);
164     get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
165         (get_pd_of_thread (kheap s) (arch_state s) tcb) x =
166        Some (PageTablePDE word1 set1 word2); x \<notin> kernel_mappings \<rbrakk>
167  \<Longrightarrow> (ptrFromPAddr word1, auth, ptrFromPAddr (base + (x && mask sz))) \<in> state_objs_to_policy s"
168  apply (simp add: state_objs_to_policy_def)
169  apply (rule sbta_vref)
170  apply (clarsimp simp: state_vrefs_def split: option.splits)
171  apply (frule pt_in_pd_page_table_at)
172     apply (simp add: get_pd_of_thread_reachable)+
173  apply (clarsimp simp: typ_at_eq_kheap_obj)
174
175  apply (clarsimp simp: vs_refs_no_global_pts_def)
176  apply (rule_tac x="(ucast ((x >> 12) && mask 8),  ptrFromPAddr base, sz,
177                      vspace_cap_rights_to_auth r)" in bexI)
178   apply clarsimp
179   apply (rule_tac x="(ptrFromPAddr base + (x && mask sz), auth)" in image_eqI)
180    apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
181   apply (simp add: ptr_offset_in_ptr_range)
182
183  apply (clarsimp simp: graph_of_def)
184  apply (clarsimp simp: get_page_info_def get_pd_entry_def get_pt_info_def
185                        get_pt_entry_def pte_ref_def
186                  split: option.splits pte.splits pde.splits arch_kernel_obj.splits)
187   apply (clarsimp simp: get_arch_obj_def
188                   split: option.splits kernel_object.splits arch_kernel_obj.splits)+
189  done
190
191lemma user_op_access:
192  "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb;
193     ptable_lift tcb s x = Some ptr;
194     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk>
195   \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag (ptrFromPAddr ptr)) \<in> pasPolicy aag"
196  apply (case_tac "x \<in> kernel_mappings")
197   apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits)
198   apply (frule some_get_page_info_kmapsD)
199      apply (fastforce simp: invs_valid_global_pd_mappings invs_equal_kernel_mappings
200                             vspace_cap_rights_to_auth_def)+
201
202  apply (case_tac "get_pd_of_thread (kheap s) (arch_state s) tcb
203                 = arm_global_pd (arch_state s)")
204   apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits)
205   apply (frule get_page_info_gpd_kmaps[rotated, rotated])
206     apply (fastforce simp: invs_valid_global_objs invs_arch_state)+
207
208  apply (subst pd_of_thread_same_agent)
209      apply fastforce+
210
211  apply (case_tac "\<exists>word1 set1 word2. get_pd_entry (\<lambda>obj. get_arch_obj (kheap s obj))
212                          (get_pd_of_thread (kheap s) (arch_state s) tcb) x =
213                          Some (PageTablePDE word1 set1 word2)")
214   apply (clarsimp simp: ptable_lift_def ptable_rights_def split: option.splits)
215   apply (frule pd_of_thread_same_agent)
216      apply fastforce+
217   apply (subst pt_in_pd_same_agent)
218       apply fastforce+
219   apply (rule pas_refined_mem[rotated], simp)
220   apply (rule get_page_info_state_objs_to_policy)
221        apply fastforce+
222
223  apply (rule pas_refined_mem[rotated], simp)
224  apply (rule ptable_state_objs_to_policy)
225       apply simp+
226  done
227
228lemma user_op_access':
229  "\<lbrakk> invs s; pas_refined aag s; is_subject aag tcb;
230     ptable_lift tcb s x = Some (addrFromPPtr ptr);
231     auth \<in> vspace_cap_rights_to_auth (ptable_rights tcb s x) \<rbrakk>
232   \<Longrightarrow> (pasObjectAbs aag tcb, auth, pasObjectAbs aag ptr) \<in> pasPolicy aag"
233  apply (drule user_op_access)
234        apply auto
235  done
236
237lemma integrity_underlying_mem_update:
238  "\<lbrakk> integrity aag X st s;
239     \<forall>x\<in>xs. (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag;
240     \<forall>x\<in>-xs. um' x = underlying_memory (machine_state s) x\<rbrakk>
241    \<Longrightarrow> integrity aag X st
242          (machine_state_update (\<lambda>ms. underlying_memory_update (\<lambda>_. um') ms) s)"
243  apply (clarsimp simp: integrity_def)
244  apply (case_tac "x \<in> xs")
245   apply (erule_tac x=x in ballE)
246    apply (rule trm_write)
247    apply simp+
248  done
249
250lemma dmo_user_memory_update_respects_Write:
251  "\<lbrace>integrity aag X st and K (\<forall>p \<in> dom um. aag_has_auth_to aag Write p)\<rbrace>
252  do_machine_op (user_memory_update um)
253  \<lbrace>\<lambda>a. integrity aag X st\<rbrace>"
254  unfolding user_memory_update_def
255  apply (wp dmo_wp)
256  apply clarsimp
257  apply (simp cong: abstract_state.fold_congs option.case_cong_weak)
258  apply (rule integrity_underlying_mem_update)
259    apply simp+
260  apply (simp add: dom_def)+
261  done
262
263lemma integrity_device_state_update:
264  "\<lbrakk>integrity aag X st s;
265    \<forall>x\<in>xs. (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag;
266    \<forall>x\<in>-xs. um' x = None
267    \<rbrakk> \<Longrightarrow>  integrity aag X st (machine_state_update (\<lambda>v. v\<lparr>device_state := device_state v ++ um'\<rparr>) s)"
268  apply (clarsimp simp: integrity_def)
269  apply (case_tac "x \<in> xs")
270   apply (erule_tac x=x in ballE)
271    apply (rule trd_write)
272    apply simp+
273  apply (erule_tac x = x in allE, erule integrity_device.cases)
274    apply (erule trd_lrefl)
275   apply (rule trd_orefl)
276   apply (clarsimp simp: map_add_def)
277  apply (erule trd_write)
278  done
279
280lemma dmo_device_update_respects_Write:
281  "\<lbrace>integrity aag X st and (\<lambda>s. device_state (machine_state s) = um)
282    and K (\<forall>p \<in> dom um'. aag_has_auth_to aag Write p)\<rbrace>
283    do_machine_op (device_memory_update um')
284  \<lbrace>\<lambda>a. integrity aag X st\<rbrace>"
285  apply (simp add: device_memory_update_def)
286  apply (rule hoare_pre)
287   apply (wp dmo_wp)
288  apply clarsimp
289  apply (simp cong: abstract_state.fold_congs)
290  apply (rule integrity_device_state_update)
291    apply simp
292   apply clarify
293   apply (drule(1) bspec)
294   apply simp
295  apply fastforce
296  done
297
298lemma dmo_um_upd_machine_state:
299  "\<lbrace>\<lambda>s. P (device_state (machine_state s))\<rbrace>
300       do_machine_op (user_memory_update ms)
301   \<lbrace>\<lambda>_ s. P (device_state (machine_state s))\<rbrace>"
302  including no_pre
303  apply (wp dmo_wp)
304  by (simp add:user_memory_update_def simpler_modify_def valid_def)
305
306lemma do_user_op_respects:
307 "\<lbrace> invs and integrity aag X st and is_subject aag \<circ> cur_thread and pas_refined aag \<rbrace>
308    do_user_op uop tc
309  \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
310  apply (simp add: do_user_op_def)
311  apply (wp | simp | wpc)+
312           apply (rule dmo_device_update_respects_Write)
313          apply (wp dmo_um_upd_machine_state
314                    dmo_user_memory_update_respects_Write hoare_vcg_all_lift hoare_vcg_imp_lift
315                  | wpc | clarsimp)+
316          apply (rule hoare_pre_cont)
317         apply (wp   select_wp | wpc | clarsimp)+
318  apply (simp add: restrict_map_def split:if_splits)
319  apply (rule conjI)
320   apply (clarsimp split: if_splits)
321   apply (drule_tac auth=Write in user_op_access')
322       apply (simp add: vspace_cap_rights_to_auth_def)+
323  apply (rule conjI,simp)
324  apply (clarsimp split: if_splits)
325  apply (drule_tac auth=Write in user_op_access')
326      apply (simp add: vspace_cap_rights_to_auth_def)+
327  done
328
329end
330
331end
332