--- a/no_shm_selinux/Co2sobj_prop.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Co2sobj_prop.thy Tue Dec 31 14:57:13 2013 +0800
@@ -80,9 +80,11 @@
lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2'
cm2smsg_removemsgq cm2smsg_other
+(*
lemma init_cm2smsg_has_smsg:
"\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk> \<Longrightarrow> \<exists> sm. init_cm2smsg q m = Some sm"
by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt)
+*)
lemma hd_set_prop1:
"hd l \<notin> set l \<Longrightarrow> l = []"
@@ -262,7 +264,7 @@
apply (frule vd_cons, frule vt_grant_os)
apply (frule cqm2sms_createmsgq)
apply (rule ext, auto simp:cq2smsgq_def sec_createmsgq
- split:option.splits if_splits dest:not_died_init_msgq)
+ split:option.splits if_splits)
done
lemma cq2smsg_sendmsg:
--- a/no_shm_selinux/Enrich.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Enrich.thy Tue Dec 31 14:57:13 2013 +0800
@@ -141,77 +141,6 @@
apply (simp add:parentf_is_dir_prop2)
done
-(* enrich s target_proc duplicated_pro *)
-fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
-where
- "enrich_proc [] tp dp = []"
-| "enrich_proc (Execve p f fds # s) tp dp = (
- if (tp = p)
- then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
- else Execve p f fds # (enrich_proc s tp dp))"
-| "enrich_proc (Clone p p' fds # s) tp dp = (
- if (tp = p')
- then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
- else Clone p p' fds # (enrich_proc s tp dp))"
-| "enrich_proc (Open p f flags fd opt # s) tp dp = (
- if (tp = p)
- then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
- else Open p f flags fd opt # (enrich_proc s tp dp))"
-| "enrich_proc (ReadFile p fd # s) tp dp = (
- if (tp = p)
- then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
- else ReadFile p fd # (enrich_proc s tp dp))"
-(*
-| "enrich_proc (CloseFd p fd # s) tp dp = (
- if (tp = p \<and> fd \<in> proc_file_fds s p)
- then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
- else CloseFd p fd # (enrich_proc s tp dp))"
-*)
-(*
-| "enrich_proc (Attach p h flag # s) tp dp = (
- if (tp = p)
- then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp)
- else Attach p h flag # (enrich_proc s tp dp))"
-| "enrich_proc (Detach p h # s) tp dp = (
- if (tp = p)
- then Detach dp h # Detach p h # (enrich_proc s tp dp)
- else Detach p h # (enrich_proc s tp dp))"
-*)
-(*
-| "enrich_proc (Kill p p' # s) tp dp = (
- if (tp = p') then Kill p p' # s
- else Kill p p' # (enrich_proc s tp dp))"
-| "enrich_proc (Exit p # s) tp dp = (
- if (tp = p) then Exit p # s
- else Exit p # (enrich_proc s tp dp))"
-*)
-| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
-
-definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
-where
- "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
-
-definition is_created_proc':: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
-where
- "is_created_proc' s p \<equiv> p \<in> current_procs s \<and> p \<notin> init_procs"
-
-lemma no_del_died:
- "\<lbrakk>no_del_event s; died obj s\<rbrakk> \<Longrightarrow> (\<exists> p fd. obj = O_fd p fd \<or> obj = O_tcp_sock (p, fd) \<or> obj = O_udp_sock (p, fd))
- \<or> (\<exists> q m. obj = O_msg q m) "
-apply (induct s)
-apply simp
-apply (case_tac a)
-apply (auto split:option.splits)
-done
-
-lemma no_del_created_eq:
- "no_del_event s \<Longrightarrow> is_created_proc s p = is_created_proc' s p"
-apply (induct s)
-apply (simp add:is_created_proc_def is_created_proc'_def)
-apply (case_tac a)
-apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
-done
-
lemma enrich_search_check:
assumes grant: "search_check s (up, rp, tp) f"
and cf2sf: "\<forall> f. f \<in> current_files s \<longrightarrow> cf2sfile s' f = cf2sfile s f"
@@ -1248,74 +1177,44 @@
qed
qed
-lemma created_proc_clone:
- "valid (Clone p p' fds # s) \<Longrightarrow>
- is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)"
-apply (drule vt_grant_os)
-apply (auto simp:is_created_proc_def dest:not_all_procs_prop2)
-using not_died_init_proc
-by auto
-
-lemma created_proc_exit:
- "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)"
-by (simp add:is_created_proc_def)
-
-lemma created_proc_kill:
- "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)"
-by (simp add:is_created_proc_def)
+lemma current_proc_fds_in_curp:
+ "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+apply (induct s)
+apply (simp add:init_fds_of_proc_prop1)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto split:if_splits option.splits)
+done
-lemma created_proc_other:
- "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds;
- \<And> p. e \<noteq> Exit p;
- \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp"
-by (case_tac e, auto simp:is_created_proc_def)
-
-lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other
-(*
-
-
-
-
- (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>
- (\<forall> obj. alive s obj \<longrightarrow> alive (enrich_proc s p p') obj) \<and>
- (\<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 {})))"*)
-
-lemma enrich_proc_dup_in:
- "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
- \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
-apply (induct s, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
+lemma get_parentfs_ctxts_prop:
+ "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk>
+ \<Longrightarrow> ctxt \<in> set (ctxts)"
+apply (induct f)
+apply (auto split:option.splits)
done
-lemma enrich_proc_dup_ffd:
- "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
- \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
-apply (induct s, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
- dest:not_all_procs_prop3 split:if_splits option.splits)
-done
+lemma search_check_allp_intro:
+ "\<lbrakk>search_check s sp pf; get_parentfs_ctxts s pf = Some ctxts; valid s; is_dir s pf\<rbrakk>
+ \<Longrightarrow> search_check_allp sp (set ctxts)"
+apply (case_tac pf)
+apply (simp split:option.splits if_splits add:search_check_allp_def)
+apply (rule ballI)
+apply (auto simp:search_check_ctxt_def search_check_dir_def split:if_splits option.splits)
+apply (auto simp:search_check_allp_def search_check_file_def)
+apply (frule is_dir_not_file, simp)
+done
-lemma enrich_proc_dup_ffd':
- "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
- no_del_event s; valid s\<rbrakk>
- \<Longrightarrow> file_of_proc_fd s p fd = Some f"
-apply (induct s, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
- dest:not_all_procs_prop3 split:if_splits option.splits)
-done
+lemma search_check_leveling_f:
+ "\<lbrakk>search_check s sp pf; parent f = Some pf; is_file s f; valid s;
+ sectxt_of_obj s (O_file f) = Some fctxt; search_check_file sp fctxt\<rbrakk>
+ \<Longrightarrow> search_check s sp f"
+apply (case_tac f, simp+)
+apply (auto split:option.splits simp:search_check_ctxt_def)
+apply (frule parentf_is_dir_prop2, simp)
+apply (erule get_pfs_secs_prop, simp)
+apply (erule_tac search_check_allp_intro, simp_all)
+apply (simp add:parentf_is_dir_prop2)
+done
-lemma enrich_proc_dup_ffd_eq:
- "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
- \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = file_of_proc_fd s p fd"
-apply (case_tac "file_of_proc_fd s p fd")
-apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
-apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
-done
lemma current_fflag_in_fds:
"\<lbrakk>flags_of_proc_fd s p fd = Some flag; valid s\<rbrakk> \<Longrightarrow> fd \<in> current_proc_fds s p"
@@ -1333,37 +1232,6 @@
apply (auto split:if_splits option.splits dest:proc_fd_in_fds)
done
-lemma enrich_proc_dup_fflags:
- "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
- \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
- flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
-apply (induct s arbitrary:p, simp add:is_created_proc_def)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
- dest:not_all_procs_prop3 split:if_splits option.splits)
-done
-
-lemma enrich_proc_dup_ffds:
- "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
- \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
-apply (auto simp:proc_file_fds_def)
-apply (rule_tac x = f in exI)
-apply (erule enrich_proc_dup_ffd', simp+)
-apply (rule_tac x = f in exI)
-apply (erule enrich_proc_dup_ffd, simp+)
-done
-
-lemma enrich_proc_dup_ffds_eq_fds:
- "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
- \<Longrightarrow> current_proc_fds (enrich_proc s p p') p' = proc_file_fds s p"
-apply (induct s arbitrary:p)
-apply (simp add: is_created_proc_def)
-apply (frule not_all_procs_prop3)
-apply (frule vd_cons, frule vt_grant_os, case_tac a)
-apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3
- simp:proc_file_fds_def is_created_proc_def)
-done
-
lemma oflags_check_remove_create:
"oflags_check flags sp sf \<Longrightarrow> oflags_check (remove_create_flag flags) sp sf"
apply (case_tac flags)
--- a/no_shm_selinux/Enrich2.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Enrich2.thy Tue Dec 31 14:57:13 2013 +0800
@@ -5,44 +5,147 @@
context tainting_s begin
-(* \<And> *)
-lemma current_proc_fds_in_curp:
- "\<lbrakk>fd \<in> current_proc_fds s p; valid s\<rbrakk> \<Longrightarrow> p \<in> current_procs s"
+
+fun enrich_msgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msgq \<Rightarrow> t_state"
+where
+ "enrich_msgq [] tq dq = []"
+| "enrich_msgq (CreateMsgq p q # s) tq dq =
+ (if (tq = q)
+ then (CreateMsgq p dq # CreateMsgq p q # s)
+ else CreateMsgq p q # (enrich_msgq s tq dq))"
+| "enrich_msgq (SendMsg p q m # s) tq dq =
+ (if (tq = q)
+ then (SendMsg p dq m # SendMsg p q m # (enrich_msgq s tq dq))
+ else SendMsg p q m # (enrich_msgq s tq dq))"
+| "enrich_msgq (RecvMsg p q m # s) tq dq =
+ (if (tq = q)
+ then (RecvMsg p dq m # RecvMsg p q m # (enrich_msgq s tq dq))
+ else RecvMsg p q m # (enrich_msgq s tq dq))"
+| "enrich_msgq (e # s) tq dq = e # (enrich_msgq s tq dq)"
+
+
+
+(* enrich s target_proc duplicated_pro *)
+fun enrich_proc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> t_state"
+where
+ "enrich_proc [] tp dp = []"
+| "enrich_proc (Execve p f fds # s) tp dp = (
+ if (tp = p)
+ then Execve dp f (fds \<inter> proc_file_fds s p) # Execve p f fds # (enrich_proc s tp dp)
+ else Execve p f fds # (enrich_proc s tp dp))"
+| "enrich_proc (Clone p p' fds # s) tp dp = (
+ if (tp = p')
+ then Clone p dp (fds \<inter> proc_file_fds s p) # Clone p p' fds # s
+ else Clone p p' fds # (enrich_proc s tp dp))"
+| "enrich_proc (Open p f flags fd opt # s) tp dp = (
+ if (tp = p)
+ then Open dp f (remove_create_flag flags) fd None # Open p f flags fd opt # (enrich_proc s tp dp)
+ else Open p f flags fd opt # (enrich_proc s tp dp))"
+| "enrich_proc (ReadFile p fd # s) tp dp = (
+ if (tp = p)
+ then ReadFile dp fd # ReadFile p fd # (enrich_proc s tp dp)
+ else ReadFile p fd # (enrich_proc s tp dp))"
+(*
+| "enrich_proc (CloseFd p fd # s) tp dp = (
+ if (tp = p \<and> fd \<in> proc_file_fds s p)
+ then CloseFd dp fd # CloseFd p fd # (enrich_proc s tp dp)
+ else CloseFd p fd # (enrich_proc s tp dp))"
+*)
+(*
+| "enrich_proc (Attach p h flag # s) tp dp = (
+ if (tp = p)
+ then Attach dp h flag # Attach p h flag # (enrich_proc s tp dp)
+ else Attach p h flag # (enrich_proc s tp dp))"
+| "enrich_proc (Detach p h # s) tp dp = (
+ if (tp = p)
+ then Detach dp h # Detach p h # (enrich_proc s tp dp)
+ else Detach p h # (enrich_proc s tp dp))"
+*)
+(*
+| "enrich_proc (Kill p p' # s) tp dp = (
+ if (tp = p') then Kill p p' # s
+ else Kill p p' # (enrich_proc s tp dp))"
+| "enrich_proc (Exit p # s) tp dp = (
+ if (tp = p) then Exit p # s
+ else Exit p # (enrich_proc s tp dp))"
+*)
+| "enrich_proc (e # s) tp dp = e # (enrich_proc s tp dp)"
+
+definition is_created_proc:: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+ "is_created_proc s p \<equiv> p \<in> current_procs s \<and> (p \<in> init_procs \<longrightarrow> died (O_proc p) s)"
+
+definition is_created_proc':: "t_state \<Rightarrow> t_process \<Rightarrow> bool"
+where
+ "is_created_proc' s p \<equiv> p \<in> current_procs s \<and> p \<notin> init_procs"
+
+lemma created_proc_clone:
+ "valid (Clone p p' fds # s) \<Longrightarrow>
+ is_created_proc (Clone p p' fds # s) tp = (if (tp = p') then True else is_created_proc s tp)"
+apply (drule vt_grant_os)
+apply (auto simp:is_created_proc_def dest:not_all_procs_prop2)
+using not_died_init_proc
+by auto
+
+lemma created_proc_exit:
+ "is_created_proc (Exit p # s) tp = (if (tp = p) then False else is_created_proc s tp)"
+by (simp add:is_created_proc_def)
+
+lemma created_proc_kill:
+ "is_created_proc (Kill p p' # s) tp = (if (tp = p') then False else is_created_proc s tp)"
+by (simp add:is_created_proc_def)
+
+lemma created_proc_other:
+ "\<lbrakk>\<And> p p' fds. e \<noteq> Clone p p' fds;
+ \<And> p. e \<noteq> Exit p;
+ \<And> p p'. e \<noteq> Kill p p'\<rbrakk> \<Longrightarrow> is_created_proc (e # s) tp = is_created_proc s tp"
+by (case_tac e, auto simp:is_created_proc_def)
+
+lemmas is_created_proc_simps = created_proc_clone created_proc_exit created_proc_kill created_proc_other
+
+lemma no_del_died:
+ "\<lbrakk>no_del_event s; died obj s\<rbrakk> \<Longrightarrow> (\<exists> p fd. obj = O_fd p fd \<or> obj = O_tcp_sock (p, fd) \<or> obj = O_udp_sock (p, fd))
+ \<or> (\<exists> q m. obj = O_msg q m) "
apply (induct s)
-apply (simp add:init_fds_of_proc_prop1)
-apply (frule vt_grant_os, frule vd_cons)
-apply (case_tac a, auto split:if_splits option.splits)
-done
-
-lemma get_parentfs_ctxts_prop:
- "\<lbrakk>get_parentfs_ctxts s (a # f) = Some ctxts; sectxt_of_obj s (O_dir f) = Some ctxt; valid s\<rbrakk>
- \<Longrightarrow> ctxt \<in> set (ctxts)"
-apply (induct f)
+apply simp
+apply (case_tac a)
apply (auto split:option.splits)
done
-lemma search_check_allp_intro:
- "\<lbrakk>search_check s sp pf; get_parentfs_ctxts s pf = Some ctxts; valid s; is_dir s pf\<rbrakk>
- \<Longrightarrow> search_check_allp sp (set ctxts)"
-apply (case_tac pf)
-apply (simp split:option.splits if_splits add:search_check_allp_def)
-apply (rule ballI)
-apply (auto simp:search_check_ctxt_def search_check_dir_def split:if_splits option.splits)
-apply (auto simp:search_check_allp_def search_check_file_def)
-apply (frule is_dir_not_file, simp)
+lemma no_del_created_eq:
+ "no_del_event s \<Longrightarrow> is_created_proc s p = is_created_proc' s p"
+apply (induct s)
+apply (simp add:is_created_proc_def is_created_proc'_def)
+apply (case_tac a)
+apply (auto simp add:is_created_proc_def is_created_proc'_def dest:no_del_died)
+done
+
+lemma enrich_proc_dup_in:
+ "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+ \<Longrightarrow> p' \<in> current_procs (enrich_proc s p p')"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def dest:not_all_procs_prop3)
done
-lemma search_check_leveling_f:
- "\<lbrakk>search_check s sp pf; parent f = Some pf; is_file s f; valid s;
- sectxt_of_obj s (O_file f) = Some fctxt; search_check_file sp fctxt\<rbrakk>
- \<Longrightarrow> search_check s sp f"
-apply (case_tac f, simp+)
-apply (auto split:option.splits simp:search_check_ctxt_def)
-apply (frule parentf_is_dir_prop2, simp)
-apply (erule get_pfs_secs_prop, simp)
-apply (erule_tac search_check_allp_intro, simp_all)
-apply (simp add:parentf_is_dir_prop2)
-done
+lemma enrich_proc_dup_ffd:
+ "\<lbrakk>file_of_proc_fd s p fd = Some f; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+ \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = Some f"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+ dest:not_all_procs_prop3 split:if_splits option.splits)
+done
+
+lemma enrich_proc_dup_ffd':
+ "\<lbrakk>file_of_proc_fd (enrich_proc s p p') p' fd = Some f; is_created_proc s p; p' \<notin> all_procs s;
+ no_del_event s; valid s\<rbrakk>
+ \<Longrightarrow> file_of_proc_fd s p fd = Some f"
+apply (induct s, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def
+ dest:not_all_procs_prop3 split:if_splits option.splits)
+done
lemma enrich_proc_dup_ffds':
"\<lbrakk>fd \<notin> current_proc_fds (enrich_proc s p p') p'; is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
@@ -51,6 +154,46 @@
apply (simp add:proc_file_fds_def)
done
+lemma enrich_proc_dup_ffd_eq:
+ "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+ \<Longrightarrow> file_of_proc_fd (enrich_proc s p p') p' fd = file_of_proc_fd s p fd"
+apply (case_tac "file_of_proc_fd s p fd")
+apply (case_tac[!] "file_of_proc_fd (enrich_proc s p p') p' fd")
+apply (auto dest:enrich_proc_dup_ffd enrich_proc_dup_ffd')
+done
+
+
+lemma enrich_proc_dup_fflags:
+ "\<lbrakk>flags_of_proc_fd s p fd = Some flag; is_created_proc s p; p' \<notin> all_procs s; valid s\<rbrakk>
+ \<Longrightarrow> flags_of_proc_fd (enrich_proc s p p') p' fd = Some (remove_create_flag flag) \<or>
+ flags_of_proc_fd (enrich_proc s p p') p' fd = Some flag"
+apply (induct s arbitrary:p, simp add:is_created_proc_def)
+apply (frule vt_grant_os, frule vd_cons)
+apply (case_tac a, auto simp:is_created_proc_def proc_file_fds_def is_creat_flag_def
+ dest:not_all_procs_prop3 split:if_splits option.splits)
+done
+
+lemma enrich_proc_dup_ffds:
+ "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+ \<Longrightarrow> proc_file_fds (enrich_proc s p p') p' = proc_file_fds s p"
+apply (auto simp:proc_file_fds_def)
+apply (rule_tac x = f in exI)
+apply (erule enrich_proc_dup_ffd', simp+)
+apply (rule_tac x = f in exI)
+apply (erule enrich_proc_dup_ffd, simp+)
+done
+
+lemma enrich_proc_dup_ffds_eq_fds:
+ "\<lbrakk>is_created_proc s p; p' \<notin> all_procs s; no_del_event s; valid s\<rbrakk>
+ \<Longrightarrow> current_proc_fds (enrich_proc s p p') p' = proc_file_fds s p"
+apply (induct s arbitrary:p)
+apply (simp add: is_created_proc_def)
+apply (frule not_all_procs_prop3)
+apply (frule vd_cons, frule vt_grant_os, case_tac a)
+apply (auto split:if_splits option.splits dest:proc_fd_in_fds set_mp not_all_procs_prop3
+ simp:proc_file_fds_def is_created_proc_def)
+done
+
lemma enrich_proc_cur_inof:
"\<lbrakk>valid s; no_del_event s\<rbrakk> \<Longrightarrow> inum_of_file (enrich_proc s p p') f = inum_of_file s f"
apply (induct s arbitrary:f)
--- a/no_shm_selinux/Finite_current.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Finite_current.thy Tue Dec 31 14:57:13 2013 +0800
@@ -92,6 +92,12 @@
apply (case_tac a, auto simp: init_finite_sets)
done
+lemma maxium_queue:
+ "valid s \<Longrightarrow> length (msgs_of_queue s q) \<le> max_queue"
+apply (induct s)
+apply (simp add:init_msgq_valid)
+apply (frule vt_grant_os, frule vd_cons, case_tac a, auto)
+done
lemma finite_option: "finite {x. \<exists> y. f x = Some y} \<Longrightarrow> finite {y. \<exists> x. f x = Some y}"
apply (drule_tac h = f in finite_imageI)
--- a/no_shm_selinux/Flask.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Flask.thy Tue Dec 31 14:57:13 2013 +0800
@@ -135,8 +135,11 @@
*)
and init_socket_state :: "t_socket \<rightharpoonup> t_sock_state"
+(*
and init_msgqs :: "t_msgq set"
and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"
+*)
+ and max_queue :: "nat"
(*
and init_shms :: "t_shm set"
and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"
@@ -162,8 +165,12 @@
and init_procs_has_shm: "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms \<and> init_flag_of_proc_shm p h = Some flag"
and init_shmflag_has_proc: "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"
*)
+
+(*
and init_msgs_distinct: "\<And> q. distinct (init_msgs_of_queue q)"
and init_msgs_valid: "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"
+ and init_msgq_valid: "\<And> q. length (init_msgs_of_queue q) \<le> max_queue"
+*)
and init_socket_has_inode: "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p \<and> init_file_of_proc_fd p fd = None"
and inos_has_sock_tag: "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"
@@ -174,7 +181,7 @@
and init_netobj_has_raddr: "\<And> s. after_conacc (init_netobj_state s) \<Longrightarrow> init_netobj_remoteaddr s \<noteq> None"
*)
- and init_finite_sets: "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_msgqs \<and> finite init_users"
+ and init_finite_sets: "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_users" (* finite init_msgqs *)
begin
@@ -226,8 +233,8 @@
(*
| "init_alive (O_shm h) = (h \<in> init_shms)"
*)
-| "init_alive (O_msgq q) = (q \<in> init_msgqs)"
-| "init_alive (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
+| "init_alive (O_msgq q) = False" (* (q \<in> init_msgqs) *)
+| "init_alive (O_msg q m) = False" (* (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)" *)
(************ system listeners, event-related ***********)
@@ -512,14 +519,14 @@
fun current_msgqs :: "t_state \<Rightarrow> t_msgq set"
where
- "current_msgqs [] = init_msgqs"
+ "current_msgqs [] = {}" (* init_msgqs *)
| "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"
| "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}"
| "current_msgqs (_ # \<tau>) = current_msgqs \<tau>"
fun msgs_of_queue :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list"
where
- "msgs_of_queue [] = init_msgs_of_queue"
+ "msgs_of_queue [] = (\<lambda> x. [])" (* init_msgs_of_queue*)
| "msgs_of_queue (CreateMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"
| "msgs_of_queue (SendMsg p q m # \<tau>) = (msgs_of_queue \<tau>)(q := msgs_of_queue \<tau> q @ [m])"
| "msgs_of_queue (RecvMsg p q m # \<tau>) = (msgs_of_queue \<tau>)(q := tl (msgs_of_queue \<tau> q))"
@@ -720,7 +727,8 @@
| "os_grant \<tau> (CreateMsgq p q) =
(p \<in> current_procs \<tau> \<and> q \<notin> (current_msgqs \<tau>))"
| "os_grant \<tau> (SendMsg p q m) =
- (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)))"
+ (p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m \<notin> (set (msgs_of_queue \<tau> q)) \<and>
+ length (msgs_of_queue \<tau> q) < max_queue)"
| "os_grant \<tau> (RecvMsg p q m) =
(p \<in> current_procs \<tau> \<and> q \<in> current_msgqs \<tau> \<and> m = hd (msgs_of_queue \<tau> q) \<and> msgs_of_queue \<tau> q \<noteq> [])"
| "os_grant \<tau> (RemoveMsgq p q) =
@@ -1477,7 +1485,8 @@
"valid []"
| "\<lbrakk>valid s; os_grant s e; grant s e\<rbrakk> \<Longrightarrow> valid (e # s)"
-(* tobj: object that can be tainted *)
+
+(* tobj: object that can be tainted
fun tobj_in_init :: "t_object \<Rightarrow> bool"
where
"tobj_in_init (O_proc p) = (p \<in> init_procs)"
@@ -1489,6 +1498,8 @@
| "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
*)
| "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
+*)
+
(* no use
fun no_del_event:: "t_event list \<Rightarrow> bool"
--- a/no_shm_selinux/Init_prop.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Init_prop.thy Tue Dec 31 14:57:13 2013 +0800
@@ -334,13 +334,13 @@
lemma init_alive_node: "n \<in> init_nodes \<Longrightarrow> init_alive (O_node n)" by simp
(*
lemma init_alive_shm: "h \<in> init_shms \<Longrightarrow> init_alive (O_shm h)" by simp
-*)
lemma init_alive_msgq: "q \<in> init_msgqs \<Longrightarrow> init_alive (O_msgq q)" by simp
lemma init_alive_msg: "\<lbrakk>m \<in> set (init_msgs_of_queue q); q \<in> init_msgqs\<rbrakk>
\<Longrightarrow> init_alive (O_msg q m)" by simp
+*)
lemmas init_alive_intros = init_alive_proc init_alive_file init_alive_dir init_alive_fd
- init_alive_tcp init_alive_udp init_alive_node init_alive_msgq init_alive_msg (*init_alive_shm*)
+ init_alive_tcp init_alive_udp init_alive_node (*init_alive_msgq init_alive_msg*) (*init_alive_shm*)
lemma init_file_type_prop1: "is_init_file f \<Longrightarrow> \<exists> t. init_type_of_obj (O_file f) = Some t"
@@ -541,6 +541,7 @@
by (rule notI, drule init_shm_has_ctxt, simp)
*)
+(*
lemma init_msgq_has_ctxt:
"q \<in> init_msgqs \<Longrightarrow> \<exists> sec. init_sectxt_of_obj (O_msgq q) = Some sec"
apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -560,6 +561,7 @@
lemma init_msg_has_ctxt':
"init_sectxt_of_obj (O_msg q m) = None \<Longrightarrow> m \<notin> set (init_msgs_of_queue q) \<or> q \<notin> init_msgqs"
by (auto dest:init_msg_has_ctxt)
+*)
lemma init_rootf_has_ctxt:
"\<exists> sec. init_sectxt_of_obj (O_dir []) = Some sec"
@@ -571,12 +573,12 @@
using init_rootf_has_ctxt by auto
lemmas init_has_ctxt = init_file_has_ctxt init_dir_has_ctxt init_proc_has_ctxt init_fd_has_ctxt
- init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) init_msgq_has_ctxt
- init_msg_has_ctxt init_rootf_has_ctxt
+ init_node_has_ctxt init_tcp_has_ctxt init_udp_has_ctxt (* init_shm_has_ctxt *) (* init_msgq_has_ctxt
+ init_msg_has_ctxt*) init_rootf_has_ctxt
lemmas init_has_ctxt' = init_file_has_ctxt' init_dir_has_ctxt' init_proc_has_ctxt' init_fd_has_ctxt'
- init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) init_msgq_has_ctxt'
- init_msg_has_ctxt' init_rootf_has_ctxt'
+ init_node_has_ctxt' init_tcp_has_ctxt' init_udp_has_ctxt' (* init_shm_has_ctxt' *) (*init_msgq_has_ctxt'
+ init_msg_has_ctxt'*) init_rootf_has_ctxt'
lemma sec_of_root_valid:
"init_sectxt_of_obj (O_dir []) = Some sec_of_root"
@@ -668,6 +670,7 @@
apply (simp add:init_cp2sproc_def)
by (case_tac sec, simp+)
+(*
lemma init_cqm2sms_has_sms_aux:
"\<forall> m \<in> set ms. init_sectxt_of_obj (O_msg q m) \<noteq> None \<Longrightarrow> (\<exists> sms. init_cqm2sms q ms = Some sms)"
by (induct ms, auto split:option.splits simp:init_cm2smsg_def)
@@ -682,6 +685,7 @@
apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
apply (simp add:init_cq2smsgq_def)
by (case_tac sec, simp+)
+*)
lemma cf2sfile_nil_prop:
"f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
@@ -758,6 +762,7 @@
by (auto simp add:init_cp2sproc_def cp2sproc_def init_sectxt_prop cpfd2sfds_nil_prop (*cph2spshs_nil_prop*)
split:option.splits)
+(*
lemma msg_has_sec_imp_init:
"init_sectxt_of_obj (O_msg q m) = Some sec \<Longrightarrow> q \<in> init_msgqs \<and> m \<in> set (init_msgs_of_queue q)"
apply (simp add:init_sectxt_of_obj_def split:option.splits)
@@ -783,14 +788,15 @@
"cq2smsgq [] q = init_cq2smsgq q"
by (auto simp add:cq2smsgq_def init_cq2smsgq_def init_sectxt_prop cqm2sms_nil_prop
intro:msgq_has_sec_imp_init split:option.splits)
+*)
lemma co2sobj_nil_prop:
"init_alive obj \<Longrightarrow> co2sobj [] obj = init_obj2sobj obj"
apply (case_tac obj)
-apply (auto simp add:cf2sfile_nil_prop cq2smsga_nil_prop cqm2sms_nil_prop tainted_nil_prop
+apply (auto simp add:cf2sfile_nil_prop (*cq2smsga_nil_prop cqm2sms_nil_prop*) tainted_nil_prop
cp2sproc_nil_prop cfs2sfiles_nil_prop is_init_dir_prop1 is_init_file_prop1
is_init_udp_sock_prop1 is_init_tcp_sock_prop1 (* ch2sshm_nil_prop *)
- same_inode_nil_prop cm2smsg_nil_prop
+ same_inode_nil_prop (*cm2smsg_nil_prop *)
dest:init_same_inode_prop1
split:option.splits)
apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
--- a/no_shm_selinux/ROOT Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/ROOT Tue Dec 31 14:57:13 2013 +0800
@@ -35,4 +35,10 @@
options [document = false]
theories
S2ss_prop
- S2ss_prop2
\ No newline at end of file
+ S2ss_prop2
+
+session "enrich" = "s2ss" +
+ options [document = false]
+ theories
+ Enrich
+ Enrich1
\ No newline at end of file
--- a/no_shm_selinux/Static.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Static.thy Tue Dec 31 14:57:13 2013 +0800
@@ -77,6 +77,7 @@
where
"init_o2s_afs f \<equiv> {sec. \<exists> f'. f' \<preceq> f \<and> init_sectxt_of_obj (O_dir f') = Some sec}" *)
+(*
definition init_cm2smsg :: "t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
where
"init_cm2smsg q m \<equiv> (case (init_sectxt_of_obj (O_msg q m)) of
@@ -96,6 +97,7 @@
"init_cq2smsgq q \<equiv> (case (init_sectxt_of_obj (O_msgq q), init_cqm2sms q (init_msgs_of_queue q)) of
(Some sec, Some sms) \<Rightarrow> Some (Init q, sec, sms)
| _ \<Rightarrow> None)"
+*)
fun init_obj2sobj :: "t_object \<Rightarrow> t_sobject option"
where
@@ -110,11 +112,13 @@
(case (init_cf2sfile f) of
Some sf \<Rightarrow> Some (S_dir sf)
| _ \<Rightarrow> None)"
-| "init_obj2sobj (O_msgq q) =
+| "init_obj2sobj (O_msgq q) = None"
+
+(*
(case (init_cq2smsgq q) of
Some sq \<Rightarrow> Some (S_msgq sq)
| _ \<Rightarrow> None)"
-(*
+
| "init_obj2sobj (O_shm h) =
(case (init_ch2sshm h) of
Some sh \<Rightarrow> Some (S_shm sh)
@@ -184,6 +188,7 @@
cpfd2sfds s p)
| _ \<Rightarrow> None)"
+(*
definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
where
"cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
@@ -191,6 +196,13 @@
Some (if (\<not> died (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q)) then Init m else Created,
sec, O_msg q m \<in> tainted s)
| _ \<Rightarrow> None)"
+*)
+
+definition cm2smsg :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg \<Rightarrow> t_smsg option"
+where
+ "cm2smsg s q m \<equiv> (case (sectxt_of_obj s (O_msg q m)) of
+ Some sec \<Rightarrow> Some (Created, sec, O_msg q m \<in> tainted s)
+ | _ \<Rightarrow> None)"
fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
where
@@ -199,7 +211,7 @@
(case (cqm2sms s q ms, cm2smsg s q m) of
(Some sms, Some sm) \<Rightarrow> Some (sm#sms)
| _ \<Rightarrow> None)"
-
+(*
definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
where
"cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
@@ -207,6 +219,13 @@
Some (if (\<not> died (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
sec, sms)
| _ \<Rightarrow> None)"
+*)
+
+definition cq2smsgq :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_smsgq option"
+where
+ "cq2smsgq s q \<equiv> (case (sectxt_of_obj s (O_msgq q), cqm2sms s q (msgs_of_queue s q)) of
+ (Some sec, Some sms) \<Rightarrow> Some (Created, sec, sms)
+ | _ \<Rightarrow> None)"
fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
where
@@ -266,22 +285,24 @@
"is_many_sproc (Created, sec,fds) = True"
| "is_many_sproc _ = False"
+(*
fun is_many_smsg :: "t_smsg \<Rightarrow> bool"
where
"is_many_smsg (Created,sec,tag) = True"
| "is_many_smsg _ = False"
-
+*)
(* wrong def
fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
where
"is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))"
| "is_many_smsgq _ = False"
*)
-
+(*
fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool"
where
"is_many_smsgq (Created,sec,sms) = True"
| "is_many_smsgq _ = False"
+*)
(*
fun is_many_sshm :: "t_sshm \<Rightarrow> bool"
where
@@ -293,16 +314,17 @@
"is_many (S_proc sp tag) = is_many_sproc sp"
| "is_many (S_file sfs tag) = (\<forall> sf \<in> sfs. is_many_sfile sf)"
| "is_many (S_dir sf ) = is_many_sfile sf"
-| "is_many (S_msgq sq ) = is_many_smsgq sq"
+| "is_many (S_msgq sq ) = True"
(*
| "is_many (S_shm sh ) = is_many_sshm sh"
*)
+(*
fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool"
where
"is_init_smsgq (Init q,sec,sms) = True"
| "is_init_smsgq _ = False"
-
+*)
(*
fun is_init_sshm :: "t_sshm \<Rightarrow> bool"
where
@@ -314,7 +336,7 @@
"is_init_sobj (S_proc sp tag ) = is_init_sproc sp"
| "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)"
| "is_init_sobj (S_dir sf ) = is_init_sfile sf"
-| "is_init_sobj (S_msgq sq ) = is_init_smsgq sq"
+| "is_init_sobj (S_msgq sq ) = False"
(*
| "is_init_sobj (S_shm sh ) = is_init_sshm sh"
*)
--- a/no_shm_selinux/Temp.thy Mon Dec 30 23:41:58 2013 +0800
+++ b/no_shm_selinux/Temp.thy Tue Dec 31 14:57:13 2013 +0800
@@ -124,7 +124,7 @@
| s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
permission_check pctxt qctxt C_msgq P_enqueue;
permission_check pctxt qctxt C_msgq P_write;
- permission_check pctxt pctxt C_msg P_create\<rbrakk>
+ permission_check pctxt pctxt C_msg P_create; length sms < max_queue\<rbrakk>
\<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms))
(S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static"
| s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds) tagp \<in> ss;