diff -r 34d01e9a772e -r 7d9c0ed02b56 Static_type.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Static_type.thy	Fri May 03 08:20:21 2013 +0100
@@ -0,0 +1,95 @@
+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
\ No newline at end of file