# HG changeset patch # User chunhan # Date 1377564653 -28800 # Node ID aa1375b6c0eb09e35b8f2b6675e17adc2b36a555 # Parent 01274a64aece495ae48ed82b06b8498938c09b8f find bugs in os_grant, case RecvMsg diff -r 01274a64aece -r aa1375b6c0eb Co2sobj_prop.thy --- a/Co2sobj_prop.thy Mon Aug 05 12:30:26 2013 +0800 +++ b/Co2sobj_prop.thy Tue Aug 27 08:50:53 2013 +0800 @@ -1,28 +1,248 @@ (*<*) theory Co2sobj_prop -imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop +imports Main Flask Flask_type Static Static_type Sectxt_prop Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Tainted_prop Valid_prop Init_prop begin (*<*) +ML {* +fun print_ss ss = +let +val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss +in +simps +end +*} + + context tainting_s begin (********************* cm2smsg simpset ***********************) -lemma cm2smsg_other: "\valid (e # s); \ p q m. e \ SendMsg p q m\ \ cm2smsg (e # s) = cm2smsg s" +lemma cm2smsg_other: + "\valid (e # s); \ p q m. e \ SendMsg p q m; \ p q m. e \ RecvMsg p q m; \ p q. e \ RemoveMsgq p q\ + \ cm2smsg (e # s) = cm2smsg s" apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) +unfolding cm2smsg_def apply (case_tac e) -apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits -intro:tainted.intro +apply (auto simp:sectxt_of_obj_simps tainted_eq_Tainted + split:t_object.splits option.splits if_splits + dest:not_deleted_init_msg dest!:current_has_sec') +done + +lemma cm2smsg_sendmsg: + "valid (SendMsg p q m # s) \ cm2smsg (SendMsg p q m # s) = (\ q' m'. + if (q' = q \ m' = m) + then (case (sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of + Some sec \ Some (Created, sec, O_msg q m \ tainted (SendMsg p q m # s)) + | _ \ None) + else cm2smsg s q' m') " +apply (frule vd_cons, frule vt_grant_os, rule ext, rule ext) +apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps + split:if_splits option.splits + dest:not_deleted_init_msg dest!:current_has_sec') +done + +lemma cm2smsg_recvmsg1: + "\q' \ q; valid (RecvMsg p q m # s)\ \ cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" +apply (frule vd_cons, frule vt_grant_os, rule ext) +apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps + split:if_splits option.splits) +done + +lemma cm2smsg_recvmsg2: + "\m' \ m; valid (RecvMsg p q m # s)\ \ cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'" +apply (frule vd_cons, frule vt_grant_os) +apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps + split:if_splits option.splits) +done + +lemma cm2smsg_recvmsg1': + "\valid (RecvMsg p q m # s); q' \ q\ \ cm2smsg (RecvMsg p q m # s) q' = cm2smsg s q'" +apply (frule vd_cons, frule vt_grant_os, rule ext) +apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps + split:if_splits option.splits) +done + +lemma cm2smsg_recvmsg2': + "\valid (RecvMsg p q m # s); m' \ m\ \ cm2smsg (RecvMsg p q m # s) q m' = cm2smsg s q m'" +apply (frule vd_cons, frule vt_grant_os) +apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps + split:if_splits option.splits) +done + +lemma cm2smsg_removemsgq: + "\q' \ q; valid (RemoveMsgq p q # s)\ \ cm2smsg (RemoveMsgq p q # s) q' = cm2smsg s q'" +apply (frule vd_cons, frule vt_grant_os, rule ext) +apply (auto simp:cm2smsg_def tainted_eq_Tainted sectxt_of_obj_simps + split:if_splits option.splits) +done + +lemmas cm2smsg_simps = cm2smsg_nil_prop cm2smsg_sendmsg cm2smsg_recvmsg1' cm2smsg_recvmsg2' + cm2smsg_removemsgq cm2smsg_other + +lemma init_cm2smsg_has_smsg: + "\m \ set (init_msgs_of_queue q); q \ init_msgqs\ \ \ sm. init_cm2smsg q m = Some sm" +by (auto simp:init_cm2smsg_def split:option.splits dest:init_msg_has_ctxt) + +lemma hd_set_prop1: + "hd l \ set l \ l = []" +by (case_tac l, auto) + +lemma tl_set_prop1: + "a \ set (tl l) \ a \ set l" +by (case_tac l, auto) + +lemma current_has_smsg: + "\m \ set (msgs_of_queue s q); q \ current_msgqs s; valid s\ \ \ sm. cm2smsg s q m = Some sm" +apply (induct s) +apply (simp only:cm2smsg_nil_prop msgs_of_queue.simps current_msgqs.simps init_cm2smsg_has_smsg) + +apply (frule vt_grant_os, frule vd_cons, case_tac a) +apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:if_splits option.splits + dest!:current_has_sec' hd_set_prop1 dest:not_deleted_init_msg tl_set_prop1) +done + +lemma current_has_smsg': + "\cm2smsg s q m = None; q \ current_msgqs s; valid s\ \ m \ set (msgs_of_queue s q)" +by (auto dest:current_has_smsg) + +lemma cqm2sms_has_sms_aux: + "\ m \ set ms. sectxt_of_obj s (O_msg q m) \ None \ (\ sms. cqm2sms s q ms = Some sms)" +by (induct ms, auto split:option.splits simp:cm2smsg_def) + +lemma current_has_sms: + "\q \ current_msgqs s; valid s\ \ \ sms. cqm2sms s q (msgs_of_queue s q) = Some sms" +apply (rule cqm2sms_has_sms_aux) +apply (auto dest:current_msg_has_sec) +done + +lemma current_has_sms': + "\cqm2sms s q (msgs_of_queue s q) = None; valid s\ \ q \ current_msgqs s" +by (auto dest:current_has_sms) + +(********************* cqm2sms simpset ***********************) + +lemma cqm2sms_other: + "\valid (e # s); \ p m. e \ CreateMsgq p q; \ p q m. e \ SendMsg p q m; + \ p q m. e \ RecvMsg p q m; \ p q. e \ RemoveMsgq p q\ + \ cqm2sms (e # s) = cqm2sms s" +apply (rule ext, rule ext) +apply (induct_tac xa, simp) +apply (frule vt_grant_os, frule vd_cons, case_tac e) +apply (auto split:option.splits dest:cm2smsg_other) +done -lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other +lemma cqm2sms_createmsgq: + "valid (CreateMsgq p q # s) \ cqm2sms (CreateMsgq p q # s) = (\ q' ms'. + if (q' = q \ ms' = []) then Some [] + else cqm2sms s q' ms')" +apply (rule ext, rule ext) +apply (frule vt_grant_os, frule vd_cons, induct_tac ms') +apply (auto split:if_splits option.splits dest:cm2smsg_other) +done + +lemma cqm2sms_2: + "cqm2sms s q (ms @ [m]) = + (case (cqm2sms s q ms, cm2smsg s q m) of + (Some sms, Some sm) \ Some (sms @ [sm]) + | _ \ None)" +apply (induct ms, simp split:option.splits) +by (auto split:option.splits) + +lemmas cqm2sms_simps2 = cqm2sms.simps(1) cqm2sms_2 + +declare cqm2sms.simps [simp del] + +lemma cqm2sms_prop1: + "cqm2sms s q ms = None \ \ m \ set ms. cm2smsg s q m = None" +by (induct ms, auto simp:cqm2sms.simps split:option.splits) + +lemma cqm2sms_sendmsg1: + "\valid (SendMsg p q m # s); m \ set ms\ + \ cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms" +apply (frule vt_grant_os, frule vd_cons) +apply (frule cm2smsg_sendmsg) +apply (induct ms rule:rev_induct) +apply (auto split:if_splits option.splits simp:cqm2sms_simps2) +done + +lemma cqm2sms_sendmsg2: + "\valid (SendMsg p q m # s); q' \ q\ + \ cqm2sms (SendMsg p q m # s) q' ms = cqm2sms s q' ms" +apply (frule vt_grant_os, frule vd_cons) +apply (frule cm2smsg_sendmsg) +apply (induct ms rule:rev_induct) +apply (auto split:if_splits option.splits simp:cqm2sms_simps2) +done + +lemma cqm2sms_sendmsg3: + "\valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q\ + \ cqm2sms (SendMsg p q m # s) q ms' = + (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of + (Some sms, Some sec) \ Some (sms @ [(Created, sec, O_msg q m \ tainted (SendMsg p q m # s))]) + | _ \ None)" +apply (frule vt_grant_os, frule vd_cons) +apply (frule cm2smsg_sendmsg) +apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cqm2sms_sendmsg1) +done + +lemma cqm2sms_sendmsg: + "\valid (SendMsg p q m # s); ms' = msgs_of_queue (SendMsg p q m # s) q'\ + \ cqm2sms (SendMsg p q m # s) q' ms' = ( + if (q' = q) + then (case (cqm2sms s q (msgs_of_queue s q), sectxt_of_obj (SendMsg p q m # s) (O_msg q m)) of + (Some sms, Some sec) \ Some (sms @ [(Created, sec, O_msg q m \ tainted (SendMsg p q m # s))]) + | _ \ None) + else cqm2sms s q' ms' )" +apply (simp split:if_splits add:cqm2sms_sendmsg2 cqm2sms_sendmsg3) +done + +lemma cqm2sms_recvmsg1: + "\valid (RecvMsg p q m # s); m \ set ms\ + \ cqm2sms (RecvMsg p q m # s) q ms = cqm2sms s q ms" +apply (frule vt_grant_os, frule vd_cons) +apply (induct ms rule:rev_induct) +apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg2') +done + +lemma cqm2sms_recvmsg2: + "\valid (RecvMsg p q m # s); q' \ q\ + \ cqm2sms (RecvMsg p q m # s) q' ms = cqm2sms s q' ms" +apply (frule vt_grant_os, frule vd_cons) +apply (induct ms rule:rev_induct) +apply (auto split:if_splits option.splits simp:cqm2sms_simps2 cm2smsg_recvmsg1') +done + +lemma cqm2sms_recvmsg: + "\valid (RecvMsg p q m # s); ms = msgs_of_queue (RecvMsg p q m # s) q'\ + \ cqm2sms (RecvMsg p q m # s) q' ms = ( + if (q' = q) + then (case (cqm2sms s q (msgs_of_queue s q)) of + Some sms \ Some (tl sms) + | _ \ None) + else cqm2sms s q' ms)" +apply (frule vt_grant_os, frule vd_cons) +apply (auto split:if_splits option.splits simp:cqm2sms_recvmsg1 cqm2sms_recvmsg2) +using cm2smsg_recvmsg1 cm2smsg_recvmsg2 +apply (auto split:if_splits option.splits) + + +lemmas cqm2sms_simps = cqm2sms_other cqm2sms_createmsgq cqm2sms_sendmsg cqm2sms_recvmsg + +(********************* cq2smsgq simpset ***********************) + +lemma cq2smsgq_other: + "\valid (e # s); \ p m. e \ CreateMsgq p q; \ p q m. e \ SendMsg p q m; + \ p q m. e \ RecvMsg p q m; \ p q. e \ RemoveMsgq p q\ + \ cq2smsgq (e # s) = cq2smsgq s" +apply (frule vd_cons, frule vt_grant_os, rule ext, case_tac e) +apply (auto simp:cq2smsgq_def sectxt_of_obj_simps + split:t_object.splits option.splits if_splits + dest:not_deleted_init_msg dest!:current_has_sec') - -(********************* cq2smsgq simpset ***********************) + -lemma cq2smsgq_other: "\ p m. e \ CreateMsg p m \ cm2smsg (e # \) m' = cm2smsg \ m'" -apply (case_tac e) -by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other diff -r 01274a64aece -r aa1375b6c0eb Dynamic2static.thy --- a/Dynamic2static.thy Mon Aug 05 12:30:26 2013 +0800 +++ b/Dynamic2static.thy Tue Aug 27 08:50:53 2013 +0800 @@ -13,6 +13,9 @@ apply induct s, case tac e, every event analysis *) +thm s2ss_def + + sorry lemma d2s_main': diff -r 01274a64aece -r aa1375b6c0eb Flask.thy --- a/Flask.thy Mon Aug 05 12:30:26 2013 +0800 +++ b/Flask.thy Tue Aug 27 08:50:53 2013 +0800 @@ -705,7 +705,7 @@ | "os_grant \ (SendMsg p q m) = (p \ current_procs \ \ q \ current_msgqs \ \ m \ (set (msgs_of_queue \ q)))" | "os_grant \ (RecvMsg p q m) = - (p \ current_procs \ \ q \ current_msgqs \ \ m = hd (msgs_of_queue \ q))" + (p \ current_procs \ \ q \ current_msgqs \ \ m = hd (msgs_of_queue \ q) \ msgs_of_queue \ q \ [])" | "os_grant \ (RemoveMsgq p q) = (p \ current_procs \ \ q \ current_msgqs \)" | "os_grant \ (CreateShM p h) = @@ -1475,7 +1475,7 @@ | t_attach1:"\O_proc p \ tainted s; valid (Attach p h SHM_RDWR # s); (p', flag') \ procs_of_shm s h\ \ O_proc p' \ tainted (Attach p h SHM_RDWR # s)" | t_attach2:"\O_proc p' \ tainted s; valid (Attach p h flag # s); (p', SHM_RDWR) \ procs_of_shm s h\ - \ O_proc p \ tainted (Attach p h SHM_RDWR # s)" + \ O_proc p \ tainted (Attach p h flag # s)" | t_sendmsg:"\O_proc p \ tainted s; valid (SendMsg p q m # s)\ \ O_msg q m \ tainted (SendMsg p q m # s)" | t_recvmsg:"\O_msg q m \ tainted s; valid (RecvMsg p q m # s); info_flow_shm s p p'\ diff -r 01274a64aece -r aa1375b6c0eb Sectxt_prop.thy --- a/Sectxt_prop.thy Mon Aug 05 12:30:26 2013 +0800 +++ b/Sectxt_prop.thy Tue Aug 27 08:50:53 2013 +0800 @@ -600,8 +600,92 @@ dest!:current_has_type' current_proc_has_role' current_has_user') done +lemma sec_kill: + "valid (Kill p p' # s) \ sectxt_of_obj (Kill p p' # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_ptrace: + "valid (Ptrace p p' # s) \ sectxt_of_obj (Ptrace p p' # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_exit: + "valid (Exit p # s) \ sectxt_of_obj (Exit p # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_readfile: + "valid (ReadFile p fd # s) \ sectxt_of_obj (ReadFile p fd # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_writefile: + "valid (WriteFile p fd # s) \ sectxt_of_obj (WriteFile p fd # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_closefd: + "valid (CloseFd p fd # s) \ sectxt_of_obj (CloseFd p fd # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_unlink: + "valid (UnLink p f # s) \ sectxt_of_obj (UnLink p f # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_Rmdir: + "valid (Rmdir p f # s) \ sectxt_of_obj (Rmdir p f # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_truncate: + "valid (Truncate p f len # s) \ sectxt_of_obj (Truncate p f len # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_recvmsg: + "valid (RecvMsg p q m # s) \ sectxt_of_obj (RecvMsg p q m # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_removemsgq: + "valid (RemoveMsgq p q # s) \ sectxt_of_obj (RemoveMsgq p q # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_attach: + "valid (Attach p h flag # s) \ sectxt_of_obj (Attach p h flag # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_detach: + "valid (Detach p h # s) \ sectxt_of_obj (Detach p h # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_deleteshm: + "valid (DeleteShM p h # s) \ sectxt_of_obj (DeleteShM p h # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_bind: + "valid (Bind p fd addr # s) \ sectxt_of_obj (Bind p fd addr # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_connect: + "valid (Connect p fd addr # s) \ sectxt_of_obj (Connect p fd addr # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_listen: + "valid (Listen p fd # s) \ sectxt_of_obj (Listen p fd # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_sendsock: + "valid (SendSock p fd # s) \ sectxt_of_obj (SendSock p fd # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_recvsock: + "valid (RecvSock p fd # s) \ sectxt_of_obj (RecvSock p fd # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + +lemma sec_shutdown: + "valid (Shutdown p fd how # s) \ sectxt_of_obj (Shutdown p fd how # s) = sectxt_of_obj s" +by (auto dest!:sec_others) + lemmas sectxt_of_obj_simps = sec_execve sec_open sec_mkdir sec_linkhard sec_createmsgq sec_sendmsg - sec_createshm sec_createsock sec_accept sec_clone sec_others (* init_sectxt_prop *) + sec_createshm sec_createsock sec_accept sec_clone sec_kill sec_ptrace sec_exit sec_readfile + sec_writefile sec_closefd sec_unlink sec_Rmdir sec_truncate sec_recvmsg sec_removemsgq + sec_attach sec_detach sec_deleteshm sec_bind sec_connect sec_listen sec_sendsock + sec_recvsock sec_shutdown +(* init_sectxt_prop *) (**************** get_parentfs_ctxts simpset **************) diff -r 01274a64aece -r aa1375b6c0eb Tainted_prop.thy --- a/Tainted_prop.thy Mon Aug 05 12:30:26 2013 +0800 +++ b/Tainted_prop.thy Tue Aug 27 08:50:53 2013 +0800 @@ -1,5 +1,5 @@ theory Tainted_prop -imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop +imports Main Flask Flask_type Init_prop Current_files_prop Current_sockets_prop Delete_prop Proc_fd_of_file_prop Current_prop Alive_prop begin context tainting begin @@ -86,27 +86,6 @@ "\O_proc p \ Tainted s; valid s\ \ p \ current_procs s" by (drule Tainted_in_current, simp+) -lemma has_inode_tainted_aux: - "O_file f \ tainted s \ \ f'. has_same_inode s f f' \ O_file f' \ tainted s" -apply (erule tainted.induct) -apply (auto intro:tainted.intros simp:has_same_inode_def) -(*?? need simpset for tainted *) - - -sorry - -lemma has_inode_Tainted_aux: - "\O_file f \ Tainted s; has_same_inode s f f'\ \ O_file f' \ Tainted s" -apply (induct s, auto) -apply (auto intro:tainted.intros simp:has_same_inode_def) -(*?? need simpset for tainted *) -sorry - -lemma "\info_flow_shm s pa pb; info_flow_shm s pb pc; valid s\ \ info_flow_shm s pa pc" -apply (auto simp add:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2) -apply (erule_tac x = h in allE, simp) -apply (case_tac "h = ha", simp+) -sorry lemma info_flow_shm_Tainted: "\O_proc p \ Tainted s; info_flow_shm s p p'; valid s\ \ O_proc p' \ Tainted s" @@ -122,17 +101,16 @@ have p4': "\ p p' h flag. \O_proc p \ Tainted s; (p, SHM_RDWR) \ procs_of_shm s h; (p', flag) \ procs_of_shm s h\ \ O_proc p' \ Tainted s" - apply (rule p4, auto simp:info_flow_shm_def one_flow_shm_def ) (* procs_of_shm_prop2 *) - sorry - from p2 p3 have p7: "p \ current_procs (e # s)" and p8: "p' \ current_procs (e # s)" (* - by (auto dest:info_shm_flow_in_procs) *) sorry + by (rule p4, auto simp:info_flow_shm_def one_flow_shm_def procs_of_shm_prop2 p5) + from p2 p3 have p7: "p \ current_procs (e # s)" and p8: "p' \ current_procs (e # s)" + by (auto dest:info_shm_flow_in_procs) show ?case proof (cases "self_shm s p p'") case True with p1 show ?thesis by simp next case False with p1 p2 p5 p6 p7 p8 p3 show ?thesis - apply (case_tac e) + apply (case_tac e)(* prefer 7 apply (simp add:info_flow_shm_simps split:if_splits option.splits) apply (rule allI|rule impI|rule conjI)+ @@ -153,9 +131,6 @@ - - - prefer 7 apply (simp split:if_splits option.splits) apply (rule allI|rule impI|rule conjI)+ @@ -175,47 +150,60 @@ apply (drule_tac p = "nat1" and p' = p' in p4') apply (auto dest:p4'[where p = nat1 and p' = p']) -apply (induct s) (* +apply (induct s) apply simp defer apply (frule vd_cons, frule vt_grant_os, case_tac a) apply (auto simp:info_flow_shm_def elim!:disjE) sorry *) sorry -next - case (Cons e s) - show ?case - sorry +qed qed lemma tainted_imp_Tainted: "obj \ tainted s \ obj \ Tainted s" -apply (induct rule:tainted.induct) +apply (induct rule:tainted.induct) (* +apply (simp_all add:vd_cons) +apply (rule impI) + +apply (rule disjI2, rule_tac x = flag' in exI, simp) +apply ((rule impI)+, erule_tac x = p' in allE, simp) +*) apply (auto intro:info_flow_shm_Tainted dest:vd_cons) apply (case_tac e, auto split:option.splits if_splits simp:alive_simps) done +lemma Tainted_imp_tainted_aux_remain: + "\obj \ Tainted s; valid (e # s); alive (e # s) obj; \ obj. obj \ Tainted s \ obj \ tainted s\ + \ obj \ tainted (e # s)" +by (rule t_remain, auto) + lemma Tainted_imp_tainted: "\obj \ Tainted s; valid s\ \ obj \ tainted s" -proof (induct s arbitrary:obj) - case Nil - thus ?case by (auto intro:t_init) -next - case (Cons e s) - hence p1: "\ obj. obj \ Tainted s \ obj \ tainted s" - and p2: "obj \ Tainted (e # s)" and p3: "valid (e # s)" - and p4: "valid s" and p5: "os_grant s e" - by (auto dest:vd_cons intro:vd_cons vt_grant_os) - from p1 have p6: "" -apply (frule vd_cons, frule vt_grant_os, frule valid_Tainted_obj, simp) -apply (case_tac a) -apply (auto intro!:t_init t_clone t_execve t_cfile t_read t_write t_link t_trunc t_sendmsg t_recvmsg - intro:t_remain - split:if_splits option.splits dest:Tainted_in_current) -pr 25 +apply (induct s arbitrary:obj, simp add:t_init) +apply (frule Tainted_in_current, simp+) +apply (frule vt_grant_os, frule vd_cons, case_tac a) +apply (auto split:if_splits option.splits elim:Tainted_imp_tainted_aux_remain intro:tainted.intros) +done + +lemma tainted_eq_Tainted: + "valid s \ (obj \ tainted s) = (obj \ Tainted s)" +by (rule iffI, auto intro:Tainted_imp_tainted tainted_imp_Tainted) -lemma tainted_imp_Tainted: - "obj \ tainted s \ obj \ Tainted s" +lemma info_flow_shm_tainted: + "\O_proc p \ tainted s; info_flow_shm s p p'; valid s\ \ O_proc p' \ tainted s" +by (simp only:tainted_eq_Tainted info_flow_shm_Tainted) +lemma has_same_inode_Tainted: + "\O_file f \ Tainted s; has_same_inode s f f'; valid s\ \ O_file f' \ Tainted s" +apply (induct s arbitrary:f f', simp add:same_inode_in_seeds) +apply (frule vt_grant_os, frule vd_cons, case_tac a) +apply (auto split:if_splits option.splits simp:has_same_inode_def dest:iof's_im_in_cim) +apply (drule_tac obj = "O_file list2" in Tainted_in_current, simp, simp add:is_file_in_current) +done + +lemma has_same_inode_tainted: + "\O_file f \ tainted s; has_same_inode s f f'; valid s\ \ O_file f' \ tainted s" +by (simp add:has_same_inode_Tainted tainted_eq_Tainted) @@ -223,7 +211,8 @@ lemma tainted_in_current: "obj \ tainted s \ alive s obj" -apply (erule tainted.induct, auto dest:vt_grant_os vd_cons simp:is_file_simps) +apply (erule tainted.induct) +apply (auto dest:vt_grant_os vd_cons info_shm_flow_in_procs procs_of_shm_prop2 simp:is_file_simps) apply (drule seeds_in_init, simp add:tobj_in_alive) apply (erule has_same_inode_prop2, simp, simp add:vd_cons) apply (frule vt_grant_os, simp)