# HG changeset patch
# User chunhan
# Date 1370476820 -28800
# Node ID ced0fcfbcf8ea69f9b36c0a0bf57ebe8e16f2cca
# Parent  9b42765ce554b6844a379fdb4b6db666620ca9c2
reprove the top-level dynamic2static

diff -r 9b42765ce554 -r ced0fcfbcf8e Co2sobj_prop.thy
--- a/Co2sobj_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Co2sobj_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -6,9 +6,35 @@
 
 context tainting_s begin
 
-(****************** cf2sfile path simpset ***************)
+(********************* cm2smsg simpset ***********************)
+
+lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
+apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
+apply (case_tac e)
+apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits
+intro:tainted.intro
+
+lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
+
+
+
+(********************* cq2smsgq simpset ***********************) 
 
-thm cpfd2sfds_def
+lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
+apply (case_tac e) 
+by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
+
+lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
+
+
+lemma sm_in_sqsms:
+  "\<lbrakk>m \<in> set (msgs_of_queue s q); q \<in> current_msgqs s; valid s; cq2smsgq s q = Some (qi, qsec, sms);
+    cm2smsg s q m = Some sm\<rbrakk> \<Longrightarrow> sm \<in> set sms"
+sorry
+
+
+
+(****************** cf2sfile path simpset ***************)
 
 lemma sroot_only:
   "cf2sfile s [] = Some sroot"
@@ -1243,24 +1269,6 @@
 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm
   cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other 
 
-(********************* cm2smsg simpset ***********************)
-
-lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s"
-apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext)
-apply (case_tac e)
-apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits)
-
-lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other
-
-
-
-(********************* cq2smsgq simpset ***********************) 
-
-lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" 
-apply (case_tac e) 
-by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) 
-
-lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other 
 
 
 
diff -r 9b42765ce554 -r ced0fcfbcf8e Current_prop.thy
--- a/Current_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Current_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1,7 +1,8 @@
+(*<*)
 theory Current_prop
 imports Main Flask_type Flask My_list_prefix Init_prop Valid_prop Delete_prop
 begin
-(*<*)
+(*>*)
 
 context flask begin
 
@@ -46,6 +47,38 @@
   "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)"
 using not_deleted_init_proc by auto
 
+lemma has_same_inode_in_current:
+  "\<lbrakk>has_same_inode s f f'; valid s\<rbrakk> \<Longrightarrow> f \<in> current_files s \<and> f' \<in> current_files s"
+by (auto simp add:has_same_inode_def current_files_def)
+
+lemma has_same_inode_prop1:
+  "\<lbrakk>has_same_inode s f f'; is_file s f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
+by (auto simp:has_same_inode_def is_file_def)
+
+lemma has_same_inode_prop1':
+  "\<lbrakk>has_same_inode s f f'; is_file s f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
+by (auto simp:has_same_inode_def is_file_def)
+
+lemma has_same_inode_prop2:
+  "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f; valid s\<rbrakk> \<Longrightarrow> is_file s f'"
+apply (drule has_same_inode_prop1)
+apply (simp add:file_of_pfd_is_file, simp+)
+done
+
+lemma has_same_inode_prop2':
+  "\<lbrakk>has_same_inode s f f'; file_of_proc_fd s p fd = Some f'; valid s\<rbrakk> \<Longrightarrow> is_file s f"
+apply (drule has_same_inode_prop1')
+apply (simp add:file_of_pfd_is_file, simp+)
+done
+
+lemma tobj_in_init_alive:
+  "tobj_in_init obj \<Longrightarrow> init_alive obj"
+by (case_tac obj, auto)
+
+lemma tobj_in_alive:
+  "tobj_in_init obj \<Longrightarrow> alive [] obj"
+by (case_tac obj, auto simp:is_file_nil)
+
 end
 
 end
\ No newline at end of file
diff -r 9b42765ce554 -r ced0fcfbcf8e Delete_prop.thy
--- a/Delete_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Delete_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -218,6 +218,11 @@
   current_msg_imp_current_msgq)
 done
 
