-
Notifications
You must be signed in to change notification settings - Fork 0
/
ExampleSystemPolicyFlows.thy
272 lines (236 loc) · 10.8 KB
/
ExampleSystemPolicyFlows.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
(*
* Copyright 2014, NICTA
*
* This software may be distributed and modified according to the terms of
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
* See "LICENSE_GPLv2.txt" for details.
*
* @TAG(NICTA_GPL)
*)
theory ExampleSystemPolicyFlows
imports
Noninterference
"../access-control/ExampleSystem"
begin
subsection {* Example 1 -- similar to Sys1 in ../access-control/ExampleSystem.thy *}
subsubsection {* Definitions *}
datatype Sys3Labels = UT3 | T3 | EP3 | IRQ3
definition Sys3AuthGraph_aux :: "Sys3Labels subject_label auth_graph"
where
"Sys3AuthGraph_aux \<equiv>
{ (OrdinaryLabel (UT3), auth.SyncSend, OrdinaryLabel (EP3)),
(OrdinaryLabel (UT3), auth.Reset, OrdinaryLabel (EP3)),
(OrdinaryLabel (T3), auth.Receive, OrdinaryLabel (EP3)),
(OrdinaryLabel (T3), auth.Reset, OrdinaryLabel (EP3)) }"
definition Sys3AuthGraph :: "Sys3Labels subject_label auth_graph"
where
"Sys3AuthGraph \<equiv> complete_AuthGraph Sys3AuthGraph_aux {OrdinaryLabel (T3),
OrdinaryLabel (UT3)}"
definition Sys3PolicyFlows :: "(Sys3Labels partition \<times> Sys3Labels partition) set"
where
"Sys3PolicyFlows \<equiv>
{ (Partition UT3, Partition UT3),
(Partition UT3, Partition EP3),
(Partition UT3, Partition T3),
(Partition T3, Partition T3),
(Partition T3, Partition UT3),
(Partition T3, Partition EP3),
(Partition EP3, Partition UT3),
(Partition EP3, Partition EP3),
(Partition EP3, Partition T3),
(Partition IRQ3, Partition IRQ3),
(PSched, Partition EP3),
(PSched, Partition UT3),
(PSched, Partition T3),
(PSched, Partition IRQ3),
(PSched, PSched) }"
subsubsection {* Generalisations *}
definition Sys3Reads where
"Sys3Reads \<equiv> { (OrdinaryLabel (UT3)), (OrdinaryLabel (EP3)), (OrdinaryLabel (T3)) }"
definition Sys3Affects where
"Sys3Affects \<equiv> { (OrdinaryLabel (UT3)), (OrdinaryLabel (EP3)), (OrdinaryLabel (T3)) }"
lemma Sys3Reads_correct_fw : "\<lbrakk>x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (l)); l \<in> {T3, UT3, EP3}\<rbrakk> \<Longrightarrow> x \<in> Sys3Reads"
apply (induct x rule:subjectReads.induct)
apply (auto simp:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def)
done
lemma Sys3Affects_correct_fw : "\<lbrakk>x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (l)); l \<in> {T3, UT3}\<rbrakk> \<Longrightarrow> x \<in> Sys3Affects"
apply (induct x rule:subjectAffects.induct)
apply (auto simp:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Affects_def)
done
subsubsection {* UT3 *}
lemma Sys3UT3Reads_correct_bw : "x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (UT3))"
apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def)
apply (erule disjE)
(* UT3 reads UT3 *)
apply (simp add: reads_lrefl)
(* UT3 reads EP3 *)
apply (erule disjE)
apply (rule_tac auth = SyncSend in reads_ep)
apply (simp)
apply (simp add:insertI1)
(* UT3 reads T3 *)
apply (rule_tac auth = SyncSend and ep = "OrdinaryLabel (EP3)" and a = "OrdinaryLabel (UT3)" in read_sync_ep_read_receivers)
apply (simp)
apply (simp)
apply (rule_tac auth = SyncSend in reads_ep)
apply (simp)
apply (rule insertI1)
apply (simp add: insertI1)
done
lemma Sys3UT3Affects_correct_bw : "x \<in> Sys3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (UT3))"
apply (simp add:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Affects_def)
apply (erule disjE)
(* UT3 affects UT3 *)
apply (simp add:affects_lrefl)
(* UT3 affects EP3 *)
apply (erule disjE)
apply (rule_tac auth=SyncSend in affects_ep)
apply simp
apply (simp add:insertI1)
(* UT3 affects T3 *)
apply (rule_tac auth=SyncSend and l' = "OrdinaryLabel (T3)" and ep="OrdinaryLabel (EP3)" in affects_send)
apply (simp_all add:insertI1)
done
subsubsection {* T3 *}
lemma Sys3T3Reads_correct_bw : "x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (T3))"
apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def)
apply (erule disjE)
(* T3 reads UT3 *)
apply (rule_tac auth = Receive and ep = "OrdinaryLabel (EP3)" and a = "OrdinaryLabel (T3)" in read_sync_ep_read_senders)
apply (simp)
apply (simp)
apply (rule_tac auth = Receive in reads_ep)
apply (simp)
apply (simp add:insertI1)
apply (simp add: insertI1)
(* T3 reads EP3 *)
apply (erule disjE)
apply (rule_tac auth = Receive in reads_ep)
apply (simp)
apply (simp add:insertI1)
(* T3 reads T3 *)
apply (simp add: reads_lrefl)
done
lemma Sys3T3Affects_correct_bw : "x \<in> Sys3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (T3))"
apply (simp add:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Affects_def)
apply (erule disjE)
(* T3 affects UT3 *)
apply simp
apply (rule_tac l = "OrdinaryLabel (T3)" and l' = "OrdinaryLabel (UT3)" and ep="OrdinaryLabel (EP3)" in affects_recv)
apply (simp_all add:insertI1)
(* T3 affects EP3 *)
apply (erule disjE)
apply (rule_tac auth=Receive in affects_ep)
apply simp
apply (simp add:insertI1)
(* T3 affects T3 *)
apply (simp add:affects_lrefl)
done
subsubsection {* EP3 *}
definition Sys3EP3Affects :: "(Sys3Labels subject_label) set"
where
"Sys3EP3Affects \<equiv> { OrdinaryLabel (EP3) }"
lemma Sys3EP3Reads_correct_bw : "x \<in> Sys3Reads \<Longrightarrow> x \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (EP3))"
apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3Reads_def)
apply (erule disjE)
(* EP3 reads UT3 *)
apply simp
apply (rule_tac a = "OrdinaryLabel (T3)" and auth=Receive and ep = "OrdinaryLabel (EP3)" and b = "OrdinaryLabel (UT3)" in read_sync_ep_read_senders)
apply (simp)
apply (simp add:insertI1)
apply (simp add:reads_lrefl)
apply simp
(* EP3 reads EP3 *)
apply (erule disjE)
apply (simp add: reads_lrefl)
(* EP3 reads T3 *)
apply (rule_tac a = "OrdinaryLabel (UT3)" and auth = SyncSend and ep = "OrdinaryLabel (EP3)" and a = "OrdinaryLabel (T3)" in read_sync_ep_read_receivers)
apply (simp_all add:reads_lrefl)
done
lemma Sys3EP3Affects_correct_fw : "x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (EP3)) \<Longrightarrow> x \<in> Sys3EP3Affects"
apply (induct x rule:subjectAffects.induct)
apply (auto simp:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3EP3Affects_def)
done
lemma Sys3EP3Affects_correct_bw : "x \<in> Sys3EP3Affects \<Longrightarrow> x \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (EP3))"
by (simp add:Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def Sys3EP3Affects_def affects_lrefl)
lemma Sys3EP3Affects_correct : "subjectAffects Sys3AuthGraph (OrdinaryLabel (EP3)) = Sys3EP3Affects"
apply (rule subset_antisym)
apply (simp_all add:subsetI Sys3EP3Affects_correct_fw Sys3EP3Affects_correct_bw)
done
subsubsection {* Generalisations pt2 *}
lemma Sys3Reads_correct : "l \<in> {T3, UT3, EP3} \<Longrightarrow> subjectReads Sys3AuthGraph (OrdinaryLabel (l)) = Sys3Reads"
by (auto simp:subsetI Sys3Reads_correct_fw Sys3UT3Reads_correct_bw Sys3T3Reads_correct_bw Sys3EP3Reads_correct_bw)
lemma Sys3Affects_correct : "l \<in> {T3, UT3} \<Longrightarrow> subjectAffects Sys3AuthGraph (OrdinaryLabel (l)) = Sys3Affects"
by (auto simp:subsetI Sys3Affects_correct_fw Sys3UT3Affects_correct_bw Sys3T3Affects_correct_bw)
subsubsection {* IRQ3 *}
lemma IRQ3Reads : " d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (IRQ3)) \<Longrightarrow> d = OrdinaryLabel (IRQ3)"
apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def)
apply (induct d rule: subjectReads.induct, auto)
done
lemma IRQ3Affects : "d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (IRQ3)) \<Longrightarrow> d = OrdinaryLabel (IRQ3)"
apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def)
apply (induct d rule: subjectAffects.induct, auto)
done
lemma IRQ3ReadsAndAffects :
"\<lbrakk> d \<in> subjectAffects Sys3AuthGraph (OrdinaryLabel (l))
; d \<in> subjectReads Sys3AuthGraph (OrdinaryLabel (IRQ3))
\<rbrakk> \<Longrightarrow> l = IRQ3"
apply (drule IRQ3Reads)
apply (simp add: Sys3AuthGraph_def Sys3AuthGraph_aux_def complete_AuthGraph_def)
apply (erule subjectAffects.cases, auto)
done
subsubsection {* Policy flows *}
lemma Sys3_policyFlows_correct_fw : "(a,b) \<in> policyFlows Sys3AuthGraph \<Longrightarrow> (a,b) \<in> Sys3PolicyFlows"
apply (induct a b rule:policyFlows.induct)
apply (simp add:partsSubjectAffects_def label_can_affect_partition_def)
(* Partition l *)
apply (erule imageE)
apply simp
apply (case_tac "x \<in> {T3, UT3, EP3}")
(* x in {T3, UT3, EP3} *)
apply (simp add:Sys3Reads_correct Sys3Reads_def)
apply (case_tac "l \<in> {T3, UT3}")
(* l in {T3, UT3} *)
apply (simp add:Sys3Affects_correct Sys3Affects_def Sys3PolicyFlows_def)
apply (erule exE)
apply ((erule disjE)+, simp, simp, simp)+
(* l not in {T3, UT3} *)
apply (simp)
apply (case_tac l)
apply (simp, simp, simp)
apply (auto simp:Sys3PolicyFlows_def)[1]
apply (simp add:Sys3PolicyFlows_def)
apply (erule exE)
apply (erule conjE, drule IRQ3Affects)
apply (blast)
(* x not in {T3, UT3, EP3} *)
apply (case_tac x)
apply (simp, simp, simp, simp)
apply (erule exE)
apply (erule conjE)
apply (frule IRQ3ReadsAndAffects, assumption)
apply (simp add: Sys3PolicyFlows_def)
(* PSched *)
apply (case_tac d, simp add: Sys3PolicyFlows_def)
apply (rename_tac a)
apply (case_tac a)
apply (auto simp: Sys3PolicyFlows_def)
done
lemma Sys3_policyFlows_correct_bw : "(a,b) \<in> Sys3PolicyFlows \<Longrightarrow> (a,b) \<in> policyFlows Sys3AuthGraph"
apply (simp add:Sys3PolicyFlows_def)
(* All UT3/T3 cases *)
apply (erule disjE, simp, rule policy_affects, simp add: partsSubjectAffects_def label_can_affect_partition_def, rule imageI, simp add: Sys3Affects_correct Sys3Reads_correct Sys3Affects_def Sys3Reads_def, blast)+
(* All EP3 cases *)
apply (erule disjE,simp, rule policy_affects, simp add: partsSubjectAffects_def label_can_affect_partition_def, rule imageI, simp add: Sys3EP3Affects_correct Sys3Reads_correct Sys3Reads_def Sys3EP3Affects_def)+
(* IRQ3 case *)
apply (rule_tac x = "OrdinaryLabel (IRQ3)" in exI)
apply (rule conjI)
apply (rule affects_lrefl)
apply (rule reads_lrefl)
(* All PSched cases *)
apply (erule disjE, simp add: PSched_flows_to_all)+
apply (simp add: PSched_flows_to_all)
done
lemma Sys3_policyFlows_correct : "policyFlows Sys3AuthGraph = Sys3PolicyFlows"
by (auto simp:Sys3_policyFlows_correct_fw Sys3_policyFlows_correct_bw)
end