--- a/simple_selinux/Sectxt_prop.thy Mon Dec 02 10:52:40 2013 +0800
+++ b/simple_selinux/Sectxt_prop.thy Tue Dec 03 22:42:48 2013 +0800
@@ -31,14 +31,13 @@
have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. type_of_obj s (O_fd p fd) = Some t"
by (auto intro:a1)
have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. type_of_obj s (O_node n) = Some t" by (auto intro:a1)
- have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t" by (auto intro:a1)
have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t" by (auto intro:a1)
have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk>
\<Longrightarrow> \<exists> t. type_of_obj s (O_msg q m) = Some t" by (auto intro:a1)
show ?case using a5 a2 a4 a3
apply (case_tac e)
apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
- dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+ dest!:a1' intro:a1 p1 p2 p3 p4 p5 p6 p7 p9 p10 simp:alive_simps)
apply (frule_tac p = nat1 in file_fds_subset_pfds)
apply (rule a1, auto)
done
@@ -71,14 +70,13 @@
have p6: "\<And> p fd. fd \<in> current_proc_fds s p \<Longrightarrow> \<exists> t. user_of_obj s (O_fd p fd) = Some t"
by (auto intro:a1)
have p7: "\<And> n. n \<in> init_nodes \<Longrightarrow> \<exists> t. user_of_obj s (O_node n) = Some t" by (auto intro:a1)
- have p8: "\<And> h. h \<in> current_shms s \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t" by (auto intro:a1)
have p9: "\<And> q. q \<in> current_msgqs s \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t" by (auto intro:a1)
have p10: "\<And> q m. \<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s\<rbrakk>
\<Longrightarrow> \<exists> t. user_of_obj s (O_msg q m) = Some t" by (auto intro:a1)
show ?case using a5 a2 a4 a3
apply (case_tac e)
apply (auto split:option.splits t_object.splits if_splits t_socket_type.splits
- dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 simp:alive_simps)
+ dest!:a1' intro:a1 intro:p1 p2 p3 p4 p5 p6 p7 p9 p10 simp:alive_simps)
apply (frule_tac p = nat1 in file_fds_subset_pfds)
apply (rule a1, auto)
done
@@ -131,12 +129,6 @@
lemma init_node_has_type': "\<lbrakk>type_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes"
by (auto intro:notI dest:init_node_has_type)
-lemma current_shm_has_type: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_shm h) = Some t"
-by (auto intro:alive_obj_has_type)
-
-lemma current_shm_has_type': "\<lbrakk>type_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
-by (auto intro:notI dest:current_shm_has_type)
-
lemma current_msgq_has_type: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. type_of_obj s (O_msgq q) = Some t"
by (auto intro:alive_obj_has_type)
@@ -152,11 +144,11 @@
by (auto dest!:current_msg_has_type)
lemmas current_has_type = alive_obj_has_type current_proc_has_type is_file_has_type is_dir_has_type
- is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type current_shm_has_type
+ is_tcp_has_type is_udp_has_type current_fd_has_type init_node_has_type
current_msgq_has_type current_msg_has_type
lemmas current_has_type' = alive_obj_has_type' current_proc_has_type' is_file_has_type' is_dir_has_type'
- is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type' current_shm_has_type'
+ is_tcp_has_type' is_udp_has_type' current_fd_has_type' init_node_has_type'
current_msgq_has_type' current_msg_has_type'
lemma alive_obj_has_user': "\<lbrakk>user_of_obj s obj = None; valid s\<rbrakk> \<Longrightarrow> \<not> alive s obj"
@@ -206,12 +198,6 @@
lemma init_node_has_user': "\<lbrakk>user_of_obj s (O_node n) = None; valid s\<rbrakk> \<Longrightarrow> n \<notin> init_nodes"
by (auto intro:notI dest:init_node_has_user)
-lemma current_shm_has_user: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_shm h) = Some t"
-by (auto intro:alive_obj_has_user)
-
-lemma current_shm_has_user': "\<lbrakk>user_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
-by (auto intro:notI dest:current_shm_has_user)
-
lemma current_msgq_has_user: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> t. user_of_obj s (O_msgq q) = Some t"
by (auto intro:alive_obj_has_user)
@@ -227,11 +213,11 @@
by (auto dest!:current_msg_has_user)
lemmas current_has_user = alive_obj_has_user current_proc_has_user is_file_has_user is_dir_has_user
- is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user current_shm_has_user
+ is_tcp_has_user is_udp_has_user current_fd_has_user init_node_has_user
current_msgq_has_user current_msg_has_user
lemmas current_has_user' = alive_obj_has_user' current_proc_has_user' is_file_has_user' is_dir_has_user'
- is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user' current_shm_has_user'
+ is_tcp_has_user' is_udp_has_user' current_fd_has_user' init_node_has_user'
current_msgq_has_user' current_msg_has_user'
lemma current_proc_has_role:
@@ -334,15 +320,6 @@
lemma init_node_has_sec'': "\<lbrakk>n \<in> init_nodes; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_node n) = Some (u,r,t)"
by (drule init_node_has_sec, simp+)
-lemma current_shm_has_sec: "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_shm h) = Some sec"
-by (rule alive_obj_has_sec, simp+)
-
-lemma current_shm_has_sec': "\<lbrakk>sectxt_of_obj s (O_shm h) = None; valid s\<rbrakk> \<Longrightarrow> h \<notin> current_shms s"
-by (auto intro:notI dest:current_shm_has_sec)
-
-lemma current_shm_has_sec'': "\<lbrakk>h \<in> current_shms s; valid s\<rbrakk> \<Longrightarrow> \<exists> u r t. sectxt_of_obj s (O_shm h) = Some (u,r,t)"
-by (drule current_shm_has_sec, simp+)
-
lemma current_msgq_has_sec: "\<lbrakk>q \<in> current_msgqs s; valid s\<rbrakk> \<Longrightarrow> \<exists> sec. sectxt_of_obj s (O_msgq q) = Some sec"
by (rule alive_obj_has_sec, simp+)
@@ -366,15 +343,15 @@
by (drule current_msg_has_sec, simp+)
lemmas current_has_sec = alive_obj_has_sec current_proc_has_sec is_file_has_sec is_dir_has_sec
- is_tcp_has_sec is_udp_has_sec current_fd_has_sec init_node_has_sec current_shm_has_sec
+ is_tcp_has_sec is_udp_has_sec current_fd_has_sec init_node_has_sec
current_msgq_has_sec current_msg_has_sec
lemmas current_has_sec' = alive_obj_has_sec' current_proc_has_sec' is_file_has_sec' is_dir_has_sec'
- is_tcp_has_sec' is_udp_has_sec' current_fd_has_sec' init_node_has_sec' current_shm_has_sec'
+ is_tcp_has_sec' is_udp_has_sec' current_fd_has_sec' init_node_has_sec'
current_msgq_has_sec' current_msg_has_sec'
lemmas current_has_sec'' = alive_obj_has_sec'' current_proc_has_sec'' is_file_has_sec'' is_dir_has_sec''
- is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec'' current_shm_has_sec''
+ is_tcp_has_sec'' is_udp_has_sec'' current_fd_has_sec'' init_node_has_sec''
current_msgq_has_sec'' current_msg_has_sec''
(************ root sec remains ************)
@@ -443,7 +420,7 @@
done
lemma sec_clone:
- "valid (Clone p p' fds shms # s) \<Longrightarrow> sectxt_of_obj (Clone p p' fds shms # s) = (\<lambda> obj.
+ "valid (Clone p p' fds # s) \<Longrightarrow> sectxt_of_obj (Clone p p' fds # s) = (\<lambda> obj.
case obj of
O_proc p'' \<Rightarrow> if (p'' = p') then sectxt_of_obj s (O_proc p)
else sectxt_of_obj s obj
@@ -498,20 +475,6 @@
dest!:current_has_type' current_proc_has_role' current_has_user')
done
-lemma sec_linkhard:
- "valid (LinkHard p f f' # s) \<Longrightarrow> sectxt_of_obj (LinkHard p f f' # s) =
- (sectxt_of_obj s) (O_file f' :=
- (case parent f' of
- None \<Rightarrow> None
- | Some pf \<Rightarrow> (case (sectxt_of_obj s (O_proc p), sectxt_of_obj s (O_dir pf)) of
- (Some psec, Some pfsec) \<Rightarrow> Some (fst psec, R_object,
- type_transition ((snd o snd) psec) ((snd o snd) pfsec) C_file True)
- | _ \<Rightarrow> None)))"
-apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
-apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
- dest!:current_has_type' current_proc_has_role' current_has_user')
-done
-
lemma sec_createmsgq:
"valid (CreateMsgq p q # s) \<Longrightarrow> sectxt_of_obj (CreateMsgq p q # s) = (sectxt_of_obj s) (O_msgq q :=
(case (sectxt_of_obj s (O_proc p)) of
@@ -533,16 +496,6 @@
dest!:current_has_type' current_proc_has_role' current_has_user')
done
-lemma sec_createshm:
- "valid (CreateShM p h # s) \<Longrightarrow> sectxt_of_obj (CreateShM p h # s) = (sectxt_of_obj s) (O_shm h :=
- case (sectxt_of_obj s (O_proc p)) of
- Some psec \<Rightarrow> Some (fst psec, R_object, (snd o snd) psec)
- | _ \<Rightarrow> None)"
-apply (rule ext, frule vd_cons, frule vt_grant_os, case_tac x)
-apply (auto simp:sectxt_of_obj_def split:option.splits if_splits
- dest!:current_has_type' current_proc_has_role' current_has_user')
-done
-
lemma sec_createsock:
"valid (CreateSock p af st fd inum # s) \<Longrightarrow> sectxt_of_obj (CreateSock p af st fd inum # s) = (\<lambda> obj.
case obj of
@@ -588,11 +541,10 @@
lemma sec_others :
"\<lbrakk>valid (e # s);
- \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms;
+ \<forall> p p' fds. e \<noteq> Clone p p' fds;
\<forall> p f fds. e \<noteq> Execve p f fds;
\<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
\<forall> p f inum. e \<noteq> Mkdir p f inum;
- \<forall> p f f'. e \<noteq> LinkHard p f f';
\<forall> p q. e \<noteq> CreateMsgq p q;
\<forall> p q m. e \<noteq> SendMsg p q m;
\<forall> p h. e \<noteq> CreateShM p h;
@@ -648,18 +600,6 @@
"valid (RemoveMsgq p q # s) \<Longrightarrow> sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s"
by (auto dest!:sec_others)
-lemma sec_attach:
- "valid (Attach p h flag # s) \<Longrightarrow> sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s"
-by (auto dest!:sec_others)
-
-lemma sec_detach:
- "valid (Detach p h # s) \<Longrightarrow> sectxt_of_obj (Detach p h # s) = sectxt_of_obj s"
-by (auto dest!:sec_others)
-
-lemma sec_deleteshm:
- "valid (DeleteShM p h # s) \<Longrightarrow> sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s"
-by (auto dest!:sec_others)
-
lemma sec_bind:
"valid (Bind p fd addr # s) \<Longrightarrow> sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s"
by (auto dest!:sec_others)
@@ -684,11 +624,10 @@
"valid (Shutdown p fd how # s) \<Longrightarrow> sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s"
by (auto dest!:sec_others)
-lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg
- sec_createshm sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile
+lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_createmsgq sec_sendmsg
+ sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile
sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq
- sec_attach sec_detach sec_deleteshm sec_bind sec_connect sec_listen sec_sendsock
- sec_recvsock sec_shutdown
+ sec_bind sec_connect sec_listen sec_sendsock sec_recvsock sec_shutdown
(* init_sectxt_prop *)
(**************** get_parentfs_ctxts simpset **************)