89 exists ("alive") and |
89 exists ("alive") and |
90 default_fd_create_type ("default'_type") and |
90 default_fd_create_type ("default'_type") and |
91 InheritParent_file_type ("InheritPatentType") and |
91 InheritParent_file_type ("InheritPatentType") and |
92 NormalFile_type ("NormalFileType") and |
92 NormalFile_type ("NormalFileType") and |
93 deleted ("deleted _ _" [50, 100] 100) and |
93 deleted ("deleted _ _" [50, 100] 100) and |
94 taintable_s ("taintable\<^isup>s") and |
94 taintable_s ("taintable\<^sup>s") and |
95 tainted_s ("tainted\<^isup>s") and |
95 tainted_s ("tainted\<^sup>s") and |
96 all_sobjs ("reachable\<^isup>s") and |
96 all_sobjs ("reachable\<^sup>s") and |
97 init_obj2sobj ("\<lbrakk>_\<rbrakk>") and |
97 init_obj2sobj ("\<lbrakk>_\<rbrakk>") and |
98 erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle |
98 erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle |
99 efficient, but their name not same, so ..., but don't work" |
99 efficient, but their name not same, so ..., but don't work" |
100 |
100 |
101 |
101 |
771 hope for a meaningful check by just trying out all possible |
771 hope for a meaningful check by just trying out all possible |
772 valid states in our dynamic model. The reason is that there are |
772 valid states in our dynamic model. The reason is that there are |
773 potentially infinitely many of them and therefore the search space would be |
773 potentially infinitely many of them and therefore the search space would be |
774 infinite. For example starting from an |
774 infinite. For example starting from an |
775 initial state containing a process @{text p} and a file @{text pf}, |
775 initial state containing a process @{text p} and a file @{text pf}, |
776 we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."} |
776 we can create files @{text "f\<^sub>1"}, @{text "f\<^sub>2"}, @{text "..."} |
777 via @{text "CreateFile"}-events. This can be pictured roughly as follows: |
777 via @{text "CreateFile"}-events. This can be pictured roughly as follows: |
778 |
778 |
779 \begin{center} |
779 \begin{center} |
780 \begin{tabular}[t]{c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}cc} |
780 \begin{tabular}[t]{c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}cc} |
781 \begin{tabular}[t]{c} |
781 \begin{tabular}[t]{c} |
783 @{term "{p, pf}"} |
783 @{term "{p, pf}"} |
784 \end{tabular} & |
784 \end{tabular} & |
785 \begin{tabular}[t]{c} |
785 \begin{tabular}[t]{c} |
786 \\ |
786 \\ |
787 @{text "\<Longrightarrow>"}\\[2mm] |
787 @{text "\<Longrightarrow>"}\\[2mm] |
788 {\small@{term "CreateFile p (f\<^isub>1#pf)"}} |
788 {\small@{term "CreateFile p (f\<^sub>1#pf)"}} |
789 \end{tabular} |
789 \end{tabular} |
790 & |
790 & |
791 \begin{tabular}[t]{c} |
791 \begin{tabular}[t]{c} |
792 \\ |
792 \\ |
793 @{term "{p, pf, f\<^isub>1#pf}"} |
793 @{term "{p, pf, f\<^sub>1#pf}"} |
794 \end{tabular} |
794 \end{tabular} |
795 & |
795 & |
796 \begin{tabular}[t]{c} |
796 \begin{tabular}[t]{c} |
797 \\ |
797 \\ |
798 @{text "\<Longrightarrow>"}\\[2mm] |
798 @{text "\<Longrightarrow>"}\\[2mm] |
799 {\small@{term "CreateFile p (f\<^isub>2#f\<^isub>1#pf)"}} |
799 {\small@{term "CreateFile p (f\<^sub>2#f\<^sub>1#pf)"}} |
800 \end{tabular} |
800 \end{tabular} |
801 & |
801 & |
802 \begin{tabular}[t]{c} |
802 \begin{tabular}[t]{c} |
803 \\ |
803 \\ |
804 @{term "{p, pf, f\<^isub>1#pf, f\<^isub>2#f\<^isub>1#pf}"} |
804 @{term "{p, pf, f\<^sub>1#pf, f\<^sub>2#f\<^sub>1#pf}"} |
805 \end{tabular} & |
805 \end{tabular} & |
806 \begin{tabular}[t]{c} |
806 \begin{tabular}[t]{c} |
807 \\ |
807 \\ |
808 @{text "..."}\\ |
808 @{text "..."}\\ |
809 \end{tabular} |
809 \end{tabular} |
1033 The crucial difference between between the ``dynamic'' notion of validity |
1033 The crucial difference between between the ``dynamic'' notion of validity |
1034 and the ``static'' notion of @{term "all_sobjs"} |
1034 and the ``static'' notion of @{term "all_sobjs"} |
1035 is that there can be infinitely many valid states, but assuming the initial |
1035 is that there can be infinitely many valid states, but assuming the initial |
1036 state contains only finitely many objects, then also @{term "all_sobjs"} will |
1036 state contains only finitely many objects, then also @{term "all_sobjs"} will |
1037 be finite. To see the difference, consider the infinite ``chain'' of events |
1037 be finite. To see the difference, consider the infinite ``chain'' of events |
1038 just cloning a process @{text "p\<^isub>0"}: |
1038 just cloning a process @{text "p\<^sub>0"}: |
1039 |
1039 |
1040 \begin{center} |
1040 \begin{center} |
1041 \begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc} |
1041 \begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc} |
1042 \begin{tabular}[t]{c} |
1042 \begin{tabular}[t]{c} |
1043 Initial state:\\ |
1043 Initial state:\\ |
1044 @{term "{p\<^isub>0}"} |
1044 @{term "{p\<^sub>0}"} |
1045 \end{tabular} & |
1045 \end{tabular} & |
1046 \begin{tabular}[t]{c} |
1046 \begin{tabular}[t]{c} |
1047 \\ |
1047 \\ |
1048 @{text "\<Longrightarrow>"}\\[2mm] |
1048 @{text "\<Longrightarrow>"}\\[2mm] |
1049 {\small@{term "Clone p\<^isub>0 p\<^isub>1"}} |
1049 {\small@{term "Clone p\<^sub>0 p\<^sub>1"}} |
1050 \end{tabular} |
1050 \end{tabular} |
1051 & |
1051 & |
1052 \begin{tabular}[t]{c} |
1052 \begin{tabular}[t]{c} |
1053 \\ |
1053 \\ |
1054 @{term "{p\<^isub>0, p\<^isub>1}"} |
1054 @{term "{p\<^sub>0, p\<^sub>1}"} |
1055 \end{tabular} |
1055 \end{tabular} |
1056 & |
1056 & |
1057 \begin{tabular}[t]{c} |
1057 \begin{tabular}[t]{c} |
1058 \\ |
1058 \\ |
1059 @{text "\<Longrightarrow>"}\\[2mm] |
1059 @{text "\<Longrightarrow>"}\\[2mm] |
1060 {\small@{term "Clone p\<^isub>0 p\<^isub>2"}} |
1060 {\small@{term "Clone p\<^sub>0 p\<^sub>2"}} |
1061 \end{tabular} |
1061 \end{tabular} |
1062 & |
1062 & |
1063 \begin{tabular}[t]{c} |
1063 \begin{tabular}[t]{c} |
1064 \\ |
1064 \\ |
1065 @{term "{p\<^isub>0, p\<^isub>1, p\<^isub>2}"} |
1065 @{term "{p\<^sub>0, p\<^sub>1, p\<^sub>2}"} |
1066 \end{tabular} & |
1066 \end{tabular} & |
1067 \begin{tabular}[t]{c} |
1067 \begin{tabular}[t]{c} |
1068 \\ |
1068 \\ |
1069 @{text "..."}\\ |
1069 @{text "..."}\\ |
1070 \end{tabular} |
1070 \end{tabular} |
1075 The corresponding reachable objects are |
1075 The corresponding reachable objects are |
1076 |
1076 |
1077 \begin{center} |
1077 \begin{center} |
1078 \begin{tabular}[t]{cccc} |
1078 \begin{tabular}[t]{cccc} |
1079 \begin{tabular}[t]{c} |
1079 \begin{tabular}[t]{c} |
1080 @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>}"} |
1080 @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^sub>0)\<^esup>}"} |
1081 \end{tabular} & |
1081 \end{tabular} & |
1082 \begin{tabular}[t]{c} |
1082 \begin{tabular}[t]{c} |
1083 @{text "\<Longrightarrow>"} |
1083 @{text "\<Longrightarrow>"} |
1084 \end{tabular} |
1084 \end{tabular} |
1085 & |
1085 & |
1086 \begin{tabular}[t]{c} |
1086 \begin{tabular}[t]{c} |
1087 @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"} |
1087 @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^sub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"} |
1088 \end{tabular} |
1088 \end{tabular} |
1089 \end{tabular} |
1089 \end{tabular} |
1090 \end{center} |
1090 \end{center} |
1091 |
1091 |
1092 \noindent |
1092 \noindent |
1093 where no further progress can be made because the information |
1093 where no further progress can be made because the information |
1094 recorded about @{text "p\<^isub>2"}, @{text "p\<^isub>3"} and so on is just the same |
1094 recorded about @{text "p\<^sub>2"}, @{text "p\<^sub>3"} and so on is just the same |
1095 as for @{text "p\<^isub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we |
1095 as for @{text "p\<^sub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we |
1096 can prove the lemma: |
1096 can prove the lemma: |
1097 |
1097 |
1098 \begin{lemma}\label{finite} |
1098 \begin{lemma}\label{finite} |
1099 If @{text "finite init"}, then @{term "finite all_sobjs"}. |
1099 If @{text "finite init"}, then @{term "finite all_sobjs"}. |
1100 \end{lemma} |
1100 \end{lemma} |
1157 We omit the remaining rules for executing a file, cloning a process and |
1157 We omit the remaining rules for executing a file, cloning a process and |
1158 rules involving IPCs, which are similar. A simple consequence of our definitions |
1158 rules involving IPCs, which are similar. A simple consequence of our definitions |
1159 is that every tainted object is also reachable: |
1159 is that every tainted object is also reachable: |
1160 |
1160 |
1161 \begin{lemma} |
1161 \begin{lemma} |
1162 @{text "tainted\<^isup>s \<subseteq> reachable\<^isup>s"} |
1162 @{text "tainted\<^sup>s \<subseteq> reachable\<^sup>s"} |
1163 \end{lemma} |
1163 \end{lemma} |
1164 |
1164 |
1165 \noindent |
1165 \noindent |
1166 which in turn means that the set of @{term "tainted_s"} items is finite by Lemma~\ref{finite}. |
1166 which in turn means that the set of @{term "tainted_s"} items is finite by Lemma~\ref{finite}. |
1167 |
1167 |
1186 Using this function, we can define when an object is @{term taintable_s} in terms of |
1186 Using this function, we can define when an object is @{term taintable_s} in terms of |
1187 an item being @{term tainted_s}, namely |
1187 an item being @{term tainted_s}, namely |
1188 |
1188 |
1189 \begin{isabelle}\ \ \ \ \ %%% |
1189 \begin{isabelle}\ \ \ \ \ %%% |
1190 \mbox{\begin{tabular}{lcl} |
1190 \mbox{\begin{tabular}{lcl} |
1191 @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^isup>s \<and> |item| = Some obj"} |
1191 @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^sup>s \<and> |item| = Some obj"} |
1192 \end{tabular}} |
1192 \end{tabular}} |
1193 \end{isabelle} |
1193 \end{isabelle} |
1194 |
1194 |
1195 \noindent |
1195 \noindent |
1196 Note that @{term taintable_s} is only about objects that are present in |
1196 Note that @{term taintable_s} is only about objects that are present in |