theory Static_type 
imports Main OS_type_def Flask_type OS_type_def
begin

(* 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_def
apply (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)"

(* 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"     "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