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) \<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