forked from seL4/l4v
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathAccess_AC.thy
1594 lines (1322 loc) · 68.4 KB
/
Access_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 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory Access_AC
imports Access
begin
section\<open>Generic AC proofs\<close>
lemma aag_wellformed_Control:
"\<lbrakk> (x, Control, y) \<in> aag; policy_wellformed aag mirqs irqs x \<rbrakk> \<Longrightarrow> x = y"
unfolding policy_wellformed_def by metis
lemma aag_wellformed_refl:
"\<lbrakk> policy_wellformed aag mirqs irqs x \<rbrakk> \<Longrightarrow> (x, a, x) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_grant_Control_to_recv:
"\<lbrakk> (s, Grant, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (s, Control, r) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_grant_Control_to_send:
"\<lbrakk> (s, Grant, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (r, Control, s) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_reply:
"\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (r, Reply, s) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_delete_derived':
"\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (s, DeleteDerived, r) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_delete_derived:
"\<lbrakk> (s, Reply, r) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (r, DeleteDerived, s) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_delete_derived_trans:
"\<lbrakk> (l1, DeleteDerived, l2) \<in> aag; (l2, DeleteDerived, l3) \<in> aag;
policy_wellformed aag mirqs irqs l\<rbrakk>
\<Longrightarrow> (l1, DeleteDerived, l3) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_call_to_syncsend:
"\<lbrakk> (s, Call, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (s, SyncSend, ep) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_grant_Control_to_send_by_reply:
"\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag;
(r, Grant, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (r, Control, s) \<in> aag"
unfolding policy_wellformed_def by blast
lemma aag_wellformed_grant_Control_to_recv_by_reply:
"\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag;
(r, Grant, ep) \<in> aag; policy_wellformed aag mirqs irqs l \<rbrakk>
\<Longrightarrow> (s, Control, r) \<in> aag"
unfolding policy_wellformed_def by blast
lemma auth_graph_map_mem:
"(x, auth, y) \<in> auth_graph_map f S = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> (x', auth, y') \<in> S)"
by (simp add: auth_graph_map_def)
lemmas auth_graph_map_memD = auth_graph_map_mem[THEN iffD1]
lemma auth_graph_map_memE:
assumes hyp: "(x, auth, y) \<in> auth_graph_map f S"
obtains x' and y' where "x = f x'" and "y = f y'" and "(x', auth, y') \<in> S"
using hyp[THEN auth_graph_map_mem[THEN iffD1]] by fastforce
lemma auth_graph_map_memI:
"\<lbrakk> (x', auth, y') \<in> S; x = f x'; y = f y' \<rbrakk>
\<Longrightarrow> (x, auth, y) \<in> auth_graph_map f S"
by (fastforce simp add: auth_graph_map_mem)
lemma auth_graph_map_mono:
"S \<subseteq> S' \<Longrightarrow> auth_graph_map G S \<subseteq> auth_graph_map G S'"
unfolding auth_graph_map_def by auto
lemma is_transferable_capE:
assumes hyp:"is_transferable_cap cap"
obtains "cap = NullCap" | t R where "cap = ReplyCap t False R"
by (rule is_transferable.cases[OF hyp]) auto
lemma is_transferable_None[simp]: "is_transferable None"
using is_transferable.simps by simp
lemma is_transferable_Null[simp]: "is_transferable_cap NullCap"
using is_transferable.simps by simp
lemma is_transferable_Reply[simp]: "is_transferable_cap (ReplyCap t False R)"
using is_transferable.simps by simp
lemma is_transferable_NoneE:
assumes hyp: "is_transferable opt_cap"
obtains "opt_cap = None" | cap where "opt_cap = Some cap" and "is_transferable_cap cap"
by (rule is_transferable.cases[OF hyp];simp)
lemma is_transferable_Untyped[simp]: "\<not> is_transferable (Some (UntypedCap dev ptr sz freeIndex))"
by (blast elim: is_transferable.cases)
lemma is_transferable_IRQ[simp]: "\<not> is_transferable_cap IRQControlCap"
by (blast elim: is_transferable.cases)
lemma is_transferable_Zombie[simp]: "\<not> is_transferable (Some (Zombie ptr sz n))"
by (blast elim: is_transferable.cases)
lemma is_transferable_Ntfn[simp]: "\<not> is_transferable (Some (NotificationCap ntfn badge R))"
by (blast elim: is_transferable.cases)
lemma is_transferable_Endpoint[simp]: "\<not> is_transferable (Some (EndpointCap ntfn badge R))"
by (blast elim: is_transferable.cases)
(* FIXME MOVE *)
lemmas descendants_incD = descendants_inc_def[THEN meta_eq_to_obj_eq, THEN iffD1, rule_format]
(* FIXME MOVE *)
lemmas all_childrenI = all_children_def[THEN meta_eq_to_obj_eq, THEN iffD2, rule_format]
lemmas all_childrenD = all_children_def[THEN meta_eq_to_obj_eq, THEN iffD1, rule_format]
(* FIXME MOVE *)
lemma valid_mdb_descendants_inc[elim!]:
"valid_mdb s \<Longrightarrow> descendants_inc (cdt s) (caps_of_state s)"
by (simp add:valid_mdb_def)
(* FIXME MOVE *)
lemma valid_mdb_mdb_cte_at [elim!]:
"valid_mdb s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)"
by (simp add:valid_mdb_def)
(* FIXME MOVE *)
lemma descendants_inc_cap_classD:
"\<lbrakk> descendants_inc m caps; p \<in> descendants_of p' m; caps p = Some cap ; caps p' = Some cap' \<rbrakk>
\<Longrightarrow> cap_class cap = cap_class cap'"
by (fastforce dest:descendants_incD)
locale Access_AC_1 =
fixes aag :: "'a PAS"
and user_monad_t :: "'b user_monad"
assumes acap_class_reply:
"acap_class acap \<noteq> ReplyClass t"
and arch_troa_tro_alt[elim!]:
"arch_integrity_obj_atomic aag subjects l ko ko'
\<Longrightarrow> arch_integrity_obj_alt aag subjects l ko ko'"
and arch_tro_alt_trans_spec:
"\<lbrakk> arch_integrity_obj_alt aag subjects l ko ko';
arch_integrity_obj_alt aag subjects l ko' ko'' \<rbrakk>
\<Longrightarrow> arch_integrity_obj_alt aag subjects l ko ko''"
and clas_caps_of_state:
"\<lbrakk> caps_of_state s slot = Some cap; pas_refined aag s \<rbrakk>
\<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst slot)) cap"
begin
lemma cap_class_reply:
"(cap_class cap = ReplyClass t) = (\<exists>r m. cap = ReplyCap t m r)"
by (cases cap; simp add: acap_class_reply)
lemma reply_cap_no_children:
"\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk> \<Longrightarrow> cdt s p' \<noteq> Some p"
apply (clarsimp simp: valid_mdb_def)
apply (frule descendants_incD[where p=p' and p'=p])
apply (rule child_descendant)
apply (fastforce)
apply clarsimp
apply (subgoal_tac "caps_of_state s p' \<noteq> None")
apply (clarsimp simp: cap_class_reply)
apply (simp only: reply_mdb_def reply_caps_mdb_def reply_masters_mdb_def)
apply (elim conjE allE[where x=p'])
apply simp
apply (drule(1) mdb_cte_atD)
apply (fastforce simp add: cte_wp_at_def caps_of_state_def)
done
lemma is_transferable_all_children:
"valid_mdb s \<Longrightarrow> all_children (\<lambda>slot . is_transferable (caps_of_state s slot)) (cdt s)"
apply (rule all_childrenI)
apply (erule is_transferable.cases)
apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at
simp: mdb_cte_at_def cte_wp_at_def caps_of_state_def)
apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at
simp: mdb_cte_at_def cte_wp_at_def caps_of_state_def)
apply (blast dest: reply_cap_no_children)
done
end
lemmas state_objs_to_policy_mem = eqset_imp_iff[OF state_objs_to_policy_def]
lemmas state_objs_to_policy_intros
= state_bits_to_policy.intros[THEN state_objs_to_policy_mem[THEN iffD2]]
(* FIXME: brittle when adding rules to or removing rules from state_bits_to_policy *)
lemmas sta_caps = state_objs_to_policy_intros(1)
and sta_untyped = state_objs_to_policy_intros(2)
and sta_ts = state_objs_to_policy_intros(3)
and sta_bas = state_objs_to_policy_intros(4)
and sta_cdt = state_objs_to_policy_intros(5)
and sta_cdt_transferable = state_objs_to_policy_intros(6)
and sta_vref = state_objs_to_policy_intros(7)
lemmas state_objs_to_policy_cases
= state_bits_to_policy.cases[OF state_objs_to_policy_mem[THEN iffD1]]
lemma tcb_states_of_state_preserved:
"\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk>
\<Longrightarrow> tcb_states_of_state (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = tcb_states_of_state s"
by (auto split: option.splits simp: tcb_states_of_state_def get_tcb_def)
lemma thread_st_auth_preserved:
"\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk>
\<Longrightarrow> thread_st_auth (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = thread_st_auth s"
by (simp add: tcb_states_of_state_preserved thread_st_auth_def)
lemma thread_bound_ntfns_preserved:
"\<lbrakk> get_tcb thread s = Some tcb; tcb_bound_notification tcb' = tcb_bound_notification tcb \<rbrakk>
\<Longrightarrow> thread_bound_ntfns (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = thread_bound_ntfns s"
by (auto simp: thread_bound_ntfns_def get_tcb_def split: option.splits)
lemma is_transferable_null_filter[simp]:
"is_transferable (null_filter caps ptr) = is_transferable (caps ptr)"
by (auto simp: is_transferable.simps null_filter_def)
lemma tcb_domain_map_wellformed_mono:
"\<lbrakk> domains_of_state s' \<subseteq> domains_of_state s; tcb_domain_map_wellformed pas s \<rbrakk>
\<Longrightarrow> tcb_domain_map_wellformed pas s'"
by (auto simp: tcb_domain_map_wellformed_aux_def get_etcb_def)
lemma pas_refined_mem:
"\<lbrakk> (x, auth, y) \<in> state_objs_to_policy s; pas_refined aag s \<rbrakk>
\<Longrightarrow> abs_has_auth_to aag auth x y"
by (auto simp: pas_refined_def intro: auth_graph_map_memI)
lemma pas_refined_wellformed[elim!]:
"pas_refined aag s \<Longrightarrow> pas_wellformed aag"
unfolding pas_refined_def by simp
lemmas pas_refined_Control
= aag_wellformed_Control[OF _ pas_refined_wellformed]
and pas_refined_refl = aag_wellformed_refl [OF pas_refined_wellformed]
lemma caps_of_state_pasObjectAbs_eq:
"\<lbrakk> caps_of_state s p = Some cap; Control \<in> cap_auth_conferred cap;
is_subject aag (fst p); pas_refined aag s; x \<in> obj_refs cap \<rbrakk>
\<Longrightarrow> is_subject aag x"
apply (frule sta_caps, simp+)
apply (drule pas_refined_mem, simp+)
apply (drule pas_refined_Control, simp+)
done
lemma pas_refined_state_objs_to_policy_subset:
"\<lbrakk> pas_refined aag s;
state_objs_to_policy s' \<subseteq> state_objs_to_policy s;
state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s;
state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s;
domains_of_state s' \<subseteq> domains_of_state s;
interrupt_irq_node s' = interrupt_irq_node s \<rbrakk>
\<Longrightarrow> pas_refined aag s'"
by (simp add: pas_refined_def)
(blast dest: tcb_domain_map_wellformed_mono auth_graph_map_mono[where G="pasObjectAbs aag"])
lemma aag_wellformed_all_auth_is_owns':
"\<lbrakk> Control \<in> S; pas_wellformed aag \<rbrakk>
\<Longrightarrow> (\<forall>auth \<in> S. aag_has_auth_to aag auth x) = (is_subject aag x)"
by (fastforce simp: aag_wellformed_refl dest: aag_wellformed_Control)
lemmas aag_wellformed_all_auth_is_owns
= aag_wellformed_all_auth_is_owns'[where S=UNIV, simplified]
aag_wellformed_all_auth_is_owns'[where S="{Control}", simplified]
lemmas aag_wellformed_control_is_owns
= aag_wellformed_all_auth_is_owns'[where S="{Control}", simplified]
lemmas pas_refined_all_auth_is_owns = aag_wellformed_all_auth_is_owns[OF pas_refined_wellformed]
lemma pas_refined_sita_mem:
"\<lbrakk> (x, auth, y) \<in> state_irqs_to_policy aag s; pas_refined aag s \<rbrakk>
\<Longrightarrow> (x, auth, y) \<in> pasPolicy aag"
by (auto simp: pas_refined_def)
lemma receive_blocked_on_can_receive_ipc[elim!,simp]:
"receive_blocked_on ref ts \<Longrightarrow> can_receive_ipc ts"
by (cases ts; simp)
lemma receive_blocked_on_can_receive_ipc'[elim!,simp]:
"case_option False (receive_blocked_on ref) tsopt \<Longrightarrow> case_option False can_receive_ipc tsopt"
by (cases tsopt;simp)
lemma tcb_bound_notification_reset_integrity_refl[simp]:
"tcb_bound_notification_reset_integrity ntfn ntfn subjects aag"
by (simp add: tcb_bound_notification_reset_integrity_def)
lemma allowed_call_blocked_call_blocked[elim!]:
"allowed_call_blocked ep tst \<Longrightarrow> call_blocked ep tst"
unfolding allowed_call_blocked_def call_blocked_def by fastforce
lemmas reply_cap_deletion_integrityI1 =
reply_cap_deletion_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2,OF disjI1]
lemmas reply_cap_deletion_integrityI2 =
reply_cap_deletion_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2, OF disjI2, OF exI,
OF exI, OF conjI [OF _ conjI], rule_format]
lemmas reply_cap_deletion_integrity_intros =
reply_cap_deletion_integrityI1 reply_cap_deletion_integrityI2
lemma reply_cap_deletion_integrityE:
assumes hyp: "reply_cap_deletion_integrity subjects aag cap cap'"
obtains "cap = cap'" | caller R where "cap = ReplyCap caller False R"
and "cap' = NullCap" and "pasObjectAbs aag caller \<in> subjects"
using hyp reply_cap_deletion_integrity_def by blast
lemma reply_cap_deletion_integrity_refl[simp]:
"reply_cap_deletion_integrity subjects aag cap cap"
by (rule reply_cap_deletion_integrityI1) simp
lemmas cnode_integrityI = cnode_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2,rule_format]
lemmas cnode_integrityD = cnode_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD1,rule_format]
lemma cnode_integrityE:
assumes hyp:"cnode_integrity subjects aag content content'"
obtains "content l = content' l" | cap cap' where "content l = Some cap"
and "content' l = Some cap'" and "reply_cap_deletion_integrity subjects aag cap cap'"
using hyp cnode_integrityD by blast
subsubsection \<open>Introduction rules for object integrity\<close>
lemma troa_tro:
"integrity_obj_atomic aag activate subjects l ko ko'
\<Longrightarrow> integrity_obj aag activate subjects l ko ko'"
unfolding integrity_obj_def by (rule r_into_rtranclp)
lemmas tro_lrefl = troa_lrefl[THEN troa_tro]
lemma tro_orefl:
"ko = ko' \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'"
unfolding integrity_obj_def by simp
lemmas tro_ntfn = troa_ntfn[THEN troa_tro]
lemmas tro_ep = troa_ep[THEN troa_tro]
lemmas tro_ep_unblock = troa_ep_unblock[THEN troa_tro]
lemmas tro_tcb_send = troa_tcb_send[THEN troa_tro]
lemmas tro_tcb_call = troa_tcb_call[THEN troa_tro]
lemmas tro_tcb_reply = troa_tcb_reply[THEN troa_tro]
lemmas tro_tcb_receive = troa_tcb_receive[THEN troa_tro]
lemmas tro_tcb_restart = troa_tcb_restart[THEN troa_tro]
lemmas tro_tcb_unbind = troa_tcb_unbind[THEN troa_tro]
lemmas tro_tcb_empty_ctable = troa_tcb_empty_ctable[THEN troa_tro]
lemmas tro_tcb_empty_caller = troa_tcb_empty_caller[THEN troa_tro]
lemmas tro_tcb_activate = troa_tcb_activate[THEN troa_tro]
lemmas tro_arch = troa_arch[THEN troa_tro]
lemmas tro_cnode = troa_cnode[THEN troa_tro]
lemmas tro_intros = tro_lrefl tro_orefl tro_ntfn tro_ep tro_ep_unblock tro_tcb_send tro_tcb_call
tro_tcb_reply tro_tcb_receive tro_tcb_restart tro_tcb_unbind tro_tcb_empty_ctable
tro_tcb_empty_caller tro_tcb_activate tro_arch tro_cnode
lemma tro_tcb_unbind':
"\<lbrakk> ko = Some (TCB tcb); ko' = Some (TCB tcb');
tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>;
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag \<rbrakk>
\<Longrightarrow> integrity_obj aag activate subjects l' ko ko'"
apply (clarsimp simp:tcb_bound_notification_reset_integrity_def)
apply (elim disjE)
apply (rule tro_orefl;fastforce)
apply (rule tro_tcb_unbind;fastforce)
done
lemmas rtranclp_transp[intro!] = transp_rtranclp
lemma tro_transp[intro!]:
"transp (integrity_obj aag activate es subjects)"
unfolding integrity_obj_def by simp
lemmas tro_trans_spec = tro_transp[THEN transpD]
lemma tro_tcb_generic':
"\<lbrakk> ko = Some (TCB tcb); ko' = Some (TCB tcb');
tcb' = tcb \<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>;
tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag;
reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap';
reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap' \<rbrakk>
\<Longrightarrow> integrity_obj aag activate subjects l' ko ko'"
apply clarsimp
apply (rule tro_trans_spec)
apply (rule tro_tcb_empty_caller[OF refl refl refl];simp)
apply (rule tro_trans_spec)
apply (rule tro_tcb_empty_ctable[OF refl refl refl];simp)
apply (rule tro_trans_spec)
apply (rule tro_tcb_unbind'[OF refl refl refl];simp)
apply (fastforce intro!: tro_orefl tcb.equality)
done
lemma tro_tcb_reply':
"\<lbrakk> ko = Some (TCB tcb); ko' = Some (TCB tcb');
tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb),
tcb_state := new_st, tcb_fault := None\<rparr>;
new_st = Running \<or> (tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> new_st = Inactive));
direct_reply subjects aag l' tcb \<rbrakk>
\<Longrightarrow> integrity_obj aag activate subjects l' ko ko'"
apply (clarsimp simp:direct_reply_def simp del:not_None_eq)
apply (erule disjE, (rule tro_tcb_reply[OF refl refl], force; force)) (* Warning: schematics *)
apply (clarsimp simp del:not_None_eq)
apply (rule tro_trans_spec)
apply (frule allowed_call_blocked_def[THEN meta_eq_to_obj_eq,THEN iffD1],clarsimp)
apply (rule tro_tcb_receive[OF refl refl refl, where new_st=BlockedOnReply];force)
apply (rule tro_trans_spec)
apply (rule tro_tcb_reply[OF refl refl refl, where new_st=new_st];force)
by (fastforce intro!: tro_orefl tcb.equality)
context Access_AC_1 begin
lemma troa_tro_alt[elim!]:
"integrity_obj_atomic aag activate subjects l ko ko'
\<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'"
apply (erule integrity_obj_atomic.cases)
text \<open>Single out TCB cases for special handling. We manually simplify
the TCB updates in the tro_alt rules using @{thm tcb.equality}.\<close>
(* somewhat slow 10s *)
apply (find_goal \<open>match premises in "ko = Some (TCB _)" \<Rightarrow> succeed\<close>,
((erule(1) integrity_obj_alt.intros[OF tro_tagI],
(intro exI tcb.equality; solves \<open>simp\<close>));
fastforce simp: reply_cap_deletion_integrity_def direct_reply_def
tcb_bound_notification_reset_integrity_def))+
text \<open>Remaining cases.\<close>
apply (fastforce intro: integrity_obj_alt.intros[OF tro_tagI])+
done
end
lemma integrity_ready_queues_refl[simp]: "integrity_ready_queues aag subjects ptr s s"
unfolding integrity_ready_queues_def by simp
(* FIXME MOVE *)
lemma caps_of_state_tcb':
"\<lbrakk> get_tcb p s = Some tcb; option_map fst (tcb_cap_cases idx) = Some getF \<rbrakk>
\<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb)"
apply (drule get_tcb_SomeD)
apply clarsimp
apply (drule (1) cte_wp_at_tcbI [where t = "(p, idx)" and P = "(=) (getF tcb)", simplified])
apply simp
apply (clarsimp simp: cte_wp_at_caps_of_state)
done
(* FIXME MOVE *)
lemma caps_of_state_tcb_cap_cases:
"\<lbrakk> get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases \<rbrakk>
\<Longrightarrow> caps_of_state s (p, idx) = Some ((the (option_map fst (tcb_cap_cases idx))) tcb)"
apply (clarsimp simp: dom_def)
apply (erule caps_of_state_tcb')
apply simp
done
lemmas integrity_obj_simps [simp] =
tro_orefl[OF refl]
tro_lrefl[OF singletonI]
trm_orefl[OF refl]
trd_orefl[OF refl]
tre_lrefl[OF singletonI]
tre_orefl[OF refl]
lemma cdt_change_allowedI:
"\<lbrakk> m \<Turnstile> pptr \<rightarrow>* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr \<rbrakk>
\<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr"
by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex)
lemma cdt_change_allowedE:
assumes "cdt_change_allowed aag subjects m tcbsts ptr"
obtains pptr where "m \<Turnstile> pptr \<rightarrow>* ptr" "cdt_direct_change_allowed aag subjects tcbsts pptr"
using assms by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex)
lemma cdca_ccaI:
"\<lbrakk> cdt_direct_change_allowed aag subjects tcbsts ptr \<rbrakk>
\<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr"
by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex)
lemmas cca_owned = cdt_change_allowedI[OF _ cdca_owned]
lemmas cca_reply' = cdt_change_allowedI[OF _ cdca_owned]
lemmas cca_direct[intro] = cdca_ccaI[OF cdca_owned]
lemmas cca_reply = cdca_ccaI[OF cdca_reply]
lemma cca_direct_single[intro]:
"is_subject aag (fst ptr) \<Longrightarrow> cdt_change_allowed aag {pasSubject aag} m kh ptr"
by (rule cca_direct) blast
lemma integrity_cdtE:
assumes hyp:"integrity_cdt aag subjects m tcbsts ptr v v'"
obtains "v = v'" | "cdt_change_allowed aag subjects m tcbsts ptr"
using hyp integrity_cdt_def by blast
lemma integrity_cdt_refl[simp]: "integrity_cdt aag subjects m kh ptr v v"
by (simp add: integrity_cdt_def)
lemma integrity_cdt_change_allowed[simp,intro]:
"cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt aag subjects m kh ptr v v'"
by (simp add: integrity_cdt_def)
lemmas integrity_cdt_intros = integrity_cdt_refl integrity_cdt_change_allowed
lemmas integrity_cdt_direct = cca_direct[THEN integrity_cdt_change_allowed]
lemma integrity_cdt_list_refl[simp]: "integrity_cdt_list aag subjects m kh ptr v v"
by (simp add: integrity_cdt_list_def)
lemma integrity_cdt_list_filt:
"filtered_eq (cdt_change_allowed aag subjects m kh) l l'
\<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'"
by (simp add: integrity_cdt_list_def)
lemma integrity_cdt_list_change_allowed:
"cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'"
by (simp add: integrity_cdt_list_def)
lemmas integrity_cdt_list_intros = integrity_cdt_list_filt integrity_cdt_list_change_allowed
lemma integrity_cdt_listE:
assumes hyp:"integrity_cdt_list aag subjects m kh ptr l l'"
obtains "filtered_eq (cdt_change_allowed aag subjects m kh) l l'" |
"cdt_change_allowed aag subjects m kh ptr"
using hyp integrity_cdt_list_def by blast
lemma integrity_interrupts_refl[simp]: "integrity_interrupts aag subjects ptr v v"
by (simp add: integrity_interrupts_def)
section \<open>Integrity transitivity\<close>
subsection \<open>Object integrity transitivity\<close>
lemma tcb_bound_notification_reset_integrity_trans[elim]:
"\<lbrakk> tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag;
tcb_bound_notification_reset_integrity ntfn' ntfn'' subjects aag \<rbrakk>
\<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn'' subjects aag"
by (auto simp: tcb_bound_notification_reset_integrity_def)
lemma reply_cap_deletion_integrity_trans[elim]:
"\<lbrakk> reply_cap_deletion_integrity subjects aag cap cap';
reply_cap_deletion_integrity subjects aag cap' cap'' \<rbrakk>
\<Longrightarrow> reply_cap_deletion_integrity subjects aag cap cap''"
by (auto simp: reply_cap_deletion_integrity_def)
lemma cnode_integrity_trans[elim]:
"\<lbrakk> cnode_integrity subjects aag cont cont';
cnode_integrity subjects aag cont' cont'' \<rbrakk>
\<Longrightarrow> cnode_integrity subjects aag cont cont''"
unfolding cnode_integrity_def
apply (intro allI)
apply (drule_tac x=l in spec)+
by fastforce
lemma tcb_bound_notification_reset_eq_or_none:
"tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag \<Longrightarrow> ntfn = ntfn' \<or> ntfn' = None"
by (auto simp: tcb_bound_notification_reset_integrity_def)
context Access_AC_1 begin
lemma tro_alt_trans_spec: (* this takes a long time to process *)
"\<lbrakk> integrity_obj_alt aag activate es subjects ko ko';
integrity_obj_alt aag activate es subjects ko' ko'' \<rbrakk>
\<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko''"
(* We need to consider nearly 200 cases, one for each possible pair
of integrity steps. We use the tro_tags to select subsets of goals
that can be solved by the same method. *)
(* Expand the first integrity step *)
apply (erule integrity_obj_alt.cases[where ko=ko and ko'=ko'])
(* LRefl and ORefl trivially collapse into the second integrity step *)
apply (find_goal \<open>match premises in "tro_tag LRefl" \<Rightarrow> -\<close>)
subgoal by (rule tro_alt_lrefl, simp)
apply (find_goal \<open>match premises in "tro_tag ORefl" \<Rightarrow> -\<close>)
subgoal by simp
(* Now re-tag the first step with tro_tag' *)
apply (all \<open>simp only:tro_tag_to_prime\<close>)
(* Expand the second integrity step, which will be tagged with tro_tag *)
apply (all \<open>erule integrity_obj_alt.cases\<close>)
(* There are some special cases that would be too slow or unsolvable by the bulk tactics.
We move them up here and solve manually *)
apply (find_goal \<open>match premises in "tro_tag' TCBReply" and "tro_tag TCBActivate" \<Rightarrow> -\<close>)
apply (clarsimp, rule tro_alt_tcb_reply[OF tro_tagI refl refl],
(rule exI; rule tcb.equality; simp); fastforce)
apply (find_goal \<open>match premises in "tro_tag' TCBReceive" and "tro_tag TCBReply" \<Rightarrow> -\<close>)
apply (clarsimp, rule tro_alt_tcb_reply[OF tro_tagI refl refl],
(rule exI; rule tcb.equality; simp);
fastforce simp: direct_reply_def allowed_call_blocked_def)
apply (find_goal \<open>match premises in "tro_tag TCBGeneric" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>)
subgoal
apply (erule integrity_obj_alt.intros[simplified tro_tag_to_prime])
apply (simp | rule tcb.equality | fastforce)+
done
apply (find_goal \<open>match premises in "tro_tag TCBActivate" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>)
apply (rule tro_alt_tcb_restart[OF tro_tagI], (fastforce simp: tcb.splits fun_upd_def)+)[1]
apply (find_goal \<open>match premises in "tro_tag REp" and "tro_tag' REp" \<Rightarrow> -\<close>)
subgoal by (erule integrity_obj_alt.intros, (rule refl | assumption)+)
(* Select groups of subgoals by tag, then solve with the given methods *)
apply (all \<open>fails \<open>erule thin_rl[of "tro_tag LRefl"]\<close>
| time_methods \<open>fastforce intro: tro_alt_lrefl\<close>\<close>)
apply (all \<open>fails \<open>erule thin_rl[of "tro_tag ORefl"]\<close>
| time_methods \<open>solves \<open>
drule sym[where t="ko''"];
erule integrity_obj_alt.intros[simplified tro_tag_to_prime];
solves \<open>simp\<close>\<close>\<close>\<close>)
apply (all \<open>fails \<open>erule thin_rl[of "tro_tag RNtfn"] thin_rl[of "tro_tag' RNtfn"]\<close>
| time_methods \<open>fastforce intro: tro_alt_ntfn\<close>\<close>)
apply (all \<open>fails \<open>erule thin_rl[of "tro_tag REp"]
| erule thin_rl[of "tro_tag' REp"]
| erule thin_rl[of "tro_tag RArch"]
| erule thin_rl[of "tro_tag' RArch"]
| erule thin_rl[of "tro_tag EpUnblock"]
| erule thin_rl[of "tro_tag' EpUnblock"]
| erule thin_rl[of "tro_tag RCNode"]
| erule thin_rl[of "tro_tag' RCNode"]\<close>
| time_methods \<open>fastforce intro: integrity_obj_alt.intros
simp: arch_tro_alt_trans_spec\<close>\<close>)
(* TCB-TCB steps, somewhat slow *)
apply (all \<open>fails \<open>erule thin_rl[of "tro_tag TCBGeneric"]\<close>
| time_methods \<open>solves \<open>
erule integrity_obj_alt.intros[simplified tro_tag_to_prime],
(assumption | rule refl
| ((erule exE)+)?, (rule exI)?, force intro: tcb.equality)+\<close>\<close>\<close>)
apply (all \<open>fails \<open>erule thin_rl[of "tro_tag' TCBGeneric"]\<close>
| time_methods \<open>solves \<open>
erule integrity_obj_alt.intros,
(assumption | rule refl
| (elim exE)?, (intro exI)?, fastforce intro: tcb.equality
| fastforce simp: indirect_send_def direct_send_def direct_call_def direct_reply_def
dest: tcb_bound_notification_reset_eq_or_none)+\<close>\<close>\<close>)
apply (time_methods \<open>
succeeds \<open>match premises in T: "tro_tag _" and T': "tro_tag' _" \<Rightarrow>
\<open>print_fact T, print_fact T'\<close>\<close>,
fastforce intro: integrity_obj_alt.intros tcb.equality
simp: indirect_send_def direct_send_def direct_call_def direct_reply_def
call_blocked_def allowed_call_blocked_def\<close>)+
done
lemma tro_alt_transp[intro!]:
"transp (integrity_obj_alt (aag :: 'a PAS) activate es subjects)"
by (rule transpI) (rule tro_alt_trans_spec)
lemma tro_alt_reflp[intro!]:
"reflp (integrity_obj_alt aag activate es subjects)"
by (rule reflpI) (rule tro_alt_orefl; blast)
lemma tro_tro_alt[elim!]:
"integrity_obj aag activate es subjects ko ko'
\<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'"
unfolding integrity_obj_def
by (subst rtranclp_id[symmetric]; fastforce elim: rtranclp_mono[THEN predicate2D,rotated])
lemmas integrity_objE = tro_tro_alt[THEN integrity_obj_alt.cases
[simplified tro_tag_def True_implies_equals]]
end
lemma tro_trans:
"\<lbrakk> integrity_obj_state aag activate es s s'; integrity_obj_state aag activate es s' s'' \<rbrakk>
\<Longrightarrow> integrity_obj_state aag activate es s s''"
unfolding integrity_obj_def
apply clarsimp
apply (drule_tac x = x in spec)+
by force
lemma tre_trans:
"\<lbrakk> (\<forall>x. integrity_eobj aag es (pasObjectAbs aag x) (ekh x) (ekh' x));
(\<forall>x. integrity_eobj aag es (pasObjectAbs aag x) (ekh' x) (ekh'' x)) \<rbrakk>
\<Longrightarrow> (\<forall>x. integrity_eobj aag es (pasObjectAbs aag x) (ekh x) (ekh'' x))"
by (fastforce elim!: integrity_eobj.cases intro: integrity_eobj.intros)
subsection \<open>Integrity transitivity\<close>
lemma tcb_caller_slot_empty_on_recieve:
"\<lbrakk> valid_mdb s; valid_objs s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb) \<rbrakk>
\<Longrightarrow> tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr,(tcb_cnode_index 3)) = None \<and>
descendants_of (tcb_ptr,(tcb_cnode_index 3)) (cdt s) = {}"
apply (simp only:valid_objs_def)
apply (drule bspec,fastforce)
apply (simp add:valid_obj_def)
apply (simp only:valid_tcb_def)
apply (drule conjunct1)
apply (drule_tac x="the (tcb_cap_cases (tcb_cnode_index 3))" in bspec)
apply (fastforce simp:tcb_cap_cases_def)
apply (simp add:tcb_cap_cases_def split: thread_state.splits)
apply (subgoal_tac "caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap")
apply (simp only: valid_mdb_def2, drule conjunct1)
apply (intro conjI)
apply (simp add: mdb_cte_at_def)
apply (rule classical)
apply fastforce
apply (rule mdb_cte_at_no_descendants, fastforce+)[1]
apply (fastforce simp add: tcb_cnode_map_def caps_of_state_tcb_index_trans[OF get_tcb_rev])
done
(* FIXME MOVE next to tcb_states_of_state definition *)
lemma tcb_states_of_state_kheap:
"\<lbrakk> kheap s slot = Some (TCB tcb)\<rbrakk>
\<Longrightarrow> tcb_states_of_state s slot = Some (tcb_state tcb)"
by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits)
lemma tcb_states_of_state_kheapI:
"\<lbrakk> kheap s slot = Some (TCB tcb); tcb_state tcb = tcbst \<rbrakk>
\<Longrightarrow> tcb_states_of_state s slot = Some tcbst"
by (simp add: tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits)
lemma tcb_states_of_state_kheapD:
"tcb_states_of_state s slot = Some tcbst \<Longrightarrow>
\<exists>tcb. kheap s slot = Some (TCB tcb) \<and> tcb_state tcb = tcbst"
by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits)
lemma tcb_states_of_state_kheapE:
assumes "tcb_states_of_state s slot = Some tcbst"
obtains tcb where "kheap s slot = Some (TCB tcb)" "tcb_state tcb = tcbst"
using assms tcb_states_of_state_kheapD by blast
lemma cdt_change_allowed_to_child:
"\<lbrakk> cdt_change_allowed aag subjects m tcbsts pptr; m ptr = Some pptr \<rbrakk>
\<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr"
apply (elim cdt_change_allowedE)
apply (erule cdt_change_allowedI[rotated])
by (fastforce intro: rtrancl_into_rtrancl simp: cdt_parent_of_def)
lemma trinterrupts_trans:
"\<lbrakk> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x)
(interrupt_irq_node s' x, interrupt_states s' x));
(\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x)
(interrupt_irq_node s'' x, interrupt_states s'' x)) \<rbrakk>
\<Longrightarrow> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x)
(interrupt_irq_node s'' x, interrupt_states s'' x))"
apply (simp add: integrity_interrupts_def del: split_paired_All)
apply metis
done
lemma trrqs_trans:
"\<lbrakk> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d)
(ready_queues s d p) (ready_queues s' d p));
(\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d)
(ready_queues s' d p) (ready_queues s'' d p)) \<rbrakk>
\<Longrightarrow> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d)
(ready_queues s d p) (ready_queues s'' d p))"
apply (clarsimp simp: integrity_ready_queues_def)
apply (metis append_assoc)
done
context Access_AC_1 begin
lemma cdt_direct_change_allowed_backward:
"\<lbrakk> integrity_obj_state aag activate subjects s s';
cdt_direct_change_allowed aag subjects (tcb_states_of_state s') ptr \<rbrakk>
\<Longrightarrow> cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr"
apply (erule cdt_direct_change_allowed.cases)
subgoal by (rule cdca_owned)
apply (erule tcb_states_of_state_kheapE)
by (drule spec,
erule integrity_objE, erule cdca_owned;
(elim exE)?;
simp;
rule cdca_reply[rotated], assumption, assumption,
fastforce elim:tcb_states_of_state_kheapI simp:direct_call_def)
lemma cdt_change_allowed_backward:
"\<lbrakk> integrity_obj_state aag activate subjects s s';
integrity_cdt_state aag subjects s s';
cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') ptr \<rbrakk>
\<Longrightarrow> cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) ptr"
apply (elim cdt_change_allowedE)
apply (drule(1) cdt_direct_change_allowed_backward)
apply (erule rtrancl_induct)
subgoal by (rule cdca_ccaI)
apply (rename_tac pptr0 ptr)
apply (frule_tac x=ptr in spec)
apply (elim integrity_cdtE; simp; elim conjE)
apply (erule cdt_change_allowed_to_child)
by (simp add: cdt_parent_of_def)
lemma trcdt_trans:
"\<lbrakk> integrity_cdt_state aag subjects s s' ;
integrity_obj_state aag activate subjects s s' ;
integrity_cdt_state aag subjects s' s'' \<rbrakk>
\<Longrightarrow> integrity_cdt_state aag subjects s s''"
apply (intro allI)
apply (frule_tac x=x in spec)
apply (frule_tac x=x in spec[where P = "\<lambda>x. integrity_cdt _ _ (cdt s') _ x (_ x) (_ x)"])
apply (erule integrity_cdtE)+
apply simp
by (blast dest: cdt_change_allowed_backward)+
lemma trcdtlist_trans:
"\<lbrakk> integrity_cdt_list_state aag subjects s s' ;
integrity_obj_state aag activate subjects s s' ;
integrity_cdt_state aag subjects s s' ;
integrity_cdt_list_state aag subjects s' s'' \<rbrakk>
\<Longrightarrow> integrity_cdt_list_state aag subjects s s''"
apply (intro allI)
apply (drule_tac x=x in spec [where P="\<lambda>ptr. integrity_cdt_list _ _ _ _ ptr (_ ptr) (_ ptr)"] )+
apply (erule integrity_cdt_listE)+
apply (rule integrity_cdt_list_filt)
apply (simp del: split_paired_All split_paired_Ex)
apply (erule weaken_filter_eq')
by (blast intro: integrity_cdt_list_intros dest: cdt_change_allowed_backward)+
(* FIXME RENAME *)
lemma tsos_tro:
"\<lbrakk> integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a;
receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
\<Longrightarrow> tcb_states_of_state s p = Some a"
apply (drule_tac x = p in spec)
apply (erule integrity_objE, simp_all add: tcb_states_of_state_def get_tcb_def)
by fastforce+
lemma can_receive_ipc_backward:
"\<lbrakk> integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a;
can_receive_ipc a; pasObjectAbs aag p \<notin> subjects \<rbrakk>
\<Longrightarrow> case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x"
apply (drule_tac x = p in spec)
apply (erule integrity_objE;
(fastforce simp: tcb_states_of_state_def get_tcb_def
call_blocked_def allowed_call_blocked_def
split: option.splits kernel_object.splits
| cases a \<comment> \<open>only split when needed\<close>)+)
done
lemma tsos_tro_running:
"\<lbrakk> \<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x);
tcb_states_of_state s p = Some Running; pasObjectAbs aag p \<notin> subjects \<rbrakk>
\<Longrightarrow> tcb_states_of_state s' p = Some Running"
by (drule_tac x=p in spec, erule integrity_objE,
simp_all add: tcb_states_of_state_def get_tcb_def indirect_send_def direct_send_def
direct_call_def direct_reply_def call_blocked_def allowed_call_blocked_def)
end
locale Access_AC_2 = Access_AC_1 +
assumes auth_ipc_buffers_tro:
"\<And>x. \<lbrakk> integrity_obj_state aag activate subjects s s';
x \<in> auth_ipc_buffers s' p; pasObjectAbs aag p \<notin> subjects \<rbrakk>
\<Longrightarrow> x \<in> auth_ipc_buffers s p "
and integrity_asids_refl[simp]:
"\<And>x. integrity_asids aag subjects x (s :: det_ext state) s"
and trasids_trans:
"\<lbrakk> (\<forall>x. integrity_asids aag subjects x s (s' :: det_ext state));
(\<forall>x. integrity_asids aag subjects x s' (s'' :: det_ext state))\<rbrakk>
\<Longrightarrow> (\<forall>x. integrity_asids aag subjects x s s'')"
begin
section \<open>Generic AC stuff\<close>
subsection \<open>Basic integrity lemmas\<close>
lemma integrity_trans:
assumes t1: "integrity_subjects subjects aag activate X s s'"
and t2: "integrity_subjects subjects aag activate X s' s''"
shows "integrity_subjects subjects aag activate X s s''"
proof -
from t1 have tro1: "integrity_obj_state aag activate subjects s s'"
unfolding integrity_subjects_def by simp
from t2 have tro2: "integrity_obj_state aag activate subjects s' s''"
unfolding integrity_subjects_def by simp
have intm: "\<forall>x. integrity_mem aag subjects x
(tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X
(underlying_memory (machine_state s) x)
(underlying_memory (machine_state s'') x)" (is "\<forall>x. ?P x s s''")
proof
fix x
from t1 t2 have m1: "?P x s s'" and m2: "?P x s' s''" unfolding integrity_subjects_def by auto
from m1 show "?P x s s''"
proof cases
case trm_lrefl thus ?thesis by (rule integrity_mem.intros)
next
case trm_globals thus ?thesis by (rule integrity_mem.intros)
next
case trm_orefl
from m2 show ?thesis
proof cases
case (trm_ipc p')
show ?thesis
proof (rule integrity_mem.trm_ipc)
from trm_ipc show "case_option False can_receive_ipc (tcb_states_of_state s p')"
by (fastforce split: option.splits dest: can_receive_ipc_backward [OF tro1])
from trm_ipc show "x \<in> auth_ipc_buffers s p'"
by (fastforce split: option.splits intro: auth_ipc_buffers_tro [OF tro1])
qed (simp_all add: trm_ipc)
qed (auto simp add: trm_orefl intro: integrity_mem.intros)
next
case trm_write thus ?thesis by (rule integrity_mem.intros)
next
case (trm_ipc p')
note trm_ipc1 = trm_ipc
from m2 show ?thesis
proof cases
case trm_orefl
thus ?thesis using trm_ipc1
by (auto intro!: integrity_mem.trm_ipc simp add: restrict_map_Some_iff elim!: tsos_tro_running [OF tro2, rotated])
next
case (trm_ipc p'')
show ?thesis
proof (cases "p' = p''")
case True thus ?thesis using trm_ipc trm_ipc1 by (simp add: restrict_map_Some_iff)
next
(* 2 tcbs sharing same IPC buffer, we can appeal to either t1 or t2 *)
case False
thus ?thesis using trm_ipc1
by (auto intro!: integrity_mem.trm_ipc simp add: restrict_map_Some_iff elim!: tsos_tro_running [OF tro2, rotated])
qed
qed (auto simp add: trm_ipc intro: integrity_mem.intros)
qed
qed
moreover have "\<forall>x. integrity_device aag subjects x
(tcb_states_of_state s) (tcb_states_of_state s'')
(device_state (machine_state s) x)
(device_state (machine_state s'') x)" (is "\<forall>x. ?P x s s''")
proof
fix x
from t1 t2 have m1: "?P x s s'" and m2: "?P x s' s''" unfolding integrity_subjects_def by auto
from m1 show "?P x s s''"
proof cases
case trd_lrefl thus ?thesis by (rule integrity_device.intros)
next
case torel1: trd_orefl
from m2 show ?thesis
proof cases
case (trd_lrefl) thus ?thesis by (rule integrity_device.trd_lrefl)
next
case trd_orefl thus ?thesis
by (simp add: torel1)
next
case trd_write thus ?thesis by (rule integrity_device.trd_write)
qed
next
case trd_write thus ?thesis by (rule integrity_device.intros)
qed
qed
thus ?thesis using tro_trans[OF tro1 tro2] t1 t2 intm
apply (clarsimp simp add: integrity_subjects_def simp del: split_paired_All)
apply (frule(2) trcdt_trans)
apply (frule(3) trcdtlist_trans)
apply (frule(1) trinterrupts_trans[simplified])
apply (frule(1) trasids_trans[simplified])
apply (frule(1) tre_trans[simplified])
apply (frule(1) trrqs_trans[simplified])
by blast
qed
lemma integrity_refl [simp]:
"integrity_subjects S aag activate X s s"
unfolding integrity_subjects_def
by simp
lemma integrity_update_autarch:
"\<lbrakk> integrity aag X st s; is_subject aag ptr \<rbrakk>
\<Longrightarrow> integrity aag X st (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>)"
unfolding integrity_subjects_def
apply (intro conjI,simp_all)
apply clarsimp
apply (drule_tac x = x in spec, erule integrity_mem.cases)
apply ((auto intro: integrity_mem.intros)+)[4]
apply (erule trm_ipc, simp_all)
apply (clarsimp simp: restrict_map_Some_iff tcb_states_of_state_def get_tcb_def)
apply clarsimp
apply (drule_tac x = x in spec, erule integrity_device.cases)
apply (erule integrity_device.trd_lrefl)
apply (erule integrity_device.trd_orefl)
apply (erule integrity_device.trd_write)
done
lemma set_object_integrity_autarch:
"\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace> set_object ptr obj \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (wpsimp wp: set_object_wp)
apply (rule integrity_update_autarch, simp_all)
done