--- a/Static.thy Thu Oct 24 09:42:35 2013 +0800
+++ b/Static.thy Wed Oct 30 08:18:40 2013 +0800
@@ -122,6 +122,122 @@
definition
"init_static_state \<equiv> {sobj. \<exists> obj. init_alive obj \<and> init_obj2sobj obj = Some sobj}"
+(**************** translation from dynamic to static *******************)
+
+definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
+where
+ "cf2sfile s f \<equiv>
+ case (parent f) of
+ None \<Rightarrow> Some sroot
+ | Some pf \<Rightarrow> if (is_file s f)
+ then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
+ (Some sec, Some psec, Some asecs) \<Rightarrow>
+ Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
+ | _ \<Rightarrow> None)
+ else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
+ (Some sec, Some psec, Some asecs) \<Rightarrow>
+ Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
+ | _ \<Rightarrow> None)"
+
+definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
+where
+ "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
+
+(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
+definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option"
+where
+ "cfd2sfd s p fd \<equiv>
+ (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
+ (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of
+ Some sf \<Rightarrow> Some (sec, flags, sf)
+ | _ \<Rightarrow> None)
+ | _ \<Rightarrow> None)"
+
+
+definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
+where
+ "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
+
+definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
+where
+ "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
+ Some sec \<Rightarrow>
+ Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
+ | _ \<Rightarrow> None)"
+
+definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
+where
+ "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
+
+definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
+where
+ "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of
+ Some sec \<Rightarrow>
+ Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
+ cpfd2sfds s p, cph2spshs 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
+ Some sec \<Rightarrow>
+ Some (if (\<not> deleted (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)"
+
+fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
+where
+ "cqm2sms s q [] = Some []"
+| "cqm2sms s q (m#ms) =
+ (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
+ (Some sec, Some sms) \<Rightarrow>
+ Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
+ sec, sms)
+ | _ \<Rightarrow> None)"
+
+fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
+where
+ "co2sobj s (O_proc p) =
+ (case (cp2sproc s p) of
+ Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
+ | _ \<Rightarrow> None)"
+| "co2sobj s (O_file f) =
+ Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
+| "co2sobj s (O_dir f) =
+ (case (cf2sfile s f) of
+ Some sf \<Rightarrow> Some (S_dir sf)
+ | _ \<Rightarrow> None)"
+| "co2sobj s (O_msgq q) =
+ (case (cq2smsgq s q) of
+ Some sq \<Rightarrow> Some (S_msgq sq)
+ | _ \<Rightarrow> None)"
+| "co2sobj s (O_shm h) =
+ (case (ch2sshm s h) of
+ Some sh \<Rightarrow> Some (S_shm sh)
+ | _ \<Rightarrow> None)"
+(*
+| "co2sobj s (O_msg q m) =
+ (case (cq2smsgq s q, cm2smsg s q m) of
+ (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
+ | _ \<Rightarrow> None)"
+*)
+| "co2sobj s _ = None"
+
+
+definition s2ss :: "t_state \<Rightarrow> t_static_state"
+where
+ "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
+
+
+(* ******************************************************** *)
+
+
fun is_init_sfile :: "t_sfile \<Rightarrow> bool"
where
"is_init_sfile (Init _, sec, psec,asec) = True"
@@ -204,18 +320,6 @@
else (ss - {S_dir sf tag}) \<union> {S_dir sf' tag'})"
*)
-definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
-where
- "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}"
-
-definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
-where
- "add_ss ss so \<equiv> ss \<union> {so}"
-
-definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state"
-where
- "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}"
-
(*
fun sparent :: "t_sfile \<Rightarrow> t_sfile option"
where
@@ -487,147 +591,6 @@
| "\<lbrakk>info_flow_sshm sp (pi,sec,fds,shms); info_flow_sproc_sshms shms shms'\<rbrakk>
\<Longrightarrow> info_flow_sshm sp (pi',sec',fds',shms')"
-definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state"
-where
- "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss.
- (case sobj' of
- S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp)
- then if (is_many_sproc sp)
- then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag))
- else (sobj = S_proc sp (tagp \<or> tag))
- else (sobj = S_proc sp tag)
- | _ \<Rightarrow> sobj = sobj')}"
-
-
-
-(* all reachable static states(sobjects set) *)
-inductive_set static :: "t_static_state set"
-where
- s_init: "init_static_state \<in> static"
-| s_execve: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
- (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt';
- grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True;
- inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp)
- (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static"
-| s_clone: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss;
- permission_check pctxt pctxt C_process P_fork;
- inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds;
- inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk>
- \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static"
-| s_kill: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss;
- S_proc (pi', pctxt', fds', shms') tagp' \<in> ss;
- permission_check pctxt pctxt' C_process P_sigkill\<rbrakk>
- \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static"
-| s_ptrace: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss;
- permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk>
- \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static"
-| s_exit: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static"
-| s_open: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs;
- search_check_s pctxt sf True; \<not> is_creat_excl_flag flags;
- oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp)
- (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static"
-| s_open': "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags;
- S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False;
- nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec;
- permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk>
- \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp))
- (S_proc (pi, pctxt, fds, shms) tagp)
- (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp)
- ) \<in> static"
-| S_readf: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds;
- permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs;
- permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk>
- \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static"
-| S_writef: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds;
- permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss;
- permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static"
-| S_unlink: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
- (Init f,fsec,Some pfsec,asecs) \<in> sfs;
- search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True;
- permission_check pctxt fsec C_file P_unlink;
- permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>
- \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static"
-| S_rmdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss;
- S_dir (fi,fsec,Some pfsec,asecs) \<in> ss;
- search_check_s pctxt (fi,fsec,Some pfsec,asecs) False;
- permission_check pctxt fsec C_dir P_rmdir;
- permission_check pctxt pfsec C_dir P_remove_name\<rbrakk>
- \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static"
-| S_mkdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss;
- search_check_s pctxt (fi,fsec,pfsec,asecs) False;
- permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create;
- permission_check pctxt fsec C_dir P_add_name\<rbrakk>
- \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static"
-| s_link: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss;
- S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file;
- search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True;
- permission_check pctxt (sectxt_of_sfile sf) C_file P_link;
- permission_check pctxt pfsec C_dir P_add_name\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_file sfs tagf)
- (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static"
-| s_trunc: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs;
- search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static"
-(*
-| s_rename: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss;
- (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf));
- search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True;
- sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;
- permission_check pctxt fctxt C_file P_rename;
- permission_check pctxt pfctxt C_dir P_add_name;
- ss_rename ss (sf#spf') (sf#spf) ss';
- ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>
- \<Longrightarrow> ss' \<in> static"
-| s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss;
- S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf));
- search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True;
- sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt;
- permission_check pctxt fctxt C_dir P_reparent;
- permission_check pctxt pfctxt C_dir P_add_name;
- ss_rename ss (sf#spf') (sf#spf) ss';
- ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk>
- \<Longrightarrow> ss' \<in> static"
-*)
-| s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss;
- permission_check pctxt pctxt C_msgq P_associate;
- permission_check pctxt pctxt C_msgq P_create\<rbrakk>
- \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static"
-| s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) 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>
- \<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,shms) tagp \<in> ss;
- S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss;
- permission_check pctxt qctxt C_msgq P_read;
- permission_check pctxt mctxt C_msg P_receive\<rbrakk>
- \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm))
- (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms))
- (S_msgq (qi, qctxt, sms))) \<in> static"
-| s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss;
- permission_check pctxt qctxt C_msgq P_destroy\<rbrakk>
- \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static"
-| s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss;
- permission_check pctxt pctxt C_shm P_associate;
- permission_check pctxt pctxt C_shm P_create\<rbrakk>
- \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static"
-| s_attach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;
- if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read
- else (permission_check pctxt hctxt C_shm P_read \<and>
- permission_check pctxt hctxt C_shm P_write)\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)
- (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static"
-| s_detach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss;
- (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk>
- \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp)
- (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static"
-| s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss;
- permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk>
- \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static"
(*
fun smsg_related :: "t_msg \<Rightarrow> t_smsg list \<Rightarrow> bool"
@@ -672,144 +635,6 @@
*)
| "init_obj_related _ _ = False"
-fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
-where
- "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)"
-| "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)"
-(*
-| "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) =
- (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)"
-*)
-| "tainted_s ss _ = False"
-
-(*
-fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool"
-where
- "tainted_s (O_proc p) ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)"
-| "tainted_s (O_file f) ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)"
-| "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)"
-| "tainted_s _ ss = False"
-*)
-
-definition taintable_s :: "t_object \<Rightarrow> bool"
-where
- "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj"
-
-definition deletable_s :: "t_object \<Rightarrow> bool"
-where
- "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)"
-
-definition undeletable_s :: "t_object \<Rightarrow> bool"
-where
- "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)"
-
-
-(**************** translation from dynamic to static *******************)
-
-definition cf2sfile :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile option"
-where
- "cf2sfile s f \<equiv>
- case (parent f) of
- None \<Rightarrow> Some sroot
- | Some pf \<Rightarrow> if (is_file s f)
- then (case (sectxt_of_obj s (O_file f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
- (Some sec, Some psec, Some asecs) \<Rightarrow>
- Some (if (\<not> deleted (O_file f) s \<and> is_init_file f) then Init f else Created, sec, Some psec, set asecs)
- | _ \<Rightarrow> None)
- else (case (sectxt_of_obj s (O_dir f), sectxt_of_obj s (O_dir pf), get_parentfs_ctxts s pf) of
- (Some sec, Some psec, Some asecs) \<Rightarrow>
- Some (if (\<not> deleted (O_dir f) s \<and> is_init_dir f) then Init f else Created, sec, Some psec, set asecs)
- | _ \<Rightarrow> None)"
-
-definition cf2sfiles :: "t_state \<Rightarrow> t_file \<Rightarrow> t_sfile set"
-where
- "cf2sfiles s f \<equiv> {sf. \<exists> f' \<in> (same_inode_files s f). cf2sfile s f' = Some sf}"
-
-(* here cf2sfile is passed with True, because, process' fds are only for files not dirs *)
-definition cfd2sfd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_sfd option"
-where
- "cfd2sfd s p fd \<equiv>
- (case (file_of_proc_fd s p fd, flags_of_proc_fd s p fd, sectxt_of_obj s (O_fd p fd)) of
- (Some f, Some flags, Some sec) \<Rightarrow> (case (cf2sfile s f) of
- Some sf \<Rightarrow> Some (sec, flags, sf)
- | _ \<Rightarrow> None)
- | _ \<Rightarrow> None)"
-
-
-definition cpfd2sfds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sfd set"
-where
- "cpfd2sfds s p \<equiv> {sfd. \<exists> fd \<in> proc_file_fds s p. cfd2sfd s p fd = Some sfd}"
-
-definition ch2sshm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_sshm option"
-where
- "ch2sshm s h \<equiv> (case (sectxt_of_obj s (O_shm h)) of
- Some sec \<Rightarrow>
- Some (if (\<not> deleted (O_shm h) s \<and> h \<in> init_shms) then Init h else Created, sec)
- | _ \<Rightarrow> None)"
-
-definition cph2spshs :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc_sshm set"
-where
- "cph2spshs s p \<equiv> {(sh, flag)| sh flag h. (p, flag) \<in> procs_of_shm s h \<and> ch2sshm s h = Some sh}"
-
-definition cp2sproc :: "t_state \<Rightarrow> t_process \<Rightarrow> t_sproc option"
-where
- "cp2sproc s p \<equiv> (case (sectxt_of_obj s (O_proc p)) of
- Some sec \<Rightarrow>
- Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec,
- cpfd2sfds s p, cph2spshs 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
- Some sec \<Rightarrow>
- Some (if (\<not> deleted (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)"
-
-fun cqm2sms:: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list \<Rightarrow> (t_smsg list) option"
-where
- "cqm2sms s q [] = Some []"
-| "cqm2sms s q (m#ms) =
- (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
- (Some sec, Some sms) \<Rightarrow>
- Some (if (\<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs) then Init q else Created,
- sec, sms)
- | _ \<Rightarrow> None)"
-
-fun co2sobj :: "t_state \<Rightarrow> t_object \<Rightarrow> t_sobject option"
-where
- "co2sobj s (O_proc p) =
- (case (cp2sproc s p) of
- Some sp \<Rightarrow> Some (S_proc sp (O_proc p \<in> tainted s))
- | _ \<Rightarrow> None)"
-| "co2sobj s (O_file f) =
- Some (S_file (cf2sfiles s f) (O_file f \<in> tainted s))"
-| "co2sobj s (O_dir f) =
- (case (cf2sfile s f) of
- Some sf \<Rightarrow> Some (S_dir sf)
- | _ \<Rightarrow> None)"
-| "co2sobj s (O_msgq q) =
- (case (cq2smsgq s q) of
- Some sq \<Rightarrow> Some (S_msgq sq)
- | _ \<Rightarrow> None)"
-| "co2sobj s (O_shm h) =
- (case (ch2sshm s h) of
- Some sh \<Rightarrow> Some (S_shm sh)
- | _ \<Rightarrow> None)"
-(*
-| "co2sobj s (O_msg q m) =
- (case (cq2smsgq s q, cm2smsg s q m) of
- (Some sq, Some sm) \<Rightarrow> Some (S_msg sq sm)
- | _ \<Rightarrow> None)"
-*)
-| "co2sobj s _ = None"
(***************** for backward proof when Instancing static objects ******************)
@@ -863,10 +688,6 @@
where
"new_childf pf \<tau> = next_fname pf \<tau> # pf"
-definition s2ss :: "t_state \<Rightarrow> t_static_state"
-where
- "s2ss s \<equiv> {sobj. \<exists> obj. alive s obj \<and> co2sobj s obj = Some sobj}"
-
end
end
\ No newline at end of file