Mercurial Mercurial > hg > selinux / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Dynamic2static.thy
changeset 1 7d9c0ed02b56
child 19 ced0fcfbcf8e 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Dynamic2static.thy	Fri May 03 08:20:21 2013 +0100
@@ -0,0 +1,205 @@
+theory Dynamic2static
+imports Main Flask Static Init_prop Valid_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 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
+
+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_prop1, frule tainted_prop2)
+apply (simp add:s2ss_def)
+apply (case_tac sobj, simp_all)
+apply (case_tac [!] obj, simp_all split:option.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 (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 *)
+
+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 static: "s2ss s \<in> static" using d2s_main by auto
+  from tainted have alive: "alive s obj" 
+    using tainted_prop1 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 (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
+  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 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
+
+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)+
+
+apply (erule exE, erule conjE)+
+
+sorry
+
+
+
+lemma tainted_s_imp_tainted:
+  "\<lbrakk>tainted_s ss sobj; ss \<in> static\<rbrakk> \<Longrightarrow> \<exists> obj s. s2ss s = ss \<and> valid s \<and> co2sobj s obj = Some sobj \<and> obj \<in> tainted s"
+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 
+  obtain s obj' where s2ss: "s2ss s = ss" and co2sobj: "co2sobj s obj' = Some sobj"
+    and tainted: "obj' \<in> tainted s" and vs: "valid s" by blast
+  
+  from co2sobj related
+  have eq:"obj = obj'"
+    apply (case_tac obj', case_tac [!] obj, case_tac [!] sobj)
+    apply auto
+    apply (auto split:option.splits if_splits)
+    apply (case_tac a, simp+)
+    apply (simp add:cp2sproc_def split:option.splits if_splits)
+    apply simp
+    sorry
+  with tainted 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
\ No newline at end of file
selinux