67 \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp)) |
67 \<Longrightarrow> (update_ss (add_ss ss (S_file {(Created, nfsec, Some fsec, asecs \<union> {fsec})} tagp)) |
68 (S_proc (pi, pctxt, fds, shms) tagp) |
68 (S_proc (pi, pctxt, fds, shms) tagp) |
69 (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp) |
69 (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp) |
70 ) \<in> static" |
70 ) \<in> static" |
71 | S_readf: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
71 | S_readf: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
72 permission_check pctxt fdctxt C_fd P_setattr; S_file sfs tagf \<in> ss; sf \<in> sfs; |
72 permission_check pctxt fdctxt C_fd P_setattr; S_file sf tagf \<in> ss; |
73 permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk> |
73 permission_check pctxt (sectxt_of_sfile sf) C_file P_read\<rbrakk> |
74 \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static" |
74 \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static" |
|
75 (*add following to locale assumptions: |
|
76 \<And> pctxt fctxt. permission_check pctxt fctxt C_file P_read/P_write \<Longrightarrow> |
|
77 permission_check pctxt pctxt C_fd P_setattr \<and> |
|
78 search_check_s pctxt sf True; not \<forall> sf, should be \<forall> sf \<in> static \<and> sectxt_of_sfile sf = fctxt. |
|
79 |
|
80 *) |
75 | S_writef: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
81 | S_writef: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; (fdctxt,flags,sf) \<in> fds; |
76 permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; |
82 permission_check pctxt fdctxt C_fd P_setattr; sf \<in> sfs; S_file sfs tagf \<in> ss; |
77 permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk> |
83 permission_check pctxt (sectxt_of_sfile sf) C_file P_write; is_write_flag flags\<rbrakk> |
78 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static" |
84 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagp \<or> tagf))) \<in> static" |
79 | S_unlink: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
85 | S_unlink: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |