84 |
84 |
85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
85 definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool" |
86 where |
86 where |
87 "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s" |
87 "is_created_proc s p \<equiv> p \<in> init_procs \<longrightarrow> deleted (O_proc p) s" |
88 |
88 |
|
89 lemma enrich_proc_aux1: |
|
90 assumes vs': "valid s'" |
|
91 and os: "os_grant s e" and grant: "grant s e" |
|
92 and alive: "\<forall> obj. alive s obj \<longrightarrow> alive s' obj" |
|
93 and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p" |
|
94 and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f" |
|
95 shows "valid (e # s')" |
|
96 proof (cases e) |
|
97 case (Execve p f fds) |
|
98 have p_in: "p \<in> current_procs s'" using os alive |
|
99 apply (erule_tac x = "O_proc p" in allE) |
|
100 by (auto simp:Execve) |
|
101 have f_in: "is_file s' f" using os alive |
|
102 apply (erule_tac x = "O_file f" in allE) |
|
103 by (auto simp:Execve) |
|
104 have fd_in: "fds \<subseteq> current_proc_fds s' p" using os alive |
|
105 apply (auto simp:Execve) |
|
106 by (erule_tac x = "O_fd p x" in allE, auto) |
|
107 have "os_grant s' e" using p_in f_in fd_in by (simp add:Execve) |
|
108 moreover have "grant s' e" |
|
109 proof- |
|
110 from grant obtain up rp tp uf rf tf |
|
111 where p1: "sectxt_of_obj s (O_proc p) = Some (up, rp, tp)" |
|
112 and p2: "sectxt_of_obj s (O_file f) = Some (uf, rf, tf)" |
|
113 by (simp add:Execve split:option.splits, blast) |
|
114 with grant obtain pu nr nt where p3: "npctxt_execve (up, rp, tp) (uf, rf, tf) = Some (pu, nr, nt)" |
|
115 by (simp add:Execve split:option.splits del:npctxt_execve.simps, blast) |
|
116 from p1 have p1': "sectxt_of_obj s' (O_proc p) = Some (up, rp, tp)" |
|
117 using os cp2sp |
|
118 apply (erule_tac x = p in allE) |
|
119 by (auto simp:Execve co2sobj.simps cp2sproc_def split:option.splits) |
|
120 from p2 have p2': "sectxt_of_obj s' (O_file f) = Some (uf, rf, tf)" |
|
121 using os cf2sf |
|
122 apply (erule_tac x = "f" in allE) |
|
123 apply (auto simp:Execve dest:is_file_in_current) |
|
124 thm cf2sfile_def |
|
125 apply (auto simp:cf2sfile_def split:option.splits) |
|
126 apply (auto simp:Execve co2sobj.simps cf2sfile_simps split:option.splits) |
|
127 apply (simp add:cf2sfiles_def) |
|
128 apply (auto)[1] |
|
129 using os pre |
|
130 show ?thesis |
|
131 proof- |
|
132 have |
|
133 |
|
134 |
|
135 |
|
136 |
89 lemma enrich_proc_prop: |
137 lemma enrich_proc_prop: |
90 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
138 "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
91 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
139 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
92 co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p) \<and> |
140 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
93 (alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
141 (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
94 proof (induct s) |
142 proof (induct s) |
95 case Nil |
143 case Nil |
96 thus ?case by (auto simp:is_created_proc_def) |
144 thus ?case by (auto simp:is_created_proc_def) |
97 next |
145 next |
98 case (Cons e s) |
146 case (Cons e s) |
99 hence p1: "\<lbrakk>p \<in> current_procs s; valid s; is_created_proc s p; p' \<notin> current_procs s\<rbrakk> |
147 hence p1: "\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk> |
100 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
148 \<Longrightarrow> valid (enrich_proc s p p') \<and> |
101 p' \<in> current_procs (enrich_proc s p p') \<and> |
149 (p \<in> current_procs s \<longrightarrow> co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p)) \<and> |
102 co2sobj (enrich_proc s p p') (O_proc p') = co2sobj (enrich_proc s p p') (O_proc p) \<and> |
|
103 (alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
150 (alive s obj \<longrightarrow> alive (enrich_proc s p p') obj \<and> co2sobj (enrich_proc s p p') obj = co2sobj s obj)" |
104 and p2: "p \<in> current_procs (e # s)" and p3: "valid (e # s)" |
151 and p2: "valid (e # s)" and p3: "is_created_proc (e # s) p" and p4: "p' \<notin> all_procs (e # s)" |
105 and p4: "is_created_proc (e # s) p" and p5: "p' \<notin> current_procs (e # s)" |
|
106 by auto |
152 by auto |
107 from p4 p2 have p4': "is_created_proc s p" |
153 from p2 have vd: "valid s" and os: "os_grant s e" and grant: "grant s e" |
108 by (case_tac e, auto simp:is_created_proc_def) |
|
109 from p3 have vd: "valid s" and os: "os_grant s e" and grant: "grant s e" |
|
110 by (auto dest:vd_cons vt_grant vt_grant_os) |
154 by (auto dest:vd_cons vt_grant vt_grant_os) |
111 from p1 p4' have a1: "\<lbrakk>p \<in> current_procs s; p' \<notin> current_procs s\<rbrakk> |
155 from p4 have p4': "p' \<notin> all_procs s" by (case_tac e, auto) |
112 \<Longrightarrow> valid (enrich_proc s p p')" by (auto simp:vd) |
156 from p1 p4' have a1: "is_created_proc s p \<Longrightarrow> valid (enrich_proc s p p')" by (auto simp:vd) |
113 have c1: "valid (enrich_proc (e # s) p p')" |
157 have c1: "valid (enrich_proc (e # s) p p')" |
114 apply (case_tac e) |
158 apply (case_tac e) |
115 using a1 os p5 |
159 using a1 os p3 |
116 apply (auto) |
160 apply (auto simp:is_created_proc_def) |
117 sorry |
161 sorry |
118 moreover have c2: "p' \<in> current_procs (enrich_proc (e # s) p p')" |
162 moreover have c2: "p' \<in> current_procs (enrich_proc (e # s) p p')" |
119 sorry |
163 sorry |
120 moreover have c3: "co2sobj (enrich_proc (e # s) p p') (O_proc p') = co2sobj (enrich_proc (e # s) p p') (O_proc p)" |
164 moreover have c3: "co2sobj (enrich_proc (e # s) p p') (O_proc p') = co2sobj (enrich_proc (e # s) p p') (O_proc p)" |
121 sorry |
165 sorry |