1963 apply simp |
2003 apply simp |
1964 apply (rule_tac x = obj in exI) |
2004 apply (rule_tac x = obj in exI) |
1965 apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits) |
2005 apply (auto simp add:co2sobj_createmsgq alive_simps split:t_object.splits if_splits) |
1966 done |
2006 done |
1967 |
2007 |
1968 lemma s2ss_sendmsg: |
2008 ML {*fun my_clarify_tac i = |
1969 |
2009 REPEAT (( rtac @{thm impI} |
1970 lemma s2ss_recvmsg: |
2010 ORELSE' rtac @{thm allI} |
1971 |
2011 ORELSE' rtac @{thm ballI} |
1972 lemma s2ss_removemsgq: |
2012 ORELSE' rtac @{thm conjI} |
|
2013 ORELSE' etac @{thm conjE} |
|
2014 ORELSE' etac @{thm exE} |
|
2015 ORELSE' etac @{thm bexE} |
|
2016 ORELSE' etac @{thm disjE}) i) |
|
2017 *} |
|
2018 |
|
2019 lemma s2ss_sendmsg: "valid (SendMsg p q m # s) \<Longrightarrow> s2ss (SendMsg p q m # s) = ( |
|
2020 case (cq2smsgq s q, cq2smsgq (SendMsg p q m # s) q) of |
|
2021 (Some sq, Some sq') \<Rightarrow> update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq') |
|
2022 | _ \<Rightarrow> {})" |
|
2023 apply (frule vd_cons, frule vt_grant_os, clarsimp) |
|
2024 apply (case_tac "cq2smsgq s q") |
|
2025 apply (drule current_has_smsgq', simp+) |
|
2026 apply (case_tac "cq2smsgq (SendMsg p q m # s) q") |
|
2027 apply (drule current_has_smsgq', simp+) |
|
2028 |
|
2029 apply (simp add:update_s2ss_obj_def) |
|
2030 apply (tactic {*my_clarify_tac 1*}) |
|
2031 apply (simp add:s2ss_def) |
|
2032 apply (tactic {*my_seteq_tac 1*}) |
|
2033 apply (case_tac "obj = O_msgq q") |
|
2034 apply (rule disjI1, simp add:co2sobj.simps) |
|
2035 apply (rule disjI2, simp, rule_tac x = obj in exI) |
|
2036 apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits) |
|
2037 apply (simp add:co2sobj.simps) |
|
2038 apply (simp add:co2sobj.simps) |
|
2039 apply (simp add:co2sobj.simps) |
|
2040 apply (tactic {*my_setiff_tac 1*}) |
|
2041 apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps) |
|
2042 apply (tactic {*my_setiff_tac 1*}) |
|
2043 apply (case_tac "obj = O_msgq q") |
|
2044 apply (rule_tac x = obj' in exI) |
|
2045 apply (simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits if_splits) |
|
2046 apply (auto simp:co2sobj.simps)[1] |
|
2047 apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits) |
|
2048 apply (auto simp:co2sobj.simps)[1] |
|
2049 |
|
2050 apply (rule impI) |
|
2051 apply (simp add:s2ss_def) |
|
2052 apply (tactic {*my_seteq_tac 1*}) |
|
2053 apply (case_tac "obj = O_msgq q") |
|
2054 apply (rule disjI1, simp add:co2sobj.simps) |
|
2055 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI) |
|
2056 apply (simp add:co2sobj_sendmsg is_file_simps is_dir_simps split:t_object.splits if_splits) |
|
2057 apply (simp add:co2sobj.simps) |
|
2058 apply (simp add:co2sobj.simps) |
|
2059 apply (simp add:co2sobj.simps) |
|
2060 apply (rule notI, simp) |
|
2061 apply (frule_tac obj = obj in co2sobj_smsgq_imp, erule exE, simp) |
|
2062 apply (erule_tac x = obj in allE, simp add:co2sobj_sendmsg) |
|
2063 apply (tactic {*my_setiff_tac 1*}) |
|
2064 apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps) |
|
2065 apply (tactic {*my_setiff_tac 1*}) |
|
2066 apply (case_tac "obj = O_msgq q") |
|
2067 apply (simp add:co2sobj.simps) |
|
2068 apply (rule_tac x = obj in exI, simp add:co2sobj_sendmsg alive_sendmsg split:t_object.splits) |
|
2069 apply (auto simp:co2sobj.simps)[1] |
|
2070 done |
|
2071 |
|
2072 lemma alive_co2sobj_removemsgq: |
|
2073 "\<lbrakk>alive s obj; valid (RemoveMsgq p q # s); co2sobj s obj = Some sobj; obj \<noteq> O_msgq q\<rbrakk> |
|
2074 \<Longrightarrow> alive (RemoveMsgq p q # s) obj" |
|
2075 apply (erule co2sobj_some_caseD) |
|
2076 apply (auto simp:is_file_simps is_dir_simps) |
|
2077 done |
|
2078 |
|
2079 lemma s2ss_removemsgq: "valid (RemoveMsgq p q # s) \<Longrightarrow> s2ss (RemoveMsgq p q # s) = |
|
2080 (case (cq2smsgq s q) of |
|
2081 Some sq \<Rightarrow> del_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) |
|
2082 | _ \<Rightarrow> {})" |
|
2083 apply (frule vd_cons, frule vt_grant_os, clarsimp) |
|
2084 apply (split option.splits, rule conjI, rule impI) |
|
2085 apply (drule current_has_smsgq', simp, simp) |
|
2086 apply (rule allI, rule impI) |
|
2087 |
|
2088 apply (simp add:del_s2ss_obj_def) |
|
2089 apply (tactic {*my_clarify_tac 1*}) |
|
2090 apply (simp add:s2ss_def) |
|
2091 apply (tactic {*my_seteq_tac 1*}) |
|
2092 apply (case_tac "obj = O_msgq q", simp) |
|
2093 apply (rule_tac x = obj in exI) |
|
2094 apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits) |
|
2095 apply (tactic {*my_setiff_tac 1*}) |
|
2096 apply (case_tac "obj = O_msgq q", simp) |
|
2097 apply (rule_tac x = obj' in exI) |
|
2098 apply (frule_tac obj = obj' in co2sobj_smsgq_imp, erule exE) |
|
2099 apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits) |
|
2100 apply (simp add:co2sobj.simps) |
|
2101 apply (rule_tac x = obj in exI) |
|
2102 apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq) |
|
2103 |
|
2104 apply (rule impI) |
|
2105 apply (simp add:s2ss_def) |
|
2106 apply (tactic {*my_seteq_tac 1*}) |
|
2107 apply (case_tac "obj = O_msgq q", simp) |
|
2108 apply (simp, rule conjI, rule_tac x = obj in exI) |
|
2109 apply (simp add:co2sobj_removemsgq alive_simps split:t_object.splits if_splits) |
|
2110 apply (rule notI, simp, frule_tac obj = obj in co2sobj_smsgq_imp, erule exE) |
|
2111 apply (erule_tac x = obj in allE, simp add:co2sobj_removemsgq alive_co2sobj_removemsgq) |
|
2112 apply (tactic {*my_setiff_tac 1*}) |
|
2113 apply (case_tac "obj = O_msgq q", simp) |
|
2114 apply (simp add:co2sobj.simps) |
|
2115 apply (rule_tac x = obj in exI) |
|
2116 apply (simp add:co2sobj_removemsgq alive_co2sobj_removemsgq) |
|
2117 done |
|
2118 |
|
2119 declare Product_Type.split_paired_Ex Product_Type.split_paired_All [simp del] |
|
2120 |
|
2121 lemma s2ss_shm_no_bk_elim': |
|
2122 "\<lbrakk>x \<notin> s2ss_shm_no_backup s pfrom; co2sobj s (O_proc p) = Some x; O_proc p \<notin> Tainted s; |
|
2123 valid s; info_flow_shm s pfrom p\<rbrakk> |
|
2124 \<Longrightarrow> \<exists> p'. \<not> info_flow_shm s pfrom p' \<and> p' \<in> current_procs s \<and> co2sobj s (O_proc p') = Some x" |
|
2125 apply (auto simp:s2ss_shm_no_backup_def co2sobj.simps tainted_eq_Tainted split:option.splits) |
|
2126 apply (erule_tac x = p in allE, auto) |
|
2127 apply (rule_tac x = p' in exI, auto) |
|
2128 done |
|
2129 |
|
2130 lemma s2ss_recvmsg: "valid (RecvMsg p q m # s) \<Longrightarrow> s2ss (RecvMsg p q m # s) = ( |
|
2131 case (cq2smsgq s q, cq2smsgq (RecvMsg p q m # s) q) of |
|
2132 (Some sq, Some sq') \<Rightarrow> if (O_msg q m \<in> Tainted s \<and> O_proc p \<notin> Tainted s) |
|
2133 then update_s2ss_obj s (update_s2ss_shm s p) (O_msgq q) (S_msgq sq) (S_msgq sq') |
|
2134 else update_s2ss_obj s (s2ss s) (O_msgq q) (S_msgq sq) (S_msgq sq') |
|
2135 | _ \<Rightarrow> {})" |
|
2136 apply (frule vt_grant_os, frule vd_cons) |
|
2137 apply (case_tac "cq2smsgq s q") |
|
2138 apply (drule current_has_smsgq', simp, simp) |
|
2139 apply (case_tac "cq2smsgq (RecvMsg p q m # s) q") |
|
2140 apply (drule current_has_smsgq', simp, simp) |
|
2141 apply (simp split:if_splits add:update_s2ss_obj_def) |
|
2142 |
|
2143 apply (tactic {*my_clarify_tac 1*}) |
|
2144 unfolding s2ss_def update_s2ss_shm_def |
|
2145 apply (tactic {*my_seteq_tac 1*}) |
|
2146 apply (case_tac "obj = O_msgq q") |
|
2147 apply (rule disjI1, simp add:co2sobj.simps) |
|
2148 apply (rule disjI2) |
|
2149 apply (rule DiffI) |
|
2150 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2151 apply (case_tac "info_flow_shm s p pa") |
|
2152 apply (rule UnI2) |
|
2153 apply (simp add:co2sobj_recvmsg del:Product_Type.split_paired_Ex |
|
2154 split:t_object.splits option.splits) |
|
2155 apply (rule_tac x = ab in exI, simp, rule_tac x = pa in exI, simp) |
|
2156 apply (rule UnI1,simp, rule_tac x = obj in exI) |
|
2157 apply (simp add:co2sobj_recvmsg split:t_object.splits option.splits) |
|
2158 apply (rule UnI1,simp, rule_tac x = obj in exI) |
|
2159 apply (simp add:co2sobj_recvmsg is_file_simps split:t_object.splits option.splits) |
|
2160 apply (rule UnI1, simp,rule_tac x = obj in exI) |
|
2161 apply (simp add:co2sobj_recvmsg split:t_object.splits option.splits) |
|
2162 apply (rule UnI1, simp,rule_tac x = obj in exI) |
|
2163 apply (simp add:co2sobj_recvmsg is_dir_simps split:t_object.splits option.splits) |
|
2164 apply (rule UnI1, simp, rule_tac x = obj in exI) |
|
2165 apply (simp add:co2sobj_recvmsg split:t_object.splits option.splits if_splits) |
|
2166 apply (rule notI, simp add:s2ss_shm_no_backup_def del:Product_Type.split_paired_Ex) |
|
2167 apply (erule exE|erule conjE)+ |
|
2168 apply (simp, frule co2sobj_sproc_imp, erule exE, simp) |
|
2169 apply (simp add:co2sobj_recvmsg split:if_splits option.splits) |
|
2170 apply (erule_tac x = paa in allE, simp) |
|
2171 apply (tactic {*my_setiff_tac 1*}) |
|
2172 apply (rule_tac x = "O_msgq q" in exI, simp add:co2sobj.simps alive_recvmsg) |
|
2173 apply (tactic {*my_setiff_tac 1*}, erule UnE) |
|
2174 apply (tactic {*my_setiff_tac 1*}) |
|
2175 apply (case_tac "obj = O_msgq q") |
|
2176 apply (rule_tac x = obj' in exI) |
|
2177 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2178 split:t_object.splits if_splits option.splits) |
|
2179 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] |
|
2180 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2181 apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s") |
|
2182 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) |
|
2183 apply (erule exE|erule conjE)+ |
|
2184 apply (rule_tac x = "O_proc p'" in exI) |
|
2185 apply (simp add:co2sobj_recvmsg alive_simps) |
|
2186 apply (rule_tac x = obj in exI) |
|
2187 apply (case_tac "info_flow_shm s p pa", simp) |
|
2188 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2189 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) |
|
2190 apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) |
|
2191 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2192 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) |
|
2193 apply (rule_tac x = obj in exI) |
|
2194 apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits) |
|
2195 apply (simp split:t_object.splits) |
|
2196 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) |
|
2197 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) |
|
2198 apply (tactic {*my_setiff_tac 1*}) |
|
2199 apply (rule_tac x = "O_proc pa" in exI) |
|
2200 apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg) |
|
2201 apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs) |
|
2202 |
|
2203 apply (tactic {*my_clarify_tac 1*}) |
|
2204 apply (tactic {*my_seteq_tac 1*}) |
|
2205 apply (case_tac "obj = O_msgq q") |
|
2206 apply (rule disjI1, simp add:co2sobj.simps) |
|
2207 apply (rule disjI2, simp, rule_tac x = obj in exI) |
|
2208 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps split:t_object.splits if_splits option.splits) |
|
2209 apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) |
|
2210 apply (simp add:co2sobj.simps) |
|
2211 apply (simp add:co2sobj.simps) |
|
2212 apply (case_tac "msgs_of_queue s q", simp, simp) |
|
2213 apply (tactic {*my_setiff_tac 1*}) |
|
2214 apply (rule_tac x = "O_msgq q" in exI) |
|
2215 apply (simp add:co2sobj.simps) |
|
2216 apply (tactic {*my_setiff_tac 1 *}) |
|
2217 apply (case_tac "obj = O_msgq q") |
|
2218 apply (rule_tac x = obj' in exI) |
|
2219 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2220 split:t_object.splits if_splits option.splits) |
|
2221 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] |
|
2222 apply (rule_tac x = obj in exI) |
|
2223 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2224 split:t_object.splits if_splits option.splits) |
|
2225 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps tainted_eq_Tainted info_flow_shm_Tainted)[1] |
|
2226 |
|
2227 apply (tactic {*my_clarify_tac 1*}) |
|
2228 apply (tactic {*my_seteq_tac 1*}) |
|
2229 apply (case_tac "obj = O_msgq q") |
|
2230 apply (rule disjI1, simp add:co2sobj.simps) |
|
2231 apply (rule disjI2) |
|
2232 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2233 apply (case_tac "info_flow_shm s p pa") |
|
2234 apply (case_tac "O_proc pa \<in> Tainted s") |
|
2235 apply (rule DiffI, rule UnI1, simp) |
|
2236 apply (rule_tac x = obj in exI) |
|
2237 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2238 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
2239 apply (erule s2ss_shm_no_bk_intro2, simp, simp) |
|
2240 apply (rule DiffI, rule UnI2, rule CollectI) |
|
2241 apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp) |
|
2242 apply (rule_tac x = ab in exI, simp) |
|
2243 apply (rule_tac x = pa in exI, simp add:cp2sproc_other) |
|
2244 apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp) |
|
2245 apply (rule DiffI, rule UnI1, simp) |
|
2246 apply (rule_tac x = obj in exI) |
|
2247 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2248 apply (rule_tac p = pa in s2ss_shm_no_bk_intro3) |
|
2249 apply (simp add:co2sobj_recvmsg, simp, simp) |
|
2250 apply (rule DiffI, rule UnI1, simp) |
|
2251 apply (rule_tac x = obj in exI) |
|
2252 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_file_simps split:option.splits) |
|
2253 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2254 apply (rule DiffI, rule UnI1, simp) |
|
2255 apply (rule_tac x = obj in exI) |
|
2256 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2257 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2258 apply (rule DiffI, rule UnI1, simp) |
|
2259 apply (rule_tac x = obj in exI) |
|
2260 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_dir_simps split:option.splits) |
|
2261 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2262 apply (rule DiffI, rule UnI1, simp) |
|
2263 apply (rule_tac x = obj in exI) |
|
2264 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2265 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2266 |
|
2267 apply (tactic {*my_setiff_tac 1*}) |
|
2268 apply (rule_tac x = "O_msgq q" in exI) |
|
2269 apply (simp add:co2sobj.simps) |
|
2270 apply (tactic {*my_setiff_tac 1*}) |
|
2271 apply (erule UnE, tactic {*my_setiff_tac 1*}) |
|
2272 apply (case_tac "obj = O_msgq q") |
|
2273 apply (rule_tac x = obj' in exI) |
|
2274 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2275 split:t_object.splits if_splits option.splits) |
|
2276 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] |
|
2277 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2278 apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s") |
|
2279 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) |
|
2280 apply (erule exE|erule conjE)+ |
|
2281 apply (rule_tac x = "O_proc p'" in exI) |
|
2282 apply (simp add:co2sobj_recvmsg alive_simps) |
|
2283 apply (rule_tac x = obj in exI) |
|
2284 apply (case_tac "info_flow_shm s p pa", simp) |
|
2285 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2286 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) |
|
2287 apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) |
|
2288 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2289 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) |
|
2290 apply (rule_tac x = obj in exI) |
|
2291 apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits) |
|
2292 apply (simp split:t_object.splits) |
|
2293 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) |
|
2294 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) |
|
2295 apply (tactic {*my_setiff_tac 1*}) |
|
2296 apply (rule_tac x = "O_proc pa" in exI) |
|
2297 apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg) |
|
2298 apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs) |
|
2299 |
|
2300 apply (rule impI, tactic {*my_seteq_tac 1*}) |
|
2301 apply (case_tac "obj = O_msgq q") |
|
2302 apply (rule disjI1, simp add:co2sobj.simps) |
|
2303 apply (rule disjI2, simp, rule conjI) |
|
2304 apply (rule_tac x = obj in exI) |
|
2305 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2306 split:t_object.splits if_splits option.splits) |
|
2307 apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) |
|
2308 apply (simp add:co2sobj_recvmsg) |
|
2309 apply (simp add:alive_recvmsg split:if_splits) |
|
2310 apply (erule_tac x = obj in allE, simp split:t_object.splits if_splits option.splits) |
|
2311 apply (rule notI, simp add:co2sobj.simps) |
|
2312 apply (tactic {*my_setiff_tac 1*}) |
|
2313 apply (rule_tac x = "O_msgq q" in exI) |
|
2314 apply (simp add:co2sobj.simps) |
|
2315 apply (tactic {*my_setiff_tac 1*}) |
|
2316 apply simp |
|
2317 apply (tactic {*my_clarify_tac 1*}) |
|
2318 apply (case_tac "obj = O_msgq q") |
|
2319 apply (rule_tac x = obj' in exI) |
|
2320 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2321 split:t_object.splits if_splits option.splits) |
|
2322 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] |
|
2323 apply (rule_tac x = obj in exI) |
|
2324 apply (frule_tac obj = obj in co2sobj_recvmsg) |
|
2325 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) |
|
2326 apply (rule conjI) |
|
2327 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) |
|
2328 apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1] |
|
2329 |
|
2330 apply (tactic {*my_clarify_tac 1*}) |
|
2331 apply (tactic {*my_seteq_tac 1*}) |
|
2332 apply (case_tac "obj = O_msgq q") |
|
2333 apply (rule disjI1, simp add:co2sobj.simps) |
|
2334 apply (rule disjI2) |
|
2335 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2336 apply (case_tac "info_flow_shm s p pa") |
|
2337 apply (case_tac "O_proc pa \<in> Tainted s") |
|
2338 apply (rule DiffI, rule UnI1, simp) |
|
2339 apply (rule_tac x = obj in exI) |
|
2340 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2341 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
2342 apply (erule s2ss_shm_no_bk_intro2, simp, simp) |
|
2343 apply (rule DiffI, rule UnI2, rule CollectI) |
|
2344 apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp) |
|
2345 apply (rule_tac x = ab in exI, simp) |
|
2346 apply (rule_tac x = pa in exI, simp add:cp2sproc_other) |
|
2347 apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp) |
|
2348 apply (rule DiffI, rule UnI1, simp) |
|
2349 apply (rule_tac x = obj in exI) |
|
2350 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2351 apply (rule_tac p = pa in s2ss_shm_no_bk_intro3) |
|
2352 apply (simp add:co2sobj_recvmsg, simp, simp) |
|
2353 apply (rule DiffI, rule UnI1, simp) |
|
2354 apply (rule_tac x = obj in exI) |
|
2355 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_file_simps split:option.splits) |
|
2356 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2357 apply (rule DiffI, rule UnI1, simp) |
|
2358 apply (rule_tac x = obj in exI) |
|
2359 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2360 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2361 apply (rule DiffI, rule UnI1, simp) |
|
2362 apply (rule_tac x = obj in exI) |
|
2363 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_dir_simps split:option.splits) |
|
2364 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2365 apply (rule DiffI, rule UnI1, simp) |
|
2366 apply (rule_tac x = obj in exI) |
|
2367 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2368 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2369 apply (tactic {*my_setiff_tac 1*}) |
|
2370 apply (rule_tac x = "O_msgq q" in exI) |
|
2371 apply (simp add:co2sobj.simps) |
|
2372 apply (tactic {*my_setiff_tac 1*}) |
|
2373 apply (erule UnE, tactic {*my_setiff_tac 1*}) |
|
2374 apply (case_tac "obj = O_msgq q") |
|
2375 apply (rule_tac x = obj' in exI) |
|
2376 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2377 split:t_object.splits if_splits option.splits) |
|
2378 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] |
|
2379 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2380 apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s") |
|
2381 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) |
|
2382 apply (erule exE|erule conjE)+ |
|
2383 apply (rule_tac x = "O_proc p'" in exI) |
|
2384 apply (simp add:co2sobj_recvmsg alive_simps) |
|
2385 apply (rule_tac x = obj in exI) |
|
2386 apply (case_tac "info_flow_shm s p pa", simp) |
|
2387 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2388 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) |
|
2389 apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) |
|
2390 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2391 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) |
|
2392 apply (rule_tac x = obj in exI) |
|
2393 apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits) |
|
2394 apply (simp split:t_object.splits) |
|
2395 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) |
|
2396 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) |
|
2397 apply (tactic {*my_setiff_tac 1*}) |
|
2398 apply (rule_tac x = "O_proc pa" in exI) |
|
2399 apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg) |
|
2400 apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs) |
|
2401 |
|
2402 apply (rule impI, tactic {*my_seteq_tac 1*}) |
|
2403 apply (case_tac "obj = O_msgq q") |
|
2404 apply (rule disjI1, simp add:co2sobj.simps) |
|
2405 apply (rule disjI2, simp) |
|
2406 apply (rule_tac x = obj in exI) |
|
2407 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2408 split:t_object.splits if_splits option.splits) |
|
2409 apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) |
|
2410 apply (tactic {*my_setiff_tac 1*}) |
|
2411 apply (rule_tac x = "O_msgq q" in exI) |
|
2412 apply (simp add:co2sobj.simps) |
|
2413 apply (tactic {*my_setiff_tac 1*}) |
|
2414 apply (case_tac "obj = O_msgq q") |
|
2415 apply (rule_tac x = obj' in exI) |
|
2416 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2417 split:t_object.splits if_splits option.splits) |
|
2418 apply (auto simp:co2sobj.simps is_file_simps is_dir_simps)[1] |
|
2419 apply (rule_tac x = obj in exI) |
|
2420 apply (frule_tac obj = obj in co2sobj_recvmsg) |
|
2421 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) |
|
2422 apply (rule conjI) |
|
2423 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) |
|
2424 apply (auto simp:co2sobj.simps tainted_eq_Tainted split:t_object.splits option.splits if_splits)[1] |
|
2425 |
|
2426 apply (tactic {*my_clarify_tac 1*}) |
|
2427 apply (tactic {*my_seteq_tac 1*}) |
|
2428 apply (case_tac "obj = O_msgq q") |
|
2429 apply (rule disjI1, simp add:co2sobj.simps) |
|
2430 apply (rule disjI2) |
|
2431 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2432 apply (case_tac "info_flow_shm s p pa") |
|
2433 apply (case_tac "O_proc pa \<in> Tainted s") |
|
2434 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
2435 apply (rule_tac x = obj in exI) |
|
2436 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2437 apply (simp add:co2sobj.simps tainted_eq_Tainted) |
|
2438 apply (erule s2ss_shm_no_bk_intro2, simp, simp) |
|
2439 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
2440 apply (rule DiffI, rule DiffI, rule UnI2, rule CollectI) |
|
2441 apply (simp only:co2sobj.simps tainted_eq_Tainted split:option.splits, simp) |
|
2442 apply (rule_tac x = ab in exI, simp) |
|
2443 apply (rule_tac x = pa in exI, simp add:cp2sproc_other) |
|
2444 apply (rule s2ss_shm_no_bk_intro2, simp, simp, simp) |
|
2445 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
2446 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
2447 apply (rule_tac x = obj in exI) |
|
2448 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2449 apply (rule_tac p = pa in s2ss_shm_no_bk_intro3) |
|
2450 apply (simp add:co2sobj_recvmsg, simp, simp) |
|
2451 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
2452 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
2453 apply (rule_tac x = obj in exI) |
|
2454 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_file_simps split:option.splits) |
|
2455 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2456 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
2457 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
2458 apply (rule_tac x = obj in exI) |
|
2459 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2460 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2461 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
2462 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
2463 apply (rule_tac x = obj in exI) |
|
2464 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp add:is_dir_simps split:option.splits) |
|
2465 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2466 apply (simp, rule notI, simp add:co2sobj.simps split:option.splits) |
|
2467 apply (rule DiffI, rule DiffI, rule UnI1, simp) |
|
2468 apply (rule_tac x = obj in exI) |
|
2469 apply (frule_tac obj = obj in co2sobj_recvmsg, simp, simp split:option.splits) |
|
2470 apply (simp add:co2sobj_recvmsg s2ss_shm_no_bk_intro1) |
|
2471 apply (simp, rule notI, erule_tac x = obj in allE, simp) |
|
2472 apply (simp add:co2sobj_recvmsg) |
|
2473 apply (tactic {*my_setiff_tac 1*}) |
|
2474 apply (rule_tac x = "O_msgq q" in exI) |
|
2475 apply (simp add:co2sobj.simps) |
|
2476 apply (tactic {*my_setiff_tac 1*}) |
|
2477 apply (erule UnE, tactic {*my_setiff_tac 1*}) |
|
2478 apply (case_tac "obj = O_msgq q") |
|
2479 apply (simp add:co2sobj.simps) |
|
2480 apply (erule_tac obj = obj in co2sobj_some_caseD) |
|
2481 apply (case_tac "info_flow_shm s p pa \<and> O_proc pa \<notin> Tainted s") |
|
2482 apply (drule_tac p = pa in s2ss_shm_no_bk_elim', simp+) |
|
2483 apply (erule exE|erule conjE)+ |
|
2484 apply (rule_tac x = "O_proc p'" in exI) |
|
2485 apply (simp add:co2sobj_recvmsg alive_simps) |
|
2486 apply (rule_tac x = obj in exI) |
|
2487 apply (case_tac "info_flow_shm s p pa", simp) |
|
2488 apply (frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2489 apply (case_tac "cp2sproc s pa", simp add:co2sobj.simps) |
|
2490 apply (simp, simp add:co2sobj.simps tainted_eq_Tainted) |
|
2491 apply (simp, frule_tac obj = obj in co2sobj_recvmsg, simp+) |
|
2492 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg alive_simps) |
|
2493 apply (rule_tac x = obj in exI) |
|
2494 apply (frule_tac obj = obj in co2sobj_recvmsg, simp split:t_object.splits) |
|
2495 apply (simp split:t_object.splits) |
|
2496 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg is_dir_simps) |
|
2497 apply (rule_tac x = obj in exI, simp add:co2sobj_recvmsg) |
|
2498 apply (tactic {*my_setiff_tac 1*}) |
|
2499 apply (rule_tac x = "O_proc pa" in exI) |
|
2500 apply (frule_tac obj = "O_proc pa" in co2sobj_recvmsg) |
|
2501 apply (simp add:info_shm_flow_in_procs, simp add:info_shm_flow_in_procs) |
|
2502 |
|
2503 apply (rule impI, tactic {*my_seteq_tac 1*}) |
|
2504 apply (case_tac "obj = O_msgq q") |
|
2505 apply (rule disjI1, simp add:co2sobj.simps) |
|
2506 apply (rule disjI2, simp, rule conjI) |
|
2507 apply (rule_tac x = obj in exI) |
|
2508 apply (simp add:co2sobj_recvmsg is_file_simps is_dir_simps alive_recvmsg |
|
2509 split:t_object.splits if_splits option.splits) |
|
2510 apply (simp add:co2sobj.simps tainted_eq_Tainted info_flow_shm_Tainted) |
|
2511 apply (rule notI, simp) |
|
2512 apply (frule co2sobj_smsgq_imp, erule exE, simp) |
|
2513 apply (simp add:co2sobj_recvmsg) |
|
2514 apply (erule_tac x = obj in allE, simp) |
|
2515 apply (tactic {*my_setiff_tac 1*}) |
|
2516 apply (rule_tac x = "O_msgq q" in exI) |
|
2517 apply (simp add:co2sobj.simps) |
|
2518 apply (tactic {*my_setiff_tac 1*}) |
|
2519 apply (simp, erule exE, erule conjE) |
|
2520 apply (case_tac "obj = O_msgq q") |
|
2521 apply (simp add:co2sobj.simps) |
|
2522 apply (rule_tac x = obj in exI) |
|
2523 apply (frule_tac obj = obj in co2sobj_recvmsg) |
|
2524 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) |
|
2525 apply (rule conjI) |
|
2526 apply (simp add:alive_recvmsg, rule notI, simp add:co2sobj.simps) |
|
2527 apply (auto simp:co2sobj.simps tainted_eq_Tainted intro: info_flow_shm_Tainted |
|
2528 split:t_object.splits option.splits if_splits)[1] |
|
2529 done |
|
2530 |
|
2531 lemma s2ss_createshm: |
|
2532 "valid (CreateShM p h # s) \<Longrightarrow> s2ss (CreateShM p h # s) = |
|
2533 (case (ch2sshm (CreateShM p h # s) h) of |
|
2534 Some sh \<Rightarrow> s2ss s \<union> {S_shm sh} |
|
2535 | _ \<Rightarrow> {})" |
|
2536 apply (frule vd_cons, frule vt_grant_os, clarsimp) |
|
2537 apply (case_tac "ch2sshm (CreateShM p h # s) h") |
|
2538 apply (drule current_shm_has_sh', simp+) |
|
2539 apply (simp add:s2ss_def) |
|
2540 apply (tactic {*my_seteq_tac 1*}) |
|
2541 apply (case_tac "obj = O_shm h") |
|
2542 apply (rule disjI1, simp add:co2sobj.simps) |
|
2543 apply (rule disjI2, simp, rule_tac x = obj in exI) |
|
2544 apply (simp add:co2sobj_createshm is_file_simps is_dir_simps split:t_object.splits if_splits) |
|
2545 apply (simp add:co2sobj.simps) |
|
2546 apply (simp add:co2sobj.simps) |
|
2547 apply (tactic {*my_setiff_tac 1*}) |
|
2548 apply (rule_tac x = "O_shm h" in exI, simp add:co2sobj.simps) |
|
2549 apply (tactic {*my_setiff_tac 1*}) |
|
2550 apply (case_tac "obj = O_shm h") |
|
2551 apply simp |
|
2552 apply (rule_tac x = obj in exI) |
|
2553 apply (auto simp add:co2sobj_createshm alive_simps split:t_object.splits if_splits) |
|
2554 done |
|
2555 |
|
2556 |
|
2557 lemma s2ss_attach1: |
|
2558 "valid (Attach p h SHM_RDWR # s) \<Longrightarrow> s2ss (Attach p h SHM_RDWR # s) = " |
|
2559 |
|
2560 lemma s2ss_attach1: |
|
2561 "valid (Attach p h SHM_RDONLY # s) \<Longrightarrow> s2ss (Attach p h SHM_RDONLY # s) = " |
|
2562 |
|
2563 lemma s2ss_attach1: |
|
2564 "valid (Attach p h flag # s) \<Longrightarrow> s2ss (Attach p h flag # s) = " |
|
2565 |
|
2566 lemma s2ss_Detach: |
|
2567 "valid (Detach p h # s) \<Longrightarrow> s2ss (Detach p h # s) = " |
|
2568 |
|
2569 lemma s2ss_deleteshm: |
|
2570 "valid (DeleteShM p h # s) \<Longrightarrow> s2ss (DeleteShM p h # s)" |
|
2571 |
1973 |
2572 |
1974 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
2573 lemmas s2ss_simps = s2ss_execve s2ss_clone s2ss_ptrace s2ss_kill s2ss_exit s2ss_open |
1975 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
2574 s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard |
1976 s2ss_truncate s2ss_createmsgq |
2575 s2ss_truncate s2ss_createmsgq s2ss_sendmsg s2ss_removemsgq s2ss_recvmsg |
1977 |
2576 s2ss_createshm |
|
2577 |