|
1 theory Dynamic2static |
|
2 imports Main Flask Static Init_prop Valid_prop |
|
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 *) |
|
16 sorry |
|
17 |
|
18 lemma is_file_has_sfile: "is_file s f \<Longrightarrow> \<exists> sf. cf2sfile s f True = Some sf" |
|
19 sorry |
|
20 |
|
21 lemma is_dir_has_sfile: "is_dir s f \<Longrightarrow> \<exists> sf. cf2sfile s f False = Some sf" |
|
22 sorry |
|
23 |
|
24 lemma is_file_imp_alive: "is_file s f \<Longrightarrow> alive s (O_file f)" |
|
25 sorry |
|
26 |
|
27 |
|
28 lemma d2s_main': |
|
29 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
|
30 apply (induct s) |
|
31 apply (simp add:s2ss_def) |
|
32 apply (rule_tac x = obj in exI, simp) |
|
33 sorry |
|
34 |
|
35 lemma tainted_prop1: |
|
36 "obj \<in> tainted s \<Longrightarrow> alive s obj" |
|
37 sorry |
|
38 |
|
39 lemma tainted_prop2: |
|
40 "obj \<in> tainted s \<Longrightarrow> valid s" |
|
41 sorry |
|
42 |
|
43 lemma alive_has_sobj: |
|
44 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
|
45 sorry |
|
46 |
|
47 lemma t2ts: |
|
48 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
|
49 apply (frule tainted_prop1, frule tainted_prop2) |
|
50 apply (simp add:s2ss_def) |
|
51 apply (case_tac sobj, simp_all) |
|
52 apply (case_tac [!] obj, simp_all split:option.splits) |
|
53 apply (rule_tac x = "O_proc nat" in exI, simp) |
|
54 apply (rule_tac x = "O_file list" in exI, simp) |
|
55 defer defer defer |
|
56 apply (case_tac prod1, simp, case_tac prod2, clarsimp) |
|
57 apply (rule conjI) |
|
58 apply (rule_tac x = "O_msgq nat1" in exI, simp) |
|
59 sorry (* doable, need properties about cm2smsg and cq2smsgq *) |
|
60 |
|
61 lemma delq_imp_delqm: |
|
62 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
|
63 apply (induct s, simp) |
|
64 by (case_tac a, auto) |
|
65 |
|
66 lemma undel_init_file_remains: |
|
67 "\<lbrakk>is_init_file f; \<not> deleted (O_file f) s\<rbrakk> \<Longrightarrow> is_file s f" |
|
68 sorry |
|
69 |
|
70 |
|
71 theorem static_complete: |
|
72 assumes undel: "undeletable obj" and tbl: "taintable obj" |
|
73 shows "taintable_s obj" |
|
74 proof- |
|
75 from tbl obtain s where tainted: "obj \<in> tainted s" |
|
76 by (auto simp:taintable_def) |
|
77 hence vs: "valid s" by (simp add:tainted_prop2) |
|
78 hence static: "s2ss s \<in> static" using d2s_main by auto |
|
79 from tainted have alive: "alive s obj" |
|
80 using tainted_prop1 by auto |
|
81 then obtain sobj where sobj: "co2sobj s obj = Some sobj" |
|
82 using vs alive_has_sobj by blast |
|
83 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
|
84 by (auto simp:undeletable_def) |
|
85 with vs sobj have "init_obj_related sobj obj" |
|
86 apply (case_tac obj, case_tac [!] sobj) |
|
87 apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def) |
|
88 apply (frule undel_init_file_remains, simp, drule is_file_has_sfile, erule exE) |
|
89 apply (rule_tac x = sf in bexI) |
|
90 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
|
91 apply (simp add:same_inode_files_def cfs2sfiles_def) |
|
92 apply (rule_tac x = list in exI, simp) |
|
93 apply (case_tac list, auto split:option.splits simp:is_init_dir_props delq_imp_delqm) |
|
94 done |
|
95 with tainted t2ts init_alive sobj static |
|
96 show ?thesis unfolding taintable_s_def |
|
97 apply (rule_tac x = "s2ss s" in bexI, simp) |
|
98 apply (rule_tac x = "sobj" in exI, auto) |
|
99 done |
|
100 qed |
|
101 |
|
102 lemma init_deled_imp_deled_s: |
|
103 "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj" |
|
104 apply (induct s, simp) |
|
105 apply (frule vd_cons) |
|
106 apply (case_tac a, auto) |
|
107 (* need simpset for s2ss *) |
|
108 sorry |
|
109 |
|
110 lemma deleted_imp_deletable_s: |
|
111 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
|
112 apply (simp add:deletable_s_def) |
|
113 apply (rule_tac x = "s2ss s" in bexI) |
|
114 apply (clarify, simp add:init_deled_imp_deled_s) |
|
115 apply (erule d2s_main) |
|
116 done |
|
117 |
|
118 theorem undeletable_s_complete: |
|
119 assumes undel_s: "undeletable_s obj" |
|
120 shows "undeletable obj" |
|
121 proof- |
|
122 from undel_s have init_alive: "init_alive obj" |
|
123 and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj" |
|
124 using undeletable_s_def by auto |
|
125 have "\<not> (\<exists> s. valid s \<and> deleted obj s)" |
|
126 proof |
|
127 assume "\<exists> s. valid s \<and> deleted obj s" |
|
128 then obtain s where vs: "valid s" and del: "deleted obj s" by auto |
|
129 from vs have vss: "s2ss s \<in> static" by (rule d2s_main) |
|
130 with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" |
|
131 and related: "init_obj_related sobj obj" by auto |
|
132 from init_alive del vs have "deletable_s obj" |
|
133 by (auto elim:deleted_imp_deletable_s) |
|
134 with alive_s |
|
135 show False by (auto simp:deletable_s_def) |
|
136 qed |
|
137 with init_alive show ?thesis |
|
138 by (simp add:undeletable_def) |
|
139 qed |
|
140 |
|
141 theorem final_offer: |
|
142 "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj" |
|
143 apply (erule swap) |
|
144 by (simp add:static_complete undeletable_s_complete) |
|
145 |
|
146 |
|
147 |
|
148 (************** static \<rightarrow> dynamic ***************) |
|
149 |
|
150 lemma created_can_have_many: |
|
151 "\<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'" |
|
152 sorry |
|
153 |
|
154 lemma s2d_main: |
|
155 "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss" |
|
156 apply (erule static.induct) |
|
157 apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros) |
|
158 |
|
159 apply (erule exE|erule conjE)+ |
|
160 |
|
161 apply (erule exE, erule conjE)+ |
|
162 |
|
163 sorry |
|
164 |
|
165 |
|
166 |
|
167 lemma tainted_s_imp_tainted: |
|
168 "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> obj s. s2ss s = ss \<and> valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s" |
|
169 sorry |
|
170 |
|
171 |
|
172 theorem static_sound: |
|
173 assumes tbl_s: "taintable_s obj" |
|
174 shows "taintable obj" |
|
175 proof- |
|
176 from tbl_s obtain ss sobj where static: "ss \<in> static" |
|
177 and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj" |
|
178 and init_alive: "init_alive obj" by (auto simp:taintable_s_def) |
|
179 from static sobj tainted_s_imp_tainted |
|
180 obtain s obj' where s2ss: "s2ss s = ss" and co2sobj: "co2sobj s obj' = Some sobj" |
|
181 and tainted: "obj' \<in> tainted s" and vs: "valid s" by blast |
|
182 |
|
183 from co2sobj related |
|
184 have eq:"obj = obj'" |
|
185 apply (case_tac obj', case_tac [!] obj, case_tac [!] sobj) |
|
186 apply auto |
|
187 apply (auto split:option.splits if_splits) |
|
188 apply (case_tac a, simp+) |
|
189 apply (simp add:cp2sproc_def split:option.splits if_splits) |
|
190 apply simp |
|
191 sorry |
|
192 with tainted vs init_alive |
|
193 show ?thesis by (auto simp:taintable_def) |
|
194 qed |
|
195 |
|
196 |
|
197 |
|
198 lemma ts2t: |
|
199 "obj \<in> tainted_s ss \<Longrightarrow> \<exists> s. obj \<in> tainted s" |
|
200 "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. " |
|
201 |
|
202 |
|
203 |
|
204 |
|
205 end |