|
1 theory Static_type |
|
2 imports Main OS_type_def Flask_type OS_type_def |
|
3 begin |
|
4 |
|
5 (* option: if some \<rightarrow> initial else none \<rightarrow> new created |
|
6 * the constructor each is one-to-one according to security_class_t |
|
7 * but dynamic-special objects are not included, such as: |
|
8 * 1. file-descriptor: C_fd |
|
9 * 2. network node : C_node |
|
10 * 3. |
|
11 *) |
|
12 (* Init \<rightarrow> exists in the initial state; Only: the only static object(cannot be cloned, e.g.) |
|
13 * Many \<rightarrow> Many instantiation of this static object in the dynamic world |
|
14 * tainted under: |
|
15 * Init \<rightarrow> this init obj is tainted |
|
16 * Only \<rightarrow> this new created is tainted |
|
17 * Many \<rightarrow> at least one of them is tainted or all of them can be tainted |
|
18 *) |
|
19 datatype 'a Instance = |
|
20 Init 'a |
|
21 | Created (* new created *) |
|
22 (* |
|
23 | Only (* for process, cannot clone(that means no childprocesses in ss!); |
|
24 for file, renamed init-file(still keeps Init fname!)) *) |
|
25 | Many |
|
26 *) |
|
27 |
|
28 (* (fi, file sectxt, parent file's sectxt, ancestral files' sectxts) *) |
|
29 type_synonym t_sfile = "(t_file Instance) \<times> security_context_t \<times> (security_context_t option) \<times> (security_context_t set)" |
|
30 |
|
31 (* |
|
32 type_synonym t_sfn = "(t_fname Instance) \<times> security_context_t" |
|
33 type_synonym t_sfile = "t_sfn list" (* apparently, "sfile set" is not a finite set! *) |
|
34 *) |
|
35 (* |
|
36 (* Sroot si sectxt : root sfile |
|
37 * Sfile si sectxt Sdir : normal sfile *) |
|
38 datatype t_sfile = |
|
39 Sroot "t_file Instance" "security_context_t" |
|
40 | Sfile "t_file Instance" "security_context_t" "t_sfile" |
|
41 *) |
|
42 |
|
43 |
|
44 (* This is not finite set! think it as nature numbers |
|
45 lemma finite_sfile_set: "finite (UNIV::(t_sfile set))" |
|
46 apply (rule finite.intros) |
|
47 unfolding UNIV_def |
|
48 apply (induct x rule:t_sfile.induct) |
|
49 apply (simp add:UNIV_def) |
|
50 |
|
51 done *) |
|
52 |
|
53 (* the flags tells the sfile is a file or dir: NO! |
|
54 * here sfile means sfd is opened to a sfile that has that "type", it is associated with all dynamic |
|
55 * files that according to this sfile. When we need to give such a file instance, we can give any dynamic |
|
56 * file in that state which according to this sfd's "creating static_state", so we might record ss in fds?? |
|
57 * that means our static is a "(static-state list) set"?? *) |
|
58 type_synonym t_sfd = "(security_context_t \<times> t_open_flags \<times> t_sfile)" |
|
59 |
|
60 type_synonym t_sshm = "(t_shm Instance \<times> security_context_t)" |
|
61 |
|
62 type_synonym t_sproc_sshm = "(t_sshm \<times> t_shm_attach_flag)" |
|
63 |
|
64 (* (si, sectxt, sectxts of fds, sectxt of attached shms) *) |
|
65 type_synonym t_sproc = |
|
66 "t_process Instance \<times> security_context_t \<times> (t_sfd set) \<times> (t_sproc_sshm set)" |
|
67 |
|
68 (* here is a exception, the tainted-flag is in this type, case, msgq will not be-tainted *) |
|
69 type_synonym t_smsg = "t_msg Instance \<times> security_context_t \<times> bool" |
|
70 |
|
71 (* (qmi, sectxt, sectxt of queue) *) |
|
72 type_synonym t_smsgq = "t_msgq Instance \<times> security_context_t \<times> (t_smsg list)" |
|
73 |
|
74 (* O_fd, O_*_sock, O_shm, O_msgq are all that can not be tainted *) |
|
75 datatype t_sobject = |
|
76 S_proc "t_sproc" "bool" |
|
77 | S_file "t_sfile set" "bool" (* here sfile set is for "linking", tainted is the inode *) |
|
78 | S_dir "t_sfile" |
|
79 | S_msgq "t_smsgq" |
|
80 | S_shm "t_sshm" |
|
81 | S_msg "t_smsgq" "t_smsg" |
|
82 |
|
83 (* |
|
84 datatype t_tainted_sobj = |
|
85 TS_proc "t_sproc" "bool" |
|
86 | TS_file "t_sfile set" "bool" |
|
87 | TS_msg "t_smsgq" "t_smsg" |
|
88 *) |
|
89 |
|
90 (* the static state is the current static objects |
|
91 * But, how to record the static fds ??? fd is a dynamic concept !!! |
|
92 *) |
|
93 type_synonym t_static_state = "t_sobject set" |
|
94 |
|
95 end |