|
1 theory OS_type_def |
|
2 imports Main Flask_type |
|
3 begin |
|
4 |
|
5 (****************************** os files ***************************) |
|
6 |
|
7 datatype t_open_must_flag = |
|
8 OF_RDONLY |
|
9 | OF_WRONLY |
|
10 | OF_RDWR |
|
11 |
|
12 datatype t_open_option_flag = |
|
13 OF_APPEND |
|
14 | OF_CREAT |
|
15 (* |
|
16 | OF_TRUNC |
|
17 *) |
|
18 | OF_EXCL |
|
19 (* |
|
20 | OF_DIRECTORY |
|
21 |
|
22 | OF_OTHER |
|
23 *) |
|
24 |
|
25 type_synonym t_open_flags = "t_open_must_flag \<times> t_open_option_flag set" |
|
26 |
|
27 definition is_read_flag :: "t_open_flags \<Rightarrow> bool" |
|
28 where |
|
29 "is_read_flag flag \<equiv> let (mflag, oflag) = flag in (mflag = OF_RDONLY \<or> mflag = OF_RDWR)" |
|
30 |
|
31 definition is_write_flag :: "t_open_flags \<Rightarrow> bool" |
|
32 where |
|
33 "is_write_flag flag \<equiv> let (mflag, oflag) = flag in (mflag = OF_WRONLY \<or> mflag = OF_RDWR)" |
|
34 |
|
35 definition is_excl_flag :: "t_open_flags \<Rightarrow> bool" |
|
36 where |
|
37 "is_excl_flag flag \<equiv> let (mflag, oflag) = flag in (OF_EXCL \<in> oflag)" |
|
38 |
|
39 definition is_creat_flag :: "t_open_flags \<Rightarrow> bool" |
|
40 where |
|
41 "is_creat_flag flag \<equiv> let (mflag, oflag) = flag in (OF_CREAT \<in> oflag)" |
|
42 |
|
43 definition is_creat_excl_flag :: "t_open_flags \<Rightarrow> bool" |
|
44 where |
|
45 "is_creat_excl_flag flag \<equiv> let (mflag, oflag) = flag in (OF_CREAT \<in> oflag \<and> OF_EXCL \<in> oflag)" |
|
46 (* |
|
47 definition is_trunc_flag :: "t_open_flags \<Rightarrow> bool" |
|
48 where |
|
49 "is_trunc_flag flag \<equiv> let (mflag, oflag) = flag in (OF_TRUNC \<in> oflag \<and> is_write_flag flag)" |
|
50 |
|
51 definition is_cloexec_flag :: "t_open_flags \<Rightarrow> bool" |
|
52 where |
|
53 "is_cloexec_flag flag \<equiv> let (mflag, oflag) = flag in (OF_CLOEXEC \<in> oflag)" |
|
54 *) |
|
55 definition is_append_flag :: "t_open_flags \<Rightarrow> bool" |
|
56 where |
|
57 "is_append_flag flag \<equiv> let (mflag, oflag) = flag in (OF_APPEND \<in> oflag)" |
|
58 |
|
59 (* |
|
60 definition is_dir_flag :: "t_open_flags \<Rightarrow> bool" |
|
61 where |
|
62 "is_dir_flag flag \<equiv> let (mflag, oflag) = flag in (OF_DIRECTORY \<in> oflag)" |
|
63 *) |
|
64 |
|
65 |
|
66 type_synonym t_fname = string |
|
67 |
|
68 (* listing of file path: |
|
69 * a#b#c:: b is a's parent and c is b's parent; |
|
70 * [] represents the root file |
|
71 *) |
|
72 type_synonym t_file = "t_fname list" |
|
73 |
|
74 type_synonym t_fd = "nat" (* given a fd, must has funs to tell its corresponding: "t_file \<times> t_open_flags \<times> t_inode" *) |
|
75 |
|
76 |
|
77 (* need not consideration, for rdonly transfer virus too |
|
78 datatype t_sharememo_flag = |
|
79 SHM_RDONLY |
|
80 | SHM_OTHER |
|
81 |
|
82 type_synonym t_sharememo_flags = "t_sharememo_flag set" |
|
83 *) |
|
84 |
|
85 |
|
86 |
|
87 (****************************** os sockets ***************************) |
|
88 |
|
89 datatype t_shutdown_how = |
|
90 SHUT_RD |
|
91 | SHUT_WR |
|
92 | SHUT_RDWR |
|
93 |
|
94 datatype t_zero_one = |
|
95 Z |
|
96 | O |
|
97 |
|
98 type_synonym t_inet_addr = "t_zero_one list" |
|
99 |
|
100 type_synonym t_socket_port = nat |
|
101 |
|
102 type_synonym t_netif = string |
|
103 |
|
104 (* |
|
105 datatype t_socket_af = |
|
106 AF_UNIX "t_file \<times> t_file" |
|
107 | AF_INET "t_inet_addr \<times> t_socket_port \<times> t_inet_addr \<times> t_socket_port \<times> t_netdev" |
|
108 *) |
|
109 |
|
110 datatype t_socket_af = |
|
111 (* AF_UNIX |
|
112 | *)AF_INET |
|
113 |
|
114 datatype t_socket_type = |
|
115 STREAM |
|
116 | DGRAM |
|
117 |
|
118 datatype t_sock_addr = |
|
119 INET_ADDR t_inet_addr t_socket_port(* |
|
120 | UNIX_ADDR t_file*) |
|
121 |
|
122 type_synonym t_node = t_inet_addr (* a endpoint in the netword *) |
|
123 |
|
124 datatype t_sock_trans_state = |
|
125 Trans_Recv |
|
126 | Trans_Send |
|
127 | Trans_RS |
|
128 | Trans_No |
|
129 |
|
130 datatype t_sock_state = |
|
131 SS_create |
|
132 | SS_bind |
|
133 | SS_connect |
|
134 | SS_listen |
|
135 | SS_accepted |
|
136 | SS_trans "t_sock_trans_state" |
|
137 |
|
138 |
|
139 (****************************** os other IPCs ***************************) |
|
140 |
|
141 datatype t_shm_attach_flag = |
|
142 SHM_RDONLY |
|
143 | SHM_RDWR |
|
144 |
|
145 type_synonym t_shm = nat |
|
146 |
|
147 |
|
148 (* message queue is indexed by a nat, in OS |
|
149 * but logically it is a list, created as [], updated as a queue |
|
150 * so, it type should not be nat, but a t_msg list |
|
151 *) |
|
152 type_synonym t_msgq = nat |
|
153 |
|
154 (* a message of ID nat, but it has meaning under "in what message queue" *) |
|
155 type_synonym t_msg = "nat" |
|
156 |
|
157 (****************************** os inodes ***************************) |
|
158 |
|
159 type_synonym t_inode_num = nat |
|
160 |
|
161 (* |
|
162 datatype t_sock_af = |
|
163 Tag_AF_UNIX "(t_file option \<times> t_file option)" "t_socket_type" |
|
164 | Tag_AF_INET "(t_inet_addr \<times> t_socket_port) option \<times> (t_inet_addr \<times> t_socket_port) option \<times> t_netdev option" "t_socket_type" |
|
165 *) |
|
166 |
|
167 datatype t_inode_tag = |
|
168 Tag_FILE (* this inode is a file, and its file is: "t_file" :: no need to do that and another reason is link may add two or more files to the inode, so it should be a list, can the maintainment of this list is tough *) |
|
169 | Tag_DIR (* do not contain chs anymore, for more infomation see svn log |
|
170 "t_inode_num list" *) (* Tag_DIR inode number list: the inode number list of subchild files (direct son the file) , means: new created child file should add to this field. *) |
|
171 | Tag_TCP_SOCK (* information below is turn to seperative listener functions |
|
172 "(t_inet_addr \<times> t_socket_port) option \<times> (t_inet_addr \<times> t_socket_port) option \<times> t_netdev option" "t_socket_type" *) |
|
173 | Tag_UDP_SOCK |
|
174 |
|
175 (* type_synonym t_inode = "nat \<times> t_inode_tag" (* inode (id, tag) contains file internal id and directory tag attributes *) |
|
176 // not needed any more: for inode num and its tag now are seperated by two funcs. |
|
177 *) |
|
178 |
|
179 |
|
180 type_synonym t_process = nat |
|
181 |
|
182 type_synonym t_trunc_len = nat |
|
183 |
|
184 type_synonym t_socket = "t_process \<times> t_fd" |
|
185 |
|
186 (* each constructor is defined according to each security-class *) |
|
187 datatype t_object = |
|
188 O_proc "t_process" |
|
189 |
|
190 | O_file "t_file" |
|
191 | O_fd "t_process" "t_fd" |
|
192 | O_dir "t_file" |
|
193 |
|
194 | O_node "t_node" |
|
195 | O_tcp_sock "t_socket" |
|
196 | O_udp_sock "t_socket" |
|
197 |
|
198 | O_shm "t_shm" |
|
199 | O_msgq "t_msgq" |
|
200 | O_msg "t_msgq" "t_msg" |
|
201 |
|
202 (* |
|
203 datatype t_tainted_obj = |
|
204 TO_proc "t_process" |
|
205 | TO_file "t_file" |
|
206 | TO_msg "t_msgq" "t_msg" |
|
207 *) |
|
208 |
|
209 |
|
210 (* not needed anymore |
|
211 datatype t_clone_share_flag = |
|
212 | CF_share_ipc |
|
213 | CF_share_fd |
|
214 | CF_share_both |
|
215 | CF_no_share *) |
|
216 |
|
217 (* unformalised system calls: |
|
218 * 1. process management |
|
219 * 1.1 wait: nothing to do with tainting relation |
|
220 * 1.2 getpriority/setpriority/getsched/setsched: nothing to do with security |
|
221 * 1.3 getcap/setcap: "at this time that will not be done" |
|
222 * 1.4 getpgid/setpgid: ... |
|
223 *) |
|
224 datatype t_event = |
|
225 (* process management *) |
|
226 (* trace can be done trough tags of cloning and execving, but I ignore this. *) |
|
227 Execve "t_process" "t_file" "t_fd set" |
|
228 (* | Uselib "t_process" "t_file" *) |
|
229 | Clone "t_process" "t_process" "t_fd set" "t_shm set" (* "t_clone_share_flag" is not needed, as event should record the fds and shms that passed to childprocess *) |
|
230 | Kill "t_process" "t_process" |
|
231 | Ptrace "t_process" "t_process" |
|
232 | Exit "t_process" |
|
233 |
|
234 | Open "t_process" "t_file" "t_open_flags" "t_fd" "nat option" (* the last nat option : if create file, the is Some inode_num else None *) |
|
235 | ReadFile "t_process" "t_fd" |
|
236 | WriteFile "t_process" "t_fd" |
|
237 (* | Sendfile "t_process" "t_fd" "t_fd" |
|
238 can be modeled as readfile then writefile *) |
|
239 | CloseFd "t_process" "t_fd" |
|
240 | UnLink "t_process" "t_file" |
|
241 | Rmdir "t_process" "t_file" |
|
242 | Mkdir "t_process" "t_file" "nat" (* last nat: inode_num *) |
|
243 | LinkHard "t_process" "t_file" "t_file" |
|
244 | Truncate "t_process" "t_file" "t_trunc_len" |
|
245 (* | FTruncate "t_process" "t_fd" "t_trunc_len" *) |
|
246 (* |
|
247 | Rename "t_process" "t_file" "t_file" |
|
248 *) |
|
249 |
|
250 (* the message is in the msgq, so we must build a cache(list) |
|
251 * to store the unreceived msg yet. And the os_grant should |
|
252 * check if a message queue is empty before RecvMsg. |
|
253 *) |
|
254 | CreateMsgq "t_process" "t_msgq" |
|
255 | SendMsg "t_process" "t_msgq" "t_msg" |
|
256 | RecvMsg "t_process" "t_msgq" "t_msg" |
|
257 | RemoveMsgq "t_process" "t_msgq" |
|
258 |
|
259 | CreateShM "t_process" "t_shm" |
|
260 | Attach "t_process" "t_shm" "t_shm_attach_flag" |
|
261 | Detach "t_process" "t_shm" |
|
262 | DeleteShM "t_process" "t_shm" |
|
263 |
|
264 | CreateSock "t_process" "t_socket_af" "t_socket_type" "t_fd" "nat" (* last nat: inode_num *) |
|
265 | Bind "t_process" "t_fd" "t_sock_addr" |
|
266 | Connect "t_process" "t_fd" "t_sock_addr" |
|
267 | Listen "t_process" "t_fd" |
|
268 | Accept "t_process" "t_fd" "t_sock_addr" "nat" "t_fd" "nat" (* addr: remote socket address; nat: port num; last nat: inode_num *) |
|
269 | SendSock "t_process" "t_fd" |
|
270 | RecvSock "t_process" "t_fd" |
|
271 | Shutdown "t_process" "t_fd" "t_shutdown_how" |
|
272 |
|
273 (* the state of the system is decided by the initial state and the event trace*) |
|
274 type_synonym t_state = "t_event list" |
|
275 |
|
276 end |