-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathArch_AC.thy
1261 lines (1122 loc) · 57.6 KB
/
Arch_AC.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(NICTA_GPL)
*)
theory Arch_AC
imports Retype_AC
begin
text{*
Arch-specific access control.
*}
lemma store_pde_respects:
"\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pd_bits)) \<rbrace>
store_pde p pde
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: store_pde_def set_pd_def)
apply (wp get_object_wp set_object_integrity_autarch)
apply simp
done
lemma store_pte_respects:
"\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pt_bits)) \<rbrace>
store_pte p pte
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: store_pte_def set_pt_def)
apply (wp get_object_wp set_object_integrity_autarch)
apply simp
done
lemma integrity_arch_state [iff]:
"\<lbrakk>arm_asid_table v = arm_asid_table (arch_state s)\<rbrakk> \<Longrightarrow>
integrity aag X st (s\<lparr>arch_state := v\<rparr>) = integrity aag X st s"
unfolding integrity_def
by (simp )
lemma integrity_arm_asid_map [iff]:
"integrity aag X st (s\<lparr>arch_state := ((arch_state s)\<lparr>arm_asid_map := v\<rparr>)\<rparr>) = integrity aag X st s"
unfolding integrity_def
by (simp )
lemma integrity_arm_hwasid_table [iff]:
"integrity aag X st (s\<lparr>arch_state := ((arch_state s)\<lparr>arm_hwasid_table := v\<rparr>)\<rparr>) = integrity aag X st s"
unfolding integrity_def
by (simp )
lemma integrity_arm_next_asid [iff]:
"integrity aag X st (s\<lparr>arch_state := ((arch_state s)\<lparr>arm_next_asid := v\<rparr>)\<rparr>) = integrity aag X st s"
unfolding integrity_def
by (simp )
declare dmo_mol_respects [wp]
crunch respects[wp]: arm_context_switch "integrity X aag st"
(simp: dmo_bind_valid dsb_def isb_def writeTTBR0_def invalidateTLB_ASID_def
setHardwareASID_def setCurrentPD_def
ignore: do_machine_op)
crunch respects[wp]: find_pd_for_asid "integrity X aag st"
crunch respects[wp]: set_vm_root "integrity X aag st"
(wp: crunch_wps
simp: setCurrentPD_def isb_def dsb_def writeTTBR0_def dmo_bind_valid crunch_simps
ignore: do_machine_op)
crunch respects[wp]: set_vm_root_for_flush "integrity X aag st"
(wp: crunch_wps simp: setCurrentPD_def crunch_simps ignore: do_machine_op)
crunch respects[wp]: flush_table "integrity X aag st"
(wp: crunch_wps simp: invalidateTLB_ASID_def crunch_simps ignore: do_machine_op)
crunch respects[wp]: page_table_mapped "integrity X aag st"
lemma kheap_eq_state_vrefsD:
"kheap s p = Some ko \<Longrightarrow> state_vrefs s p = vs_refs_no_global_pts ko"
by (simp add: state_vrefs_def)
lemma kheap_eq_state_vrefs_pas_refinedD:
"\<lbrakk> kheap s p = Some ko;
(p', r, a) \<in> vs_refs_no_global_pts ko; pas_refined aag s \<rbrakk>
\<Longrightarrow> (pasObjectAbs aag p, a, pasObjectAbs aag p') \<in> pasPolicy aag"
apply (drule kheap_eq_state_vrefsD)
apply (erule pas_refined_mem[OF sta_vref, rotated])
apply simp
done
lemma find_pd_for_asid_authority1:
"\<lbrace>pas_refined aag\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>pd s. (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag\<rbrace>,-"
apply (rule hoare_pre)
apply (simp add: find_pd_for_asid_def)
apply (wp | wpc)+
apply (clarsimp simp: obj_at_def pas_refined_def)
apply (erule subsetD, erule sata_asid_lookup)
apply (simp add: state_vrefs_def vs_refs_no_global_pts_def image_def)
apply (rule rev_bexI, erule graph_ofI)
apply (simp add: mask_asid_low_bits_ucast_ucast)
done
lemma find_pd_for_asid_authority2:
"\<lbrace>\<lambda>s. \<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag)
\<and> (pspace_aligned s \<and> valid_arch_objs s \<longrightarrow> is_aligned pd pd_bits)
\<and> (\<exists>\<rhd> pd) s
\<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, -"
(is "\<lbrace>?P\<rbrace> ?f \<lbrace>Q\<rbrace>,-")
apply (clarsimp simp: validE_R_def validE_def valid_def imp_conjL[symmetric])
apply (frule in_inv_by_hoareD[OF find_pd_for_asid_inv], clarsimp)
apply (drule spec, erule mp)
apply (simp add: use_validE_R[OF _ find_pd_for_asid_authority1]
use_validE_R[OF _ find_pd_for_asid_aligned_pd_bits]
use_validE_R[OF _ find_pd_for_asid_lookup])
done
lemma find_pd_for_asid_pd_slot_authorised [wp]:
"\<lbrace>pas_refined aag and K (is_subject_asid aag asid) and pspace_aligned and valid_arch_objs\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>rv s. is_subject aag (lookup_pd_slot rv vptr && ~~ mask pd_bits) \<rbrace>, -"
apply (wp find_pd_for_asid_authority2)
apply (clarsimp simp: lookup_pd_slot_pd)
apply (fastforce dest: pas_refined_Control)
done
lemma unmap_page_table_respects:
"\<lbrace>integrity aag X st and pas_refined aag and invs
and K (is_subject_asid aag asid \<and> vaddr < kernel_base)\<rbrace>
unmap_page_table asid vaddr pt
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: unmap_page_table_def page_table_mapped_def )
apply (rule hoare_pre)
apply (wp store_pde_respects page_table_mapped_wp_weak get_pde_wp
hoare_vcg_all_lift_R dmo_mol_respects
| wpc
| simp add: cleanByVA_PoU_def
| wp_once hoare_drop_imps)+
apply auto
done
definition
authorised_page_table_inv :: "'a PAS \<Rightarrow> ArchInvocation_A.page_table_invocation \<Rightarrow> bool"
where
"authorised_page_table_inv aag pti \<equiv> case pti of
ArchInvocation_A.page_table_invocation.PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow>
is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits)
\<and> (case_option True (is_subject aag o fst) (pde_ref2 pde))
\<and> pas_cap_cur_auth aag cap
| ArchInvocation_A.page_table_invocation.PageTableUnmap cap cslot_ptr \<Rightarrow>
is_subject aag (fst cslot_ptr) \<and> aag_cap_auth aag (pasSubject aag) cap
\<and> (\<forall>p asid vspace_ref. cap = cap.ArchObjectCap (arch_cap.PageTableCap p (Some (asid, vspace_ref)))
\<longrightarrow> is_subject_asid aag asid
\<and> (\<forall>x \<in> set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)))"
lemma perform_page_table_invocation_respects:
"\<lbrace>integrity aag X st and pas_refined aag and invs
and valid_pti page_table_invocation
and K (authorised_page_table_inv aag page_table_invocation)\<rbrace>
perform_page_table_invocation page_table_invocation
\<lbrace>\<lambda>s. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: perform_page_table_invocation_def
cong: ArchInvocation_A.page_table_invocation.case_cong option.case_cong prod.case_cong
cap.case_cong arch_cap.case_cong)
apply (rule hoare_pre)
apply (wp store_pde_respects get_cap_integrity_autarch set_cap_integrity_autarch store_pte_respects unmap_page_table_respects mapM_wp'
| wpc
| simp add: mapM_x_mapM authorised_page_table_inv_def cleanByVA_PoU_def)+
apply (auto simp: cap_auth_conferred_def is_page_cap_def
pas_refined_all_auth_is_owns
valid_pti_def valid_cap_simps)
done
crunch arch_state [wp]: do_machine_op "\<lambda>s. P (arch_state s)"
crunch arm_asid_table_inv [wp]: unmap_page_table "\<lambda>s. P (arm_asid_table (arch_state s))"
(wp: crunch_wps simp: crunch_simps)
lemma clas_update_map_data_strg:
"(is_pg_cap cap \<or> is_pt_cap cap) \<longrightarrow> cap_links_asid_slot aag p (cap.ArchObjectCap (update_map_data (the_arch_cap cap) None))"
unfolding cap_links_asid_slot_def
by (fastforce simp: is_cap_simps update_map_data_def)
lemmas pte_ref_simps = pte_ref_def[split_simps ARM_Structs_A.pte.split]
lemmas store_pde_pas_refined_simple
= store_pde_pas_refined[where pde=InvalidPDE, simplified pde_ref_simps, simplified]
crunch pas_refined[wp]: unmap_page_table "pas_refined aag"
(wp: crunch_wps store_pde_pas_refined_simple
simp: crunch_simps pde_ref_simps)
lemma pde_ref_pde_ref2:
"\<lbrakk> pde_ref x = Some v; pde_ref2 x = Some v' \<rbrakk> \<Longrightarrow> v' = (v, 0, {Control})"
unfolding pde_ref_def pde_ref2_def
by (cases x, simp_all)
lemma ptr_range_0 [simp]: "ptr_range (p :: word32) 0 = {p}"
unfolding ptr_range_def by simp
lemma mask_PTCap_eq:
"(ArchObjectCap (PageTableCap a b) = mask_cap R cap) = (cap = ArchObjectCap (PageTableCap a b))"
by (auto simp: mask_cap_def cap_rights_update_def acap_rights_update_def
split: arch_cap.splits cap.splits)
lemma perform_page_table_invocation_pas_refined [wp]:
"\<lbrace> pas_refined aag and valid_pti page_table_invocation
and K (authorised_page_table_inv aag page_table_invocation)\<rbrace>
perform_page_table_invocation page_table_invocation
\<lbrace>\<lambda>s. pas_refined aag\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: perform_page_table_invocation_def
cong: ArchInvocation_A.page_table_invocation.case_cong option.case_cong prod.case_cong
cap.case_cong arch_cap.case_cong)
apply (rule hoare_pre)
apply (wp get_cap_wp mapM_wp' store_pte_cte_wp_at do_machine_op_cte_wp_at hoare_vcg_all_lift
| (wp hoare_vcg_imp_lift, unfold disj_not1)
| wpc
| simp add: mapM_x_mapM authorised_page_table_inv_def imp_conjR disj_not1
pte_ref_simps)+
apply (cases page_table_invocation)
apply (fastforce simp: valid_pti_def is_cap_simps pas_refined_refl auth_graph_map_def2 dest: pde_ref_pde_ref2)
apply clarsimp
apply (subgoal_tac "cte_wp_at (op = xc) (aa, ba) s \<longrightarrow>
pas_cap_cur_auth aag (cap.ArchObjectCap (update_map_data (the_arch_cap xc) None))")
apply simp
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule (1) cap_cur_auth_caps_of_state)
apply simp
apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state is_cap_simps is_arch_diminished_def)
apply (clarsimp simp: diminished_def mask_PTCap_eq)
apply (clarsimp simp: cap_auth_conferred_def update_map_data_def is_page_cap_def cap_links_asid_slot_def cap_links_irq_def aag_cap_auth_def)
done
definition
authorised_slots :: "'a PAS \<Rightarrow> ARM_Structs_A.pte \<times> (obj_ref list) + ARM_Structs_A.pde \<times> (obj_ref list) \<Rightarrow> bool"
where
"authorised_slots aag m \<equiv> case m of
Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a \<in> (snd (snd x)). \<forall>p \<in> ptr_range (fst x) (fst (snd x)).(aag_has_auth_to aag a p)))
\<and> (\<forall>x \<in> set slots. is_subject aag (x && ~~ mask pt_bits))
| Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a \<in> (snd (snd x)). \<forall>p \<in> ptr_range (fst x) (fst (snd x)). (aag_has_auth_to aag a p)))
\<and> (\<forall>x \<in> set slots. is_subject aag (x && ~~ mask pd_bits))"
definition
authorised_page_inv :: "'a PAS \<Rightarrow> ArchInvocation_A.page_invocation \<Rightarrow> bool"
where
"authorised_page_inv aag pi \<equiv> case pi of
ArchInvocation_A.PageMap asid cap ptr slots \<Rightarrow>
pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> authorised_slots aag slots
| ArchInvocation_A.PageRemap asid slots \<Rightarrow> authorised_slots aag slots
| ArchInvocation_A.PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (Structures_A.ArchObjectCap cap) \<and> is_subject aag (fst ptr)
| ArchInvocation_A.PageFlush typ start end pstart pd asid \<Rightarrow> True
| ArchInvocation_A.PageGetAddr ptr \<Rightarrow> True"
crunch respects[wp]: check_mapping_pptr "integrity X aag st"
crunch respects[wp]: lookup_pt_slot "integrity X aag st"
lemma ptrFromPAddr_inj: "inj Platform.ptrFromPAddr"
by (auto intro: injI simp: Platform.ptrFromPAddr_def)
lemma vs_refs_no_global_pts_pdI:
"\<lbrakk>pd (ucast r) = ARM_Structs_A.pde.PageTablePDE x a b;
((ucast r)::12 word) < ucast (kernel_base >> 20) \<rbrakk> \<Longrightarrow>
(Platform.ptrFromPAddr x, VSRef (r && mask 12)
(Some APageDirectory), Control)
\<in> vs_refs_no_global_pts (ArchObj (PageDirectory pd))"
apply(clarsimp simp: vs_refs_no_global_pts_def)
apply (drule_tac f=pde_ref2 in arg_cong, simp add: pde_ref_simps o_def)
apply (rule rev_bexI, rule DiffI, erule graph_ofI)
apply simp
apply (clarsimp simp: ucast_ucast_mask )
done
lemma aag_has_auth_to_Control_eq_owns:
"pas_refined aag s \<Longrightarrow> aag_has_auth_to aag Control p = is_subject aag p"
by (auto simp: pas_refined_refl elim: aag_Control_into_owns)
lemma lookup_pt_slot_authorised:
"\<lbrace>\<exists>\<rhd> pd and valid_arch_objs and pspace_aligned and pas_refined aag
and K (is_subject aag pd) and K (is_aligned pd 14 \<and> vptr < kernel_base)\<rbrace>
lookup_pt_slot pd vptr
\<lbrace>\<lambda>rv s. is_subject aag (rv && ~~ mask pt_bits)\<rbrace>, -"
apply (simp add: lookup_pt_slot_def)
apply (wp get_pde_wp | wpc)+
apply (subgoal_tac "is_aligned pd pd_bits")
apply (clarsimp simp: lookup_pd_slot_pd)
apply (drule(2) valid_arch_objsD)
apply (clarsimp simp: obj_at_def)
apply (drule kheap_eq_state_vrefs_pas_refinedD)
apply (erule vs_refs_no_global_pts_pdI)
apply (drule(1) less_kernel_base_mapping_slots)
apply (simp add: kernel_mapping_slots_def)
apply assumption
apply (simp add: aag_has_auth_to_Control_eq_owns)
apply (drule_tac f="\<lambda>pde. valid_pde pde s" in arg_cong, simp)
apply (clarsimp simp: obj_at_def a_type_def less_kernel_base_mapping_slots)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm)
apply (erule pspace_alignedE, erule domI)
apply (simp add: pt_bits_def pageBits_def)
apply (subst is_aligned_add_helper, assumption)
apply (rule shiftl_less_t2n)
apply (rule order_le_less_trans, rule word_and_le1, simp)
apply simp
apply simp
apply (simp add: pd_bits_def pageBits_def)
done
lemma is_aligned_6_masks:
"\<lbrakk> is_aligned p 6; bits = pt_bits \<or> bits = pd_bits \<rbrakk>
\<Longrightarrow> \<forall>x \<in> set [0, 4 .e. 0x3C]. x + p && ~~ mask bits = p && ~~ mask bits"
apply clarsimp
apply (drule subsetD[OF upto_enum_step_subset])
apply (subst mask_lower_twice[symmetric, where n=6])
apply (auto simp add: pt_bits_def pageBits_def pd_bits_def)[1]
apply (subst add.commute, subst is_aligned_add_helper, assumption)
apply (simp add: order_le_less_trans)
apply simp
done
lemma lookup_pt_slot_authorised2:
"\<lbrace>\<exists>\<rhd> pd and K (is_subject aag pd) and
K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and
valid_arch_objs and valid_arch_state and equal_kernel_mappings and
valid_global_objs and pspace_aligned and pas_refined aag\<rbrace>
lookup_pt_slot pd vptr
\<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + rv && ~~ mask pt_bits)\<rbrace>, -"
apply (clarsimp simp: validE_R_def valid_def validE_def
split: sum.split)
apply (frule use_validE_R[OF _ lookup_pt_slot_authorised])
apply fastforce
apply (frule use_validE_R[OF _ lookup_pt_slot_is_aligned_6])
apply (fastforce simp add: vmsz_aligned_def pd_bits_def pageBits_def)
apply (simp add: is_aligned_6_masks)
done
lemma lookup_pt_slot_authorised3:
"\<lbrace>\<exists>\<rhd> pd and K (is_subject aag pd) and
K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and
valid_arch_objs and valid_arch_state and equal_kernel_mappings and
valid_global_objs and pspace_aligned and pas_refined aag\<rbrace>
lookup_pt_slot pd vptr
\<lbrace>\<lambda>rv s. \<forall>x\<in>set [rv , rv + 4 .e. rv + 0x3C]. is_subject aag (x && ~~ mask pt_bits)\<rbrace>, -"
apply (rule hoare_post_imp_R [where Q' = "\<lambda>rv s. is_aligned rv 6 \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + rv && ~~ mask pt_bits))"])
apply (rule hoare_pre)
apply (wp lookup_pt_slot_is_aligned_6 lookup_pt_slot_authorised2)
apply (fastforce simp: vmsz_aligned_def pd_bits_def pageBits_def)
apply simp
apply (simp add: p_0x3C_shift)
done
lemma mapM_set':
assumes ip: "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>I x and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace>"
and rl: "\<And>s. (\<forall>x \<in> set xs. I x s) \<Longrightarrow> P s"
shows "\<lbrace>\<lambda>s. (\<forall>x \<in> set xs. I x s)\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>"
apply (rule hoare_post_imp [OF rl])
apply assumption
apply (rule mapM_set)
apply (rule hoare_pre)
apply (rule hoare_vcg_ball_lift)
apply (erule (1) ip)
apply clarsimp
apply (rule hoare_pre)
apply (rule ip)
apply assumption
apply assumption
apply clarsimp
apply (rule hoare_pre)
apply (rule ip)
apply simp+
done
lemma mapM_set'':
assumes ip: "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>I x and I y and Q\<rbrace> f x \<lbrace>\<lambda>_. I y and Q\<rbrace>"
and rl: "\<And>s. (\<forall>x \<in> set xs. I x s) \<and> Q s \<Longrightarrow> P s"
shows "\<lbrace>\<lambda>s. (\<forall>x \<in> set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>"
apply (rule hoare_post_imp [OF rl])
apply assumption
apply (cases "xs = []")
apply (simp add: mapM_Nil)
apply (rule hoare_pre)
apply (rule mapM_set' [where I = "\<lambda>x s. I x s \<and> Q s"])
apply (rule hoare_pre)
apply (rule ip [simplified pred_conj_def])
apply simp_all
apply (clarsimp simp add: neq_Nil_conv)
done
crunch respects [wp]: flush_page "integrity aag X st"
(simp: invalidateTLB_VAASID_def ignore: do_machine_op)
lemma find_pd_for_asid_pd_owned[wp]:
"\<lbrace>pas_refined aag and K (is_subject_asid aag asid)\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>rv s. is_subject aag rv\<rbrace>,-"
apply (wp find_pd_for_asid_authority2)
apply (auto simp: aag_has_auth_to_Control_eq_owns)
done
lemmas store_pte_pas_refined_simple
= store_pte_pas_refined[where pte=InvalidPTE, simplified pte_ref_simps, simplified]
crunch pas_refined[wp]: unmap_page "pas_refined aag"
(wp: crunch_wps store_pde_pas_refined_simple store_pte_pas_refined_simple
simp: crunch_simps)
crunch pspace_aligned[wp]: flush_page "pspace_aligned"
lemma unmap_page_respects:
"\<lbrace>integrity aag X st and K (is_subject_asid aag asid) and pas_refined aag and pspace_aligned and valid_arch_objs
and K (vmsz_aligned vptr sz \<and> vptr < kernel_base)\<rbrace>
unmap_page sz asid vptr pptr
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: unmap_page_def swp_def cong: vmpage_size.case_cong)
apply (rule hoare_pre)
apply (wp store_pte_respects store_pde_respects
hoare_drop_imps[where Q="\<lambda>rv. integrity aag X st"]
lookup_pt_slot_authorised
| wpc
| simp add: is_aligned_6_masks is_aligned_mask[symmetric] cleanByVA_PoU_def
| wp_once hoare_drop_imps
mapM_set'' [where f = "(\<lambda>a. store_pte a ARM_Structs_A.pte.InvalidPTE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)" and Q = "integrity aag X st"]
mapM_set'' [where f = "(\<lambda>a. store_pde a ARM_Structs_A.pde.InvalidPDE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)" and Q = "integrity aag X st"]
| wp_once hoare_drop_imps[where R="\<lambda>rv s. rv"])+
done
(* FIXME: MOVE *)
lemma less_shiftr:
shows "\<lbrakk> x < y; is_aligned y n \<rbrakk> \<Longrightarrow> x >> n < y >> n"
apply (simp add: word_less_nat_alt shiftr_div_2n')
apply (subst td_gal_lt[symmetric])
apply simp
apply (subst dvd_div_mult_self)
apply (simp add: is_aligned_def)
apply simp
done
lemma kernel_base_aligned_20:
"is_aligned kernel_base 20"
apply(simp add: kernel_base_def is_aligned_def)
done
lemma diminished_PageCapD:
"diminished (ArchObjectCap (PageCap p R sz m)) cap
\<Longrightarrow> \<exists>R'. cap = ArchObjectCap (PageCap p R' sz m)"
apply (cases cap, auto simp add: diminished_def mask_cap_def cap_rights_update_def)
apply (auto simp: acap_rights_update_def split: arch_cap.splits)
done
(* FIXME: CLAG *)
lemmas do_machine_op_bind =
submonad_bind [OF submonad_do_machine_op submonad_do_machine_op
submonad_do_machine_op]
(* FIXME: CLAG *)
lemma ef_machine_op_lift [simp]:
"empty_fail (machine_op_lift f)"
by (simp add: machine_op_lift_def)
lemma mol_mem[wp]:
"\<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>rv ms. P (underlying_memory ms)\<rbrace>"
by (simp add: machine_op_lift_def machine_rest_lift_def split_def | wp)+
lemmas do_flush_defs = cleanCacheRange_RAM_def cleanCacheRange_PoC_def cleanCacheRange_PoU_def invalidateCacheRange_RAM_def cleanInvalidateCacheRange_RAM_def branchFlushRange_def invalidateCacheRange_I_def
lemma do_flush_respects[wp]:
"\<lbrace>integrity aag X st\<rbrace> do_machine_op (do_flush typ start end pstart)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (cases "typ")
apply (wp dmo_no_mem_respects | simp add: do_flush_def cache_machine_op_defs do_flush_defs)+
done
crunch pspace_aligned[wp]: flush_page "pspace_aligned"
lemma invalidate_tlb_by_asid_respects[wp]:
"\<lbrace>integrity aag X st\<rbrace> invalidate_tlb_by_asid asid
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: invalidate_tlb_by_asid_def)
apply (wp dmo_no_mem_respects | wpc | simp add: invalidateTLB_ASID_def )+
done
lemma invalidate_tlb_by_asid_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
by (wp dmo_no_mem_respects | wpc | simp add: invalidate_tlb_by_asid_def invalidateTLB_ASID_def)+
crunch pas_refined[wp]: set_message_info "pas_refined aag"
(* FIXME: move *)
lemma set_message_info_mdb[wp]:
"\<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_message_info thread info \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>"
unfolding set_message_info_def by wp
crunch state_vrefs[wp]: do_machine_op "\<lambda>s::'z::state_ext state. P (state_vrefs s)"
crunch thread_states[wp]: do_machine_op "\<lambda>s. P (thread_states s)"
(* FIXME: move *)
lemma set_mrs_state_vrefs[wp]:
"\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>"
apply (simp add: set_mrs_def split_def set_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
| wpc
| simp split del: split_if add: zipWithM_x_mapM_x split_def store_word_offs_def)+
apply (auto simp: obj_at_def state_vrefs_def get_tcb_ko_at
elim!: rsubst[where P=P, OF _ ext]
split: split_if_asm simp: vs_refs_no_global_pts_def)
done
(* FIXME: move *)
lemma set_mrs_thread_states[wp]:
"\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>"
apply (simp add: set_mrs_def split_def set_object_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp'
| wpc
| simp split del: split_if add: zipWithM_x_mapM_x split_def store_word_offs_def)+
apply (clarsimp simp: fun_upd_def[symmetric] thread_states_preserved)
done
lemma set_mrs_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: pas_refined_def state_objs_to_policy_def)
apply (rule hoare_pre)
apply (wp | wps)+
apply (clarsimp dest!: auth_graph_map_memD)
done
crunch integrity_autarch: set_message_info "integrity aag X st"
lemma storeWord_respects:
"\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (\<forall>p' \<in> ptr_range p 2. aag_has_auth_to aag Write p')\<rbrace> storeWord p v \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>"
unfolding storeWord_def
apply wp
apply (auto simp: integrity_def is_aligned_mask [symmetric] intro!: trm_write ptr_range_memI ptr_range_add_memI)
done
lemma dmo_storeWord_respects_Write:
"\<lbrace>integrity aag X st and K (\<forall>p' \<in> ptr_range p 2. aag_has_auth_to aag Write p')\<rbrace>
do_machine_op (storeWord p v)
\<lbrace>\<lambda>a. integrity aag X st\<rbrace>"
apply (rule hoare_pre)
apply (wp dmo_wp storeWord_respects)
apply simp
done
(* c.f. auth_ipc_buffers *)
definition
ipc_buffer_has_auth :: "'a PAS \<Rightarrow> word32 \<Rightarrow> word32 option \<Rightarrow> bool"
where
"ipc_buffer_has_auth aag thread \<equiv>
case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits \<and> (\<forall>x \<in> ptr_range buf' msg_align_bits. (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag))"
lemma ipc_buffer_has_auth_wordE:
"\<lbrakk> ipc_buffer_has_auth aag thread (Some buf); p \<in> ptr_range (buf + off) sz; is_aligned off sz; sz \<le> msg_align_bits; off < 2 ^ msg_align_bits \<rbrakk>
\<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag p) \<in> pasPolicy aag"
unfolding ipc_buffer_has_auth_def
apply clarsimp
apply (erule bspec)
apply (erule (4) set_mp [OF ptr_range_subset])
done
lemma is_aligned_word_size_2 [simp]:
"is_aligned (p * of_nat word_size) 2"
unfolding word_size_def
by (simp add: is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv)
lemma mul_word_size_lt_msg_align_bits_ofnat:
"p < 2 ^ (msg_align_bits - 2) \<Longrightarrow> of_nat p * of_nat word_size < (2 :: word32) ^ msg_align_bits"
unfolding word_size_def
apply simp
apply (rule word_less_power_trans_ofnat [where k = 2, simplified])
apply (simp_all add: msg_align_bits word_bits_conv)
done
lemma store_word_offs_integrity_autarch:
"\<lbrace>integrity aag X st and K (is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> r < 2 ^ (msg_align_bits - 2))\<rbrace>
store_word_offs buf r v
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (simp add: store_word_offs_def)
apply (rule hoare_pre)
apply (wp dmo_storeWord_respects_Write)
apply clarsimp
apply (drule (1) ipc_buffer_has_auth_wordE)
apply simp
apply (simp add: msg_align_bits)
apply (erule mul_word_size_lt_msg_align_bits_ofnat)
apply simp
done
lemma set_mrs_integrity_autarch:
"\<lbrace>integrity aag X st and K (is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf)\<rbrace>
set_mrs thread buf msgs
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (rule hoare_gen_asm)
apply (simp add: set_mrs_def)
apply (wp gets_the_wp get_wp put_wp mapM_x_wp' store_word_offs_integrity_autarch [where aag = aag and thread = thread]
| wpc
| simp split del: split_if add: split_def zipWithM_x_mapM_x )+
apply (clarsimp elim!: in_set_zipE split: split_if_asm)
apply (rule order_le_less_trans [where y = msg_max_length])
apply (fastforce simp add: le_eq_less_or_eq)
apply (simp add: msg_max_length_def msg_align_bits)
apply simp
apply (wp set_object_integrity_autarch hoare_drop_imps hoare_vcg_all_lift)
apply simp
done
lemma perform_page_invocation_respects:
"\<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pi) and valid_page_inv pi and valid_arch_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace>
perform_page_invocation pi
\<lbrace>\<lambda>s. integrity aag X st\<rbrace>"
proof -
(* does not work as elim rule with clarsimp, which hammers Ball in concl. *)
have set_tl_subset_mp: "\<And>xs a. a \<in> set (tl xs) \<Longrightarrow> a \<in> set xs" by (case_tac xs,clarsimp+)
have hd_valid_slots:
"\<And>a xs s. valid_slots (Inl (a, xs)) s \<Longrightarrow> hd xs \<in> set xs"
"\<And>a xs s. valid_slots (Inr (a, xs)) s \<Longrightarrow> hd xs \<in> set xs"
by (simp_all add: valid_slots_def)
show ?thesis
apply (simp add: perform_page_invocation_def mapM_discarded swp_def
valid_page_inv_def valid_unmap_def
authorised_page_inv_def authorised_slots_def
split: ArchInvocation_A.page_invocation.split sum.split
arch_cap.split option.split,
safe)
apply (wp set_cap_integrity_autarch unmap_page_respects
mapM_x_and_const_wp[OF store_pte_respects] store_pte_respects
mapM_x_and_const_wp[OF store_pde_respects] store_pde_respects
| elim conjE hd_valid_slots[THEN bspec[rotated]]
| clarsimp dest!:set_tl_subset_mp
| wpc )+
apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_diminished_def
cap_auth_conferred_def cap_rights_update_def
acap_rights_update_def update_map_data_def is_pg_cap_def
valid_page_inv_def valid_cap_simps
dest!: diminished_PageCapD cap_master_cap_eqDs)
apply (drule (1) clas_caps_of_state)
apply (simp add: cap_links_asid_slot_def label_owns_asid_slot_def)
apply (auto dest: pas_refined_Control)[1]
apply (wp set_mrs_integrity_autarch set_message_info_integrity_autarch | simp add: ipc_buffer_has_auth_def)+
done
qed
lemma perform_page_invocation_pas_refined [wp]:
"\<lbrace>pas_refined aag and K (authorised_page_inv aag pi) and valid_page_inv pi\<rbrace>
perform_page_invocation pi
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: perform_page_invocation_def mapM_discarded
valid_page_inv_def valid_unmap_def swp_def
authorised_page_inv_def authorised_slots_def
cong: ArchInvocation_A.page_invocation.case_cong sum.case_cong)
apply (rule hoare_pre)
apply wpc
apply (wp set_cap_pas_refined unmap_page_pas_refined case_sum_wp case_prod_wp
mapM_x_and_const_wp [OF store_pte_pas_refined] mapM_x_and_const_wp [OF store_pde_pas_refined]
hoare_vcg_all_lift hoare_vcg_const_imp_lift get_cap_wp
| (wp hoare_vcg_imp_lift, unfold disj_not1)
| strengthen clas_update_map_data_strg
| wpc
| simp)+
apply (case_tac pi)
apply (clarsimp simp: valid_slots_def pte_ref_def
pde_ref2_def auth_graph_map_mem pas_refined_refl split:sum.splits)
apply (clarsimp simp: pte_ref_def pde_ref2_def pte_ref_def
valid_slots_def auth_graph_map_mem pas_refined_refl split:sum.splits)
apply (clarsimp simp: cte_wp_at_caps_of_state
is_arch_diminished_def pte_ref_def pde_ref2_def
is_cap_simps is_pg_cap_def cap_auth_conferred_def
dest!: diminished_PageCapD)
apply (frule(1) cap_cur_auth_caps_of_state,simp)
apply (((rule conjI, rule impI)+)?, clarsimp,
clarsimp simp: update_map_data_def clas_no_asid aag_cap_auth_def
cap_auth_conferred_def vspace_cap_rights_to_auth_def
cli_no_irqs is_pg_cap_def pte_ref_def
[simplified aag_cap_auth_def])+
done
definition
authorised_asid_control_inv :: "'a PAS \<Rightarrow> asid_control_invocation \<Rightarrow> bool"
where
"authorised_asid_control_inv aag aci \<equiv> case aci of
asid_control_invocation.MakePool frame slot parent base \<Rightarrow>
is_subject aag (fst slot) \<and> is_aligned frame pageBits \<and> (\<forall>asid. is_subject_asid aag asid) \<and> is_subject aag (fst parent) \<and>
(\<forall>x \<in> {frame..frame + 2 ^ pageBits - 1}. is_subject aag x)"
lemma integrity_arm_asid_table_entry_update':
"\<lbrakk>integrity aag X st s; asid_table = arm_asid_table (arch_state s);
(\<forall>asid'.
asid' \<noteq> 0 \<and>
asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow>
is_subject_asid aag asid')\<rbrakk> \<Longrightarrow>
integrity aag X st
(s\<lparr>arch_state := arch_state s
\<lparr>arm_asid_table :=
\<lambda>a. if a = asid_high_bits_of asid then v
else asid_table a\<rparr>\<rparr>)"
apply(clarsimp simp: integrity_def integrity_asids_def)
done
lemma arm_asid_table_entry_update_integrity[wp]:
"\<lbrace>integrity aag X st and (\<lambda> s. asid_table = arm_asid_table (arch_state s)) and K (\<forall>asid'.
asid' \<noteq> 0 \<and>
asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow>
is_subject_asid aag asid')\<rbrace>
modify
(\<lambda>s. s\<lparr>arch_state := arch_state s
\<lparr>arm_asid_table := asid_table
(asid_high_bits_of asid := v)\<rparr>\<rparr>)
\<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (wp| simp)+
apply (blast intro: integrity_arm_asid_table_entry_update')
done
lemma perform_asid_control_invocation_respects:
"\<lbrace>integrity aag X st and K (authorised_asid_control_inv aag aci)\<rbrace>
perform_asid_control_invocation aci
\<lbrace>\<lambda>s. integrity aag X st\<rbrace>"
apply (simp add: perform_asid_control_invocation_def)
apply (rule hoare_pre)
apply (wpc, simp)
apply (wp set_cap_integrity_autarch cap_insert_integrity_autarch retype_region_integrity[where sz=12] static_imp_wp | simp)+
apply (clarsimp simp: authorised_asid_control_inv_def
ptr_range_def pageBits_def word_bits_def page_bits_def
is_aligned_neg_mask_eq add.commute
range_cover_def obj_bits_api_def default_arch_object_def
pageBits_def word_bits_def)
apply(subst is_aligned_neg_mask_eq[THEN sym], assumption)
apply(simp add: mask_neg_mask_is_zero)
done
lemma pas_refined_cdt:
"\<lbrakk> cdt s slot' = Some slot; pas_refined aag s \<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst slot), Control, pasObjectAbs aag (fst slot')) \<in> pasPolicy aag"
unfolding pas_refined_def
apply (drule sta_cdt)
apply (fastforce simp add: auth_graph_map_def)
done
lemma pas_refined_set_asid_strg:
"pas_refined aag s \<and> is_subject aag pool \<and> (\<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid)
\<longrightarrow>
pas_refined aag (s\<lparr>arch_state := arch_state s \<lparr>arm_asid_table := (arm_asid_table (arch_state s))(base \<mapsto> pool)\<rparr>\<rparr>)"
apply (clarsimp simp: pas_refined_def state_objs_to_policy_def)
apply (erule state_asids_to_policy_aux.cases, simp_all split: split_if_asm)
apply (auto intro: state_asids_to_policy_aux.intros auth_graph_map_memI[OF sbta_vref] pas_refined_refl[simplified pas_refined_def state_objs_to_policy_def])
done
(* FIXME: copied from Machine_R. *)
lemma ef_storeWord: "empty_fail (storeWord x y)"
by (simp add: storeWord_def)
lemma empty_fail_clearMemory [intro!]:
"\<And>a b. empty_fail (clearMemory a b)"
by (simp add: clearMemory_def mapM_x_mapM ef_storeWord)
(* FIXME: copied from Detype_R. *)
lemma gets_modify_comm2:
"\<forall>s. g (f s) = g s \<Longrightarrow>
(do x \<leftarrow> modify f; y \<leftarrow> gets g; m x y od) =
(do y \<leftarrow> gets g; x \<leftarrow> modify f; m x y od)"
apply (rule ext)
apply (drule spec)
by (rule gets_modify_comm)
lemma dmo_detype_comm:
assumes "empty_fail f"
shows "do_machine_op f >>= (\<lambda>s. modify (detype S)) =
modify (detype S) >>= (\<lambda>s. do_machine_op f)"
proof -
have machine_state_detype: "\<forall>s. machine_state (detype S s) = machine_state s"
by (simp add: detype_def)
have detype_msu_independent:
"\<And>f. detype S \<circ> machine_state_update f = machine_state_update f \<circ> detype S"
by (simp add: detype_def ext)
from assms
show ?thesis
apply (simp add: do_machine_op_def split_def bind_assoc)
apply (simp add: gets_modify_comm2[OF machine_state_detype])
apply (rule arg_cong2[where f=bind, OF refl], rule ext)
apply (simp add: empty_fail_def select_f_walk[OF empty_fail_modify]
modify_modify detype_msu_independent)
done
qed
(* FIXME: copied from Detype_R. *)
lemma empty_fail_freeMemory: "empty_fail (freeMemory ptr bits)"
by (simp add: freeMemory_def mapM_x_mapM ef_storeWord)
(* FIXME: copied from Detype_R. *)
lemma delete_objects_def2:
"delete_objects ptr bits \<equiv>
do modify (detype {ptr..ptr + 2 ^ bits - 1});
do_machine_op (freeMemory ptr bits)
od"
by (rule eq_reflection)
(simp add: delete_objects_def dmo_detype_comm[OF empty_fail_freeMemory])
lemma delete_objects_pas_refined[wp]:
"\<lbrace>pas_refined aag\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (rule hoare_pre)
apply (simp add: delete_objects_def2)
apply wp
apply (erule pas_refined_detype)
done
lemma delete_objects_pspace_no_overlap:
"\<lbrace> pspace_aligned and valid_objs and
(\<lambda> s. \<exists> idx. cte_wp_at (op = (UntypedCap ptr sz idx)) slot s)\<rbrace>
delete_objects ptr sz
\<lbrace>\<lambda>rv. pspace_no_overlap ptr sz\<rbrace>"
unfolding delete_objects_def do_machine_op_def
apply(wp | simp add: split_def detype_msu_comm)+
apply(clarsimp)
apply(rule pspace_no_overlap_detype)
apply(auto dest: cte_wp_at_valid_objs_valid_cap)
done
lemma delete_objects_invs_ex:
"\<lbrace>(\<lambda>s. \<exists>slot f.
cte_wp_at (op = (UntypedCap ptr bits f)) slot s \<and>
descendants_range (UntypedCap ptr bits f) slot s) and
invs and
ct_active\<rbrace>
delete_objects ptr bits \<lbrace>\<lambda>_. invs\<rbrace>"
apply(clarsimp simp: valid_def)
apply(erule use_valid)
apply wp
apply auto
done
lemma perform_asid_control_invocation_pas_refined [wp]:
notes delete_objects_invs[wp del]
shows
"\<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and
K (authorised_asid_control_inv aag aci)\<rbrace>
perform_asid_control_invocation aci
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: perform_asid_control_invocation_def)
apply (rule hoare_pre)
apply (wp cap_insert_pas_refined static_imp_wp
| strengthen pas_refined_set_asid_strg
| wpc
| simp add: delete_objects_def2 fun_upd_def[symmetric])+
apply (wp retype_region_pas_refined'[where sz=pageBits]
max_index_upd_invs_simple max_index_upd_caps_overlap_reserved
hoare_vcg_ex_lift set_cap_cte_wp_at hoare_vcg_disj_lift
set_cap_descendants_range_in set_cap_no_overlap get_cap_wp
hoare_vcg_all_lift static_imp_wp
| simp add: do_machine_op_def split_def)+
apply(rename_tac word1 prod1 prod2 word2 cap)
apply(rule_tac Q="\<lambda> rv s. (\<exists> idx. cte_wp_at (op = (UntypedCap word1 pageBits idx)) prod2 s) \<and>
(\<forall> x\<in>ptr_range word1 pageBits. is_subject aag x) \<and>
pas_refined aag s \<and>
pas_cur_domain aag s \<and>
pspace_no_overlap word1 pageBits s \<and>
invs s \<and>
descendants_range_in
{word1..(word1 && ~~ mask pageBits) + 2 ^ pageBits - 1} prod2
s \<and>
range_cover word1 pageBits
(obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and>
is_subject aag (fst prod1) \<and>
is_subject aag (fst prod2) \<and>
pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap word1 word2)) \<and>
is_subject aag word1 \<and>
(\<forall>x. asid_high_bits_of x = asid_high_bits_of word2 \<longrightarrow>
is_subject_asid aag x)" in hoare_strengthen_post)
apply (wp delete_objects_pspace_no_overlap hoare_vcg_ex_lift
delete_objects_descendants_range_in delete_objects_invs_ex
| simp add: page_bits_def)+
apply clarsimp
apply (frule untyped_cap_aligned, simp add: invs_valid_objs)
apply (fastforce simp: cte_wp_at_def aag_cap_auth_def ptr_range_def pas_refined_refl cap_links_asid_slot_def cap_links_irq_def is_aligned_neg_mask_eq obj_bits_api_def default_arch_object_def retype_addrs_def)
apply (clarsimp simp: valid_aci_def authorised_asid_control_inv_def)
apply (subgoal_tac "is_aligned x pageBits")
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (rule conjI)
apply(drule untyped_slots_not_in_untyped_range)
apply(erule empty_descendants_range_in)
apply(simp add: cte_wp_at_caps_of_state)
apply simp
apply(rule refl)
apply(rule subset_refl)
apply(simp add: page_bits_def)
apply(clarsimp simp: ptr_range_def invs_psp_aligned invs_valid_objs)
apply(rule conjI, fastforce)
apply(rule conjI)
apply(fastforce simp: descendants_range_def2 elim!: empty_descendants_range_in)
apply(rule conjI)
apply(fastforce simp: descendants_range_def2 elim!: empty_descendants_range_in)
apply(rule conjI)
apply(clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def)
apply(subst is_aligned_neg_mask_eq[THEN sym], assumption)
apply(simp add: mask_neg_mask_is_zero pageBits_def)
apply(clarsimp simp: aag_cap_auth_def pas_refined_refl)
apply(drule_tac x=x in bspec)
apply(simp add: is_aligned_no_overflow)
apply(clarsimp simp: pas_refined_refl cap_links_asid_slot_def label_owns_asid_slot_def cap_links_irq_def)
apply(fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def)
done
lemma set_asid_pool_respects:
"\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace>
set_asid_pool ptr pool
\<lbrace>\<lambda>s. integrity aag X st\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp get_object_wp set_object_integrity_autarch)
apply simp
done
definition
authorised_asid_pool_inv :: "'a PAS \<Rightarrow> asid_pool_invocation \<Rightarrow> bool"
where
"authorised_asid_pool_inv aag api \<equiv> case api of
asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow>
is_subject aag pool_ptr \<and> is_subject aag (fst ct_slot)
\<and> asid \<noteq> 0
\<and> (\<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of asid \<and> asid' \<noteq> 0
\<longrightarrow> is_subject_asid aag asid')"
lemma perform_asid_pool_invocation_respects:
"\<lbrace>integrity aag X st and K (authorised_asid_pool_inv aag api)\<rbrace>
perform_asid_pool_invocation api
\<lbrace>\<lambda>s. integrity aag X st\<rbrace>"
apply (simp add: perform_asid_pool_invocation_def)
apply (rule hoare_pre)
apply (wp set_asid_pool_respects get_cap_wp get_cap_integrity_autarch set_cap_integrity_autarch
| wpc
| simp)+
apply (auto iff: authorised_asid_pool_inv_def)
done
lemma is_subject_asid_into_loas:
"\<lbrakk> is_subject_asid aag asid; pas_refined aag s \<rbrakk> \<Longrightarrow> label_owns_asid_slot aag (pasSubject aag) asid"
unfolding label_owns_asid_slot_def
by (clarsimp simp: pas_refined_refl)
lemma asid_pool_into_aag:
"\<lbrakk>kheap s p = Some (ArchObj (arch_kernel_obj.ASIDPool pool)); pool r = Some p'; pas_refined aag s \<rbrakk>
\<Longrightarrow> (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag"
apply (rule pas_refined_mem [rotated], assumption)
apply (rule sta_vref)
apply (fastforce simp add: state_vrefs_def vs_refs_no_global_pts_def intro!: graph_ofI)
done
lemma asid_pool_uniqueness:
"\<lbrakk> ([VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p) s;
arm_asid_table (arch_state s) (asid_high_bits_of asid') = Some p;
invs s; \<forall>pt. \<not> ko_at (ArchObj (PageTable pt)) p s \<rbrakk>
\<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid"
apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp)
apply (drule vs_lookup_atI, drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp)
apply (clarsimp dest!: obj_ref_elemD)
apply (drule(1) unique_table_refsD[where cps="caps_of_state s", rotated])
apply simp
apply (clarsimp simp: vs_cap_ref_def table_cap_ref_def up_ucast_inj_eq
split: vmpage_size.splits option.splits cap.splits arch_cap.splits)+
done
lemma perform_asid_pool_invocation_pas_refined [wp]:
"\<lbrace>pas_refined aag and invs and valid_apinv api and K (authorised_asid_pool_inv aag api)\<rbrace>
perform_asid_pool_invocation api
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
apply (simp add: perform_asid_pool_invocation_def)
apply (rule hoare_pre)
apply (wp get_cap_auth_wp [where aag = aag] | wpc)+
apply (clarsimp simp: authorised_asid_pool_inv_def cap_links_asid_slot_def is_subject_asid_into_loas aag_cap_auth_def)
apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def auth_graph_map_mem
pas_refined_all_auth_is_owns pas_refined_refl cli_no_irqs
dest!: graph_ofD)
apply (clarsimp split: split_if_asm)
apply (clarsimp simp add: pas_refined_refl auth_graph_map_def2
mask_asid_low_bits_ucast_ucast[symmetric]
valid_apinv_def obj_at_def)
apply (drule(2) asid_pool_uniqueness)
apply (simp add: obj_at_def)
apply (case_tac "asid = 0", simp_all add: pas_refined_refl)[1]
apply (simp add: asid_low_high_bits[rotated, OF arg_cong[where f=ucast]])
apply (clarsimp simp: obj_at_def)
apply (frule (2) asid_pool_into_aag)
apply (drule kheap_eq_state_vrefsD)
apply (clarsimp simp: auth_graph_map_def2 pas_refined_refl)
apply (clarsimp simp: pas_refined_def vs_refs_no_global_pts_def)
apply (erule subsetD, erule state_asids_to_policy_aux.intros,
simp add: split_def, rule image_eqI[rotated], erule graph_ofI)
apply simp
done