+lemma not_deleted_imp_alive_cons:
+  "\<lbrakk>\<not> deleted obj (e # s); valid (e # s); alive s obj\<rbrakk> \<Longrightarrow> alive (e # s) obj"
+using not_deleted_imp_alive_app[where s = s and s' = "[e]" and obj = obj]
+by auto
+
 (*
 
 lemma nodel_imp_un_deleted:
diff -r 9b42765ce554 -r ced0fcfbcf8e Dynamic2static.thy
--- a/Dynamic2static.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Dynamic2static.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1,5 +1,5 @@
 theory Dynamic2static
-imports Main Flask Static Init_prop Valid_prop
+imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop
 begin
 
 context tainting_s begin
@@ -15,30 +15,9 @@
 *)
 sorry
 
-lemma is_file_has_sfile: "is_file s f \<Longrightarrow> \<exists> sf. cf2sfile s f True = Some sf"
-sorry
-
-lemma is_dir_has_sfile: "is_dir s f \<Longrightarrow> \<exists> sf. cf2sfile s f False = Some sf"
-sorry
-
-lemma is_file_imp_alive: "is_file s f \<Longrightarrow> alive s (O_file f)"
-sorry
-
-
 lemma d2s_main':
   "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"
-apply (induct s)
-apply (simp add:s2ss_def)
-apply (rule_tac x = obj in exI, simp)
-sorry
-
-lemma tainted_prop1:
-  "obj \<in> tainted s \<Longrightarrow> alive s obj"
-sorry
-
-lemma tainted_prop2:
-  "obj \<in> tainted s \<Longrightarrow> valid s"
-sorry
+by (simp add:s2ss_def, rule_tac x = obj in exI, simp)
 
 lemma alive_has_sobj:
   "\<lbrakk>alive s obj; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj"
@@ -46,52 +25,50 @@
 
 lemma t2ts:
   "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"
-apply (frule tainted_prop1, frule tainted_prop2)
+apply (frule tainted_in_current, frule tainted_is_valid)
 apply (simp add:s2ss_def)
 apply (case_tac sobj, simp_all)
-apply (case_tac [!] obj, simp_all split:option.splits)
+apply (case_tac [!] obj, simp_all split:option.splits if_splits)
 apply (rule_tac x = "O_proc nat" in exI, simp)
 apply (rule_tac x = "O_file list" in exI, simp)
-defer defer defer
+apply (drule dir_not_tainted, simp)
+apply (drule msgq_not_tainted, simp)
+apply (drule shm_not_tainted, simp)
 apply (case_tac prod1, simp, case_tac prod2, clarsimp)
 apply (rule conjI)
 apply (rule_tac x = "O_msgq nat1" in exI, simp)
-sorry (* doable, need properties about cm2smsg and cq2smsgq *)
+apply (rule conjI) defer
+apply (simp add:cm2smsg_def split:option.splits) 
+sorry
 
 lemma delq_imp_delqm:
   "deleted (O_msgq q) s \<Longrightarrow> deleted (O_msg q m) s"
 apply (induct s, simp)
 by (case_tac a, auto)
 
-lemma undel_init_file_remains:
-  "\<lbrakk>is_init_file f; \<not> deleted (O_file f) s\<rbrakk> \<Longrightarrow> is_file s f"
-sorry
-
-
 theorem static_complete: 
   assumes undel: "undeletable obj" and tbl: "taintable obj"
   shows "taintable_s obj"
 proof-
   from tbl obtain s where tainted: "obj \<in> tainted s"
     by (auto simp:taintable_def)
-  hence vs: "valid s" by (simp add:tainted_prop2)
+  hence vs: "valid s" by (simp add:tainted_is_valid)
   hence static: "s2ss s \<in> static" using d2s_main by auto
   from tainted have alive: "alive s obj" 
-    using tainted_prop1 by auto
+    using tainted_in_current by auto
   then obtain sobj where sobj: "co2sobj s obj = Some sobj"
     using vs alive_has_sobj by blast
   from undel vs have "\<not> deleted obj s" and init_alive: "init_alive obj" 
     by (auto simp:undeletable_def)
   with vs sobj have "init_obj_related sobj obj"
     apply (case_tac obj, case_tac [!] sobj)
-    apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def)
-    apply (frule undel_init_file_remains, simp, drule is_file_has_sfile, erule exE)
+    apply (auto split:option.splits if_splits simp:cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm)
+    apply (frule not_deleted_init_file, simp+) (*
+apply (drule is_file_has_sfile, erule exE)
     apply (rule_tac x = sf in bexI)
     apply (case_tac list, auto split:option.splits simp:is_init_file_props)[1]
-    apply (simp add:same_inode_files_def cfs2sfiles_def)
-    apply (rule_tac x = list in exI, simp)
-    apply (case_tac list, auto split:option.splits simp:is_init_dir_props delq_imp_delqm)
-    done
+    apply (simp add:same_inode_files_def cfs2sfiles_def) *)  
+    sorry
   with tainted t2ts init_alive sobj static
   show ?thesis unfolding taintable_s_def
     apply (rule_tac x = "s2ss s" in bexI, simp)
