# HG changeset patch # User chunhan # Date 1382343499 -28800 # Node ID 0d219ddd63545f8bea49b402146cd4a6c09be624 # Parent 03d173288afeb86b326de51f3b56b5826b5a58c5 appropriate object for taintable diff -r 03d173288afe -r 0d219ddd6354 Dynamic2static.thy --- a/Dynamic2static.thy Wed Oct 16 14:43:28 2013 +0800 +++ b/Dynamic2static.thy Mon Oct 21 16:18:19 2013 +0800 @@ -1,39 +1,72 @@ theory Dynamic2static -imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop +imports Main Flask Static Init_prop Valid_prop Tainted_prop Delete_prop Co2sobj_prop S2ss_prop S2ss_prop2 begin context tainting_s begin +lemma many_sq_imp_sms: + "\<lbrakk>S_msgq (Create, sec, sms) \<in> ss; ss \<in> static\<rbrakk> \<Longrightarrow> \<forall> sm \<in> (set sms). is_many_smsg sm" +sorry + +definition init_ss_eq:: "t_static_state \<Rightarrow> t_static_state \<Rightarrow> bool" (infix "\<doteq>" 100) +where + "ss \<doteq> ss' \<equiv> ss \<subseteq> ss' \<and> {sobj. is_init_sobj sobj \<and> sobj \<in> ss'} \<subseteq> ss" + +lemma [simp]: "ss \<doteq> ss" +by (auto simp:init_ss_eq_def) + +definition init_ss_in:: "t_static_state \<Rightarrow> t_static_state set \<Rightarrow> bool" (infix "\<propto>" 101) +where + "ss \<propto> sss \<equiv> \<exists> ss' \<in> sss. ss \<doteq> ss'" + +lemma s2ss_included_sobj: + "\<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 init_ss_in_prop: + "\<lbrakk>s2ss s \<propto> static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\<rbrakk> + \<Longrightarrow> \<exists> ss \<in> static. sobj \<in> ss" +apply (simp add:init_ss_in_def init_ss_eq_def) +apply (erule bexE, erule conjE) +apply (rule_tac x = ss' in bexI, auto dest!:s2ss_included_sobj) +done + + + + + + +lemma d2s_main_execve: + "valid (Execve p f fds # s) \<Longrightarrow> s2ss (Execve p f fds # s) \<in> static" +apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve) +sorry + 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 -*) -thm s2ss_def + "valid s \<Longrightarrow> s2ss s \<propto> static" +apply (induct s, simp add:s2ss_nil_prop init_ss_in_def) +apply (rule_tac x = "init_static_state" in bexI, simp, simp add:s_init) +apply (frule vd_cons, frule vt_grant_os, simp) +apply (case_tac a) +apply (clarsimp simp add:s2ss_execve) +apply (rule conjI, rule impI) + 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 tainted_has_sobj: "\<lbrakk>obj \<in> tainted s; valid s\<rbrakk> \<Longrightarrow> \<exists> sobj. co2sobj s obj = Some sobj" -sorry +apply (frule tainted_in_current, case_tac obj) +apply (auto dest:valid_tainted_obj simp:co2sobj.simps split:option.splits) +oops 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 (frule d2s_main', simp) 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 (case_tac [!] obj, simp_all add:co2sobj.simps split:option.splits if_splits) apply (drule dir_not_tainted, simp) apply (drule msgq_not_tainted, simp) apply (drule shm_not_tainted, simp) @@ -44,6 +77,12 @@ apply (induct s, simp) by (case_tac a, auto) +lemma tainted_s_subset_prop: + "\<lbrakk>tainted_s ss sobj; ss \<subseteq> ss'\<rbrakk> \<Longrightarrow> tainted_s ss' sobj" +apply (case_tac sobj) +apply auto +done + theorem static_complete: assumes undel: "undeletable obj" and tbl: "taintable obj" shows "taintable_s obj" @@ -51,14 +90,15 @@ 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 obtain sobj where sobj: "co2sobj s obj = Some sobj" - using vs tainted_has_sobj by blast + hence static: "s2ss s \<propto> static" using d2s_main by auto + from tainted obtain sobj where sobj: "co2sobj s obj = Some sobj" sorry +(* should constrain undeletable with file/dir/process only, while msg and fd are excluded + using vs tainted_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 (auto split:option.splits if_splits simp:co2sobj.simps cp2sproc_def ch2sshm_def cq2smsgq_def cm2smsg_def delq_imp_delqm) apply (frule not_deleted_init_file, simp+) apply (drule is_file_has_sfile', simp, erule exE) apply (rule_tac x = sf in bexI) @@ -75,10 +115,13 @@ apply (drule file_dir_conflict, simp+) 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 + show ?thesis unfolding taintable_s_def + apply (simp add:init_ss_in_def) + apply (erule bexE) + apply (simp add:init_ss_eq_def) + apply (rule_tac x = "ss'" in bexI) + apply (rule_tac x = "sobj" in exI) + by (auto intro:tainted_s_subset_prop) qed lemma cp2sproc_pi: @@ -117,17 +160,26 @@ 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 +apply (auto split:option.splits if_splits dest!:cp2sproc_pi cq2smsgq_qi ch2sshm_hi cm2smsg_mi cf2sfile_fi simp:co2sobj.simps) +apply (auto simp:cf2sfiles_def same_inode_files_def has_same_inode_prop1' is_file_def is_dir_def co2sobj.simps 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) +apply (frule d2s_main) +apply (simp add:init_ss_in_def) +apply (erule bexE) +apply (rule_tac x = ss' in bexI) +apply (auto simp add: init_ss_eq_def dest!:init_deled_imp_deled_s) +apply (case_tac obj, case_tac [!] sobj) +apply auto +apply (erule set_mp) +apply (simp) +apply auto +apply (rule_tac x = "(Init list, (aa, ab, b), ac, ba)" in bexI) +apply auto done theorem undeletable_s_complete: @@ -141,9 +193,9 @@ 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) + from vs have vss: "s2ss s \<propto> 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 + and related: "init_obj_related sobj obj" apply auto from init_alive del vs have "deletable_s obj" by (auto elim:deleted_imp_deletable_s) with alive_s diff -r 03d173288afe -r 0d219ddd6354 Flask.thy --- a/Flask.thy Wed Oct 16 14:43:28 2013 +0800 +++ b/Flask.thy Mon Oct 21 16:18:19 2013 +0800 @@ -1483,9 +1483,28 @@ | t_remain: "\<lbrakk>obj \<in> tainted s; valid (e # s); alive (e # s) obj\<rbrakk> \<Longrightarrow> obj \<in> tainted (e # s)" +(* reasonable tainted object, fd and sock and msgq and msg is excluded + * this is different from tainted, which already excluded some of them, + * tainted not excluded msg, which does not have the meaning of "tainteable", but + * but acting as a media to "pass" the virus. We normally will not say that + * a message is tableable or not. + *) +fun appropriate :: "t_object \<Rightarrow> bool" +where + "appropriate (O_proc p) = (p \<in> init_procs)" +| "appropriate (O_file f) = (is_init_file f)" +| "appropriate (O_dir f) = False" +| "appropriate (O_fd p fd) = False" +| "appropriate (O_node n) = False" (* cause socket is temperary not considered *) +| "appropriate (O_tcp_sock k) = False" +| "appropriate (O_udp_sock k) = False" +| "appropriate (O_shm h) = False" +| "appropriate (O_msgq q) = False" +| "appropriate (O_msg q m) = False" + definition taintable:: "t_object \<Rightarrow> bool" where - "taintable obj \<equiv> init_alive obj \<and> (\<exists> s. obj \<in> tainted s)" + "taintable obj \<equiv> init_alive obj \<and> appropriate obj \<and> (\<exists> s. obj \<in> tainted s)" definition undeletable :: "t_object \<Rightarrow> bool" where diff -r 03d173288afe -r 0d219ddd6354 Static.thy --- a/Static.thy Wed Oct 16 14:43:28 2013 +0800 +++ b/Static.thy Mon Oct 21 16:18:19 2013 +0800 @@ -147,24 +147,23 @@ "is_many_smsg (Created,sec,tag) = True" | "is_many_smsg _ = False" +(* wrong def fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" where "is_many_smsgq (Created,sec,sms) = (True \<and> (\<forall> sm \<in> (set sms). is_many_smsg sm))" | "is_many_smsgq _ = False" +*) + +fun is_many_smsgq :: "t_smsgq \<Rightarrow> bool" +where + "is_many_smsgq (Created,sec,sms) = True" +| "is_many_smsgq _ = False" fun is_many_sshm :: "t_sshm \<Rightarrow> bool" where "is_many_sshm (Created, sec) = True" | "is_many_sshm _ = False" -(* -fun is_init_sobj :: "t_sobject \<Rightarrow> bool" -where - "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \<noteq> None)" -| "is_init_sobj (S_file sf tag) = (is_init_sfile sf)" -| "is_init_sobj (S_dir sf tag) = (is_init_sfile sf)" -| "is_init_sobj (S_msg" *) - fun is_many :: "t_sobject \<Rightarrow> bool" where "is_many (S_proc sp tag) = is_many_sproc sp" @@ -173,6 +172,24 @@ | "is_many (S_msgq sq ) = is_many_smsgq sq" | "is_many (S_shm sh ) = is_many_sshm sh" +fun is_init_smsgq :: "t_smsgq \<Rightarrow> bool" +where + "is_init_smsgq (Init q,sec,sms) = True" +| "is_init_smsgq _ = False" + +fun is_init_sshm :: "t_sshm \<Rightarrow> bool" +where + "is_init_sshm (Init h,sec) = True" +| "is_init_sshm _ = False" + +fun is_init_sobj :: "t_sobject \<Rightarrow> bool" +where + "is_init_sobj (S_proc sp tag ) = is_init_sproc sp" +| "is_init_sobj (S_file sfs tag) = (\<exists> sf \<in> sfs. is_init_sfile sf)" +| "is_init_sobj (S_dir sf ) = is_init_sfile sf" +| "is_init_sobj (S_msgq sq ) = is_init_smsgq sq" +| "is_init_sobj (S_shm sh ) = is_init_sshm sh" + (* fun update_ss_sp:: "t_static_state \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" where