-
Notifications
You must be signed in to change notification settings - Fork 0
/
CHERI_Lemmas.thy
2738 lines (2413 loc) · 130 KB
/
CHERI_Lemmas.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
section \<open>Manually proved helper lemmas\<close>
theory CHERI_Lemmas
imports CHERI_Gen_Lemmas
begin
context Morello_Axiom_Automaton
begin
definition VAIsTaggedCap :: "VirtualAddress \<Rightarrow> bool" where
"VAIsTaggedCap va \<longleftrightarrow> (VAIsCapability va \<and> CapIsTagSet (VirtualAddress_base va))"
definition VAIsSealedCap :: "VirtualAddress \<Rightarrow> bool" where
"VAIsSealedCap va \<longleftrightarrow> (VAIsCapability va \<and> CapIsSealed (VirtualAddress_base va))"
lemma CheckCapability_CapIsSealed_False:
assumes "Run (CheckCapability c addr sz perms acctype) t a"
shows "CapIsSealed c \<longleftrightarrow> False"
using assms
by (auto simp: CheckCapability_def elim!: Run_bindE)
lemma Run_VAToBits64_vatype_Bits64[simp]:
assumes "Run (VAToBits64 va) t addr"
shows "VirtualAddress_vatype va = VA_Bits64"
using assms
by (auto simp: VAToBits64_def VAIsBits64_def)
lemma VADeref_VAIsSealedCap_False[simp]:
assumes "Run (VACheckAddress va addr sz perms acctype) t u"
shows "VAIsSealedCap va \<longleftrightarrow> False"
using assms
unfolding VACheckAddress_def
by (auto simp: VAIsSealedCap_def VAIsCapability_def VAIsBits64_def CheckCapability_CapIsSealed_False elim!: Run_bindE Run_ifE)
lemma VADeref_not_sealed[derivable_capsE]:
assumes "Run (VACheckAddress va addr sz perms acctype) t u"
shows "\<not>VAIsSealedCap va"
using assms
by auto
lemma if_VADerefs_VAIsSealedCap_False[derivable_capsE]:
assumes "Run (if b then VACheckAddress va vaddr sz perms acctype else VACheckAddress va vaddr sz' perms' acctype') t u"
shows "\<not>VAIsSealedCap va"
using assms
by (auto split: if_splits)
(*lemma Run_case_MemOp_LOAD_STORE_not_VAIsSealedCap[derivable_capsE]:
assumes "Run (case memop of MemOp_LOAD \<Rightarrow> VACheckAddress va addr sz perms acctype \<bind> m | MemOp_STORE \<Rightarrow> VACheckAddress va addr' sz' perms' acctype' \<bind> m' | MemOp_PREFETCH \<Rightarrow> return ()) t a"
and "memop \<noteq> MemOp_PREFETCH"
and "\<not>VAIsPCCRelative va"
shows "\<not>VAIsSealedCap va"
using assms
by (cases memop) (auto elim!: Run_bindE)
lemma Run_case_MemOp_LOAD_STORE_not_VAIsSealedCap_pre_idx[derivable_capsE]:
assumes "Run (case memop of MemOp_LOAD \<Rightarrow> VACheckAddress va addr sz perms acctype \<bind> m | MemOp_STORE \<Rightarrow> VACheckAddress va addr' sz' perms' acctype' \<bind> m' | MemOp_PREFETCH \<Rightarrow> return ()) t a"
and "memop \<noteq> MemOp_PREFETCH"
and "\<not>VAIsPCCRelative va"
and "VAIsSealedCap va = VAIsSealedCap va'"
shows "\<not>VAIsSealedCap va'"
using assms
by (cases memop) (auto elim!: Run_bindE)*)
lemma Run_case_MemOp_LOAD_STORE_not_VAIsSealedCap_generic[derivable_capsE]:
assumes "Run (case memop of MemOp_LOAD \<Rightarrow> VACheckAddress va addr sz perms acctype \<bind> m | MemOp_STORE \<Rightarrow> VACheckAddress va addr' sz' perms' acctype' \<bind> m' | MemOp_PREFETCH \<Rightarrow> m'') t a"
and "memop = MemOp_PREFETCH \<longrightarrow> Run m'' t a \<longrightarrow> \<not>VAIsSealedCap va"
shows "\<not>VAIsSealedCap va"
using assms
by (cases memop) (auto elim!: Run_bindE)
declare Run_bindE'[where P = "\<lambda>t. VA_derivable va (run s t)" for va s, simplified, derivable_caps_combinators]
lemma VAAdd_derivable[derivable_capsE]:
assumes t: "Run (VAAdd va offset) t va'"
and "VAIsTaggedCap va \<and> VAIsTaggedCap va' \<and> (VAIsSealedCap va' \<longleftrightarrow> VAIsSealedCap va) \<longrightarrow> \<not>VAIsSealedCap va"
and "VAIsTaggedCap va \<and> \<not>VAIsSealedCap va \<longrightarrow> VA_derivable va s"
shows "VA_derivable va' s"
proof -
have *: "VAIsSealedCap va' \<longleftrightarrow> VAIsSealedCap va"
using t
by (auto simp: VAAdd_def VAIsSealedCap_def VAIsCapability_def elim!: Run_bindE Run_ifE)
have **: "VAIsTaggedCap va' \<longrightarrow> VAIsTaggedCap va"
using t
by (auto simp: VAAdd_def VAIsTaggedCap_def VAIsCapability_def elim!: Run_bindE Run_ifE Run_CapAdd_tag_imp)
have "\<not>VAIsTaggedCap va' \<longrightarrow> VA_derivable va' s"
by (cases "VirtualAddress_vatype va'")
(auto simp add: VA_derivable_def derivable_caps_def VAIsTaggedCap_def VAIsCapability_def)
moreover have "VAIsTaggedCap va' \<longrightarrow> VA_derivable va' (run s t)"
using assms **
unfolding VAAdd_def *
by - (derivable_capsI simp: VAIsSealedCap_def)
ultimately show ?thesis
using non_cap_exp_Run_run_invI[OF non_cap_exp_VAAdd t]
by auto
qed
lemma VAFromCapability_base_derivable_run:
assumes "Run (VAFromCapability c) t va"
and "c \<in> derivable_caps s"
shows "VirtualAddress_base va \<in> derivable_caps (run s t)"
using assms
by (auto simp: VAFromCapability_base_derivable non_cap_exp_VAFromCapability[THEN non_cap_exp_Run_run_invI])
lemma BaseReg_read_VA_derivable[derivable_capsE]:
assumes "Run (BaseReg_read n is_prefetch) t va"
and "{''_R29'', ''PCC''} \<subseteq> accessible_regs s"
shows "VA_derivable va (run s t)"
proof (cases "VirtualAddress_vatype va")
case VA_Bits64
then show ?thesis
by (auto simp: VA_derivable_def)
next
case VA_Capability
then have "VirtualAddress_base va \<in> derivable_caps (run s t)"
using assms
unfolding BaseReg_read_def
by - (derivable_capsI elim: VAFromCapability_base_derivable_run)
then show ?thesis
using VA_Capability
by (auto simp: VA_derivable_def)
qed
lemmas BaseReg_read__1_VA_derivable[derivable_capsE] =
BaseReg_read_VA_derivable[where is_prefetch = False, folded BaseReg_read__1_def]
lemma AltBaseReg_read_VA_derivable[derivable_capsE]:
assumes "Run (AltBaseReg_read n is_prefetch) t va"
and "{''_R29''} \<subseteq> accessible_regs s"
shows "VA_derivable va (run s t)"
proof (cases "VirtualAddress_vatype va")
case VA_Bits64
then show ?thesis
by (auto simp: VA_derivable_def)
next
case VA_Capability
then have "VirtualAddress_base va \<in> derivable_caps (run s t)"
using assms
unfolding AltBaseReg_read_def
by - (derivable_capsI elim: VAFromCapability_base_derivable_run)
then show ?thesis
using VA_Capability
by (auto simp: VA_derivable_def)
qed
declare AltBaseReg_read_VA_derivable[where is_prefetch = False, folded AltBaseReg_read__1_def, derivable_capsE]
lemmas VA_derivable_combinators[derivable_caps_combinators] =
Run_bindE'[where P = "\<lambda>t. VA_derivable va (run s t)" for va s, simplified]
Run_ifE[where thesis = "VA_derivable va (run s t)" and t = t for va s t]
Run_letE[where thesis = "VA_derivable va (run s t)" and t = t for va s t]
Run_case_prodE[where thesis = "VA_derivable va (run s t)" and t = t for va s t]
end
definition "determ_instrs_of_exp m \<equiv>
(\<forall>t. hasTrace t m \<longrightarrow> instrs_of_exp m = set_option (instr_of_trace t))"
lemma hasTrace_determ_instrs_eqs:
assumes "hasTrace t m" and "determ_instrs_of_exp m"
shows "exp_invokes_regs m = trace_invokes_regs t"
and "exp_invokes_indirect_regs m = trace_invokes_indirect_regs t"
and "exp_load_auths m = trace_load_auths t"
and "exp_is_indirect_branch m = trace_is_indirect_branch t"
using assms
unfolding exp_invokes_regs_def trace_invokes_regs_def
unfolding exp_invokes_indirect_regs_def trace_invokes_indirect_regs_def
unfolding exp_load_auths_def trace_load_auths_def
unfolding trace_is_indirect_branch_def
by (auto simp: determ_instrs_of_exp_def split: option.splits)
lemma T_bind_leftI:
assumes "(m, e, m') \<in> T"
shows "(bind m f, e, bind m' f) \<in> T"
using assms
by induction auto
lemma Traces_bind_leftI:
assumes "(m, t, m') \<in> Traces"
shows "(bind m f, t, bind m' f) \<in> Traces"
using assms
by induction (auto intro: T_bind_leftI)
lemma instr_of_trace_no_writes_None:
assumes "\<nexists>v. E_write_reg ''__ThisInstrAbstract'' v \<in> set t"
shows "instr_of_trace t = None"
using assms
by (cases t rule: instr_of_trace.cases) auto
lemma instr_of_trace_append_no_writes:
assumes "\<nexists>v. E_write_reg ''__ThisInstrAbstract'' v \<in> set t2"
shows "instr_of_trace (t1 @ t2) = instr_of_trace t1"
using assms
by (cases t1 rule: instr_of_trace.cases) (auto simp: instr_of_trace_no_writes_None)
lemma instrs_of_exp_bind_no_writes:
assumes "\<forall>a. no_reg_writes_to {''__ThisInstrAbstract''} (f a)"
shows "instrs_of_exp (bind m f) = instrs_of_exp m"
using assms
by (fastforce simp: instrs_of_exp_def instr_of_trace_append_no_writes no_reg_writes_to_def
intro: Traces_bind_leftI elim!: bind_Traces_cases)
lemma determ_instrs_of_exp_bind_write_reg_ThisInstrAbstract:
"determ_instrs_of_exp (write_reg ThisInstrAbstract_ref instr \<bind> f)"
by (auto simp: determ_instrs_of_exp_def instr_of_trace_bind_write_reg_ThisInstrAbstract)
lemma no_reg_writes_to_instr_of_trace_None:
assumes "hasTrace t m" and "no_reg_writes_to {''__ThisInstrAbstract''} m"
shows "instr_of_trace t = None"
using assms
by (intro instr_of_trace_no_writes_None) (auto simp: no_reg_writes_to_def hasTrace_iff_Traces_final)
lemma no_reg_writes_to_determ_instrs_of_exp:
assumes "no_reg_writes_to {''__ThisInstrAbstract''} m"
shows "determ_instrs_of_exp m"
using assms
by (auto simp: determ_instrs_of_exp_def no_reg_writes_to_instrs_of_exp no_reg_writes_to_instr_of_trace_None)
(* TODO: Move *)
lemma if_split_no_asm: "P x \<Longrightarrow> P y \<Longrightarrow> P (if b then x else y)"
by auto
lemmas determ_instrs_of_exp_if_split_no_asm = if_split_no_asm[where P = determ_instrs_of_exp]
lemma hasTrace_intros:
"Run m t a \<Longrightarrow> hasTrace t m"
"hasException t m \<Longrightarrow> hasTrace t m"
"hasFailure t m \<Longrightarrow> hasTrace t m"
by (auto simp: hasTrace_iff_Traces_final hasException_iff_Traces_Exception hasFailure_iff_Traces_Fail)
lemma determ_instrs_of_exp_bind_no_reg_writes:
assumes "determ_instrs_of_exp m" and"\<forall>a. no_reg_writes_to {''__ThisInstrAbstract''} (f a)"
shows "determ_instrs_of_exp (bind m f)"
proof (unfold determ_instrs_of_exp_def, intro allI impI)
fix t
assume "hasTrace t (m \<bind> f)"
then show "instrs_of_exp (m \<bind> f) = set_option (instr_of_trace t)"
proof (cases rule: hasTrace_bind_cases)
case (Bind tm am tf)
then have "instr_of_trace (tm @ tf) = instr_of_trace tm"
using assms(2)
by (intro instr_of_trace_append_no_writes)
(auto simp: no_reg_writes_to_def hasTrace_iff_Traces_final)
with assms Bind show ?thesis
by (auto simp: determ_instrs_of_exp_def instrs_of_exp_bind_no_writes hasTrace_intros)
next
case Fail
with assms show ?thesis
by (auto simp: determ_instrs_of_exp_def instrs_of_exp_bind_no_writes hasTrace_intros)
next
case Ex
with assms show ?thesis
by (auto simp: determ_instrs_of_exp_def instrs_of_exp_bind_no_writes hasTrace_intros)
qed
qed
lemma trace_invokes_indirect_regs_None[simp]:
assumes "instr_of_trace t = None"
shows "trace_invokes_indirect_regs t = {}"
using assms
by (auto simp: trace_invokes_indirect_regs_def)
lemma instr_trace_invokes_indirect_regs[simp]:
assumes "instr_of_trace t = Some instr"
shows "trace_invokes_indirect_regs t = instr_invokes_indirect_regs instr"
using assms
by (auto simp: trace_invokes_indirect_regs_def)
lemma trace_invokes_indirect_caps_no_regs[simp]:
assumes "trace_invokes_indirect_regs t = {}"
shows "trace_invokes_indirect_caps t = {}"
using assms
by (auto simp: trace_invokes_indirect_caps_def)
context Morello_Axiom_Automaton
begin
lemma determ_instrs_of_exp_DecodeA64:
"determ_instrs_of_exp (DecodeA64 pc opcode)"
by (unfold DecodeA64_def Let_def)
(intro determ_instrs_of_exp_if_split_no_asm determ_instrs_of_exp_bind_write_reg_ThisInstrAbstract no_reg_writes_to_determ_instrs_of_exp;
no_reg_writes_toI)
(*lemma determ_instrs_of_exp_DecodeExecute:
"determ_instrs_of_exp (DecodeExecute enc opcode)"
by (cases enc; auto simp: ExecuteA64_def ExecuteA32_def ExecuteT16_def ExecuteT32_def determ_instrs_of_exp_DecodeA64 no_reg_writes_to_determ_instrs_of_exp)*)
lemma determ_instrs_instr_sem:
"determ_instrs_of_exp (instr_sem instr)"
unfolding instr_sem_def Step_PC_def
by (intro determ_instrs_of_exp_DecodeA64[THEN determ_instrs_of_exp_bind_no_reg_writes]; no_reg_writes_toI)
lemma instrs_eq_instr_exp_assms_iff:
assumes "instrs_of_exp m1 = instrs_of_exp m2"
shows "instr_exp_assms m1 \<longleftrightarrow> instr_exp_assms m2"
using assms
unfolding instr_exp_assms_def invocation_instr_exp_assms_def load_instr_exp_assms_def
unfolding exp_invokes_regs_def exp_invokes_indirect_regs_def exp_load_auths_def
by auto
(*lemma instr_exp_assms_TryInstructionExecute_iff:
"instr_exp_assms (TryInstructionExecute enc instr) \<longleftrightarrow> instr_exp_assms (DecodeExecute enc instr)"
unfolding TryInstructionExecute_def SSAdvance_def bind_assoc
by (intro instrs_eq_instr_exp_assms_iff instrs_of_exp_bind_no_writes allI)
(no_reg_writes_toI simp: register_defs)*)
lemma instr_exp_assms_instr_sem_iff:
"instr_exp_assms (instr_sem instr) \<longleftrightarrow> instr_exp_assms (DecodeA64 0 instr)"
unfolding instr_sem_def Step_PC_def bind_assoc
by (intro instrs_eq_instr_exp_assms_iff instrs_of_exp_bind_no_writes allI) (no_reg_writes_toI)
end
context Morello_Write_Cap_Automaton
begin
lemmas traces_enabled_return = non_cap_exp_return[THEN non_cap_exp_traces_enabledI]
lemma traces_enabled_Mem_read[traces_enabledI]:
shows "traces_enabled (Mem_read addrdesc sz accdesc) s"
by (unfold Mem_read_def, traces_enabledI)
lemma traces_enabled_ReadMem[traces_enabledI]:
shows "traces_enabled (ReadMem addrdesc sz accdesc) s"
by (unfold ReadMem_def, traces_enabledI)
lemma traces_enabled_ReadTaggedMem[traces_enabledI]:
shows "traces_enabled (ReadTaggedMem addrdesc sz accdesc) s"
by (unfold ReadTaggedMem_def, traces_enabledI intro: traces_enabled_return)
lemma traces_enabled_ReadTags[traces_enabledI]:
shows "traces_enabled (ReadTags addrdesc sz accdesc) s"
by (unfold ReadTags_def, traces_enabledI intro: traces_enabled_return)
lemma traces_enabled_Mem_set[traces_enabledI]:
shows "traces_enabled (Mem_set addrdesc sz accdesc data) s"
by (unfold Mem_set_def, traces_enabledI intro: traces_enabled_return)
lemma traces_enabled_WriteTaggedMem[traces_enabledI]:
fixes tags :: "'a::len word" and data :: "'b::len word"
assumes "Capability_of_tag_word (tags !! 0) (ucast data) \<in> derivable_caps s"
and "sz \<noteq> 16 \<longrightarrow> Capability_of_tag_word (tags !! 1) (Word.slice 128 data) \<in> derivable_caps s"
shows "traces_enabled (WriteTaggedMem addrdesc sz accdesc tags data) s"
unfolding WriteTaggedMem_def
by (traces_enabledI assms: assms intro: traces_enabled_return
simp: cap_of_mem_bytes_of_word_Capability_of_tag_word nth_ucast)
lemma cap_of_mem_bytes_B0_untagged[simp]:
"cap_of_mem_bytes bytes B0 = Some c \<Longrightarrow> c !! 128 = False"
by (auto simp: cap_of_mem_bytes_def bind_eq_Some_conv nth_ucast test_bit_above_size)
lemma traces_enabled_WriteTags[traces_enabledI]:
assumes "tags = 0" and "LENGTH('a) = nat sz"
shows "traces_enabled (WriteTags addrdesc sz (tags :: 'a::len word) accdesc) s"
unfolding WriteTags_def write_tag_bool_def
by (traces_enabledI assms: assms intro: traces_enabled_return not_tagged_derivable
intro: non_cap_exp_mword_nondet[THEN non_cap_exp_traces_enabledI]
simp: cap_of_mem_bytes_of_word_Capability_of_tag_word[where tag = False, simplified])
text \<open>Capability invocation\<close>
definition enabled_pcc :: "Capability \<Rightarrow> (Capability, register_value) axiom_state \<Rightarrow> bool" where
"enabled_pcc c s \<equiv>
c \<in> derivable_caps s \<or>
(c \<in> exception_targets (read_from_KCC s) \<and> ex_traces) \<or>
(c \<in> invoked_caps \<and>
((\<exists>c' \<in> derivable_caps s.
CapIsTagSet c' \<and> CapGetObjectType c' = CAP_SEAL_TYPE_RB \<and>
leq_cap CC c (CapUnseal c')) \<or>
(\<exists>cc cd.
cc \<in> derivable_caps s \<and> cd \<in> derivable_caps s \<and>
invokable CC cc cd \<and>
leq_cap CC c (CapUnseal cc)) \<or>
(\<exists>c' \<in> derivable_mem_caps s.
invokes_indirect_caps \<and> load_caps_permitted \<and>
(leq_cap CC c c' \<or> leq_cap CC c (CapUnseal c') \<and> CapIsTagSet c' \<and> CapGetObjectType c' = CAP_SEAL_TYPE_RB))))"
lemma derivable_mem_caps_run_imp:
assumes "c \<in> derivable_mem_caps s"
shows "c \<in> derivable_mem_caps (run s t)"
using assms derivable_mono[OF Un_mono[OF subset_refl[where A = UNKNOWN_caps] accessed_mem_caps_run_mono]]
by (auto simp: derivable_mem_caps_def)
lemma run_append_derivable_mem_capsE[derivable_caps_combinators]:
assumes "t = t1 @ t2" and "t = t1 @ t2 \<longrightarrow> c \<in> derivable_mem_caps (run (run s t1) t2)"
shows "c \<in> derivable_mem_caps(run s t)"
using assms
by auto
lemma traces_enabled_PCC_set:
assumes "enabled_pcc c s"
shows "traces_enabled (write_reg PCC_ref c) s"
using assms
unfolding enabled_pcc_def derivable_caps_def derivable_mem_caps_def
by (intro traces_enabled_write_reg)
(auto simp: register_defs is_sentry_def invokable_def CapIsSealed_def leq_cap_tag_imp[of CC, simplified])
definition enabled_branch_target :: "Capability \<Rightarrow> (Capability, register_value) axiom_state \<Rightarrow> bool" where
"enabled_branch_target c s \<equiv>
(CapIsTagSet c \<and> \<not>CapIsSealed c) \<longrightarrow> (\<forall>c' \<in> branch_caps c. enabled_pcc c' s)"
declare Run_ifE[where thesis = "enabled_branch_target c s" and a = c for c s, derivable_caps_combinators]
declare Run_letE[where thesis = "enabled_branch_target c s" and a = c for c s, derivable_caps_combinators]
declare Run_return_resultE[where P = "\<lambda>c. enabled_branch_target c s" for s, derivable_caps_combinators]
declare Run_bindE'[where P = "\<lambda>t. enabled_branch_target c (run s t)" for c s, simplified, derivable_caps_combinators]
declare Run_bindE[where thesis = "enabled_branch_target c s" and a = c for c s, derivable_caps_combinators]
declare if_split[where P = "\<lambda>c. enabled_branch_target c s" for s, THEN iffD2, derivable_capsI]
declare Run_ifE[where thesis = "enabled_branch_target (CapUnseal c) s" and a = c for c s, derivable_caps_combinators]
declare Run_letE[where thesis = "enabled_branch_target (CapUnseal c) s" and a = c for c s, derivable_caps_combinators]
declare Run_return_resultE[where P = "\<lambda>c. enabled_branch_target (CapUnseal c) s" for s, derivable_caps_combinators]
declare Run_bindE'[where P = "\<lambda>t. enabled_branch_target (CapUnseal c) (run s t)" for c s, simplified, derivable_caps_combinators]
declare Run_bindE[where thesis = "enabled_branch_target (CapUnseal c) s" and a = c for c s, simplified, derivable_caps_combinators]
declare if_split[where P = "\<lambda>c. enabled_branch_target (CapUnseal c) s" for s, THEN iffD2, derivable_capsI]
lemma run_append_enabled_branch_targetE[derivable_caps_combinators]:
assumes "t = t1 @ t2" and "t = t1 @ t2 \<longrightarrow> enabled_branch_target c (run (run s t1) t2)"
shows "enabled_branch_target c (run s t)"
using assms
by auto
lemma enabled_branch_targetI:
assumes "CapIsTagSet c \<and> \<not>CapIsSealed c \<longrightarrow> (\<forall>c' \<in> branch_caps c. enabled_pcc c' s)"
shows "enabled_branch_target c s"
using assms
by (auto simp: enabled_branch_target_def)
lemma exception_targets_mono:
assumes "C \<subseteq> C'"
shows "exception_targets C \<subseteq> exception_targets C'"
using assms derivable_mono[of "\<Union>(caps_of_regval ` C)" "\<Union>(caps_of_regval ` C')"]
by (auto simp: exception_targets_def)
lemma read_from_KCC_mono:
"read_from_KCC s \<subseteq> read_from_KCC (run s t)"
by (induction t rule: rev_induct) auto
lemma exception_targets_read_from_KCC_run_imp[derivable_caps_runI]:
assumes "c \<in> exception_targets (read_from_KCC s)"
shows "c \<in> exception_targets (read_from_KCC (run s t))"
using assms exception_targets_mono[OF read_from_KCC_mono]
by auto
lemma enabled_pcc_run_imp:
assumes "enabled_pcc c s"
shows "enabled_pcc c (run s t)"
using assms derivable_caps_run_imp[of _ s t] derivable_mem_caps_run_imp[of _ s t]
using exception_targets_read_from_KCC_run_imp
unfolding enabled_pcc_def
by fastforce
lemma enabled_branch_target_run_imp[derivable_caps_runI]:
assumes "enabled_branch_target c s"
shows "enabled_branch_target c (run s t)"
using assms
by (auto simp: enabled_branch_target_def intro: derivable_caps_run_imp enabled_pcc_run_imp)
lemma enabled_branch_target_CapUnseal:
assumes "c \<in> derivable_caps s"
and "CapIsTagSet c \<longrightarrow> CapGetObjectType c = CAP_SEAL_TYPE_RB \<and> branch_caps (CapUnseal c) \<subseteq> invoked_caps"
shows "enabled_branch_target (CapUnseal c) s"
using assms
unfolding enabled_branch_target_def enabled_pcc_def
by (fastforce intro: branch_caps_leq)
lemma untagged_enabled_branch_target[simp]:
"\<not>CapIsTagSet c \<longrightarrow> enabled_branch_target c s"
by (auto simp: enabled_branch_target_def)
lemma C_read_enabled_branch_target_CapUnseal[derivable_capsE]:
assumes "Run (C_read n) t c" and "invocation_trace_assms t" and "{''_R29''} \<subseteq> accessible_regs s"
and "CapIsTagSet c \<longrightarrow> CapGetObjectType c = CAP_SEAL_TYPE_RB \<and> n \<in> invoked_regs"
shows "enabled_branch_target (CapUnseal c) (run s t)"
using assms
by - (derivable_capsI intro: enabled_branch_target_CapUnseal simp: CapIsSealed_def)
lemma enabled_branch_target_CapWithTagClear[derivable_capsI]:
"enabled_branch_target (CapWithTagClear c) s"
"enabled_branch_target (CapUnseal (CapWithTagClear c)) s"
by (auto simp: enabled_branch_target_def enabled_pcc_def derivable_caps_def branch_caps_128th_iff)
lemma if_CapWithTagClear_128th_iff[simp]:
"(if clear then CapWithTagClear c else c) !! 128 \<longleftrightarrow> \<not>clear \<and> c !! 128"
by auto
lemma enabled_branch_target_CapUnseal_if_clear:
assumes "CapIsTagSet c \<longrightarrow> (\<forall>c' \<in> branch_caps (CapUnseal c). enabled_pcc c' s)"
shows "enabled_branch_target (CapUnseal (if clear then CapWithTagClear c else c)) s"
using assms
by (auto simp: enabled_branch_target_def)
lemma derivable_enabled_branch_target:
assumes "CapIsTagSet c \<longrightarrow> \<not>CapIsSealed c \<longrightarrow> c \<in> derivable_caps s"
shows "enabled_branch_target c s"
using assms branch_caps_derivable_caps[where c = c]
by (auto simp: enabled_branch_target_def enabled_pcc_def)
lemma C_read_enabled_branch_target[derivable_capsE]:
assumes "Run (C_read n) t c" and "{''_R29''} \<subseteq> accessible_regs s"
shows "enabled_branch_target c (run s t)"
using assms
by (auto intro: derivable_enabled_branch_target C_read_derivable)
lemma CapSetOffset_enabled_branch_target[derivable_capsE]:
assumes "Run (CapSetOffset c offset) t c'"
and "c \<in> derivable_caps s"
shows "enabled_branch_target c' s"
proof -
have "CapIsSealed c' \<longleftrightarrow> CapIsSealed c"
using assms
by (auto simp: CapSetOffset_def elim!: Run_bindE)
then show ?thesis
using assms
by (auto intro!: derivable_enabled_branch_target elim!: CapSetOffset_derivable)
qed
lemma CapSetValue_enabled_branch_target[derivable_capsE]:
assumes "Run (CapSetValue c addr) t c'"
and "c \<in> derivable_caps s"
shows "enabled_branch_target c' s"
proof -
have "CapIsSealed c' \<longleftrightarrow> CapIsSealed c"
using assms
unfolding CapSetValue_def CapIsSealed_def CapWithTagClear_def
by (auto elim!: Run_bindE Run_letE split: if_splits)
then show ?thesis
using assms
by (auto intro!: derivable_enabled_branch_target elim!: CapSetValue_derivable)
qed
lemma BranchAddr_enabled_pcc[derivable_capsE]:
assumes "Run (BranchAddr c el) t c'" and "enabled_branch_target c s"
shows "enabled_pcc c' s"
proof cases
assume "CapIsTagSet c'"
then have "c' \<in> branch_caps c" and "\<not>CapIsSealed c" and "CapIsTagSet c"
using BranchAddr_in_branch_caps[OF assms(1)]
using BranchAddr_not_sealed[OF assms(1)]
by auto
then show ?thesis
using assms(2)
by (auto simp: enabled_branch_target_def)
next
assume "\<not>CapIsTagSet c'"
then show ?thesis
by (auto simp: enabled_pcc_def derivable_caps_def)
qed
lemma CVBAR_read_in_read_from_KCC:
assumes "Run (CVBAR_read el) t c"
shows "Regval_bitvector_129_dec c \<in> read_from_KCC (run s t)"
using assms
by (auto simp: CVBAR_read_def register_defs elim!: Run_bindE Run_ifE Run_read_regE)
lemma CVBAR_read__1_in_read_from_KCC:
assumes "Run (CVBAR_read__1 u) t c"
shows "Regval_bitvector_129_dec c \<in> read_from_KCC (run s t)"
using assms
by (auto simp: CVBAR_read__1_def elim!: Run_bindE CVBAR_read_in_read_from_KCC)
lemma CVBAR_read__1_exception_target[derivable_capsE]:
assumes "Run (CVBAR_read__1 u) t c"
shows "c \<in> exception_targets (read_from_KCC (run s t))"
using CVBAR_read__1_in_read_from_KCC[OF assms, where s = s]
by (auto simp: exception_targets_def intro!: derivable.Copy)
lemma exception_target_enabled_branch_target:
assumes c: "CapIsTagSet c \<and> \<not>CapIsSealed c \<longrightarrow> c \<in> exception_targets (read_from_KCC s)" and ex: "ex_traces"
shows "enabled_branch_target c s"
proof (unfold enabled_branch_target_def, intro impI ballI)
fix c'
assume valid: "CapIsTagSet c \<and> \<not>CapIsSealed c" and c': "c' \<in> branch_caps c"
have "c' \<in> exception_targets (read_from_KCC s)"
using branch_caps_derivable[OF c'] valid c
by (auto simp: exception_targets_def)
with ex show "enabled_pcc c' s"
unfolding enabled_pcc_def
by blast
qed
lemma CapSetValue_exception_target_enabled_branch_target:
assumes t: "Run (CapSetValue c addr) t c'"
and c: "c \<in> exception_targets (read_from_KCC s)" and ex: "ex_traces"
shows "enabled_branch_target c' s"
proof -
from t c have "CapIsTagSet c' \<and> \<not>CapIsSealed c' \<longrightarrow> c' \<in> exception_targets (read_from_KCC s)"
unfolding CapSetValue_def exception_targets_def
by (auto simp: update_subrange_vec_dec_test_bit CapIsSealed_def
elim!: Run_bindE Run_letE
dest!: update_subrange_addr_CapIsRepresentable_derivable[where a = True and C = "\<Union>(caps_of_regval ` read_from_KCC s)"])
then show ?thesis
using ex
by (elim exception_target_enabled_branch_target)
qed
lemma invokable_enabled_pccI:
assumes "invokable CC cc cd"
and "cc \<in> derivable_caps s" and "cd \<in> derivable_caps s"
and "leq_cap CC c (CapUnseal cc)"
and "c \<in> invoked_caps"
shows "enabled_pcc c s"
using assms
unfolding enabled_pcc_def
by auto
lemma CapGetObjectType_CapWithTagClear_eq[simp]:
"CapGetObjectType (CapWithTagClear c) = CapGetObjectType c"
by (auto simp: CapGetObjectType_def CapWithTagClear_def slice_set_bit_above)
lemma CapGetObjectType_if_CapWithTagClear_eq:
"CapGetObjectType (if clear then CapWithTagClear c else c) = CapGetObjectType c"
by auto
lemma branch_sealed_pair_enabled_pcc:
assumes "CapGetObjectType (if clear then CapWithTagClear cc else cc) = CapGetObjectType cd"
and "CapIsTagSet cc" and "CapIsTagSet cd"
and "cap_permits CAP_PERM_EXECUTE cc" and "\<not>cap_permits CAP_PERM_EXECUTE cd"
and "cap_permits CAP_PERM_BRANCH_SEALED_PAIR cc" and "cap_permits CAP_PERM_BRANCH_SEALED_PAIR cd"
and "CAP_MAX_FIXED_SEAL_TYPE < uint (CapGetObjectType cc)"
and "cc \<in> derivable_caps s" and "cd \<in> derivable_caps s"
and "branch_caps (CapUnseal cc) \<subseteq> invoked_caps"
shows "\<forall>c' \<in> branch_caps (CapUnseal cc). enabled_pcc c' s"
using assms
unfolding CapGetObjectType_if_CapWithTagClear_eq
by (auto simp: invokable_def CapIsSealed_def is_sentry_def split: if_splits
intro!: branch_caps_leq invokable_enabled_pccI[of cc cd])
lemma (in Write_Cap_Assm_Automaton) traces_enabled_write_IDC_CCall:
assumes "c \<in> invoked_caps" and "invokable CC cc cd"
and "isa.caps_of_regval ISA (regval_of r v) = {c}"
and "cc \<in> derivable (initial_caps \<union> accessed_caps (\<not>invokes_indirect_caps \<and> use_mem_caps) s)"
and "cd \<in> derivable (initial_caps \<union> accessed_caps (\<not>invokes_indirect_caps \<and> use_mem_caps) s)"
and "name r \<in> IDC ISA - write_privileged_regs ISA"
and "leq_cap CC c (unseal_method CC cd)"
shows "traces_enabled (write_reg r v) s"
using assms
by (intro traces_enabled_write_reg) auto
lemma traces_enabled_C_set_29_branch_sealed_pair:
assumes "CapGetObjectType (if clear then CapWithTagClear cc else cc) = CapGetObjectType cd"
and "CapIsTagSet cc" and "CapIsTagSet cd"
and "cap_permits CAP_PERM_EXECUTE cc" and "\<not>cap_permits CAP_PERM_EXECUTE cd"
and "cap_permits CAP_PERM_BRANCH_SEALED_PAIR cc" and "cap_permits CAP_PERM_BRANCH_SEALED_PAIR cd"
and "CAP_MAX_FIXED_SEAL_TYPE < uint (CapGetObjectType cc)"
and "cc \<in> derivable_caps s" and "cd \<in> derivable_caps s"
and "CapUnseal cd \<in> invoked_caps"
shows "traces_enabled (C_set 29 (CapUnseal cd)) s"
using assms
unfolding CapGetObjectType_if_CapWithTagClear_eq
by (fastforce simp: C_set_def R_set_def derivable_caps_def invokable_def CapIsSealed_def is_sentry_def register_defs
intro: traces_enabled_write_IDC_CCall[of "CapUnseal cd" cc cd])
lemma (in Write_Cap_Assm_Automaton) traces_enabled_write_IDC_sentry:
assumes "c \<in> invoked_indirect_caps"
and "isa.caps_of_regval ISA (regval_of r v) = {c}"
and "cs \<in> derivable (initial_caps \<union> accessed_reg_caps s)"
and "is_indirect_sentry_method CC cs" and "is_sealed_method CC cs"
and "leq_cap CC c (unseal_method CC cs)"
and "name r \<in> IDC ISA - write_privileged_regs ISA"
shows "traces_enabled (write_reg r v) s"
using assms
by (intro traces_enabled_write_reg) auto
lemma traces_enabled_C_set_29:
assumes "c \<in> derivable_caps s"
shows "traces_enabled (C_set 29 c) s"
using assms
by (auto simp: C_set_def R_set_def register_defs derivable_caps_def
intro!: traces_enabled_write_reg)
lemma leq_cap_derivable_mem_caps:
assumes "c \<in> derivable_mem_caps s"
and "leq_cap CC c' c"
shows "c' \<in> derivable_mem_caps s"
using assms
by (auto simp: derivable_mem_caps_def leq_cap_def intro: derivable.Restrict)
lemma CapSquashPostLoadCap_invoked_cap[derivable_capsE]:
assumes "Run (CapSquashPostLoadCap c base) t c'"
and "CapIsTagSet c \<longrightarrow> mem_branch_caps c \<subseteq> invoked_caps"
and "CapIsTagSet c'"
shows "c' \<in> invoked_caps"
using assms
by (cases rule: CapSquashPostLoadCap_cases)
(auto simp: mem_branch_caps_def branch_caps_def CapIsSealed_def split: if_splits)
lemma traces_enabled_C_set_mem_cap:
assumes "Run (CapSquashPostLoadCap c base) t c'" "load_cap_trace_assms t"
and "VA_from_load_auth base"
and "c \<in> derivable_mem_caps s"
and "invokes_indirect_caps \<and> CapIsTagSet c' \<and> CapIsTagSet c \<longrightarrow> n = 29 \<and> mem_branch_caps c \<subseteq> invoked_caps"
shows "traces_enabled (C_set n c') s"
proof cases
assume indirect: "invokes_indirect_caps \<and> CapIsTagSet c'"
then have "load_caps_permitted"
using Run_CapSquashPostLoadCap_use_mem_caps[OF assms(1-3)]
by blast
from indirect have c: "CapIsTagSet c" and c': "c' \<in> derivable_mem_caps s"
using assms(1,4)
by (auto elim!: CapSquashPostLoadCap_cases leq_cap_derivable_mem_caps[of c s c'] intro: clear_perm_leq_cap)
then have "c' \<in> invoked_caps"
using assms(1,5) indirect
by (elim CapSquashPostLoadCap_invoked_cap) auto
then have "traces_enabled (write_reg R29_ref c') s"
using c c' assms indirect
by (intro traces_enabled_write_reg)
(auto simp: register_defs derivable_mem_caps_def intro: \<open>load_caps_permitted\<close>)
moreover have "n = 29"
using assms indirect c
by auto
ultimately show ?thesis
by (auto simp: C_set_def R_set_def)
next
assume "\<not>(invokes_indirect_caps \<and> CapIsTagSet c')"
then have "c' \<in> derivable_caps s"
using assms(1-4)
by (elim CapSquashPostLoadCap_from_load_auth_reg_derivable_caps) auto
then show ?thesis
by (auto simp: C_set_def R_set_def register_defs derivable_caps_def
intro!: traces_enabled_write_reg traces_enabled_bind non_cap_expI[THEN non_cap_exp_traces_enabledI])
qed
lemma enabled_branch_target_CapUnseal_mem_cap:
assumes "Run (CapSquashPostLoadCap c base) t c'" "load_cap_trace_assms t"
and "VA_from_load_auth base"
and "c \<in> derivable_mem_caps s"
and "CapIsTagSet c' \<and> CapIsTagSet c \<and> CapGetObjectType c' = CapGetObjectType c \<longrightarrow> CapGetObjectType c = CAP_SEAL_TYPE_RB \<and> mem_branch_caps c \<subseteq> invoked_caps"
shows "enabled_branch_target (CapUnseal c') s"
proof cases
assume tagged: "CapIsTagSet c'"
moreover have "c' \<in> derivable_mem_caps s"
using assms(1,4)
by (elim CapSquashPostLoadCap_cases leq_cap_derivable_mem_caps[of c s c']) (auto intro: clear_perm_leq_cap)
moreover have load_caps_permitted
using tagged assms(1-3)
by (elim Run_CapSquashPostLoadCap_use_mem_caps[OF _ _ _ _]) auto
ultimately have "c' \<in> derivable_mem_caps s \<and> invokes_indirect_caps \<or> c' \<in> derivable_caps s"
using assms(5) derivable_mem_caps_derivable_caps[of c' s]
unfolding derivable_caps_def
by (cases "invokes_indirect_caps") auto
moreover have "CapGetObjectType c' = CAP_SEAL_TYPE_RB \<and> branch_caps (CapUnseal c') \<subseteq> invoked_caps"
using assms(1,5) tagged
unfolding mem_branch_caps_def
by (elim CapSquashPostLoadCap_cases) (auto simp: CapIsSealed_def)
ultimately show ?thesis
using branch_caps_leq
unfolding enabled_branch_target_def enabled_pcc_def mem_branch_caps_def
by (auto intro: \<open>load_caps_permitted\<close>)
qed (auto intro: derivable_enabled_branch_target)
lemma CapSquashPostLoadCap_sealed_branch_caps_invoked_caps[derivable_capsE]:
assumes "Run (CapSquashPostLoadCap c base) t c'"
and "CapIsTagSet c'"
and "(c' = c \<or> c' = CapClearPerms c mutable_perms) \<longrightarrow> CapIsSealed c \<and> branch_caps (CapUnseal c) \<subseteq> invoked_caps"
shows "branch_caps (CapUnseal c') \<subseteq> invoked_caps"
using assms
by (cases rule: CapSquashPostLoadCap_cases) auto
lemma invokes_mem_cap_leq_enabled_pccI:
assumes "c' \<in> derivable_mem_caps s" and "leq_cap CC c c'"
and "c \<in> invoked_caps"
and "invokes_indirect_caps"
and "load_caps_permitted"
shows "enabled_pcc c s"
using assms
unfolding enabled_pcc_def
by blast
lemma VAIsBits64_iff_not_VAIsCapability:
"VAIsBits64 va \<longleftrightarrow> \<not>VAIsCapability va"
by (cases "VirtualAddress_vatype va") (auto simp: VAIsBits64_def VAIsCapability_def)
lemma enabled_branch_target_CapSquashPostLoadCap:
assumes "Run (CapSquashPostLoadCap c base) t c'" "load_cap_trace_assms t"
and "VA_from_load_auth base"
and "c \<in> derivable_mem_caps s"
and "(CapIsTagSet c \<and> \<not>CapIsSealed c \<and> invokes_indirect_caps) \<longrightarrow> mem_branch_caps c \<subseteq> invoked_caps"
shows "enabled_branch_target c' s"
proof (cases "invokes_indirect_caps \<and> CapIsTagSet c'")
case True
then have *: "invokes_indirect_caps" "load_caps_permitted"
using Run_CapSquashPostLoadCap_use_mem_caps[OF assms(1-3)]
by auto
note leqI = branch_caps_leq leq_cap_trans[OF branch_caps_leq clear_perm_leq_cap]
thm Run_CapSquashPostLoadCap_use_mem_caps
show ?thesis
using assms True
by (cases rule: CapSquashPostLoadCap_cases)
(auto simp: enabled_branch_target_def mem_branch_caps_def CapIsSealed_def
elim!: invokes_mem_cap_leq_enabled_pccI[OF _ _ _ *] leqI)
next
case False
then have "c' \<in> derivable_caps s"
using assms
by (cases "CapIsTagSet c'", elim CapSquashPostLoadCap_from_load_auth_reg_derivable_caps)
(auto simp: derivable_caps_def)
then show ?thesis
by (auto intro: derivable_enabled_branch_target)
qed
lemma clear_perm_derivable_mem_caps[derivable_capsI]:
assumes "c \<in> derivable_mem_caps s" and "CapIsTagSet c \<longrightarrow> \<not>CapIsSealed c"
shows "clear_perm perms c \<in> derivable_mem_caps s"
using assms
unfolding derivable_mem_caps_def
by (auto elim: clear_perm_derivable)
declare Run_ifE[where thesis = "c \<in> derivable_mem_caps s" and a = c for c s, derivable_caps_combinators]
declare Run_letE[where thesis = "c \<in> derivable_mem_caps s" and a = c for c s, derivable_caps_combinators]
declare Run_return_resultE[where P = "\<lambda>c. c \<in> derivable_mem_caps s" for s, derivable_caps_combinators]
declare Run_bindE'[where P = "\<lambda>t. c \<in> derivable_mem_caps (run s t)" for c s, simplified, derivable_caps_combinators]
declare Run_bindE[where thesis = "c \<in> derivable_mem_caps s" and a = c for c s, derivable_caps_combinators]
declare if_split[where P = "\<lambda>c. c \<in> derivable_mem_caps s" for s, THEN iffD2, derivable_capsI]
declare Run_case_prodE[where thesis = "c \<in> derivable_mem_caps s" and a = c for c s, derivable_caps_combinators]
lemma bind_derivable_caps[derivable_caps_combinators]:
assumes "Run (m \<bind> f) t a"
and "\<And>tm am tf. Run m tm am \<Longrightarrow> Run (f am) tf a \<Longrightarrow> t = tm @ tf \<Longrightarrow> c \<in> derivable_mem_caps (run (run s tm) tf)"
shows "c \<in> derivable_mem_caps (run s t)"
using assms
by (auto elim: Run_bindE)
lemma CapWithTagClear_derivable_mem_caps[intro, simp, derivable_capsI]:
"CapWithTagClear c \<in> derivable_mem_caps s"
by (auto simp: derivable_mem_caps_def)
lemma CapSquashPostLoadCap_derivable_mem_caps[derivable_capsE]:
assumes "Run (CapSquashPostLoadCap c base) t c'"
and "c \<in> derivable_mem_caps s"
shows "c' \<in> derivable_mem_caps s"
using assms
by (cases rule: CapSquashPostLoadCap_cases) (auto intro: clear_perm_derivable_mem_caps)
lemma CapabilityFromData_derivable_mem_caps[derivable_capsE]:
fixes s :: "(Capability, register_value) axiom_state"
shows "Run (CapabilityFromData n arg1 arg2) t c \<Longrightarrow> n = 128 \<Longrightarrow> Capability_of_tag_word (arg1 !! 0) arg2 \<in> derivable_mem_caps s \<Longrightarrow> c \<in> derivable_mem_caps s"
by (auto simp: CapabilityFromData_def)
(* Common patterns of capability/data conversions in memory access helpers *)
lemma Capability_of_tag_word_derivable_mem_caps_pairE[derivable_capsE]:
assumes "x = (tag, data)"
and "Capability_of_tag_word ((vec_of_bits [access_vec_dec (fst x) i] :: 1 word) !! 0) (slice (snd x) j 128) \<in> derivable_mem_caps s"
shows "Capability_of_tag_word ((vec_of_bits [access_vec_dec tag i] :: 1 word) !! 0) (slice data j 128) \<in> derivable_mem_caps s"
using assms
by auto
lemma Capability_of_tag_word_derivable_mem_caps_rev_pairE[derivable_capsE]:
assumes "x = (data, tag)"
and "Capability_of_tag_word ((vec_of_bits [access_vec_dec (snd x) i] :: 1 word) !! 0) (slice (fst x) j 128) \<in> derivable_mem_caps s"
shows "Capability_of_tag_word ((vec_of_bits [access_vec_dec tag i] :: 1 word) !! 0) (slice data j 128) \<in> derivable_mem_caps s"
using assms
by auto
declare Run_case_prodE[where thesis = "Capability_of_tag_word tag word \<in> derivable_mem_caps s" for tag word s, derivable_capsE]
declare Run_letE[where thesis = "Capability_of_tag_word tag word \<in> derivable_mem_caps s" for tag word s, derivable_capsE]
lemma Capability_of_tag_word_return_rev_derivable_mem_caps_pairE[derivable_capsE]:
assumes "Run (return (data, tag)) t x"
and "t = [] \<longrightarrow> Capability_of_tag_word ((vec_of_bits [access_vec_dec tag i] :: 1 word) !! 0) (slice data j 128) \<in> derivable_mem_caps s"
shows "Capability_of_tag_word ((vec_of_bits [access_vec_dec (snd x) i] :: 1 word) !! 0) (slice (fst x) j 128) \<in> derivable_mem_caps s"
using assms
by auto
lemma Capability_of_tag_word_False_derivable[intro, simp, derivable_capsI]:
"Capability_of_tag_word False data \<in> derivable_mem_caps s"
by (auto simp: derivable_mem_caps_def)
declare derivable_mem_caps_run_imp[derivable_caps_runI]
(* declare MemAtomicCompareAndSwapC_derivable[derivable_capsE del] *)
lemma MemAtomicCompareAndSwapC_from_load_auth_derivable_caps[derivable_capsE]:
assumes "Run (MemAtomicCompareAndSwapC vaddr address expectedcap newcap ldacctype stacctype) t c" and "inv_trace_assms s t"
and "VA_from_load_auth vaddr" and "\<not>invokes_indirect_caps"
shows "c \<in> derivable_caps (run s t)"
using assms
unfolding MemAtomicCompareAndSwapC_def
by - (derivable_capsI_with \<open>split_inv_trace_assms_append | solves \<open>accessible_regsI\<close>\<close>
elim: Run_ifE[where thesis = "Capability_of_tag_word ((vec_of_bits [access_vec_dec (snd x) i] :: 1 word) !! 0) (slice (fst x) j 128) \<in> derivable_mem_caps s" and a = x for x i j s])
lemma MemAtomicC_derivable_mem_caps[derivable_capsE]:
assumes "Run (MemAtomicC address op v ldacctype stacctype) t c"
shows "c \<in> derivable_mem_caps (run s t)"
using assms
unfolding MemAtomicC_def
by - (derivable_capsI elim: Run_ifE[where thesis = "Capability_of_tag_word ((vec_of_bits [access_vec_dec (snd x) i] :: 1 word) !! 0) (slice (fst x) j 128) \<in> derivable_mem_caps s" and a = x for x i j s])
lemma traces_enabled_C_set_if_sentry:
fixes c :: Capability and n :: int
assumes "indirect_sentry \<and> CapIsTagSet c \<longrightarrow> n = 29 \<and> CapGetObjectType c = CAP_SEAL_TYPE_LB \<and> c \<in> derivable_caps s \<and> CapUnseal c \<in> invoked_indirect_caps"
and "indirect_sentry \<and> \<not>CapIsTagSet c \<longrightarrow> traces_enabled (C_set n (CapUnseal c)) s"
and "\<not>indirect_sentry \<longrightarrow> traces_enabled (C_set n c) s"
shows "traces_enabled (C_set n (if indirect_sentry then CapUnseal c else c)) s"
proof cases
assume *: "indirect_sentry \<and> CapIsTagSet c"
then have "c \<in> derivable (UNKNOWN_caps \<union> accessed_reg_caps s)"
using assms
unfolding derivable_caps_def accessed_caps_def
by (auto split: if_splits)
then show ?thesis
using assms *
unfolding C_set_def R_set_def
by (auto simp: register_defs is_indirect_sentry_def derivable_caps_def CapIsSealed_def
intro!: traces_enabled_write_IDC_sentry split: if_splits)
next
assume "\<not>(indirect_sentry \<and> CapIsTagSet c)"
then show ?thesis
using assms(2,3)
by auto
qed
(* declare Run_ifE[where thesis = "CapUnseal c \<in> invoked_caps" and a = c for c, derivable_caps_combinators] *)
lemma Run_CSP_or_C_read_invoked_indirect_caps:
assumes "Run (if n = 31 then csp_read else C_read n) t c"
and "n \<noteq> 31"
and "Run (C_read n) t c \<longrightarrow> CapUnseal c \<in> invoked_indirect_caps"
shows "CapUnseal c \<in> invoked_indirect_caps"
using assms
by auto
lemma traces_enabled_BranchToCapability[traces_enabledI]:
assumes "enabled_branch_target c s"
shows "traces_enabled (BranchToCapability c branch_type) s"
unfolding BranchToCapability_def
by (traces_enabledI assms: assms intro: traces_enabled_PCC_set non_cap_expI[THEN non_cap_exp_traces_enabledI] simp: BranchTaken_ref_def PSTATE_ref_def PC_ref_def)
lemma enabled_branch_target_set_0th[derivable_capsI]:
assumes "enabled_branch_target c s"
shows "enabled_branch_target (update_vec_dec c 0 (Morello.Bit 0)) s"
using assms
by (auto simp: enabled_branch_target_def branch_caps_def CapGetValue_def nth_ucast test_bit_set_gen)
lemma traces_enabled_BranchXToCapability[traces_enabledI]:
assumes "enabled_branch_target c s"
shows "traces_enabled (BranchXToCapability c branch_type) s"
unfolding BranchXToCapability_def
by (traces_enabledI assms: assms intro: non_cap_expI[THEN non_cap_exp_traces_enabledI] simp: PSTATE_ref_def)
text \<open>Sealing and unsealing\<close>
lemma CapSetObjectType_derivable[derivable_capsI]:
assumes "c \<in> derivable_caps s" and "c' \<in> derivable_caps s"
and "CapIsTagSet c" and "CapIsTagSet c'"
and "\<not>CapIsSealed c" and "\<not>CapIsSealed c'"
and "cap_permits CAP_PERM_SEAL c'"
and "unat (CapGetValue c') \<in> get_mem_region CC c'"
shows "CapSetObjectType c (CapGetValue c') \<in> derivable_caps s"
proof -
from assms have "permits_seal_method CC c'"
by (auto simp: CC_def)
then have "seal_method CC c (get_cursor_method CC c') \<in> derivable (UNKNOWN_caps \<union> accessed_caps (invoked_indirect_caps = {} \<and> load_caps_permitted) s)"
using assms
by (intro derivable.Seal) (auto simp: derivable_caps_def)
then show ?thesis
by (auto simp: seal_def derivable_caps_def)
qed
lemma CapSetObjectType_sentry_derivable:
assumes "c \<in> derivable_caps s"
and "\<not>CapIsSealed c"
and "otype \<in> {CAP_SEAL_TYPE_RB, CAP_SEAL_TYPE_LPB, CAP_SEAL_TYPE_LB}"
shows "CapSetObjectType c otype \<in> derivable_caps s"
proof -
note simps = CapGetObjectType_CapSetObjectType_and_mask
have "seal_method CC c (unat otype) \<in> derivable (UNKNOWN_caps \<union> accessed_caps (invoked_indirect_caps = {} \<and> load_caps_permitted) s)"
if "CapIsTagSet c"
using that assms
by (intro derivable.SealEntry)
(auto simp: is_sentry_def is_indirect_sentry_def seal_def derivable_caps_def simps and_mask_bintr)
then show ?thesis
by (auto simp: seal_def derivable_caps_def)
qed
lemma CapSetObjectType_sentries_derivable[derivable_capsI]:
assumes "c \<in> derivable_caps s"
and "\<not>CapIsSealed c"
shows "CapSetObjectType c CAP_SEAL_TYPE_RB \<in> derivable_caps s"
and "CapSetObjectType c CAP_SEAL_TYPE_LPB \<in> derivable_caps s"
and "CapSetObjectType c CAP_SEAL_TYPE_LB \<in> derivable_caps s"
using assms
by (auto intro: CapSetObjectType_sentry_derivable)
lemma CapIsInBounds_cursor_in_mem_region:
assumes "Run (CapIsInBounds c) t a" and "a"
shows "unat (CapGetValue c) \<in> get_mem_region CC c"
using assms
unfolding CapIsInBounds_def get_mem_region_def
by (auto simp: CapGetBounds_get_base CapGetBounds_get_limit elim!: Run_bindE)
abbreviation check_global_perm :: "Capability \<Rightarrow> Capability \<Rightarrow> Capability" where
"check_global_perm c auth \<equiv>
(if \<not>cap_permits CAP_PERM_GLOBAL auth then clear_perm CAP_PERM_GLOBAL c else c)"
lemma CapUnseal_check_global_derivable:
assumes "cap_permits CAP_PERM_UNSEAL auth"
and "c \<in> derivable_caps s" and "auth \<in> derivable_caps s"
and "CapIsTagSet auth"
and "CapIsSealed c" and "\<not>CapIsSealed auth"