--- a/Alive_prop.thy Wed Nov 20 13:44:32 2013 +0800
+++ b/Alive_prop.thy Wed Nov 20 15:19:58 2013 +0800
@@ -1,5 +1,5 @@
theory Alive_prop
-imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop
+imports Main Flask_type Flask Current_files_prop Current_sockets_prop Init_prop Proc_fd_of_file_prop
begin
context flask begin
@@ -51,6 +51,8 @@
dest:is_dir_in_current split:if_splits option.splits)
done
+(* sock is not inherited on Execve, Clone cases, cause I simplified it with os_grant.
+ * chunhan, 2013-11-20
lemma alive_execve:
"valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
\<lambda> obj. case obj of
@@ -68,6 +70,7 @@
apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
is_tcp_sock_simps is_udp_sock_simps
dest:is_dir_in_current split:if_splits option.splits)
+
done
lemma alive_clone:
@@ -90,6 +93,48 @@
intro:is_tcp_in_current is_udp_in_current
dest:is_dir_in_current split:if_splits option.splits)
done
+*)
+
+lemma alive_execve:
+ "valid (Execve p f fds # s) \<Longrightarrow> alive (Execve p f fds # s) = (
+ \<lambda> obj. case obj of
+ O_fd p' fd \<Rightarrow> (if (p = p' \<and> fd \<in> fds) then alive s (O_fd p fd)
+ else if (p = p') then False
+ else alive s (O_fd p' fd))
+ | O_tcp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+ else alive s (O_tcp_sock (p', fd)))
+ | O_udp_sock (p', fd) \<Rightarrow> (if (p = p') then False
+ else alive s (O_udp_sock (p', fd)))
+ | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ dest:is_dir_in_current split:if_splits option.splits)
+apply (drule_tac s = s and p = p in file_fds_subset_pfds, auto)
+
+done
+
+lemma alive_clone:
+ "valid (Clone p p' fds shms # s) \<Longrightarrow> alive (Clone p p' fds shms # s) = (
+ \<lambda> obj. case obj of
+ O_proc p'' \<Rightarrow> if (p'' = p') then True else alive s obj
+ | O_fd p'' fd \<Rightarrow> if (p'' = p' \<and> fd \<in> fds) then True
+ else if (p'' = p') then False
+ else alive s obj
+ | O_tcp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_tcp_sock (p, fd))
+ else if (p'' = p') then False
+ else alive s (O_tcp_sock (p'', fd)))
+ | O_udp_sock (p'', fd) \<Rightarrow> (if (p'' = p' \<and> fd \<in> fds) then alive s (O_udp_sock (p, fd))
+ else if (p'' = p') then False
+ else alive s (O_udp_sock (p'', fd)))
+ | _ \<Rightarrow> alive s obj )"
+apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac obj)
+apply (auto simp:current_files_simps current_sockets_simps is_file_simps is_dir_simps
+ is_tcp_sock_simps is_udp_sock_simps
+ intro:is_tcp_in_current is_udp_in_current
+ dest:is_dir_in_current split:if_splits option.splits)
+done
+
lemma alive_kill:
"valid (Kill p p' # s) \<Longrightarrow> alive (Kill p p' # s) = (
--- a/Dynamic_static.thy Wed Nov 20 13:44:32 2013 +0800
+++ b/Dynamic_static.thy Wed Nov 20 15:19:58 2013 +0800
@@ -119,7 +119,7 @@
lemma enrich_inherit_fds_check:
assumes grant: "inherit_fds_check s (up, nr, nt) p fds" and vd: "valid s"
- and fd2sfd: "\<forall> fd. fd \<in> current_procs s \<longrightarrow> cp2sproc s' p = cp2sproc s p"
+ 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"
shows "inherit_fds_check s' (up, nr, nt) p fds"
--- a/Flask.thy Wed Nov 20 13:44:32 2013 +0800
+++ b/Flask.thy Wed Nov 20 15:19:58 2013 +0800
@@ -154,7 +154,7 @@
init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))"
and init_procfds_valid: "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)"
- and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"
+ and init_filefd_valid: "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags) \<and> (p, fd) \<notin> init_sockets"
and init_fileflag_valid: "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"
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"
@@ -162,7 +162,7 @@
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_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_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)"
(*
and init_netobj_has_state: "bidirect_in_init init_netobjs init_netobj_state"
@@ -260,6 +260,13 @@
where
"proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}"
+definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
+where
+ "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"
+
+definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
+where
+ "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
(****** files and directories ******)
@@ -802,16 +809,6 @@
| "deleted obj (RecvMsg p q m # s) = (obj = O_msg q m \<or> deleted obj s)"
| "deleted obj (_ # s) = deleted obj s"
-
-definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"
-where
- "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"
-
-
-definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"
-where
- "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd p fd = Some f}"
-
end
--- a/Proc_fd_of_file_prop.thy Wed Nov 20 13:44:32 2013 +0800
+++ b/Proc_fd_of_file_prop.thy Wed Nov 20 15:19:58 2013 +0800
@@ -1,5 +1,5 @@
theory Proc_fd_of_file_prop
-imports Main Flask Flask_type Valid_prop Current_files_prop
+imports Main Flask Flask_type Valid_prop Current_files_prop Current_sockets_prop
begin
context flask begin
@@ -45,6 +45,24 @@
lemma file_of_proc_fd_in_curf: "\<lbrakk>file_of_proc_fd \<tau> p fd = Some f; valid \<tau>\<rbrakk> \<Longrightarrow> f \<in> current_files \<tau>"
by (drule procfd_of_file_non_empty, simp add:proc_fd_file_in_cur')
+lemma file_fds_subset_pfds:
+ "valid s \<Longrightarrow> proc_file_fds s p \<subseteq> current_proc_fds s p"
+by (auto simp add:proc_file_fds_def intro:proc_fd_in_fds)
+
+lemma tcp_filefd_conflict:
+ "\<lbrakk>file_of_proc_fd s p fd = Some f; is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s, simp)
+apply (auto simp:is_tcp_sock_simps)
+
+
+lemma tcp_not_file_fd:
+ "\<lbrakk>is_tcp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+apply (auto simp:proc_file_fds_def)
+
+lemma udp_not_file_fd:
+ "\<lbrakk>is_udp_sock s (p, fd); valid s\<rbrakk> \<Longrightarrow> fd \<notin> proc_file_fds s p"
+
+lemma
(******************* rebuild proc_fd_of_file simpset ***********************)
(*