764 apply (erule CollectE, erule exE, erule conjE) |
764 apply (erule CollectE, erule exE, erule conjE) |
765 apply (rule CollectI, rule_tac x = obj in exI) |
765 apply (rule CollectI, rule_tac x = obj in exI) |
766 apply (simp add:co2sobj_writefile_unchange alive_simps) |
766 apply (simp add:co2sobj_writefile_unchange alive_simps) |
767 done |
767 done |
768 |
768 |
|
769 |
|
770 definition update_s2ss_obj :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_object \<Rightarrow> t_sobject \<Rightarrow> t_sobject \<Rightarrow> t_static_state" |
|
771 where |
|
772 "update_s2ss_obj s ss obj sobj sobj' = |
|
773 (if (\<exists> obj'. alive s obj' \<and> obj' \<noteq> obj \<and> co2sobj s obj' = Some sobj) |
|
774 then ss \<union> {sobj'} |
|
775 else ss - {sobj} \<union> {sobj'})" |
|
776 |
|
777 definition update_s2ss_sfile :: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state" |
|
778 where |
|
779 "update_s2ss_sfile s ss f sf \<equiv> |
|
780 if (same_inode_files s f = {f}) |
|
781 then ss |
|
782 else ss \<union> {S_file (cf2sfiles s f - {sf}) (O_file f \<in> Tainted s)}" |
|
783 |
|
784 definition del_s2ss_file:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state" |
|
785 where |
|
786 "del_s2ss_file s ss f sf = |
|
787 (if (\<exists> f' \<in> same_inode_files s f. f' \<noteq> f \<and> cf2sfile s f' = Some sf) |
|
788 then ss |
|
789 else if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f)) |
|
790 then update_s2ss_sfile s ss f sf |
|
791 else update_s2ss_sfile s (ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)}) f sf" |
|
792 |
|
793 lemma alive_co2sobj_closefd1: |
|
794 "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; |
|
795 file_of_proc_fd s p fd = Some f; \<not> (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)})\<rbrakk> |
|
796 \<Longrightarrow> alive (CloseFd p fd # s) obj" |
|
797 apply (erule co2sobj_some_caseD) |
|
798 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits) |
|
799 |
|
800 lemma alive_co2sobj_closefd3: |
|
801 "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; obj \<noteq> O_file f; |
|
802 file_of_proc_fd s p fd = Some f; f \<in> files_hung_by_del s; proc_fd_of_file s f = {(p, fd)}\<rbrakk> |
|
803 \<Longrightarrow> alive (CloseFd p fd # s) obj" |
|
804 apply (erule co2sobj_some_caseD) |
|
805 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits) |
|
806 |
|
807 lemma alive_co2sobj_closefd2: |
|
808 "\<lbrakk>alive s obj; valid (CloseFd p fd # s); co2sobj s obj = Some sobj; file_of_proc_fd s p fd = None\<rbrakk> |
|
809 \<Longrightarrow> alive (CloseFd p fd # s) obj" |
|
810 apply (erule co2sobj_some_caseD) |
|
811 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits) |
|
812 |
|
813 lemma alive_co2sobj_closefd': |
|
814 "\<lbrakk>co2sobj (CloseFd p fd # s) obj = Some sobj; alive (CloseFd p fd # s) obj; |
|
815 valid (CloseFd p fd # s)\<rbrakk> \<Longrightarrow> alive s obj" |
|
816 apply (erule co2sobj_some_caseD) |
|
817 by (auto simp:alive_simps is_file_simps is_dir_simps split:option.splits if_splits) |
|
818 |
|
819 ML {*asm_full_simp_tac*} |
|
820 |
|
821 ML {* |
|
822 fun my_setiff_tac i = |
|
823 (etac @{thm CollectE} i |
|
824 ORELSE ( asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i |
|
825 THEN etac @{thm disjE} i) |
|
826 ORELSE ( asm_full_simp_tac (HOL_ss addsimps @{thms Set.Diff_iff}) i |
|
827 THEN etac @{thm conjE} i |
|
828 THEN (REPEAT (etac @{thm CollectE} i)))) |
|
829 THEN (REPEAT (( etac @{thm exE} |
|
830 ORELSE' etac @{thm conjE} |
|
831 ORELSE' etac @{thm bexE}) i)) |
|
832 THEN (rtac @{thm CollectI} i |
|
833 ORELSE ( asm_full_simp_tac (HOL_ss addsimps @{thms Set.insert_iff}) i)) |
|
834 |
|
835 *} |
|
836 |
|
837 ML {* |
|
838 fun my_seteq_tac i = |
|
839 (simp_tac (HOL_ss addsimps @{thms s2ss_def}) 1) |
|
840 THEN (rtac @{thm set_eqI} i) |
|
841 THEN (rtac @{thm iffI} i) |
|
842 THEN my_setiff_tac i |
|
843 *} |
|
844 |
|
845 lemma co2sobj_sproc_imp: |
|
846 "co2sobj s obj = Some (S_proc sp tag) \<Longrightarrow> \<exists> p. obj = O_proc p" |
|
847 by (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
848 |
|
849 lemma co2sobj_sfile_imp: |
|
850 "co2sobj s obj = Some (S_file sfs tag) \<Longrightarrow> \<exists> f. obj = O_file f" |
|
851 by (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
852 |
|
853 lemma co2sobj_sdir_imp: |
|
854 "co2sobj s obj = Some (S_dir sf) \<Longrightarrow> \<exists> f. obj = O_dir f" |
|
855 by (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
856 |
|
857 lemma co2sobj_sshm_imp: |
|
858 "co2sobj s obj = Some (S_shm sh) \<Longrightarrow> \<exists> h. obj = O_shm h" |
|
859 by (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
860 |
|
861 lemma co2sobj_smsgq_imp: |
|
862 "co2sobj s obj = Some (S_msgq sq) \<Longrightarrow> \<exists> q. obj = O_msgq q" |
|
863 by (case_tac obj, auto simp:co2sobj.simps split:option.splits) |
|
864 |
769 lemma s2ss_closefd: |
865 lemma s2ss_closefd: |
770 "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = ( |
866 "valid (CloseFd p fd # s) \<Longrightarrow> s2ss (CloseFd p fd # s) = ( |
771 case (file_of_proc_fd s p fd) of |
867 case (file_of_proc_fd s p fd) of |
772 Some f \<Rightarrow> if (" |
868 Some f \<Rightarrow> if (f \<in> files_hung_by_del s \<and> proc_fd_of_file s f = {(p, fd)}) |
|
869 then (case (cf2sfile s f, cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of |
|
870 (Some sf, Some sp, Some sp') \<Rightarrow> |
|
871 (del_s2ss_file s ( |
|
872 update_s2ss_obj s (s2ss s) (O_proc p) |
|
873 (S_proc sp (O_proc p \<in> Tainted s)) |
|
874 (S_proc sp' (O_proc p \<in> Tainted s))) f sf) |
|
875 | _ \<Rightarrow> {}) |
|
876 else (case (cp2sproc s p, cp2sproc (CloseFd p fd # s) p) of |
|
877 (Some sp, Some sp') \<Rightarrow> |
|
878 (update_s2ss_obj s (s2ss s) (O_proc p) |
|
879 (S_proc sp (O_proc p \<in> Tainted s)) |
|
880 (S_proc sp' (O_proc p \<in> Tainted s))) |
|
881 | _ \<Rightarrow> {}) |
|
882 | _ \<Rightarrow> s2ss s)" |
|
883 apply (frule vd_cons, frule vt_grant_os) |
|
884 apply (clarsimp simp only:os_grant.simps) |
|
885 apply (frule current_proc_has_sp, simp, erule exE) |
|
886 apply (case_tac "file_of_proc_fd s p fd") |
|
887 |
|
888 apply (simp add:s2ss_def) |
|
889 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE, rule CollectI) |
|
890 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd') |
|
891 apply (frule co2sobj_closefd, simp) |
|
892 apply (frule cp2sproc_closefd, simp) |
|
893 apply (simp add:proc_file_fds_def split:t_object.splits) |
|
894 apply (simp split:if_splits add:co2sobj.simps tainted_eq_Tainted) |
|
895 apply (erule CollectE, erule exE, erule conjE, rule CollectI) |
|
896 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd2) |
|
897 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd2) |
|
898 apply (frule cp2sproc_closefd, simp) |
|
899 apply (auto simp add:proc_file_fds_def co2sobj.simps tainted_eq_Tainted |
|
900 split:t_object.splits option.splits if_splits)[1] |
|
901 |
|
902 apply (case_tac "cp2sproc (CloseFd p fd # s) p") |
|
903 apply (drule current_proc_has_sp', simp, simp) |
|
904 apply (case_tac "cf2sfile s a") |
|
905 apply (drule current_file_has_sfile', simp, simp add:file_of_pfd_in_current) |
|
906 apply (simp) |
|
907 |
|
908 apply (rule conjI, rule impI, erule conjE) |
|
909 apply (simp add:del_s2ss_file_def) |
|
910 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+ |
|
911 |
|
912 apply (simp add:update_s2ss_obj_def) |
|
913 apply (rule conjI|rule impI|erule exE|erule conjE|erule bexE)+ |
|
914 apply (tactic {*my_seteq_tac 1*}) |
|
915 apply simp |
|
916 apply (case_tac "obj = O_proc p") |
|
917 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
918 apply (rule disjI2, rule_tac x = obj in exI) |
|
919 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_simps) |
|
920 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) |
|
921 apply (tactic {*my_setiff_tac 1*}) |
|
922 apply (rule_tac x = "O_proc p" in exI) |
|
923 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
924 apply (tactic {*my_setiff_tac 1*}) |
|
925 apply (case_tac "obj = O_proc p") |
|
926 apply (rule_tac x = obj' in exI) |
|
927 apply (frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) |
|
928 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
929 apply (case_tac "obj = O_file a") |
|
930 apply (rule_tac x = "O_file f'" in exI) |
|
931 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file) |
|
932 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps) |
|
933 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) |
|
934 apply (rule_tac x = obj in exI) |
|
935 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
|
936 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
937 apply (auto simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
938 |
|
939 apply (rule impI)+ |
|
940 apply (tactic {*my_seteq_tac 1*}) |
|
941 apply (case_tac "obj = O_proc p", rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted) |
|
942 apply (rule disjI2) |
|
943 apply (case_tac "obj = O_file a", simp add:alive_simps) |
|
944 apply (rule DiffI, simp) |
|
945 apply (rule_tac x = obj in exI) |
|
946 apply (frule_tac obj = obj in alive_co2sobj_closefd', simp+) |
|
947 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
948 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) |
|
949 apply (simp, rule notI, simp, frule co2sobj_sproc_imp, erule exE, simp add:co2sobj_closefd) |
|
950 apply (erule_tac x = "O_proc pa" in allE, simp) |
|
951 apply (tactic {*my_setiff_tac 1*}) |
|
952 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
953 apply (tactic {*my_setiff_tac 1*}) |
|
954 apply (case_tac "obj = O_proc p", simp add:co2sobj.simps tainted_eq_Tainted) |
|
955 apply (case_tac "obj = O_file a", rule_tac x = "O_file f'" in exI) |
|
956 apply (case_tac "f' = a", simp add:same_inode_files_prop9 file_of_pfd_is_file) |
|
957 apply (frule_tac obj = "O_file f'" in co2sobj_closefd, simp add:alive_simps) |
|
958 apply (simp add:alive_simps co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits) |
|
959 apply (rule_tac x = obj in exI) |
|
960 apply (frule_tac obj = obj in alive_co2sobj_closefd3, simp+) |
|
961 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
962 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
963 |
|
964 apply (rule impI, tactic {*my_seteq_tac 1*}) |
|
965 apply (simp add:update_s2ss_obj_def) |
|
966 apply (rule conjI, rule impI, (erule exE|erule conjE)+) |
|
967 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
968 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) |
|
969 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) |
|
970 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
971 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
972 apply (case_tac "f = a", simp add:alive_simps) |
|
973 apply (case_tac "f \<in> same_inode_files s a", rule disjI1) |
|
974 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) |
|
975 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) |
|
976 apply (erule bexE, erule conjE) |
|
977 apply (erule_tac x = f'' in ballE, simp, simp) |
|
978 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) |
|
979 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
980 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) |
|
981 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
982 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) |
|
983 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
984 apply (rule disjI2, rule disjI2, rule_tac x = obj in exI) |
|
985 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
986 apply (rule impI) |
|
987 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
988 apply (case_tac "pa = p", simp add:co2sobj.simps tainted_eq_Tainted) |
|
989 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
990 apply (frule_tac obj = obj in co2sobj_closefd, simp) |
|
991 apply (auto simp add:co2sobj.simps tainted_eq_Tainted split:t_object.splits if_splits)[1] |
|
992 apply (rule notI, simp add:co2sobj_closefd) |
|
993 apply (erule_tac x = obj in allE, simp) |
|
994 apply (case_tac "f = a", simp add:alive_simps) |
|
995 apply (case_tac "f \<in> same_inode_files s a", rule disjI1) |
|
996 apply (simp add:co2sobj_simps split:if_splits option.splits t_sobject.splits) |
|
997 apply (simp add:co2sobj.simps tainted_eq_Tainted same_inodes_Tainted cf2sfiles_prop) |
|
998 apply (erule bexE, erule conjE) |
|
999 apply (erule_tac x = f'' in ballE, simp, simp) |
|
1000 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1001 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1002 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_file_simps) |
|
1003 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1004 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1005 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp) |
|
1006 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1007 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1008 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp add:is_dir_simps) |
|
1009 apply (rule disjI2, rule disjI2, rule conjI, rule_tac x = obj in exI) |
|
1010 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp add:alive_simps) |
|
1011 apply (rule notI, simp add:co2sobj_closefd, erule_tac x = obj in allE, simp) |
|
1012 apply (tactic {*my_setiff_tac 1*}) |
|
1013 |
|
1014 |
|
1015 |
|
1016 |
|
1017 defer |
|
1018 apply (rule impI) |
|
1019 apply (simp add:update_s2ss_obj_def) |
|
1020 apply (rule conjI, rule impI, erule exE, erule conjE) |
|
1021 apply (simp add:s2ss_def) |
|
1022 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) |
|
1023 apply (simp) |
|
1024 apply (case_tac "obj = O_proc p") |
|
1025 apply (simp add:co2sobj.simps tainted_eq_Tainted split:if_splits) |
|
1026 apply (rule disjI2, rule_tac x = obj in exI, erule conjE) |
|
1027 apply (simp add:alive_co2sobj_closefd') |
|
1028 apply (frule_tac obj = obj in co2sobj_closefd, simp, simp split:t_object.splits if_splits) |
|
1029 apply (simp, erule disjE) |
|
1030 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
1031 apply (erule exE, erule conjE) |
|
1032 apply (case_tac "obj = O_proc p") |
|
1033 apply (rule_tac x = obj' in exI, simp add:alive_co2sobj_closefd1) |
|
1034 apply (frule_tac obj = obj' in co2sobj_closefd, simp add:alive_co2sobj_closefd1) |
|
1035 apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps) |
|
1036 apply (rule_tac x = obj in exI, simp add:alive_co2sobj_closefd1) |
|
1037 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) |
|
1038 apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps) |
|
1039 apply (rule impI) |
|
1040 apply (simp add:s2ss_def) |
|
1041 apply (rule set_eqI, rule iffI, erule CollectE, erule exE, erule conjE) |
|
1042 apply (simp) |
|
1043 apply (case_tac "obj = O_proc p") |
|
1044 apply (rule disjI1, simp add:co2sobj.simps tainted_eq_Tainted split:if_splits) |
|
1045 apply (rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:alive_co2sobj_closefd') |
|
1046 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) |
|
1047 apply (clarsimp split:t_object.splits if_splits option.splits simp:tainted_eq_Tainted co2sobj.simps) |
|
1048 apply (rule notI, erule_tac x = obj in allE, simp add:alive_co2sobj_closefd') |
|
1049 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) |
|
1050 apply (clarsimp split:t_object.splits if_splits option.splits) |
|
1051 apply (simp) |
|
1052 apply (erule disjE) |
|
1053 apply (rule_tac x = "O_proc p" in exI, simp add:co2sobj.simps tainted_eq_Tainted) |
|
1054 apply (erule exE|erule conjE)+ |
|
1055 apply (rule_tac x = obj in exI) |
|
1056 apply (frule_tac obj = obj in co2sobj_closefd, simp add:alive_co2sobj_closefd1) |
|
1057 apply (clarsimp split:t_object.splits if_splits option.splits |
|
1058 simp:tainted_eq_Tainted co2sobj.simps alive_co2sobj_closefd1) |
|
1059 done |
|
1060 |
|
1061 |
|
1062 |
|
1063 |
773 |
1064 |
774 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
1065 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
775 s2ss_readfile s2ss_writefile |
1066 s2ss_readfile s2ss_writefile s2ss_closefd |
776 |
1067 |