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)+
−
apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)+
−
apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def+
−
           split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)+
−
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+
−
+
−
lemma tainted_s_in_ss:+
−
  "tainted_s ss sobj \<Longrightarrow> sobj \<in> ss"+
−
apply (case_tac sobj, simp_all)+
−
apply (case_tac bool, simp+)+
−
apply (case_tac bool, simp+)+
−
apply (case_tac prod1, case_tac prod2, simp)+
−
thm tainted_s.simps+
−
oops+
−
+
−
lemma set_eq_D:+
−
  "\<lbrakk>x \<in> S; {x. P x} = S\<rbrakk> \<Longrightarrow> P x"+
−
by auto+
−
+
−
lemma cqm2sms_prop1:+
−
  "\<lbrakk>cqm2sms s q queue = Some sms; sm \<in> set sms\<rbrakk> \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"+
−
apply (induct queue arbitrary:sms)+
−
apply (auto split:option.splits)+
−
done+
−
+
−
lemma sq_sm_prop:+
−
  "\<lbrakk>sm \<in> set sms; cq2smsgq s q = Some (qi, qsec, sms); valid s\<rbrakk>+
−
   \<Longrightarrow> \<exists> m. cm2smsg s q m = Some sm"+
−
by (auto simp:cq2smsgq_def split: option.splits intro:cqm2sms_prop1)+
−
+
−
lemma tainted_s_imp_tainted:+
−
  "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> s obj. valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"+
−
apply (drule s2d_main)+
−
apply (erule exE, erule conjE, simp add:s2ss_def)+
−
apply (rule_tac x = s in exI, simp)+
−
apply (case_tac sobj, simp_all)+
−
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) +
−
apply (rule_tac x = obj in exI, simp)+
−
apply (case_tac obj, (simp split:option.splits if_splits)+)+
−
+
−
apply (erule conjE, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) +
−
apply (rule_tac x = obj in exI, simp)+
−
apply (case_tac obj, (simp split:option.splits if_splits)+)+
−
+
−
apply (case_tac prod1, case_tac prod2, simp)+
−
apply ((erule conjE)+, drule_tac S = ss in set_eq_D, simp, (erule exE|erule conjE)+) +
−
apply (case_tac obj, simp_all split:option.splits if_splits)+
−
apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)+
−
apply (rule_tac x = "O_msg nat m" in exI)+
−
apply (simp)+
−
+
−
apply (case_tac obj, (simp split:option.splits if_splits)+)+
−
apply (erule conjE, drule_tac )+
−
+
−
+
−
+
−
lemma has_inode_tainted_aux:+
−
  "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"+
−
apply (erule tainted.induct)+
−
apply (auto intro:tainted.intros simp:has_same_inode_def)+
−
(*?? need simpset for tainted *)+
−
sorry+
−
+
−
lemma has_same_inode_tainted:+
−
  "\<lbrakk>has_same_inode s f f'; O_file f' \<in> tainted s\<rbrakk> \<Longrightarrow> O_file f \<in> tainted s"+
−
by (drule has_inode_tainted_aux, auto simp:has_same_inode_def)+
−
+
−
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 +
−
  obtain s obj' where co2sobj: "co2sobj s obj' = Some sobj"+
−
    and tainted': "obj' \<in> tainted s" and vs: "valid s" by blast+
−
  +
−
  from co2sobj related vs+
−
  have eq:"obj = obj' \<or> (\<exists> f f'. obj = O_file f \<and> obj' = O_file f' \<and> has_same_inode s f f')"+
−
    apply (case_tac obj', case_tac [!] obj)+
−
    apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi)+
−
    apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_def is_file_def is_dir_def+
−
               split:option.splits t_inode_tag.splits dest!:cf2sfile_fi)+
−
    done+
−
  with tainted' have tainted: "obj \<in> tainted s"+
−
    by (auto intro:has_same_inode_tainted)+
−
  with vs init_alive+
−
  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+
−