theory Dynamic2static

imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop

begin

context tainting_s begin

lemma d2s_main:

  "valid s \<Longrightarrow> s2ss s \<in> static"

apply (induct s, simp add:s2ss_nil_prop s_init)

apply (frule vd_cons, simp)

apply (case_tac a, simp_all) 

(*

apply 

induct s, case tac e, every event analysis

*)

sorry

lemma d2s_main':

  "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)"

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"

sorry

lemma t2ts:

  "obj \<in> tainted s \<Longrightarrow> co2sobj s obj = Some sobj \<Longrightarrow> tainted_s (s2ss s) sobj"

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

apply (rule_tac x = "O_proc nat" in exI, simp)

apply (rule_tac x = "O_file list" in exI, simp)

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)

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)

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

  hence static: "s2ss s \<in> static" using d2s_main by auto

  from tainted have alive: "alive s obj" 

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

    sorry

  with tainted t2ts init_alive sobj static

  show ?thesis unfolding taintable_s_def

    apply (rule_tac x = "s2ss s" in bexI, simp)

    apply (rule_tac x = "sobj" in exI, auto)

    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 (rule notI)

apply (clarsimp simp:s2ss_def)

apply (case_tac obj, case_tac [!] obja, case_tac sobj)

done

lemma deleted_imp_deletable_s:

  "\<lbrakk>deleted obj s; init_alive obj; valid s\<rbrakk> \<Longrightarrow> deletable_s obj"

apply (simp add:deletable_s_def)

apply (rule_tac x = "s2ss s" in bexI)

apply (clarify, simp add:init_deled_imp_deled_s)

apply (erule d2s_main)

done

theorem undeletable_s_complete:

  assumes undel_s: "undeletable_s obj"

  shows "undeletable obj"

proof-

  from undel_s have init_alive: "init_alive obj"

    and alive_s: "\<forall> ss \<in> static. \<exists> sobj \<in> ss. init_obj_related sobj obj" 

    using undeletable_s_def by auto

  have "\<not> (\<exists> s. valid s \<and> deleted obj s)" 

  proof

    assume "\<exists> s. valid s \<and> deleted obj s"

    then obtain s where vs: "valid s" and del: "deleted obj s" by auto

    from vs have vss: "s2ss s \<in> static" by (rule d2s_main) 

    with alive_s obtain sobj where in_ss: "sobj \<in> (s2ss s)" 

      and related: "init_obj_related sobj obj" by auto

    from init_alive del vs have "deletable_s obj" 

      by (auto elim:deleted_imp_deletable_s)

    with alive_s

    show False by (auto simp:deletable_s_def)

  qed

  with init_alive show ?thesis 

    by (simp add:undeletable_def)

qed

theorem final_offer:

  "\<lbrakk>undeletable_s obj; \<not> taintable_s obj; init_alive obj\<rbrakk> \<Longrightarrow> \<not> taintable obj"

apply (erule swap)

by (simp add:static_complete undeletable_s_complete)

(************** static \<rightarrow> dynamic ***************)

lemma created_can_have_many:

  "\<lbrakk>valid s; alive s obj; \<not> init_alive obj\<rbrakk> \<Longrightarrow> \<exists> s'. valid s' \<and> alive s' obj \<and> alive s' obj' \<and> s2ss s = s2ss s'"

sorry

lemma s2d_main:

  "ss \<in> static \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss"

apply (erule static.induct)

apply (rule_tac x = "[]" in exI, simp add:s2ss_nil_prop valid.intros)

apply (erule exE|erule conjE)+

sorry

theorem static_sound:

  assumes tbl_s: "taintable_s obj"

  shows "taintable obj"

proof-

  from tbl_s obtain ss sobj where static: "ss \<in> static"

    and sobj: "tainted_s ss sobj" and related: "init_obj_related sobj obj"

    and init_alive: "init_alive obj" by (auto simp:taintable_s_def)

  from static sobj tainted_s_imp_tainted 

  show ?thesis by (auto simp:taintable_def)

qed

lemma ts2t:

  "obj \<in> tainted_s ss \<Longrightarrow> \<exists> s. obj \<in> tainted s"

  "obj \<in> tainted_s ss \<Longrightarrow> \<exists> so. so True \<in> ss \<Longrightarrow> so True \<in> ss \<Longrightarrow> \<exists> s. valid s \<and> s2ss s = ss \<Longrightarrow> so True \<in> s2ss s \<Longrightarrow> tainted s obj. "

end