@@ -99,13 +76,45 @@
     done
 qed
 
+lemma cp2sproc_pi:
+  "\<lbrakk>cp2sproc s p = Some (Init p', sec, fds, shms); valid s\<rbrakk> \<Longrightarrow> p = p' \<and> \<not> deleted (O_proc p) s \<and> p \<in> init_procs"
+by (simp add:cp2sproc_def split:option.splits if_splits)
+
+lemma cq2smsgq_qi:
+  "\<lbrakk>cq2smsgq s q = Some (Init q', sec, sms); valid s\<rbrakk> \<Longrightarrow> q = q' \<and> \<not> deleted (O_msgq q) s \<and> q \<in> init_msgqs"
+by (simp add:cq2smsgq_def split:option.splits if_splits)
+
+lemma cm2smsg_mi:
+  "\<lbrakk>cm2smsg s q m = Some (Init m', sec, ttag); q \<in> init_msgqs; valid s\<rbrakk> 
+   \<Longrightarrow> m = m' \<and> \<not> deleted (O_msg q m) s \<and> m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs"
+by (clarsimp simp add:cm2smsg_def split:if_splits option.splits)
+
+lemma ch2sshm_hi:
+  "\<lbrakk>ch2sshm s h = Some (Init h', sec); valid s\<rbrakk> \<Longrightarrow> h = h' \<and> \<not> deleted (O_shm h) s \<and> h \<in> init_shms"
+by (clarsimp simp:ch2sshm_def split:if_splits option.splits)
+
+lemma root_not_deleted:
+  "\<lbrakk>deleted (O_dir []) s; valid s\<rbrakk> \<Longrightarrow> False"
+apply (induct s, simp)
+apply (frule vd_cons, frule vt_grant_os, case_tac a, auto)
+done
+
+lemma cf2sfile_fi:
+  "\<lbrakk>cf2sfile s f = Some (Init f', sec, psecopt, asecs); valid s\<rbrakk> \<Longrightarrow> f = f' \<and> 
+     (if (is_file s f) then \<not> deleted (O_file f) s \<and> is_init_file f 
+      else \<not> deleted (O_dir f) s \<and> is_init_dir f)"
+apply (case_tac f)
+by (auto simp:sroot_def cf2sfile_def root_is_init_dir dest!:root_is_dir' root_not_deleted
+        split:if_splits option.splits) 
+
 lemma init_deled_imp_deled_s: 
   "\<lbrakk>deleted obj s; init_alive obj; sobj \<in> (s2ss s); valid s\<rbrakk> \<Longrightarrow> \<not> init_obj_related sobj obj"
-apply (induct s, simp)
-apply (frule vd_cons)
-apply (case_tac a, auto)
-(* need simpset for s2ss *)
-sorry
+apply (rule notI)
+apply (clarsimp simp:s2ss_def)
+apply (case_tac obj, case_tac [!] obja, case_tac sobj)
+apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi)
+
+done
 
 lemma deleted_imp_deletable_s:
   "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"
diff -r 9b42765ce554 -r ced0fcfbcf8e Flask.thy
--- a/Flask.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Flask.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1387,12 +1387,12 @@
 fun tobj_in_init :: "t_object \<Rightarrow> bool"
 where
   "tobj_in_init (O_proc p) = (p \<in> init_procs)"
-| "tobj_in_init (O_file f) = (f \<in> init_files)"
+| "tobj_in_init (O_file f) = (is_init_file f)"
 (* directory is not taintable 
 | "tobj_in_init (O_dir  f) = (f \<in> init_files)"
 *)
 | "tobj_in_init (O_node n) = (n \<in> init_nodes)"
