theory Static_type imports Main OS_type_def Flask_type OS_type_defbegin(* option: if some \<rightarrow> initial else none \<rightarrow> new created * the constructor each is one-to-one according to security_class_t * but dynamic-special objects are not included, such as: * 1. file-descriptor: C_fd * 2. network node : C_node * 3. *)(* Init \<rightarrow> exists in the initial state; Only: the only static object(cannot be cloned, e.g.) * Many \<rightarrow> Many instantiation of this static object in the dynamic world * tainted under: * Init \<rightarrow> this init obj is tainted * Only \<rightarrow> this new created is tainted * Many \<rightarrow> at least one of them is tainted or all of them can be tainted *)datatype 'a Instance = Init 'a | Created (* new created *)(*| Only (* for process, cannot clone(that means no childprocesses in ss!); for file, renamed init-file(still keeps Init fname!)) *)| Many*)(* (fi, file sectxt, parent file's sectxt, ancestral files' sectxts) *)type_synonym t_sfile = "(t_file Instance) \<times> security_context_t \<times> (security_context_t option) \<times> (security_context_t set)" (*type_synonym t_sfn = "(t_fname Instance) \<times> security_context_t"type_synonym t_sfile = "t_sfn list" (* apparently, "sfile set" is not a finite set! *)*)(*(* Sroot si sectxt : root sfile * Sfile si sectxt Sdir : normal sfile *)datatype t_sfile = Sroot "t_file Instance" "security_context_t"| Sfile "t_file Instance" "security_context_t" "t_sfile"*)(* This is not finite set! think it as nature numbers lemma finite_sfile_set: "finite (UNIV::(t_sfile set))"apply (rule finite.intros)unfolding UNIV_defapply (induct x rule:t_sfile.induct)apply (simp add:UNIV_def)done *)(* the flags tells the sfile is a file or dir: NO! * here sfile means sfd is opened to a sfile that has that "type", it is associated with all dynamic * files that according to this sfile. When we need to give such a file instance, we can give any dynamic * file in that state which according to this sfd's "creating static_state", so we might record ss in fds?? * that means our static is a "(static-state list) set"?? *)type_synonym t_sfd = "(security_context_t \<times> t_open_flags \<times> t_sfile)"type_synonym t_sshm = "(t_shm Instance \<times> security_context_t)"type_synonym t_sproc_sshm = "(t_sshm \<times> t_shm_attach_flag)"(* (si, sectxt, sectxts of fds, sectxt of attached shms) *)type_synonym t_sproc = "t_process Instance \<times> security_context_t \<times> (t_sfd set) \<times> (t_sproc_sshm set)"(* here is a exception, the tainted-flag is in this type, case, msgq will not be-tainted *)type_synonym t_smsg = "t_msg Instance \<times> security_context_t \<times> bool"(* (qmi, sectxt, sectxt of queue) *)type_synonym t_smsgq = "t_msgq Instance \<times> security_context_t \<times> (t_smsg list)"(* O_fd, O_*_sock, O_shm, O_msgq are all that can not be tainted *)datatype t_sobject = S_proc "t_sproc" "bool"| S_file "t_sfile set" "bool" (* here sfile set is for "linking", tainted is the inode *)| S_dir "t_sfile" | S_msgq "t_smsgq"| S_shm "t_sshm" (*| S_msg "t_smsgq" "t_smsg"*)(*datatype t_tainted_sobj = TS_proc "t_sproc" "bool"| TS_file "t_sfile set" "bool"| TS_msg "t_smsgq" "t_smsg"*)(* the static state is the current static objects * But, how to record the static fds ??? fd is a dynamic concept !!! *)type_synonym t_static_state = "t_sobject set"end