selinux: comparison no_shm_selinux/Co2sobj

equal deleted inserted replaced

-:1a1df29d3507
+:d9dc04c3ea90
 (* simpset for co2sobj *)
 lemma co2sobj_execve:
-"\<lbrakk>valid (Execve p f fds # s); alive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
+"\<lbrakk>valid (Execve p f fds # s); dalive (Execve p f fds # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
-if (obj = O_proc p)
+if (obj = D_proc p)
 then (case (cp2sproc (Execve p f fds # s) p) of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_execve':
-"\<lbrakk>valid (Execve p f fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
+"\<lbrakk>valid (Execve p f fds # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Execve p f fds # s) obj = (
-if (obj = O_proc p)
+if (obj = D_proc p)
 then (case (cp2sproc (Execve p f fds # s) p) of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s \<or> O_file f \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_clone':
-"\<lbrakk>valid (Clone p p' fds # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
+"\<lbrakk>valid (Clone p p' fds # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
-if (obj = O_proc p')
+if (obj = D_proc p')
 then (case (cp2sproc (Clone p p' fds # s) p') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (frule_tac ff = list in cf2sfile_other', simp_all)
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_clone:
-"\<lbrakk>valid (Clone p p' fds # s); alive (Clone p p' fds # s) obj\<rbrakk>
+"\<lbrakk>valid (Clone p p' fds # s); dalive (Clone p p' fds # s) obj\<rbrakk>
 \<Longrightarrow> co2sobj (Clone p p' fds # s) obj = (
-if (obj = O_proc p')
+if (obj = D_proc p')
 then (case (cp2sproc (Clone p p' fds # s) p') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp add:is_dir_in_current)
 done
 (*
 lemma co2sobj_ptrace:
-"\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
+"\<lbrakk>valid (Ptrace p p' # s); dalive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
 case obj of
 O_proc p'' \<Rightarrow> if (info_flow_shm s p' p'')
 then (case (cp2sproc s p'') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 apply (simp add:is_dir_in_current)
 done
 *)
 lemma co2sobj_ptrace:
-"\<lbrakk>valid (Ptrace p p' # s); alive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
+"\<lbrakk>valid (Ptrace p p' # s); dalive s obj\<rbrakk>\<Longrightarrow> co2sobj (Ptrace p p' # s) obj = (
 case obj of
-O_proc p'' \<Rightarrow> if (p'' = p')
+D_proc p'' \<Rightarrow> if (p'' = p')
 then (case (cp2sproc s p'') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else if (p'' = p)
 then (case (cp2sproc s p'') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p'' \<in> tainted s \<or> O_proc p' \<in> tainted s))
 | _       \<Rightarrow> None)
-else co2sobj s (O_proc p'')
+else co2sobj s (D_proc p'')
 | _          \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps cq2smsgq_other cf2sfiles_other)
 apply (auto simp:cp2sproc_other split:option.splits
 apply (simp add:is_dir_in_current)
 done
 lemma co2sobj_open:
-"\<lbrakk>valid (Open p f flag fd opt # s); alive (Open p f flag fd opt # s) obj\<rbrakk>
+"\<lbrakk>valid (Open p f flag fd opt # s); dalive (Open p f flag fd opt # s) obj\<rbrakk>
 \<Longrightarrow> co2sobj (Open p f flag fd opt # s) obj = (case obj of
-O_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
+D_file f' \<Rightarrow> if (f' = f \<and> opt \<noteq> None)
 then (case (cf2sfile (Open p f flag fd opt # s) f) of
 Some sf \<Rightarrow> Some (S_file {sf} (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
-else co2sobj s (O_file f')
+else co2sobj s (D_file f')
-| O_proc p' \<Rightarrow> if (p' = p)
+| D_proc p' \<Rightarrow> if (p' = p)
 then (case (cp2sproc (Open p f flag fd opt # s) p) of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
-else co2sobj s (O_proc p')
+else co2sobj s (D_proc p')
 | _         \<Rightarrow> co2sobj s obj )"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (auto simp:cp2sproc_simps split:option.splits
 dest!:current_proc_has_sp' (* intro:info_flow_shm_tainted *))[1]
 apply (simp split:if_splits option.splits)
 done
 (*
 lemma co2sobj_readfile:
-"\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
+"\<lbrakk>valid (ReadFile p fd # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
 case obj of
 O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
 Some f \<Rightarrow> (if (info_flow_shm s p p' \<and> O_file f \<in> tainted s)
 then (case (cp2sproc s p') of
 Some sp \<Rightarrow> Some (S_proc sp True)
 simp:current_files_simps cf2sfiles_simps cf2sfile_simps
 dest:is_file_in_current is_dir_in_current)
 done
 *)
 lemma co2sobj_readfile:
-"\<lbrakk>valid (ReadFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
+"\<lbrakk>valid (ReadFile p fd # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (ReadFile p fd # s) obj = (
 case obj of
-O_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+D_proc p' \<Rightarrow> (case (file_of_proc_fd s p fd) of
 Some f \<Rightarrow> (if (p' = p \<and> O_file f \<in> tainted s)
 then (case (cp2sproc s p') of
 Some sp \<Rightarrow> Some (S_proc sp True)
 | _       \<Rightarrow> None)
 else co2sobj s obj)
 simp:current_files_simps cf2sfile_simps cf2sfiles_simps
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_writefile:
-"\<lbrakk>valid (WriteFile p fd # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
+"\<lbrakk>valid (WriteFile p fd # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (WriteFile p fd # s) obj = (
 case obj of
-O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+D_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
 Some f \<Rightarrow> (if (f \<in> same_inode_files s f')
 then Some (S_file (cf2sfiles s f')
 (O_file f' \<in> tainted s \<or> O_proc p \<in> tainted s))
 else co2sobj s obj)
 | _       \<Rightarrow> None)
 (* should delete has_same_inode !?!?*)
 by (auto simp:same_inode_files_def is_file_def has_same_inode_def split:if_splits option.splits)
 lemma co2sobj_closefd:
-"\<lbrakk>valid (CloseFd p fd # s); alive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
+"\<lbrakk>valid (CloseFd p fd # s); dalive (CloseFd p fd # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CloseFd p fd # s) obj = (
 case obj of
-O_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
+D_file f' \<Rightarrow> (case (file_of_proc_fd s p fd) of
 Some f \<Rightarrow> (if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {(p, fd)} \<and>
 f \<in> files_hung_by_del s \<and> (\<forall> f'' \<in> same_inode_files s f.
 f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-then (case (cf2sfile s f, co2sobj s (O_file f')) of
+then (case (cf2sfile s f, co2sobj s (D_file f')) of
 (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
 | _                              \<Rightarrow> None)
 else co2sobj s obj)
 | _       \<Rightarrow> co2sobj s obj)
-| O_proc p' \<Rightarrow> (if (p = p')
+| D_proc p' \<Rightarrow> (if (p = p')
 then (case (cp2sproc (CloseFd p fd # s) p) of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj)
 | _         \<Rightarrow> co2sobj s obj) "
 apply (clarsimp simp:current_files_closefd split:option.splits)
 apply (drule file_of_pfd_is_file', simp+)
 done
 lemma co2sobj_unlink:
-"\<lbrakk>valid (UnLink p f # s); alive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
+"\<lbrakk>valid (UnLink p f # s); dalive (UnLink p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (UnLink p f # s) obj = (
 case obj of
-O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and>
+D_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> proc_fd_of_file s f = {} \<and>
 (\<forall> f'' \<in> same_inode_files s f. f'' \<noteq> f \<longrightarrow> cf2sfile s f'' \<noteq> cf2sfile s f))
-then (case (cf2sfile s f, co2sobj s (O_file f')) of
+then (case (cf2sfile s f, co2sobj s (D_file f')) of
 (Some sf, Some (S_file sfs b)) \<Rightarrow> Some (S_file (sfs - {sf}) b)
 | _                              \<Rightarrow> None)
 else co2sobj s obj
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (clarsimp simp:current_files_unlink split:option.splits)
 apply (drule file_dir_conflict, simp+)
 done
 lemma co2sobj_rmdir:
-"\<lbrakk>valid (Rmdir p f # s); alive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
+"\<lbrakk>valid (Rmdir p f # s); dalive (Rmdir p f # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Rmdir p f # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps cq2smsgq_other) (* ch2sshm_other*)
 apply (auto simp:cp2sproc_simps split:option.splits if_splits
 dest!:current_proc_has_sp')[1] (* intro:info_flow_shm_tainted*)
 apply (simp add:is_file_simps dir_is_empty_def)
 apply (simp add:cf2sfiles_other)
 apply (auto simp:cf2sfile_simps dest:is_dir_in_current)
 done
 lemma co2sobj_mkdir:
-"\<lbrakk>valid (Mkdir p f i # s); alive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
+"\<lbrakk>valid (Mkdir p f i # s); dalive (Mkdir p f i # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Mkdir p f i # s) obj = (
-if (obj = O_dir f)
+if (obj = D_dir f)
 then (case (cf2sfile (Mkdir p f i # s) f) of
 Some sf \<Rightarrow> Some (S_dir sf)
 | _       \<Rightarrow> None)
 else co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (frule current_file_has_sfile, simp, erule exE, simp)
 apply (drule cf2sfile_mkdir1, simp+)
 done
 lemma co2sobj_linkhard:
-"\<lbrakk>valid (LinkHard p oldf f # s); alive (LinkHard p oldf f # s) obj\<rbrakk>
+"\<lbrakk>valid (LinkHard p oldf f # s); dalive (LinkHard p oldf f # s) obj\<rbrakk>
 \<Longrightarrow> co2sobj (LinkHard p oldf f # s) obj = (
 case obj of
-O_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
+D_file f' \<Rightarrow> if (f' = f \<or> f' \<in> same_inode_files s oldf)
 then (case (cf2sfile (LinkHard p oldf f # s) f) of
 Some sf \<Rightarrow> Some (S_file (cf2sfiles s oldf \<union> {sf}) (O_file oldf \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule current_file_has_sfile, simp)
 apply (drule cf2sfile_linkhard1, simp+)
 done
 lemma co2sobj_truncate:
-"\<lbrakk>valid (Truncate p f len # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
+"\<lbrakk>valid (Truncate p f len # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Truncate p f len # s) obj = (
 case obj of
-O_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
+D_file f' \<Rightarrow> if (f' \<in> same_inode_files s f \<and> len > 0)
 then Some (S_file (cf2sfiles s f') (O_file f' \<in> tainted s \<or> O_proc p \<in> tainted s))
 else co2sobj s obj
 | _         \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) (* ch2sshm_other *)
 same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_kill:
-"\<lbrakk>valid (Kill p p' # s); alive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
+"\<lbrakk>valid (Kill p p' # s); dalive (Kill p p' # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Kill p p' # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other) (* ch2sshm_other *)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps
 same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_exit:
-"\<lbrakk>valid (Exit p # s); alive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
+"\<lbrakk>valid (Exit p # s); dalive (Exit p # s) obj\<rbrakk> \<Longrightarrow> co2sobj (Exit p # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps
 same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_createmsgq:
-"\<lbrakk>valid (CreateMsgq p q # s); alive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
+"\<lbrakk>valid (CreateMsgq p q # s); dalive (CreateMsgq p q # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateMsgq p q # s) obj = (
 case obj of
-O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of
+D_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (CreateMsgq p q # s) q) of
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _        \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_createmsgq)
 done
 lemma co2sobj_sendmsg:
-"\<lbrakk>valid (SendMsg p q m # s); alive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (
+"\<lbrakk>valid (SendMsg p q m # s); dalive (SendMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (SendMsg p q m # s) obj = (
 case obj of
-O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of
+D_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (SendMsg p q m # s) q) of
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _        \<Rightarrow> co2sobj s obj)"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_sendmsg)
 done
 lemma co2sobj_recvmsg:
-"\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
+"\<lbrakk>valid (RecvMsg p q m # s); dalive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
 case obj of
-O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
+D_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
-| O_proc p' \<Rightarrow> if (p' = p \<and> O_msg q m \<in> tainted s)
+| D_proc p' \<Rightarrow> if (p' = p \<and> O_msg q m \<in> tainted s)
 then (case (cp2sproc s p') of
 Some sp \<Rightarrow> Some (S_proc sp True)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 | _         \<Rightarrow> co2sobj s obj)"
 dest!:current_has_smsgq'
 dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)
 done
 (*
 lemma co2sobj_recvmsg:
-"\<lbrakk>valid (RecvMsg p q m # s); alive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
+"\<lbrakk>valid (RecvMsg p q m # s); dalive (RecvMsg p q m # s) obj\<rbrakk> \<Longrightarrow> co2sobj (RecvMsg p q m # s) obj = (
 case obj of
 O_msgq q' \<Rightarrow> if (q' = q) then (case (cq2smsgq (RecvMsg p q m # s) q) of
 Some sq \<Rightarrow> Some (S_msgq sq)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 dest:is_file_in_current is_dir_in_current cq2smsg_recvmsg)
 done
 *)
 lemma co2sobj_removemsgq:
-"\<lbrakk>valid (RemoveMsgq p q # s); alive (RemoveMsgq p q # s) obj\<rbrakk>
+"\<lbrakk>valid (RemoveMsgq p q # s); dalive (RemoveMsgq p q # s) obj\<rbrakk>
 \<Longrightarrow> co2sobj (RemoveMsgq p q # s) obj = co2sobj s obj"
 apply (frule vt_grant_os, frule vd_cons, case_tac obj)
 apply (simp_all add:current_files_simps is_dir_simps cq2smsgq_other)
 apply (auto split:if_splits option.splits dest!:current_file_has_sfile' current_proc_has_sp'
 simp:current_files_simps cf2sfiles_simps cf2sfile_simps cp2sproc_simps
 dest:is_file_in_current is_dir_in_current cq2smsg_removemsgq)
 done
 (*
 lemma co2sobj_createshm:
-"\<lbrakk>valid (CreateShM p h # s); alive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
+"\<lbrakk>valid (CreateShM p h # s); dalive (CreateShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (CreateShM p h # s) obj = (
 case obj of
 O_shm h' \<Rightarrow> if (h' = h) then (case (ch2sshm (CreateShM p h # s) h) of
 Some sh \<Rightarrow> Some (S_shm sh)
 | _       \<Rightarrow> None)
 else co2sobj s obj
 dest!:current_shm_has_sh'
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_detach:
-"\<lbrakk>valid (Detach p h # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
+"\<lbrakk>valid (Detach p h # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Detach p h # s) obj = (
 case obj of
 O_proc p' \<Rightarrow> if (p' = p) then (case (cp2sproc (Detach p h # s) p) of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
 | _       \<Rightarrow> None)
 else co2sobj s obj
 dest!:current_shm_has_sh'
 dest:is_file_in_current is_dir_in_current)
 done
 lemma co2sobj_deleteshm:
-"\<lbrakk>valid (DeleteShM p h # s); alive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
+"\<lbrakk>valid (DeleteShM p h # s); dalive (DeleteShM p h # s) obj\<rbrakk> \<Longrightarrow> co2sobj (DeleteShM p h # s) obj = (
 case obj of
 O_proc p' \<Rightarrow> (case (cp2sproc (DeleteShM p h # s) p') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> tainted s))
 | _       \<Rightarrow> None)
 | _         \<Rightarrow> co2sobj s obj)"
 lemma info_flow_shm_prop1:
 "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"
 by (simp add:info_flow_shm_def)
 lemma co2sobj_attach:
-"\<lbrakk>valid (Attach p h flag # s); alive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
+"\<lbrakk>valid (Attach p h flag # s); dalive s obj\<rbrakk> \<Longrightarrow> co2sobj (Attach p h flag # s) obj = (
 case obj of
 O_proc p' \<Rightarrow> if (info_flow_shm s p p')
 then (case (cp2sproc (Attach p h flag # s) p') of
 Some sp \<Rightarrow> Some (S_proc sp (O_proc p' \<in> tainted s \<or>
 (\<exists> p''. O_proc p'' \<in> tainted s \<and> (p'', SHM_RDWR) \<in> procs_of_shm s h)))
 same_inode_files_prop6
 dest:is_file_in_current is_dir_in_current)
 done
 *)
+lemma co2sobj_bind:
+"valid (Bind p fd addr # s) \<Longrightarrow> co2sobj (Bind p fd addr # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_connect:
+"valid (Connect p fd addr # s) \<Longrightarrow> co2sobj (Connect p fd addr # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_createsock:
+"valid (CreateSock p af st fd inum # s) \<Longrightarrow> co2sobj (CreateSock p af st fd inum # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_accept:
+"valid (Accept p fd addr port fd' inum # s) \<Longrightarrow> co2sobj (Accept p fd addr port fd' inum # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_listen:
+"valid (Listen p fd # s) \<Longrightarrow> co2sobj (Listen p fd # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_sendsock:
+"valid (SendSock p fd # s) \<Longrightarrow> co2sobj (SendSock p fd # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_recvsock:
+"valid (RecvSock p fd # s) \<Longrightarrow> co2sobj (RecvSock p fd # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
+lemma co2sobj_shutdown:
+"valid (Shutdown p fd addr # s) \<Longrightarrow> co2sobj (Shutdown p fd addr # s) = co2sobj s"
+apply (frule vd_cons, frule vt_grant, rule ext, case_tac x)
+by auto
 lemma co2sobj_other:
-"\<lbrakk>valid (e # s); alive (e # s) obj;
+"\<lbrakk>valid (e # s); dalive (e # s) obj;
 \<forall> p f fds. e \<noteq> Execve p f fds;
 \<forall> p p' fds. e \<noteq> Clone p p' fds;
 \<forall> p p'. e \<noteq> Ptrace p p';
 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt;
 \<forall> p fd. e \<noteq> ReadFile p fd;
 lemmas co2sobj_simps = co2sobj_execve co2sobj_clone co2sobj_ptrace co2sobj_open co2sobj_readfile
 co2sobj_writefile co2sobj_closefd co2sobj_unlink co2sobj_rmdir co2sobj_mkdir co2sobj_linkhard
 co2sobj_truncate co2sobj_kill co2sobj_exit co2sobj_createmsgq co2sobj_sendmsg co2sobj_recvmsg
 co2sobj_removemsgq (* co2sobj_attach co2sobj_detach co2sobj_createshm co2sobj_deleteshm *)
+co2sobj_createsock co2sobj_accept co2sobj_listen co2sobj_sendsock co2sobj_recvsock
+co2sobj_shutdown co2sobj_bind co2sobj_connect
 end
 (*<*)
 end

changeset 92	d9dc04c3ea90
parent 88	e832378a2ff2