-| "tobj_in_init (O_msg q m) = (member (init_msgs_of_queue q) ((op =) m))"
+| "tobj_in_init (O_msg q m) = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"
 | "tobj_in_init _ = False" (* other kind of obj cannot be tainted *)
 
 (* no use
diff -r 9b42765ce554 -r ced0fcfbcf8e Static.thy
--- a/Static.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Static.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -640,12 +640,12 @@
 *)
 fun init_obj_related :: "t_sobject \<Rightarrow> t_object \<Rightarrow> bool"
 where
-  "init_obj_related (S_proc (Init p, sec, fds, shms) tag) (O_proc p') = (p = p')"
+  "init_obj_related (S_proc (pi, sec, fds, shms) tag) (O_proc p') = (pi = Init p')"
 | "init_obj_related (S_file sfs tag) (O_file f) = (\<exists> sf \<in> sfs. sfile_related sf f)"
 | "init_obj_related (S_dir sf) (O_dir f) = (sfile_related sf f)"
-| "init_obj_related (S_msgq (Init q, sec, sms)) (O_msgq q') = (q = q')"
-| "init_obj_related (S_shm (Init h, sec)) (O_shm h') = (h = h')"
-| "init_obj_related (S_msg (Init q, sec, sms) (Init m, secm, tagm)) (O_msg q' m') = (q = q' \<and> m = m')"
+| "init_obj_related (S_msgq (qi, sec, sms)) (O_msgq q') = (qi = Init q')"
+| "init_obj_related (S_shm (hi, sec)) (O_shm h') = (hi = Init h')"
+| "init_obj_related (S_msg (qi, sec, sms) (mi, secm, tagm)) (O_msg q' m') = (qi = Init q' \<and> mi = Init m')"
 | "init_obj_related _ _ = False"
 
 fun tainted_s :: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> bool"
diff -r 9b42765ce554 -r ced0fcfbcf8e Tainted_prop.thy
--- a/Tainted_prop.thy	Tue Jun 04 15:51:02 2013 +0800
+++ b/Tainted_prop.thy	Thu Jun 06 08:00:20 2013 +0800
@@ -1,20 +1,46 @@
 theory Tainted_prop 
-imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop
+imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop
 begin
 
 context tainting begin
 
 lemma tainted_in_current:
-  "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> alive s obj"
-apply (erule tainted.induct, auto dest:vt_grant_os simp:is_file_simps)
+  "obj \<in> tainted s \<Longrightarrow> alive s obj"
+apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps)
+apply (drule seeds_in_init, simp add:tobj_in_alive)
+apply (erule has_same_inode_prop2, simp, simp add:vd_cons)
+apply (frule vt_grant_os, simp)
+apply (erule has_same_inode_prop1, simp, simp add:vd_cons)
+done
+
+lemma tainted_is_valid:
+  "obj \<in> tainted s \<Longrightarrow> valid s"
+by (erule tainted.induct, auto intro:valid.intros)
 
+lemma t_remain_app:
+  "\<lbrakk>obj \<in> tainted s; \<not> deleted obj (s' @ s); valid (s' @ s)\<rbrakk> 
+  \<Longrightarrow> obj \<in> tainted (s' @ s)"
+apply (induct s', simp)
+apply (simp (no_asm) only:cons_app_simp_aux, rule t_remain)
+apply (simp_all add:not_deleted_cons_D vd_cons)
+apply (drule tainted_in_current, simp add:not_deleted_imp_alive_cons)
+done
 
+lemma valid_tainted_obj:
+  "obj \<in> tainted s \<Longrightarrow> (\<forall> f. obj \<noteq> O_dir f) \<and> (\<forall> q. obj \<noteq> O_msgq q) \<and> (\<forall> h. obj \<noteq> O_shm h)"
+apply (erule tainted.induct)
+apply (drule seeds_in_init)
+by auto
 
+lemma dir_not_tainted: "O_dir f \<in> tainted s \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
+
+lemma msgq_not_tainted: "O_msgq q \<in> tainted s \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
+
+lemma shm_not_tainted: "O_shm h \<in> tainted s \<Longrightarrow> False"
+by (auto dest:valid_tainted_obj)
 
 end
 
-end
-
-
-
-
+end
\ No newline at end of file