|
1 theory Temp |
|
2 imports Static_type OS_type_def Flask_type Flask Static |
|
3 begin |
|
4 |
|
5 context tainting_s |
|
6 |
|
7 begin |
|
8 |
|
9 definition update_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
10 where |
|
11 "update_ss ss so so' \<equiv> if (is_many so) then ss \<union> {so'} else (ss - {so}) \<union> {so'}" |
|
12 |
|
13 definition add_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
14 where |
|
15 "add_ss ss so \<equiv> ss \<union> {so}" |
|
16 |
|
17 definition del_ss :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
18 where |
|
19 "del_ss ss so \<equiv> if (is_many so) then ss else ss - {so}" |
|
20 |
|
21 |
|
22 definition update_ss_shms :: "t_static_state \<Rightarrow> t_sproc \<Rightarrow> bool \<Rightarrow> t_static_state" |
|
23 where |
|
24 "update_ss_shms ss spfrom tag \<equiv> {sobj. \<exists> sobj' \<in> ss. |
|
25 (case sobj' of |
|
26 S_proc sp tagp \<Rightarrow> if (info_flow_sshm spfrom sp) |
|
27 then if (is_many_sproc sp) |
|
28 then (sobj = S_proc sp tagp \<or> sobj = S_proc sp (tagp \<or> tag)) |
|
29 else (sobj = S_proc sp (tagp \<or> tag)) |
|
30 else (sobj = S_proc sp tag) |
|
31 | _ \<Rightarrow> sobj = sobj')}" |
|
32 |
|
33 |
|
34 |
|
35 (* all reachable static states(sobjects set) *) |
|
36 inductive_set static :: "t_static_state set" |
|
37 where |
|
38 s_init: "init_static_state \<in> static" |
|
39 | s_execve: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
40 (fi,fsec,pfsec,asecs) \<in> sfs; npctxt_execve pctxt fsec = Some pctxt'; |
|
41 grant_execve pctxt fsec pctxt'; search_check_s pctxt (fi,fsec,pfsec,asecs) True; |
|
42 inherit_fds_check_s pctxt' fds'; fds' \<subseteq> fds\<rbrakk> |
|
43 \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) |
|
44 (S_proc (pi, pctxt', fds', {}) (tagp \<or> tagf))) \<in> static" |
|
45 | s_clone: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; |
|
46 permission_check pctxt pctxt C_process P_fork; |
|
47 inherit_fds_check_s pctxt fds'; fds' \<subseteq> fds; |
|
48 inherit_shms_check_s pctxt shms'; shms' \<subseteq> shms\<rbrakk> |
|
49 \<Longrightarrow> (add_ss ss (S_proc (Created, pctxt, fds', shms') tagp)) \<in> static" |
|
50 | s_kill: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; |
|
51 S_proc (pi', pctxt', fds', shms') tagp' \<in> ss; |
|
52 permission_check pctxt pctxt' C_process P_sigkill\<rbrakk> |
|
53 \<Longrightarrow> (del_ss ss (S_proc (pi', pctxt', fds', shms') tagp')) \<in> static" |
|
54 | s_ptrace: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss; S_proc sp' tagp' \<in> ss; |
|
55 permission_check (sextxt_of_sproc sp) (sectxt_of_sproc sp') C_process P_ptrace\<rbrakk> |
|
56 \<Longrightarrow> (update_ss_shms (update_ss_shms ss sp tagp) sp' tagp') \<in> static" |
|
57 | s_exit: "\<lbrakk>ss \<in> static; S_proc sp tagp \<in> ss\<rbrakk> \<Longrightarrow> (del_ss ss (S_proc sp tagp)) \<in> static" |
|
58 | s_open: "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
59 search_check_s pctxt sf True; \<not> is_creat_excl_flag flags; |
|
60 oflags_check flags pctxt (sectxt_of_sfile sf); permission_check pctxt pctxt C_fd P_setattr\<rbrakk> |
|
61 \<Longrightarrow> (update_ss ss (S_proc (pi, pctxt, fds, shms) tagp) |
|
62 (S_proc (pi, pctxt, fds \<union> {(pctxt,flags,sf)}, shms) tagp)) \<in> static" |
|
63 | s_open': "\<lbrakk>ss \<in> static; S_proc (pi, pctxt, fds, shms) tagp \<in> ss; is_creat_excl_flag flags; |
|
64 S_dir (pfi,fsec,pfsec,asecs) \<in> ss; search_check_s pctxt (pfi,fsec,pfsec,asecs) False; |
|
65 nfsec = nfctxt_create pctxt fsec C_file; oflags_check flags pctxt nfsec; |
|
66 permission_check pctxt fsec C_dir P_add_rename; permission_check pctxt pctxt C_fd P_setattr\<rbrakk> |
|
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) |
|
69 (S_proc (pi, pctxt, fds \<union> {(pctxt, flags, (Created, nfsec, Some fsec, asecs \<union> {fsec}))}, shms) tagp) |
|
70 ) \<in> static" |
|
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; |
|
73 permission_check pctxt (sectxt_of_sfile sf) C_file P_read; is_read_flag flags\<rbrakk> |
|
74 \<Longrightarrow> (update_ss_shms ss (pi, pctxt,fds,shms) (tagp \<or> tagf)) \<in> static" |
|
75 | 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; |
|
77 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" |
|
79 | S_unlink: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
80 (Init f,fsec,Some pfsec,asecs) \<in> sfs; |
|
81 search_check_s pctxt (Init f,fsec,Some pfsec,asecs) True; |
|
82 permission_check pctxt fsec C_file P_unlink; |
|
83 permission_check pctxt pfsec C_dir P_remove_name\<rbrakk> |
|
84 \<Longrightarrow> ((ss - {S_file sfs tagf}) \<union> {S_file (sfs - {(Init f,fsec,Some pfsec,asecs)}) tagf}) \<in> static" |
|
85 | S_rmdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
86 S_dir (fi,fsec,Some pfsec,asecs) \<in> ss; |
|
87 search_check_s pctxt (fi,fsec,Some pfsec,asecs) False; |
|
88 permission_check pctxt fsec C_dir P_rmdir; |
|
89 permission_check pctxt pfsec C_dir P_remove_name\<rbrakk> |
|
90 \<Longrightarrow> (del_ss ss (S_dir (fi,fsec,Some pfsec,asecs))) \<in> static" |
|
91 | S_mkdir: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (fi,fsec,pfsec,asecs) \<in> ss; |
|
92 search_check_s pctxt (fi,fsec,pfsec,asecs) False; |
|
93 permission_check pctxt (nfctxt_create pctxt fsec C_dir) C_dir P_create; |
|
94 permission_check pctxt fsec C_dir P_add_name\<rbrakk> |
|
95 \<Longrightarrow> (add_ss ss (S_dir (Created,nfctxt_create pctxt fsec C_dir,Some fsec,asecs \<union> {fsec}))) \<in> static" |
|
96 | s_link: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (pfi,pfsec,ppfsec,asecs) \<in> ss; |
|
97 S_file sfs tagf \<in> ss; sf \<in> sfs; nfsec = nfctxt_create pctxt pfsec C_file; |
|
98 search_check_s pctxt (pfi,pfsec,ppfsec,asecs) False; search_check_s pctxt sf True; |
|
99 permission_check pctxt (sectxt_of_sfile sf) C_file P_link; |
|
100 permission_check pctxt pfsec C_dir P_add_name\<rbrakk> |
|
101 \<Longrightarrow> (update_ss ss (S_file sfs tagf) |
|
102 (S_file (sfs \<union> {(Created,nfsec,Some pfsec, asecs \<union> {pfsec})}) tagf)) \<in> static" |
|
103 | s_trunc: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; sf \<in> sfs; |
|
104 search_check_s pctxt sf True; permission_check pctxt (sectxt_of_sfile sf) C_file P_setattr\<rbrakk> |
|
105 \<Longrightarrow> (update_ss ss (S_file sfs tagf) (S_file sfs (tagf \<or> tagp))) \<in> static" |
|
106 (* |
|
107 | s_rename: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_file sfs tagf \<in> ss; |
|
108 (sf#spf') \<in> sfs; S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); |
|
109 search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; |
|
110 sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; |
|
111 permission_check pctxt fctxt C_file P_rename; |
|
112 permission_check pctxt pfctxt C_dir P_add_name; |
|
113 ss_rename ss (sf#spf') (sf#spf) ss'; |
|
114 ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk> |
|
115 \<Longrightarrow> ss' \<in> static" |
|
116 | s_rename': "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_dir (sf#spf') tagf \<in> ss; |
|
117 S_dir spf tagpf \<in> ss; \<not>((sf#spf') \<preceq> (sf#spf)); |
|
118 search_check_s pctxt spf False; search_check_s pctxt (sf#spf') True; |
|
119 sectxt_of_sfile (sf#spf') = Some fctxt; sectxt_of_sfile spf = Some pfctxt; |
|
120 permission_check pctxt fctxt C_dir P_reparent; |
|
121 permission_check pctxt pfctxt C_dir P_add_name; |
|
122 ss_rename ss (sf#spf') (sf#spf) ss'; |
|
123 ss_rename_no_same_fname ss (sf#spf') (sf#spf)\<rbrakk> |
|
124 \<Longrightarrow> ss' \<in> static" |
|
125 *) |
|
126 | s_createq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
127 permission_check pctxt pctxt C_msgq P_associate; |
|
128 permission_check pctxt pctxt C_msgq P_create\<rbrakk> |
|
129 \<Longrightarrow> (add_ss ss (S_msgq (Created,pctxt,[]))) \<in> static" |
|
130 | s_sendmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
|
131 permission_check pctxt qctxt C_msgq P_enqueue; |
|
132 permission_check pctxt qctxt C_msgq P_write; |
|
133 permission_check pctxt pctxt C_msg P_create\<rbrakk> |
|
134 \<Longrightarrow> (update_ss ss (S_msgq (qi,qctxt,sms)) |
|
135 (S_msgq (qi,qctxt,sms @ [(Created, pctxt, tagp)]))) \<in> static" |
|
136 | s_recvmsg: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
137 S_msgq (qi,qctxt,(mi,mctxt,tagm)#sms) \<in> ss; |
|
138 permission_check pctxt qctxt C_msgq P_read; |
|
139 permission_check pctxt mctxt C_msg P_receive\<rbrakk> |
|
140 \<Longrightarrow> (update_ss (update_ss_shms ss (pi,pctxt,fds,shms) (tagp \<or> tagm)) |
|
141 (S_msgq (qi, qctxt, (mi, mctxt, tagm)#sms)) |
|
142 (S_msgq (qi, qctxt, sms))) \<in> static" |
|
143 | s_removeq: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_msgq (qi,qctxt,sms) \<in> ss; |
|
144 permission_check pctxt qctxt C_msgq P_destroy\<rbrakk> |
|
145 \<Longrightarrow> (del_ss ss (S_msgq (qi,qctxt,sms))) \<in> static" |
|
146 | s_createh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; |
|
147 permission_check pctxt pctxt C_shm P_associate; |
|
148 permission_check pctxt pctxt C_shm P_create\<rbrakk> |
|
149 \<Longrightarrow> (add_ss ss (S_shm (Created, pctxt))) \<in> static" |
|
150 | s_attach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss; |
|
151 if flag = SHM_RDONLY then permission_check pctxt hctxt C_shm P_read |
|
152 else (permission_check pctxt hctxt C_shm P_read \<and> |
|
153 permission_check pctxt hctxt C_shm P_write)\<rbrakk> |
|
154 \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) |
|
155 (S_proc (pi,pctxt,fds,shms \<union> {((hi,hctxt),flag)}) tagp)) \<in> static" |
|
156 | s_detach: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm sh \<in> ss; |
|
157 (sh,flag) \<in> shms; \<not> is_many_sshm sh\<rbrakk> |
|
158 \<Longrightarrow> (update_ss ss (S_proc (pi,pctxt,fds,shms) tagp) |
|
159 (S_proc (pi,pctxt,fds,shms - {(sh,flag)}) tagp)) \<in> static" |
|
160 | s_deleteh: "\<lbrakk>ss \<in> static; S_proc (pi,pctxt,fds,shms) tagp \<in> ss; S_shm (hi,hctxt) \<in> ss; |
|
161 permission_check pctxt hctxt C_shm P_destroy; \<not> is_many_sshm sh\<rbrakk> |
|
162 \<Longrightarrow> (remove_sproc_sshm (del_ss ss (S_shm (hi,hctxt))) (hi,hctxt)) \<in> static" |
|
163 |
|
164 |
|
165 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool" |
|
166 where |
|
167 "tainted_s ss (S_proc sp tag) = (S_proc sp tag \<in> ss \<and> tag = True)" |
|
168 | "tainted_s ss (S_file sfs tag) = (S_file sfs tag \<in> ss \<and> tag = True)" |
|
169 (* |
|
170 | "tainted_s ss (S_msg (qi, sec, sms) (mi, secm, tag)) = |
|
171 (S_msgq (qi, sec, sms) \<in> ss \<and> (mi,secm,tag) \<in> set sms \<and> tag = True)" |
|
172 *) |
|
173 | "tainted_s ss _ = False" |
|
174 |
|
175 (* |
|
176 fun tainted_s :: "t_object \<Rightarrow> t_static_state \<Rightarrow> bool" |
|
177 where |
|
178 "tainted_s (O_proc p) ss = (\<exists> sp. S_proc sp True \<in> ss \<and> sproc_related p sp)" |
|
179 | "tainted_s (O_file f) ss = (\<exists> sfs sf. S_file sfs True \<in> ss \<and> sf \<in> sfs \<and> sfile_related f sf)" |
|
180 | "tainted_s (O_msg q m) ss = (\<exists> sq. S_msgq sq \<in> ss \<and> smsgq_smsg_relatainted q m sq)" |
|
181 | "tainted_s _ ss = False" |
|
182 *) |
|
183 |
|
184 definition taintable_s :: "t_object \<Rightarrow> bool" |
|
185 where |
|
186 "taintable_s obj \<equiv> \<exists> ss \<in> static. \<exists> sobj. tainted_s ss sobj \<and> init_obj_related sobj obj \<and> init_alive obj" |
|
187 |
|
188 (* this definition is wrong, cause process can exited from static-world |
|
189 definition deletable_s :: "t_object \<Rightarrow> bool" |
|
190 where |
|
191 "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<forall> sobj \<in> ss. \<not> init_obj_related sobj obj)" |
|
192 *) |
|
193 |
|
194 fun deleted_s :: "t_sproc \<Rightarrow> t_object \<Rightarrow> bool" |
|
195 where |
|
196 "deleted_s (pi, pctxt, fds, shms) (O_proc p) = (pi \<noteq> Init p \<and> permission_check pctxt " |
|
197 |
|
198 definition deletable_s :: "t_object \<Rightarrow> bool" |
|
199 "deletable_s obj \<equiv> init_alive obj \<and> (\<exists> ss \<in> static. \<exists> sp tagp. S_proc sp tagp \<in> ss \<and> deleted_s sp obj)" |
|
200 |
|
201 definition undeletable_s :: "t_object \<Rightarrow> bool" |
|
202 where |
|
203 "undeletable_s obj \<equiv> init_alive obj \<and> (\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj)" |
|
204 |
|
205 definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100) |
|
206 where |
|
207 "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss" |
|
208 |
|
209 lemma [simp]: "ss \<doteq> ss" |
|
210 by (auto simp:init_ss_eq_def) |
|
211 |
|
212 definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101) |
|
213 where |
|
214 "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'" |
|
215 |
|
216 lemma s2ss_included_sobj: |
|
217 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
|
218 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
|
219 |
|
220 lemma init_ss_in_prop: |
|
221 "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk> |
|
222 \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss" |
|
223 apply (simp add:init_ss_in_def init_ss_eq_def) |
|
224 apply (erule bexE, erule conjE) |
|
225 apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj) |
|
226 done |
|
227 |
|
228 |
|
229 |
|
230 |
|
231 end |
|
232 |
|
233 end |