1
+ − 1
theory Dynamic2static
32
+ − 2
imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop
1
+ − 3
begin
+ − 4
+ − 5
context tainting_s begin
+ − 6
+ − 7
lemma d2s_main:
+ − 8
"valid s \<Longrightarrow> s2ss s \<in> static"
+ − 9
apply (induct s, simp add:s2ss_nil_prop s_init)
+ − 10
apply (frule vd_cons, simp)
+ − 11
apply (case_tac a, simp_all)
+ − 12
(*
+ − 13
apply
+ − 14
induct s, case tac e, every event analysis
+ − 15
*)
31
+ − 16
thm s2ss_def
+ − 17
+ − 18
1
+ − 19
sorry
+ − 20
+ − 21
lemma d2s_main':
+ − 22
"\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
19
+ − 23
by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
1
+ − 24
+ − 25
lemma alive_has_sobj:
+ − 26
"\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
+ − 27
sorry
+ − 28
+ − 29
lemma t2ts:
+ − 30
"obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
19
+ − 31
apply (frule tainted_in_current, frule tainted_is_valid)
1
+ − 32
apply (simp add:s2ss_def)
+ − 33
apply (case_tac sobj, simp_all)
19
+ − 34
apply (case_tac [!] obj, simp_all split:option.splits if_splits)
1
+ − 35
apply (rule_tac x = "O_proc nat" in exI, simp)
+ − 36
apply (rule_tac x = "O_file list" in exI, simp)
19
+ − 37
apply (drule dir_not_tainted, simp)
+ − 38
apply (drule msgq_not_tainted, simp)
+ − 39
apply (drule shm_not_tainted, simp)
1
+ − 40
apply (case_tac prod1, simp, case_tac prod2, clarsimp)
+ − 41
apply (rule conjI)
+ − 42
apply (rule_tac x = "O_msgq nat1" in exI, simp)
19
+ − 43
apply (rule conjI) defer
+ − 44
apply (simp add:cm2smsg_def split:option.splits)
+ − 45
sorry
1
+ − 46
+ − 47
lemma delq_imp_delqm:
+ − 48
"deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"
+ − 49
apply (induct s, simp)
+ − 50
by (case_tac a, auto)
+ − 51
+ − 52
theorem static_complete:
+ − 53
assumes undel: "undeletable obj" and tbl: "taintable obj"
+ − 54
shows "taintable_s obj"
+ − 55
proof-
+ − 56
from tbl obtain s where tainted: "obj \<in> tainted s"
+ − 57
by (auto simp:taintable_def)
19
+ − 58
hence vs: "valid s" by (simp add:tainted_is_valid)
1
+ − 59
hence static: "s2ss s \<in> static" using d2s_main by auto
+ − 60
from tainted have alive: "alive s obj"
19
+ − 61
using tainted_in_current by auto
1
+ − 62
then obtain sobj where sobj: "co2sobj s obj = Some sobj"
+ − 63
using vs alive_has_sobj by blast
+ − 64
from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj"
+ − 65
by (auto simp:undeletable_def)
+ − 66
with vs sobj have "init_obj_related sobj obj"
+ − 67
apply (case_tac obj, case_tac [!] sobj)
19
+ − 68
apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
+ − 69
apply (frule not_deleted_init_file, simp+) (*
+ − 70
apply (drule is_file_has_sfile, erule exE)
1
+ − 71
apply (rule_tac x = sf in bexI)
+ − 72
apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1]
19
+ − 73
apply (simp add:same_inode_files_def cfs2sfiles_def) *)
+ − 74
sorry
1
+ − 75
with tainted t2ts init_alive sobj static
+ − 76
show ?thesis unfolding taintable_s_def
+ − 77
apply (rule_tac x = "s2ss s" in bexI, simp)
+ − 78
apply (rule_tac x = "sobj" in exI, auto)
+ − 79
done
+ − 80
qed
+ − 81
19
+ − 82
lemma cp2sproc_pi:
+ − 83
"\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs"
+ − 84
by (simp add:cp2sproc_def split:option.splits if_splits)
+ − 85
+ − 86
lemma cq2smsgq_qi:
+ − 87
"\<lbrakk>cq2smsgq s q = Some (Init q', sec, sms); valid s\<rbrakk> \<Longrightarrow> q = q' \<and> \<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs"
+ − 88
by (simp add:cq2smsgq_def split:option.splits if_splits)
+ − 89
+ − 90
lemma cm2smsg_mi:
+ − 91
"\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk>
+ − 92
\<Longrightarrow> m = m' \<and> \<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs"
+ − 93
by (clarsimp simp add:cm2smsg_def split:if_splits option.splits)
+ − 94
+ − 95
lemma ch2sshm_hi:
+ − 96
"\<lbrakk>ch2sshm s h = Some (Init h', sec); valid s\<rbrakk> \<Longrightarrow> h = h' \<and> \<not> deleted (O_shm h) s \<and> h \<in> init_shms"
+ − 97
by (clarsimp simp:ch2sshm_def split:if_splits option.splits)
+ − 98
+ − 99
lemma root_not_deleted:
+ − 100
"\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False"
+ − 101
apply (induct s, simp)
+ − 102
apply (frule vd_cons, frule vt_grant_os, case_tac a, auto)
+ − 103
done
+ − 104
+ − 105
lemma cf2sfile_fi:
+ − 106
"\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and>
+ − 107
(if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f
+ − 108
else \<not> deleted (O_dir f) s \<and> is_init_dir f)"
+ − 109
apply (case_tac f)
+ − 110
by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted
+ − 111
split:if_splits option.splits)
+ − 112
1
+ − 113
lemma init_deled_imp_deled_s:
+ − 114
"\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj"
19
+ − 115
apply (rule notI)
+ − 116
apply (clarsimp simp:s2ss_def)
+ − 117
apply (case_tac obj, case_tac [!] obja, case_tac sobj)
20
+ − 118
apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
+ − 119
apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def
+ − 120
split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
19
+ − 121
done
1
+ − 122
+ − 123
lemma deleted_imp_deletable_s:
+ − 124
"\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"
+ − 125
apply (simp add:deletable_s_def)
+ − 126
apply (rule_tac x = "s2ss s" in bexI)
+ − 127
apply (clarify, simp add:init_deled_imp_deled_s)
+ − 128
apply (erule d2s_main)
+ − 129
done
+ − 130
+ − 131
theorem undeletable_s_complete:
+ − 132
assumes undel_s: "undeletable_s obj"
+ − 133
shows "undeletable obj"
+ − 134
proof-
+ − 135
from undel_s have init_alive: "init_alive obj"
+ − 136
and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj"
+ − 137
using undeletable_s_def by auto
+ − 138
have "\<not> (\<exists> s. valid s \<and> deleted obj s)"
+ − 139
proof
+ − 140
assume "\<exists> s. valid s \<and> deleted obj s"
+ − 141
then obtain s where vs: "valid s" and del: "deleted obj s" by auto
+ − 142
from vs have vss: "s2ss s \<in> static" by (rule d2s_main)
+ − 143
with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)"
+ − 144
and related: "init_obj_related sobj obj" by auto
+ − 145
from init_alive del vs have "deletable_s obj"
+ − 146
by (auto elim:deleted_imp_deletable_s)
+ − 147
with alive_s
+ − 148
show False by (auto simp:deletable_s_def)
+ − 149
qed
+ − 150
with init_alive show ?thesis
+ − 151
by (simp add:undeletable_def)
+ − 152
qed
+ − 153
+ − 154
theorem final_offer:
+ − 155
"\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"
+ − 156
apply (erule swap)
+ − 157
by (simp add:static_complete undeletable_s_complete)
+ − 158
+ − 159
+ − 160
+ − 161
(************** static \<rightarrow> dynamic ***************)
+ − 162
+ − 163
lemma created_can_have_many:
+ − 164
"\<lbrakk>valid s; alive s obj; \<not> init_alive obj\<rbrakk> \<Longrightarrow> \<exists> s'. valid s' \<and> alive s' obj \<and> alive s' obj' \<and> s2ss s = s2ss s'"
+ − 165
sorry
+ − 166
+ − 167
lemma s2d_main:
+ − 168
"ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
+ − 169
apply (erule static.induct)
+ − 170
apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)
+ − 171
+ − 172
apply (erule exE|erule conjE)+
+ − 173
20
+ − 174
sorry
+ − 175
+ − 176
lemma tainted_s_in_ss:
+ − 177
"tainted_s ss sobj \<Longrightarrow> sobj \<in> ss"
+ − 178
apply (case_tac sobj, simp_all)
+ − 179
apply (case_tac bool, simp+)
+ − 180
apply (case_tac bool, simp+)
+ − 181
apply (case_tac prod1, case_tac prod2, simp)
+ − 182
thm tainted_s.simps
+ − 183
oops
+ − 184
+ − 185
lemma set_eq_D:
+ − 186
"\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"
+ − 187
by auto
+ − 188
+ − 189
lemma cqm2sms_prop1:
+ − 190
"\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
+ − 191
apply (induct queue arbitrary:sms)
+ − 192
apply (auto split:option.splits)
+ − 193
done
1
+ − 194
20
+ − 195
lemma sq_sm_prop:
+ − 196
"\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk>
+ − 197
\<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"
+ − 198
by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)
+ − 199
+ − 200
lemma tainted_s_imp_tainted:
+ − 201
"\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+ − 202
apply (drule s2d_main)
+ − 203
apply (erule exE, erule conjE, simp add:s2ss_def)
+ − 204
apply (rule_tac x = s in exI, simp)
+ − 205
apply (case_tac sobj, simp_all)
+ − 206
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
+ − 207
apply (rule_tac x = obj in exI, simp)
+ − 208
apply (case_tac obj, (simp split:option.splits if_splits)+)
+ − 209
+ − 210
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
+ − 211
apply (rule_tac x = obj in exI, simp)
+ − 212
apply (case_tac obj, (simp split:option.splits if_splits)+)
+ − 213
+ − 214
apply (case_tac prod1, case_tac prod2, simp)
+ − 215
apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+)
+ − 216
apply (case_tac obj, simp_all split:option.splits if_splits)
+ − 217
apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)
+ − 218
apply (rule_tac x = "O_msg nat m" in exI)
21
+ − 219
apply (simp add:cm2smsg_def split:option.splits)
+ − 220
done
1
+ − 221
20
+ − 222
lemma has_inode_tainted_aux:
+ − 223
"O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"
+ − 224
apply (erule tainted.induct)
+ − 225
apply (auto intro:tainted.intros simp:has_same_inode_def)
+ − 226
(*?? need simpset for tainted *)
1
+ − 227
sorry
+ − 228
20
+ − 229
lemma has_same_inode_tainted:
+ − 230
"\<lbrakk>has_same_inode s f f'; O_file f' \<in> tainted s\<rbrakk> \<Longrightarrow> O_file f \<in> tainted s"
+ − 231
by (drule has_inode_tainted_aux, auto simp:has_same_inode_def)
1
+ − 232
+ − 233
theorem static_sound:
+ − 234
assumes tbl_s: "taintable_s obj"
+ − 235
shows "taintable obj"
+ − 236
proof-
+ − 237
from tbl_s obtain ss sobj where static: "ss \<in> static"
+ − 238
and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj"
+ − 239
and init_alive: "init_alive obj" by (auto simp:taintable_s_def)
+ − 240
from static sobj tainted_s_imp_tainted
20
+ − 241
obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj"
+ − 242
and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast
1
+ − 243
20
+ − 244
from co2sobj related vs
+ − 245
have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')"
+ − 246
apply (case_tac obj', case_tac [!] obj)
+ − 247
apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)
+ − 248
apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def
+ − 249
split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)
+ − 250
done
+ − 251
with tainted' have tainted: "obj \<in> tainted s"
+ − 252
by (auto intro:has_same_inode_tainted)
+ − 253
with vs init_alive
1
+ − 254
show ?thesis by (auto simp:taintable_def)
+ − 255
qed
+ − 256
+ − 257
+ − 258
+ − 259
lemma ts2t:
+ − 260
"obj \<in> tainted_s ss \<Longrightarrow> \<exists> s. obj \<in> tainted s"
+ − 261
"obj \<in> tainted_s ss \<Longrightarrow> \<exists> so. so True \<in> ss \<Longrightarrow> so True \<in> ss \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<Longrightarrow> so True \<in> s2ss s \<Longrightarrow> tainted s obj. "
+ − 262
+ − 263
+ − 264
+ − 265
+ − 266
end