--- a/Dynamic_static.thy Wed Nov 20 21:33:56 2013 +0800
+++ b/Dynamic_static.thy Mon Dec 02 10:52:40 2013 +0800
@@ -117,32 +117,40 @@
by (case_tac a, simp)
qed
+lemma proc_filefd_has_sfd: "\<lbrakk>fd \<in> proc_file_fds s p; valid s\<rbrakk> \<Longrightarrow> \<exists> sfd. cfd2sfd s p fd = Some sfd"
+apply (simp add:proc_file_fds_def)
+apply (auto dest: current_filefd_has_sfd)
+done
+
lemma enrich_inherit_fds_check:
assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s"
and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
and p_in: "p \<in> current_procs s" and p_in': "p \<in> current_procs s'"
- and fd_in: "fds \<subseteq> current_proc_fds s p" and fd_in': "fds \<subseteq> current_proc_fds s' p"
+ and fd_in: "fds \<subseteq> proc_file_fds s p" and fd_in': "fds \<subseteq> proc_file_fds s' p"
shows "inherit_fds_check s' (up, nr, nt) p fds"
proof-
have "\<And> fd. fd \<in> fds \<Longrightarrow> sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)"
proof-
fix fd
assume fd_in_fds: "fd \<in> fds"
- hence fd_in_cfds: "fd \<in> current_proc_fds s p"
- and fd_in_cfds': "fd \<in> current_proc_fds s' p"
+ hence fd_in_cfds: "fd \<in> proc_file_fds s p"
+ and fd_in_cfds': "fd \<in> proc_file_fds s' p"
using fd_in fd_in' by auto
from p_in vd obtain sp where csp: "cp2sproc s p = Some sp"
by (drule_tac current_proc_has_sp, simp, erule_tac exE, simp)
with cp2sp have "cpfd2sfds s p = cpfd2sfds s' p"
apply (erule_tac x = p in allE)
by (auto simp:cp2sproc_def split:option.splits simp:p_in)
- hence "cfd2sfd s p fd = cfd2sfd s' p fd"
+ hence "cfd2sfd s p fd = cfd2sfd s' p fd" using fd_in_cfds fd_in_cfds'
apply (simp add:cpfd2sfds_def)
+ apply (frule proc_filefd_has_sfd, simp add:vd, erule exE)
+ apply (drule_tac x = sfd in eqset_imp_iff, simp)
+ (*
thm inherit_fds_check_def
thm sectxts_of_fds_def
thm cpfd2sfds_def
apply (
-
+ *)sorry
show "sectxt_of_obj s' (O_fd p fd) = sectxt_of_obj s (O_fd p fd)"
sorry
qed
@@ -160,6 +168,8 @@
and cp2sp: "\<forall> p. p \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
shows "valid (e # s')"
+
+sorry (*
proof (cases e)
case (Execve p f fds)
have p_in: "p \<in> current_procs s'" using os alive
@@ -198,7 +208,7 @@
have
-
+*)
lemma enrich_proc_prop:
"\<lbrakk>valid s; is_created_proc s p; p' \<notin> all_procs s\<rbrakk>
@@ -208,6 +218,7 @@
(\<forall> p'. p' \<in> current_procs s \<longrightarrow> cp2sproc (enrich_proc s p p') p' = cp2sproc s p) \<and>
(\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile (enrich_proc s p p') f = cf2sfile s f) \<and>
(Tainted (enrich_proc s p p') = (Tainted s \<union> (if (O_proc p \<in> Tainted s) then {O_proc p'} else {})))"
+sorry (*
proof (induct s)
case Nil
thus ?case by (auto simp:is_created_proc_def)
@@ -237,17 +248,17 @@
sorry
ultimately show ?case by auto
qed
-
+*)
lemma "alive s obj \<Longrightarrow> alive (enrich_proc s p p') obj"
apply (induct s, simp)
-apply (case_tac a, case_tac[!] obj)
+apply (case_tac a, case_tac[!] obj) sorry (*
apply (auto simp:is_file_def is_dir_def split:option.splits t_inode_tag.splits)
thm is_file_other
-
+*)
lemma enrich_proc_valid:
- "\<lbrakk>p \<in> current_procs s; valid s; p \<in> init_procs \<longrightarrow> deleted (O_proc p) s; p' \<notin> current_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')"
+ "\<lbrakk>p \<in> current_procs s; valid s; p \<in> init_procs \<longrightarrow> deleted (O_proc p) s; p' \<notin> current_procs s\<rbrakk> \<Longrightarrow> valid (enrich_proc s p p')" (*
apply (induct s, simp)
apply (frule vd_cons, frule vt_grant, frule vt_grant_os, case_tac a)
apply (auto intro!:valid.intros(2))
@@ -256,6 +267,9 @@
end
+*)
+sorry
+
(* for any created obj, we can enrich trace with events that create new objs with the same static-properties *)
definition enriched:: "t_state \<Rightarrow> t_object set \<Rightarrow> t_state \<Rightarrow> bool"
@@ -387,7 +401,6 @@
apply (auto simp:search_check_s_def search_check.simps cf2sfile_def sroot_def
root_sec_remains init_sectxt_prop sec_of_root_valid
dest!:root_is_dir' current_has_sec' split:option.splits)
-apply (simp add:search_check_allp_def)
done
lemma grant_execve_intro_execve:
@@ -437,9 +450,10 @@
\<Longrightarrow> inherit_fds_check_s sec' sfds'"
apply (frule vt_grant_os, frule vd_cons, frule vt_grant)
apply (auto simp:cp2sproc_def cpfd2sfds_execve inherit_fds_check_def inherit_fds_check_s_def split:option.splits)
+sorry (*
apply (erule_tac x = "(ad, ae, bc)" in ballE, auto simp:sectxts_of_sfds_def sectxts_of_fds_def)
apply (erule_tac x = fd in ballE, auto simp:cfd2sfd_def split:option.splits)
-done
+done *)
lemma d2s_main_execve_grant_aux:
"\<lbrakk>cp2sproc (Execve p f fds # s) p = Some (pi', sec', sfds', shms'); valid (Execve p f fds # s);
@@ -554,11 +568,10 @@
moreover from a4 os p4 have "is_file s' f"
apply (simp add:reserved_def)
by (erule_tac x = "O_file f" in allE, auto)
- moreover from a4 os p4 have "fds \<subseteq> current_proc_fds s' p"
+ moreover from a4 os p4 vd have "fds \<subseteq> proc_file_fds s' p"
apply (rule_tac subsetI, clarsimp simp:reserved_def current_proc_fds.simps)
apply (erule_tac x = "O_fd p x" in allE, erule impE)
- apply (simp, erule set_mp, simp+)
- done
+ sorry
ultimately have "os_grant s' e"
by (simp add:p4)
moreover have "grant s' e"
@@ -571,6 +584,7 @@
apply (simp)
sorry
qed
+qed
lemma s2d_main_execve:
"\<lbrakk>grant_execve pctxt fsec pctxt'; ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
@@ -582,7 +596,7 @@
thm update_ss_def
sorry
-
+(*
lemma s2d_main_execve:
"ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"
apply (erule static.induct)
@@ -592,24 +606,24 @@
apply (erule exE|erule conjE)+
-apply (simp add:update_ss_def)
sorry
-
+*)
(*********************** uppest-level 3 theorems ***********************)
lemma enrichability:
"\<lbrakk>valid s; \<forall> obj \<in> objs. alive s obj \<and> is_created s obj \<and> recorded obj\<rbrakk>
- \<Longrightarrow> enrichable s objs"
+ \<Longrightarrow> enrichable s objs" sorry (*
proof (induct s arbitrary:objs)
case Nil
hence "objs = {}"
- apply (auto simp:is_created_def)
+ apply (auto)
apply (erule_tac x = x in ballE)
+ apply (case_tac x)
apply (auto simp:init_alive_prop)
- done
+ sorry (* done *)
thus ?case using Nil unfolding enrichable_def enriched_def reserved_def
by (rule_tac x = "[]" in exI, auto)
next
@@ -676,7 +690,8 @@
done
-qed
+qed
+*)
lemma d2s_main:
"valid s \<Longrightarrow> s2ss s \<propto> static"
@@ -702,6 +717,17 @@
sorry
+lemma s2d_main':
+ "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s \<doteq> ss"
+apply (erule static.induct)
+apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)
+
+apply (erule exE|erule conjE)+
+
+apply (simp add:update_ss_def)
+
+sorry
+
end