-
Notifications
You must be signed in to change notification settings - Fork 0
/
ROOT
223 lines (192 loc) · 4.59 KB
/
ROOT
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
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
chapter "Proofs"
(*
* List of rules to make various images.
*
* Some rules have duplicate targets of the form:
*
* theories [condition = "MOO", quick_and_dirty]
* "foo"
* theories
* "foo"
*
* The idea is that if the environment variable "MOO" is defined we
* execute the first rule (doing the proof in quick-and-dirty mode), and
* then find we need not take any action for the second. Otherwise, we
* skip the first rule and only perform the second.
*)
(*
* Refinement proof.
*)
session Refine in "refine" = BaseRefine +
description \<open>Refinement between Haskell and Abstract spec.\<close>
sessions
Lib
CorresK
AInvs
directories
"$L4V_ARCH"
theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
"$L4V_ARCH/Refine"
"$L4V_ARCH/RAB_FN"
"$L4V_ARCH/EmptyFail_H"
theories [condition = "SKIP_REFINE_PROOFS", quick_and_dirty, skip_proofs]
"$L4V_ARCH/Refine"
"$L4V_ARCH/RAB_FN"
"$L4V_ARCH/EmptyFail_H"
theories
"$L4V_ARCH/Refine"
"$L4V_ARCH/RAB_FN"
"$L4V_ARCH/EmptyFail_H"
(*
* This theory is in a separate session because the proofs currently
* only work for ARM.
*)
session RefineOrphanage in "refine/$L4V_ARCH/orphanage" = Refine +
description \<open>Proof that the kernel does not orphan threads.\<close>
theories
"Orphanage"
session BaseRefine in "refine/base" = AInvs +
description \<open>Background theory and libraries for refinement proof.\<close>
sessions
Lib
CorresK
theories
"Include"
session AInvs in "invariant-abstract" = ASpec +
directories
"$L4V_ARCH"
theories [condition = "SKIP_AINVS_PROOFS", quick_and_dirty, skip_proofs]
"KernelInit_AI"
"$L4V_ARCH/ArchDetSchedSchedule_AI"
theories [condition = "AINVS_QUICK_AND_DIRTY", quick_and_dirty]
"KernelInit_AI"
"$L4V_ARCH/ArchDetSchedSchedule_AI"
theories
"KernelInit_AI"
"$L4V_ARCH/ArchDetSchedSchedule_AI"
(*
* C Refinement proof.
*)
session CRefineSyscall in "crefine/intermediate" = CBaseRefine +
sessions
CRefine
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
"Intermediate_C"
theories
"Intermediate_C"
session CRefine in "crefine" = CBaseRefine +
directories
"lib"
"$L4V_ARCH"
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
"Refine_C"
theories
"Refine_C"
session CBaseRefine in "crefine/base" = CSpec +
sessions
CLib
Refine
AutoCorres
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
(* crefine/lib/AutoCorres_C explains why L4VerifiedLinks is included here. *)
"L4VerifiedLinks"
"Include_C"
theories
"L4VerifiedLinks"
"Include_C"
session AutoCorresCRefine in "crefine/autocorres-test" = CRefine +
theories
"AutoCorresTest"
(*
* CapDL Refinement
*)
session DBaseRefine in "drefine/base" = AInvs +
sessions
DSpec
theories
"Include_D"
session DRefine in "drefine" = DBaseRefine +
theories
"Refine_D"
session DPolicy in "dpolicy" = DRefine +
sessions
Access
theories
"Dpolicy"
(*
* Infoflow and Access
*)
session Access in "access-control" = AInvs +
theories
"ADT_AC"
"ExampleSystem"
session InfoFlow in "infoflow" = Access +
theories
"InfoFlow_Image_Toplevel"
session InfoFlowCBase in "infoflow/refine/base" = CRefine +
sessions
Refine
Access
InfoFlow
theories [condition = "SKIP_DUPLICATED_PROOFS", quick_and_dirty, skip_proofs]
"Include_IF_C"
theories
"Include_IF_C"
session InfoFlowC in "infoflow/refine" = InfoFlowCBase +
theories
"Noninterference_Refinement"
"Example_Valid_StateH"
(*
* capDL
*)
session SepDSpec in "sep-capDL" = DSpec +
sessions
Sep_Algebra
SepTactics
theories
"Frame_SD"
session DSpecProofs in "capDL-api" = SepDSpec +
sessions
AInvs
theories
"Sep_Tactic_Examples"
"API_DP"
(*
* Static Separation Kernel Bisimilarity
*)
session Bisim in bisim = AInvs +
sessions
ASepSpec
theories
"Syscall_S"
document_files
"root.tex"
"build"
"Makefile"
(*
* Binary Verification Input Step
*)
session SimplExportAndRefine in "asmrefine" = SimplExport +
sessions
SimplExport
theories
"SEL4GraphRefine"
session SimplExport in "asmrefine/export" = CSpec +
theories
"SEL4SimplExport"
(*
* Libraries
*)
(* unused:
session AutoLevity = AutoLevity_Base +
theories
"../lib/autolevity_buckets/AutoLevity_Top"
session AutoLevity_Base = Word_Lib +
theories
"../lib/autolevity_buckets/AutoLevity_Base"
*)