1 theory Dynamic2static |
1 theory Dynamic2static |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop |
2 imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 |
3 begin |
3 begin |
4 |
4 |
5 context tainting_s begin |
5 context tainting_s begin |
6 |
6 |
7 lemma d2s_main: |
7 lemma many_sq_imp_sms: |
8 "valid s \<Longrightarrow> s2ss s \<in> static" |
8 "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm" |
9 apply (induct s, simp add:s2ss_nil_prop s_init) |
9 sorry |
10 apply (frule vd_cons, simp) |
10 |
11 apply (case_tac a, simp_all) |
11 definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100) |
12 (* |
12 where |
13 apply |
13 "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss" |
14 induct s, case tac e, every event analysis |
14 |
15 *) |
15 lemma [simp]: "ss \<doteq> ss" |
16 thm s2ss_def |
16 by (auto simp:init_ss_eq_def) |
17 |
17 |
18 |
18 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101) |
19 sorry |
19 where |
20 |
20 "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'" |
21 lemma d2s_main': |
21 |
|
22 lemma s2ss_included_sobj: |
22 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
23 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
23 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
24 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
24 |
25 |
|
26 lemma init_ss_in_prop: |
|
27 "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk> |
|
28 \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss" |
|
29 apply (simp add:init_ss_in_def init_ss_eq_def) |
|
30 apply (erule bexE, erule conjE) |
|
31 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj) |
|
32 done |
|
33 |
|
34 |
|
35 |
|
36 |
|
37 |
|
38 |
|
39 lemma d2s_main_execve: |
|
40 "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static" |
|
41 apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve) |
|
42 sorry |
|
43 |
|
44 lemma d2s_main: |
|
45 "valid s \<Longrightarrow> s2ss s \<propto> static" |
|
46 apply (induct s, simp add:s2ss_nil_prop init_ss_in_def) |
|
47 apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init) |
|
48 apply (frule vd_cons, frule vt_grant_os, simp) |
|
49 apply (case_tac a) |
|
50 apply (clarsimp simp add:s2ss_execve) |
|
51 apply (rule conjI, rule impI) |
|
52 |
|
53 |
|
54 |
|
55 sorry |
|
56 |
|
57 |
25 lemma tainted_has_sobj: |
58 lemma tainted_has_sobj: |
26 "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
59 "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
27 sorry |
60 apply (frule tainted_in_current, case_tac obj) |
|
61 apply (auto dest:valid_tainted_obj simp:co2sobj.simps split:option.splits) |
|
62 oops |
28 |
63 |
29 lemma t2ts: |
64 lemma t2ts: |
30 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
65 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
31 apply (frule tainted_in_current, frule tainted_is_valid) |
66 apply (frule tainted_in_current, frule tainted_is_valid) |
32 apply (simp add:s2ss_def) |
67 apply (frule d2s_main', simp) |
33 apply (case_tac sobj, simp_all) |
68 apply (case_tac sobj, simp_all) |
34 apply (case_tac [!] obj, simp_all split:option.splits if_splits) |
69 apply (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits) |
35 apply (rule_tac x = "O_proc nat" in exI, simp) |
|
36 apply (rule_tac x = "O_file list" in exI, simp) |
|
37 apply (drule dir_not_tainted, simp) |
70 apply (drule dir_not_tainted, simp) |
38 apply (drule msgq_not_tainted, simp) |
71 apply (drule msgq_not_tainted, simp) |
39 apply (drule shm_not_tainted, simp) |
72 apply (drule shm_not_tainted, simp) |
40 done |
73 done |
41 |
74 |
42 lemma delq_imp_delqm: |
75 lemma delq_imp_delqm: |
43 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
76 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
44 apply (induct s, simp) |
77 apply (induct s, simp) |
45 by (case_tac a, auto) |
78 by (case_tac a, auto) |
|
79 |
|
80 lemma tainted_s_subset_prop: |
|
81 "\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj" |
|
82 apply (case_tac sobj) |
|
83 apply auto |
|
84 done |
46 |
85 |
47 theorem static_complete: |
86 theorem static_complete: |
48 assumes undel: "undeletable obj" and tbl: "taintable obj" |
87 assumes undel: "undeletable obj" and tbl: "taintable obj" |
49 shows "taintable_s obj" |
88 shows "taintable_s obj" |
50 proof- |
89 proof- |
51 from tbl obtain s where tainted: "obj \<in> tainted s" |
90 from tbl obtain s where tainted: "obj \<in> tainted s" |
52 by (auto simp:taintable_def) |
91 by (auto simp:taintable_def) |
53 hence vs: "valid s" by (simp add:tainted_is_valid) |
92 hence vs: "valid s" by (simp add:tainted_is_valid) |
54 hence static: "s2ss s \<in> static" using d2s_main by auto |
93 hence static: "s2ss s \<propto> static" using d2s_main by auto |
55 from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" |
94 from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" sorry |
56 using vs tainted_has_sobj by blast |
95 (* should constrain undeletable with file/dir/process only, while msg and fd are excluded |
|
96 using vs tainted_has_sobj by blast *) |
57 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
97 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
58 by (auto simp:undeletable_def) |
98 by (auto simp:undeletable_def) |
59 with vs sobj have "init_obj_related sobj obj" |
99 with vs sobj have "init_obj_related sobj obj" |
60 apply (case_tac obj, case_tac [!] sobj) |
100 apply (case_tac obj, case_tac [!] sobj) |
61 apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
101 apply (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
62 apply (frule not_deleted_init_file, simp+) |
102 apply (frule not_deleted_init_file, simp+) |
63 apply (drule is_file_has_sfile', simp, erule exE) |
103 apply (drule is_file_has_sfile', simp, erule exE) |
64 apply (rule_tac x = sf in bexI) |
104 apply (rule_tac x = sf in bexI) |
65 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
105 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
66 apply (drule root_is_init_dir', simp) |
106 apply (drule root_is_init_dir', simp) |
73 apply (simp add:cf2sfile_def split:option.splits if_splits) |
113 apply (simp add:cf2sfile_def split:option.splits if_splits) |
74 apply (case_tac list, simp add:sroot_def, simp) |
114 apply (case_tac list, simp add:sroot_def, simp) |
75 apply (drule file_dir_conflict, simp+) |
115 apply (drule file_dir_conflict, simp+) |
76 done |
116 done |
77 with tainted t2ts init_alive sobj static |
117 with tainted t2ts init_alive sobj static |
78 show ?thesis unfolding taintable_s_def |
118 show ?thesis unfolding taintable_s_def |
79 apply (rule_tac x = "s2ss s" in bexI, simp) |
119 apply (simp add:init_ss_in_def) |
80 apply (rule_tac x = "sobj" in exI, auto) |
120 apply (erule bexE) |
81 done |
121 apply (simp add:init_ss_eq_def) |
|
122 apply (rule_tac x = "ss'" in bexI) |
|
123 apply (rule_tac x = "sobj" in exI) |
|
124 by (auto intro:tainted_s_subset_prop) |
82 qed |
125 qed |
83 |
126 |
84 lemma cp2sproc_pi: |
127 lemma cp2sproc_pi: |
85 "\<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" |
128 "\<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" |
86 by (simp add:cp2sproc_def split:option.splits if_splits) |
129 by (simp add:cp2sproc_def split:option.splits if_splits) |
115 lemma init_deled_imp_deled_s: |
158 lemma init_deled_imp_deled_s: |
116 "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj" |
159 "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj" |
117 apply (rule notI) |
160 apply (rule notI) |
118 apply (clarsimp simp:s2ss_def) |
161 apply (clarsimp simp:s2ss_def) |
119 apply (case_tac obj, case_tac [!] obja, case_tac sobj) |
162 apply (case_tac obj, case_tac [!] obja, case_tac sobj) |
120 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi) |
163 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps) |
121 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def |
164 apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps |
122 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
165 split:option.splits t_inode_tag.splits dest!:cf2sfile_fi) |
123 done |
166 done |
124 |
167 |
125 lemma deleted_imp_deletable_s: |
168 lemma deleted_imp_deletable_s: |
126 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
169 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
127 apply (simp add:deletable_s_def) |
170 apply (simp add:deletable_s_def) |
128 apply (rule_tac x = "s2ss s" in bexI) |
171 apply (frule d2s_main) |
129 apply (clarify, simp add:init_deled_imp_deled_s) |
172 apply (simp add:init_ss_in_def) |
130 apply (erule d2s_main) |
173 apply (erule bexE) |
|
174 apply (rule_tac x = ss' in bexI) |
|
175 apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s) |
|
176 apply (case_tac obj, case_tac [!] sobj) |
|
177 apply auto |
|
178 apply (erule set_mp) |
|
179 apply (simp) |
|
180 apply auto |
|
181 apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI) |
|
182 apply auto |
131 done |
183 done |
132 |
184 |
133 theorem undeletable_s_complete: |
185 theorem undeletable_s_complete: |
134 assumes undel_s: "undeletable_s obj" |
186 assumes undel_s: "undeletable_s obj" |
135 shows "undeletable obj" |
187 shows "undeletable obj" |