13 apply |
13 apply |
14 induct s, case tac e, every event analysis |
14 induct s, case tac e, every event analysis |
15 *) |
15 *) |
16 sorry |
16 sorry |
17 |
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': |
18 lemma d2s_main': |
29 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
19 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
30 apply (induct s) |
20 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
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 |
21 |
43 lemma alive_has_sobj: |
22 lemma alive_has_sobj: |
44 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
23 "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" |
45 sorry |
24 sorry |
46 |
25 |
47 lemma t2ts: |
26 lemma t2ts: |
48 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
27 "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj" |
49 apply (frule tainted_prop1, frule tainted_prop2) |
28 apply (frule tainted_in_current, frule tainted_is_valid) |
50 apply (simp add:s2ss_def) |
29 apply (simp add:s2ss_def) |
51 apply (case_tac sobj, simp_all) |
30 apply (case_tac sobj, simp_all) |
52 apply (case_tac [!] obj, simp_all split:option.splits) |
31 apply (case_tac [!] obj, simp_all split:option.splits if_splits) |
53 apply (rule_tac x = "O_proc nat" in exI, simp) |
32 apply (rule_tac x = "O_proc nat" in exI, simp) |
54 apply (rule_tac x = "O_file list" in exI, simp) |
33 apply (rule_tac x = "O_file list" in exI, simp) |
55 defer defer defer |
34 apply (drule dir_not_tainted, simp) |
|
35 apply (drule msgq_not_tainted, simp) |
|
36 apply (drule shm_not_tainted, simp) |
56 apply (case_tac prod1, simp, case_tac prod2, clarsimp) |
37 apply (case_tac prod1, simp, case_tac prod2, clarsimp) |
57 apply (rule conjI) |
38 apply (rule conjI) |
58 apply (rule_tac x = "O_msgq nat1" in exI, simp) |
39 apply (rule_tac x = "O_msgq nat1" in exI, simp) |
59 sorry (* doable, need properties about cm2smsg and cq2smsgq *) |
40 apply (rule conjI) defer |
|
41 apply (simp add:cm2smsg_def split:option.splits) |
|
42 sorry |
60 |
43 |
61 lemma delq_imp_delqm: |
44 lemma delq_imp_delqm: |
62 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
45 "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s" |
63 apply (induct s, simp) |
46 apply (induct s, simp) |
64 by (case_tac a, auto) |
47 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 |
48 |
71 theorem static_complete: |
49 theorem static_complete: |
72 assumes undel: "undeletable obj" and tbl: "taintable obj" |
50 assumes undel: "undeletable obj" and tbl: "taintable obj" |
73 shows "taintable_s obj" |
51 shows "taintable_s obj" |
74 proof- |
52 proof- |
75 from tbl obtain s where tainted: "obj \<in> tainted s" |
53 from tbl obtain s where tainted: "obj \<in> tainted s" |
76 by (auto simp:taintable_def) |
54 by (auto simp:taintable_def) |
77 hence vs: "valid s" by (simp add:tainted_prop2) |
55 hence vs: "valid s" by (simp add:tainted_is_valid) |
78 hence static: "s2ss s \<in> static" using d2s_main by auto |
56 hence static: "s2ss s \<in> static" using d2s_main by auto |
79 from tainted have alive: "alive s obj" |
57 from tainted have alive: "alive s obj" |
80 using tainted_prop1 by auto |
58 using tainted_in_current by auto |
81 then obtain sobj where sobj: "co2sobj s obj = Some sobj" |
59 then obtain sobj where sobj: "co2sobj s obj = Some sobj" |
82 using vs alive_has_sobj by blast |
60 using vs alive_has_sobj by blast |
83 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
61 from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" |
84 by (auto simp:undeletable_def) |
62 by (auto simp:undeletable_def) |
85 with vs sobj have "init_obj_related sobj obj" |
63 with vs sobj have "init_obj_related sobj obj" |
86 apply (case_tac obj, case_tac [!] sobj) |
64 apply (case_tac obj, case_tac [!] sobj) |
87 apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def) |
65 apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) |
88 apply (frule undel_init_file_remains, simp, drule is_file_has_sfile, erule exE) |
66 apply (frule not_deleted_init_file, simp+) (* |
|
67 apply (drule is_file_has_sfile, erule exE) |
89 apply (rule_tac x = sf in bexI) |
68 apply (rule_tac x = sf in bexI) |
90 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
69 apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1] |
91 apply (simp add:same_inode_files_def cfs2sfiles_def) |
70 apply (simp add:same_inode_files_def cfs2sfiles_def) *) |
92 apply (rule_tac x = list in exI, simp) |
71 sorry |
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 |
72 with tainted t2ts init_alive sobj static |
96 show ?thesis unfolding taintable_s_def |
73 show ?thesis unfolding taintable_s_def |
97 apply (rule_tac x = "s2ss s" in bexI, simp) |
74 apply (rule_tac x = "s2ss s" in bexI, simp) |
98 apply (rule_tac x = "sobj" in exI, auto) |
75 apply (rule_tac x = "sobj" in exI, auto) |
99 done |
76 done |
100 qed |
77 qed |
101 |
78 |
|
79 lemma cp2sproc_pi: |
|
80 "\<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" |
|
81 by (simp add:cp2sproc_def split:option.splits if_splits) |
|
82 |
|
83 lemma cq2smsgq_qi: |
|
84 "\<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" |
|
85 by (simp add:cq2smsgq_def split:option.splits if_splits) |
|
86 |
|
87 lemma cm2smsg_mi: |
|
88 "\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk> |
|
89 \<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" |
|
90 by (clarsimp simp add:cm2smsg_def split:if_splits option.splits) |
|
91 |
|
92 lemma ch2sshm_hi: |
|
93 "\<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" |
|
94 by (clarsimp simp:ch2sshm_def split:if_splits option.splits) |
|
95 |
|
96 lemma root_not_deleted: |
|
97 "\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False" |
|
98 apply (induct s, simp) |
|
99 apply (frule vd_cons, frule vt_grant_os, case_tac a, auto) |
|
100 done |
|
101 |
|
102 lemma cf2sfile_fi: |
|
103 "\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and> |
|
104 (if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f |
|
105 else \<not> deleted (O_dir f) s \<and> is_init_dir f)" |
|
106 apply (case_tac f) |
|
107 by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted |
|
108 split:if_splits option.splits) |
|
109 |
102 lemma init_deled_imp_deled_s: |
110 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" |
111 "\<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) |
112 apply (rule notI) |
105 apply (frule vd_cons) |
113 apply (clarsimp simp:s2ss_def) |
106 apply (case_tac a, auto) |
114 apply (case_tac obj, case_tac [!] obja, case_tac sobj) |
107 (* need simpset for s2ss *) |
115 apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi) |
108 sorry |
116 |
|
117 done |
109 |
118 |
110 lemma deleted_imp_deletable_s: |
119 lemma deleted_imp_deletable_s: |
111 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
120 "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj" |
112 apply (simp add:deletable_s_def) |
121 apply (simp add:deletable_s_def) |
113 apply (rule_tac x = "s2ss s" in bexI) |
122 apply (rule_tac x = "s2ss s" in bexI) |