# 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: + "\S_msgq (Create, sec, sms) \ ss; ss \ static\ \ \ sm \ (set sms). is_many_smsg sm" +sorry + +definition init_ss_eq:: "t_static_state \ t_static_state \ bool" (infix "\" 100) +where + "ss \ ss' \ ss \ ss' \ {sobj. is_init_sobj sobj \ sobj \ ss'} \ ss" + +lemma [simp]: "ss \ ss" +by (auto simp:init_ss_eq_def) + +definition init_ss_in:: "t_static_state \ t_static_state set \ bool" (infix "\" 101) +where + "ss \ sss \ \ ss' \ sss. ss \ ss'" + +lemma s2ss_included_sobj: + "\alive s obj; co2sobj s obj= Some sobj\ \ sobj \ (s2ss s)" +by (simp add:s2ss_def, rule_tac x = obj in exI, simp) + +lemma init_ss_in_prop: + "\s2ss s \ static; co2sobj s obj = Some sobj; alive s obj; init_obj_related sobj obj\ + \ \ ss \ static. sobj \ 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) \ s2ss (Execve p f fds # s) \ static" +apply (frule vd_cons, frule vt_grant_os, clarsimp simp:s2ss_execve) +sorry + lemma d2s_main: - "valid s \ s2ss s \ 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 \ s2ss s \ 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': - "\alive s obj; co2sobj s obj= Some sobj\ \ sobj \ (s2ss s)" -by (simp add:s2ss_def, rule_tac x = obj in exI, simp) lemma tainted_has_sobj: "\obj \ tainted s; valid s\ \ \ 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 \ tainted s \ co2sobj s obj = Some sobj \ 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: + "\tainted_s ss sobj; ss \ ss'\ \ 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 \ tainted s" by (auto simp:taintable_def) hence vs: "valid s" by (simp add:tainted_is_valid) - hence static: "s2ss s \ 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 \ 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 "\ 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: "\deleted obj s; init_alive obj; valid s\ \ 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 "\ s. valid s \ deleted obj s" then obtain s where vs: "valid s" and del: "deleted obj s" by auto - from vs have vss: "s2ss s \ static" by (rule d2s_main) + from vs have vss: "s2ss s \ static" by (rule d2s_main) with alive_s obtain sobj where in_ss: "sobj \ (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: "\obj \ tainted s; valid (e # s); alive (e # s) obj\ \ obj \ 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 \ bool" +where + "appropriate (O_proc p) = (p \ 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 \ bool" where - "taintable obj \ init_alive obj \ (\ s. obj \ tainted s)" + "taintable obj \ init_alive obj \ appropriate obj \ (\ s. obj \ tainted s)" definition undeletable :: "t_object \ 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 \ bool" where "is_many_smsgq (Created,sec,sms) = (True \ (\ sm \ (set sms). is_many_smsg sm))" | "is_many_smsgq _ = False" +*) + +fun is_many_smsgq :: "t_smsgq \ bool" +where + "is_many_smsgq (Created,sec,sms) = True" +| "is_many_smsgq _ = False" fun is_many_sshm :: "t_sshm \ bool" where "is_many_sshm (Created, sec) = True" | "is_many_sshm _ = False" -(* -fun is_init_sobj :: "t_sobject \ bool" -where - "is_init_sobj (S_proc (popt, sec, fds, shms) tag) = (popt \ 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 \ 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 \ bool" +where + "is_init_smsgq (Init q,sec,sms) = True" +| "is_init_smsgq _ = False" + +fun is_init_sshm :: "t_sshm \ bool" +where + "is_init_sshm (Init h,sec) = True" +| "is_init_sshm _ = False" + +fun is_init_sobj :: "t_sobject \ bool" +where + "is_init_sobj (S_proc sp tag ) = is_init_sproc sp" +| "is_init_sobj (S_file sfs tag) = (\ sf \ 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 \ t_sobject \ t_sobject \ t_static_state" where