1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Access 8imports Deterministic_AC 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13section \<open>Policy and policy refinement\<close> 14 15subsection \<open>Policy definition\<close> 16 17text\<open> 18 19The goal is to place limits on what untrusted agents can do while the 20trusted agents are not running. This supports a framing constraint in 21the descriptions (Hoare triples) of syscalls. Roughly the existing 22proofs show the effect of the syscall, and this proof summarises what 23doesn't (or isn't allowed to) change. 24 25The basic intuition is to map all object references to the agent they 26belong to and show that changes to the object reference graph are 27allowed by the policy specified by the user. The policy is a labelled 28graph amongst agents independent of the current state, i.e. a static 29external summary of what should be talking to what and how. 30 31The interesting cases occur between trusted and untrusted components: 32e.g. we assume that it is unsafe for untrusted components (UT) 33to send capabilities to trusted components (T), and so T must ensure 34that all endpoints it shares with UT that it receives on do not have 35the grant bit set. 36 37\<close> 38 39type_synonym 'a agent_map = "obj_ref \<Rightarrow> 'a" 40type_synonym 'a agent_asid_map = "asid \<Rightarrow> 'a" 41type_synonym 'a agent_irq_map = "10 word \<Rightarrow> 'a" 42type_synonym 'a agent_domain_map = "domain \<Rightarrow> 'a set" 43 44text\<open> 45 46What one agent can do to another. We allow multiple edges between 47agents in the graph. 48 49Control is special. It implies the ability to do pretty much anything, 50including get access the other rights, create, remove, etc. 51 52DeleteDerived allows you to delete a cap derived from a cap you own 53\<close> 54 55datatype auth = Control | Receive | SyncSend | Notify 56 | Reset | Grant | Call | Reply | Write | Read 57 | ASIDPoolMapsASID | DeleteDerived 58 59text\<open> 60 61The interesting case is for endpoints. 62 63Consider an EP between T and UT (across a trust boundary). We want to 64be able to say that all EPs and tcbs that T does not expose to UT do 65not change when it is not running. If UT had a direct Send right to T 66then integrity (see below) could not guarantee this, as it doesn't 67know which EP can be changed by UT. Thus we set things up like this 68(all distinct labels): 69 70T -Receive-> EP <-Send- UT 71 72Now UT can interfere with EP and all of T's tcbs blocked for receive on EP, 73but not endpoints internal to T, or tcbs blocked on other (suitably 74labelled) EPs, etc. 75 76\<close> 77 78type_synonym 'a auth_graph = "('a \<times> auth \<times> 'a) set" 79 80text \<open> 81 82Each global namespace will need a labeling function. 83 84We map each scheduling domain to a single label; concretely, each tcb 85in a scheduling domain has to have the same label. We will want to 86weaken this in the future. 87 88The booleans @{text pasMayActivate} and @{text pasMayEditReadyQueues} 89are used to weaken the integrity property. When @{const True}, 90@{text pasMayActivate} causes the integrity property to permit 91activation of newly-scheduled threads. Likewise, @{text pasMayEditReadyQueues} 92has the integrity property permit the removal of threads from ready queues, 93as occurs when scheduling a new domain for instance. By setting each of these 94@{const False} we get a more constrained integrity property that is useful for 95establishing some of the proof obligations for the infoflow proofs, particularly 96those over @{const handle_event} that neither activates new threads nor schedules 97new domains. 98 99The @{text pasDomainAbs} relation describes which labels may run in 100a given scheduler domain. This relation is not relevant to integrity 101but will be used in the information flow theory (with additional 102constraints on its structure). 103\<close> 104 105end 106 107record 'a PAS = 108 pasObjectAbs :: "'a agent_map" 109 pasASIDAbs :: "'a agent_asid_map" 110 pasIRQAbs :: "'a agent_irq_map" 111 pasPolicy :: "'a auth_graph" 112 pasSubject :: "'a" \<comment> \<open>The active label\<close> 113 pasMayActivate :: "bool" 114 pasMayEditReadyQueues :: "bool" 115 pasMaySendIrqs :: "bool" 116 pasDomainAbs :: "'a agent_domain_map" 117 118text\<open> 119 120Very often we want to say that the agent currently running owns a 121given pointer. 122 123\<close> 124 125abbreviation is_subject :: "'a PAS \<Rightarrow> word32 \<Rightarrow> bool" 126where 127 "is_subject aag ptr \<equiv> pasObjectAbs aag ptr = pasSubject aag" 128 129text\<open> 130 131Also we often want to say the current agent can do something to a 132pointer that he doesn't own but has some authority to. 133 134\<close> 135 136abbreviation(input) aag_has_auth_to :: "'a PAS \<Rightarrow> auth \<Rightarrow> word32 \<Rightarrow> bool" 137where 138 "aag_has_auth_to aag auth ptr \<equiv> (pasSubject aag, auth, pasObjectAbs aag ptr) \<in> pasPolicy aag" 139 140abbreviation aag_subjects_have_auth_to_label :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> auth \<Rightarrow> 'a \<Rightarrow> bool" 141where 142 "aag_subjects_have_auth_to_label subs aag auth label 143 \<equiv> \<exists>s \<in> subs. (s, auth, label) \<in> pasPolicy aag" 144 145abbreviation aag_subjects_have_auth_to :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> auth \<Rightarrow> obj_ref \<Rightarrow> bool" 146where 147 "aag_subjects_have_auth_to subs aag auth oref 148 \<equiv> aag_subjects_have_auth_to_label subs aag auth (pasObjectAbs aag oref)" 149 150 151context begin interpretation Arch . (*FIXME: arch_split*) 152 153subsection \<open>Policy wellformedness\<close> 154 155text\<open> 156 157Wellformedness of the agent authority function with respect to a label 158(the current thread): 159 160\begin{itemize} 161 162\item For (the current untrusted) @{term "agent"}, large enough 163 authority must be contained within the agent's boundaries. 164 165\item @{term "agent"} has all the self authority it could want. 166 167\item If an agent can grant caps through an endpoint, then it is 168 authority-equivalent to all agents that can receive on that 169 endpoint. 170 171\item Similarly, if an agent can grant through a reply cap, then 172 it is authority-equivalent to the original caller. 173 174\item Anyone can send on any IRQ notification. 175 176\item Call implies a send ability. 177 178\item If an agent could reply to a call, then the caller has the 179 authority to delete the derived reply cap. This can happen if 180 the caller thread is deleted before the reply takes place. 181 182\item Reply caps can be transferred, so the DeleteDerived 183 authority propagates transitively. 184 185\end{itemize} 186 187\<close> 188 189definition policy_wellformed 190where 191 "policy_wellformed aag maySendIrqs irqs agent \<equiv> 192 (\<forall>agent'. (agent, Control, agent') \<in> aag \<longrightarrow> agent = agent') 193 \<and> (\<forall>a. (agent, a, agent) \<in> aag) 194 \<and> (\<forall>s r ep. (s, Grant, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag 195 \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag) 196 \<and> (maySendIrqs \<longrightarrow> (\<forall>irq ntfn. irq \<in> irqs \<and> (irq, Notify, ntfn) \<in> aag 197 \<longrightarrow> (agent, Notify, ntfn) \<in> aag)) 198 \<and> (\<forall>s ep. (s, Call, ep) \<in> aag \<longrightarrow> (s, SyncSend, ep) \<in> aag) 199 \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<longrightarrow> (r, Reply, s) \<in> aag) 200 \<and> (\<forall>s r. (s, Reply, r) \<in> aag \<longrightarrow> (r, DeleteDerived, s) \<in> aag) 201 \<and> (\<forall>l1 l2 l3. (l1, DeleteDerived, l2) \<in> aag \<longrightarrow> (l2, DeleteDerived, l3) \<in> aag 202 \<longrightarrow> (l1, DeleteDerived, l3) \<in> aag) 203 \<and> (\<forall>s r ep. (s, Call, ep) \<in> aag \<and> (r, Receive, ep) \<in> aag \<and> (r, Grant, ep) \<in> aag 204 \<longrightarrow> (s, Control, r) \<in> aag \<and> (r, Control, s) \<in> aag)" 205 206abbreviation pas_wellformed 207where 208 "pas_wellformed aag \<equiv> 209 policy_wellformed (pasPolicy aag) (pasMaySendIrqs aag) (range (pasIRQAbs aag)) (pasSubject aag)" 210 211lemma aag_wellformed_Control: 212 "\<lbrakk> (x, Control, y) \<in> aag; policy_wellformed aag mirqs irqs x \<rbrakk> \<Longrightarrow> x = y" 213 unfolding policy_wellformed_def by metis 214 215lemma aag_wellformed_refl: 216 "\<lbrakk> policy_wellformed aag mirqs irqs x \<rbrakk> \<Longrightarrow> (x, a, x) \<in> aag" 217 unfolding policy_wellformed_def by blast 218 219lemma aag_wellformed_grant_Control_to_recv: 220 "\<lbrakk> (s, Grant, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> 221 \<Longrightarrow> (s, Control, r) \<in> aag" 222 unfolding policy_wellformed_def by blast 223 224lemma aag_wellformed_grant_Control_to_send: 225 "\<lbrakk> (s, Grant, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> 226 \<Longrightarrow> (r, Control, s) \<in> aag" 227 unfolding policy_wellformed_def by blast 228 229lemma aag_wellformed_reply: 230 "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> 231 \<Longrightarrow> (r, Reply, s) \<in> aag" 232 unfolding policy_wellformed_def by blast 233 234lemma aag_wellformed_delete_derived': 235 "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> 236 \<Longrightarrow> (s, DeleteDerived, r) \<in> aag" 237 unfolding policy_wellformed_def by blast 238 239lemma aag_wellformed_delete_derived: 240 "\<lbrakk> (s, Reply, r) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> 241 \<Longrightarrow> (r, DeleteDerived, s) \<in> aag" 242 unfolding policy_wellformed_def by blast 243 244lemma aag_wellformed_delete_derived_trans: 245 "\<lbrakk> (l1, DeleteDerived, l2) \<in> aag; (l2, DeleteDerived, l3) \<in> aag; 246 policy_wellformed aag mirqs irqs l\<rbrakk> 247 \<Longrightarrow> (l1, DeleteDerived, l3) \<in> aag" 248 unfolding policy_wellformed_def by blast 249 250lemma aag_wellformed_call_to_syncsend: 251 "\<lbrakk> (s, Call, ep) \<in> aag; policy_wellformed aag mirqs irqs l\<rbrakk> 252 \<Longrightarrow> (s, SyncSend, ep) \<in> aag" 253 unfolding policy_wellformed_def by blast 254 255lemma aag_wellformed_grant_Control_to_send_by_reply: 256 "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (r, Grant, ep) \<in> aag; 257 policy_wellformed aag mirqs irqs l\<rbrakk> 258 \<Longrightarrow> (r, Control, s) \<in> aag" 259 unfolding policy_wellformed_def by blast 260 261lemma aag_wellformed_grant_Control_to_recv_by_reply: 262 "\<lbrakk> (s, Call, ep) \<in> aag; (r, Receive, ep) \<in> aag; (r, Grant, ep) \<in> aag; 263 policy_wellformed aag mirqs irqs l\<rbrakk> 264 \<Longrightarrow> (s, Control, r) \<in> aag" 265 unfolding policy_wellformed_def by blast 266 267 268subsection \<open>auth_graph_map\<close> 269 270text\<open> 271 272Abstract a graph by relabelling the nodes (agents). Clearly this can 273collapse (and not create) distinctions. 274 275\<close> 276 277definition 278 auth_graph_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a auth_graph \<Rightarrow> 'b auth_graph" 279where 280 "auth_graph_map f aag \<equiv> {(f x, auth, f y) | x auth y. (x, auth, y) \<in> aag}" 281 282lemma auth_graph_map_mem: 283 "(x, auth, y) \<in> auth_graph_map f S 284 = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> (x', auth, y') \<in> S)" 285 by (simp add: auth_graph_map_def) 286 287lemmas auth_graph_map_memD = auth_graph_map_mem[THEN iffD1] 288lemma auth_graph_map_memE: 289 assumes hyp:"(x, auth, y) \<in> auth_graph_map f S" 290 obtains x' and y' where "x = f x'" and "y = f y'" and "(x', auth, y') \<in> S" 291 using hyp[THEN auth_graph_map_mem[THEN iffD1]] by fastforce 292 293lemma auth_graph_map_memI: 294 "\<lbrakk> (x', auth, y') \<in> S; x = f x'; y = f y' \<rbrakk> 295 \<Longrightarrow> (x, auth, y) \<in> auth_graph_map f S" 296 by (fastforce simp add: auth_graph_map_mem) 297 298lemma auth_graph_map_mono: 299 "S \<subseteq> S' \<Longrightarrow> auth_graph_map G S \<subseteq> auth_graph_map G S'" 300 unfolding auth_graph_map_def by auto 301 302 303 304subsection \<open>Transform caps and tcb states into authority\<close> 305 306text\<open> 307 308Abstract the state to an agent authority graph. This definition states 309what authority is conferred by a particular capability to the obj_refs 310in it. 311 312\<close> 313 314definition cap_rights_to_auth :: "cap_rights \<Rightarrow> bool \<Rightarrow> auth set" 315where 316 "cap_rights_to_auth r sync \<equiv> 317 {Reset} 318 \<union> (if AllowRead \<in> r then {Receive} else {}) 319 \<union> (if AllowWrite \<in> r then (if sync then {SyncSend} else {Notify}) else {}) 320 \<union> (if AllowGrant \<in> r then UNIV else {}) 321 \<union> (if AllowGrantReply \<in> r \<and> AllowWrite \<in> r then {Call} else {})" 322 323definition vspace_cap_rights_to_auth :: "cap_rights \<Rightarrow> auth set" 324where 325 "vspace_cap_rights_to_auth r \<equiv> 326 (if AllowWrite \<in> r then {Write} else {}) 327 \<union> (if AllowRead \<in> r then {Read} else {})" 328 329definition reply_cap_rights_to_auth :: "bool \<Rightarrow> cap_rights \<Rightarrow> auth set" 330where 331 "reply_cap_rights_to_auth master r \<equiv> if AllowGrant \<in> r \<or> master then UNIV else {Reply}" 332 333definition cap_auth_conferred :: "cap \<Rightarrow> auth set" 334where 335 "cap_auth_conferred cap \<equiv> 336 case cap of 337 Structures_A.NullCap \<Rightarrow> {} 338 | Structures_A.UntypedCap isdev oref bits freeIndex \<Rightarrow> {Control} 339 | Structures_A.EndpointCap oref badge r \<Rightarrow> 340 cap_rights_to_auth r True 341 | Structures_A.NotificationCap oref badge r \<Rightarrow> 342 cap_rights_to_auth (r - {AllowGrant, AllowGrantReply}) False 343 | Structures_A.ReplyCap oref m r \<Rightarrow> reply_cap_rights_to_auth m r 344 | Structures_A.CNodeCap oref bits guard \<Rightarrow> {Control} 345 | Structures_A.ThreadCap obj_ref \<Rightarrow> {Control} 346 | Structures_A.DomainCap \<Rightarrow> {Control} 347 | Structures_A.IRQControlCap \<Rightarrow> {Control} 348 | Structures_A.IRQHandlerCap irq \<Rightarrow> {Control} 349 | Structures_A.Zombie ptr b n \<Rightarrow> {Control} 350 | Structures_A.ArchObjectCap arch_cap \<Rightarrow> 351 (if is_page_cap (the_arch_cap cap) 352 then vspace_cap_rights_to_auth (acap_rights arch_cap) 353 else {Control})" 354 355fun tcb_st_to_auth :: "Structures_A.thread_state \<Rightarrow> (obj_ref \<times> auth) set" 356where 357 "tcb_st_to_auth (Structures_A.BlockedOnNotification ntfn) = {(ntfn, Receive)}" 358| "tcb_st_to_auth (Structures_A.BlockedOnSend ep payl) 359 = {(ep, SyncSend)} \<union> (if sender_can_grant payl then {(ep, Grant),(ep, Call)} else {}) 360 \<union> (if sender_can_grant_reply payl then {(ep, Call)} else {})" 361| "tcb_st_to_auth (Structures_A.BlockedOnReceive ep payl) 362 = {(ep, Receive)} \<union> (if receiver_can_grant payl then {(ep, Grant)} else {})" 363| "tcb_st_to_auth _ = {}" 364 365subsection \<open>FIXME MOVE\<close> 366 367definition pte_ref 368where 369 "pte_ref pte \<equiv> case pte of 370 SmallPagePTE addr atts rights 371 \<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSmallPage, vspace_cap_rights_to_auth rights) 372 | LargePagePTE addr atts rights 373 \<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMLargePage, vspace_cap_rights_to_auth rights) 374 | _ \<Rightarrow> None" 375 376definition pde_ref2 377where 378 "pde_ref2 pde \<equiv> case pde of 379 SectionPDE addr atts domain rights 380 \<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSection, vspace_cap_rights_to_auth rights) 381 | SuperSectionPDE addr atts rights 382 \<Rightarrow> Some (ptrFromPAddr addr, pageBitsForSize ARMSuperSection, vspace_cap_rights_to_auth rights) 383 | PageTablePDE addr atts domain 384 \<comment> \<open>The 0 is a hack, saying that we own only addr, although 12 would also be OK\<close> 385 \<Rightarrow> Some (ptrFromPAddr addr, 0, {Control}) 386 | _ \<Rightarrow> None" 387 388definition ptr_range 389where 390 "ptr_range p sz \<equiv> {p .. p + 2 ^ sz - 1}" 391 392(* We exclude the global page tables from the authority graph. Alternatively, 393 we could include them and add a wellformedness constraint to policies that 394 requires that every label has the necessary authority to whichever label owns 395 the global page tables, so that when a new page directory is created and 396 references to the global page tables are added to it, no new authority is gained. 397 Note: excluding the references to global page tables in this way 398 brings in some ARM arch-specific VM knowledge here *) 399definition vs_refs_no_global_pts :: "Structures_A.kernel_object \<Rightarrow> (obj_ref \<times> vs_ref \<times> auth) set" 400where 401 "vs_refs_no_global_pts \<equiv> \<lambda>ko. case ko of 402 ArchObj (ASIDPool pool) \<Rightarrow> 403 (\<lambda>(r,p). (p, VSRef (ucast r) (Some AASIDPool), Control)) ` graph_of pool 404 | ArchObj (PageDirectory pd) \<Rightarrow> 405 \<Union>(r,(p, sz, auth)) \<in> graph_of (pde_ref2 o pd) - {(x,y). (ucast (kernel_base >> 20) \<le> x)}. 406 (\<lambda>(p, a). (p, VSRef (ucast r) (Some APageDirectory), a)) ` (ptr_range p sz \<times> auth) 407 | ArchObj (PageTable pt) \<Rightarrow> 408 \<Union>(r,(p, sz, auth)) \<in> graph_of (pte_ref o pt). 409 (\<lambda>(p, a). (p, VSRef (ucast r) (Some APageTable), a)) ` (ptr_range p sz \<times> auth) 410 | _ \<Rightarrow> {}" 411 412subsection \<open>Transferability: Moving caps between agents\<close> 413 414text \<open> 415 Tells if cap can move/be derived between agents without grant 416 due to the inner workings of the system (Calling and replying for now) 417\<close> 418(* FIXME is_transferable should garantee directly that a non-NullCap cap is owned by its CDT 419 parents without using directly the CDT so that we can use it in integrity *) 420inductive is_transferable for opt_cap 421where 422 it_None: "opt_cap = None \<Longrightarrow> is_transferable opt_cap" | 423 it_Null: "opt_cap = Some NullCap \<Longrightarrow> is_transferable opt_cap" | 424 it_Reply: "opt_cap = Some (ReplyCap t False R) \<Longrightarrow> is_transferable opt_cap" 425 426abbreviation "is_transferable_cap cap \<equiv> is_transferable (Some cap)" 427abbreviation "is_transferable_in slot s \<equiv> is_transferable (caps_of_state s slot)" 428 429lemma is_transferable_capE: 430 assumes hyp:"is_transferable_cap cap" 431 obtains "cap = NullCap" | t R where "cap = ReplyCap t False R" 432 by (rule is_transferable.cases[OF hyp]) auto 433 434lemma is_transferable_None[simp]: "is_transferable None" 435 using is_transferable.simps by simp 436lemma is_transferable_Null[simp]: "is_transferable_cap NullCap" 437 using is_transferable.simps by simp 438lemma is_transferable_Reply[simp]: "is_transferable_cap (ReplyCap t False R)" 439 using is_transferable.simps by simp 440 441lemma is_transferable_NoneE: 442 assumes hyp: "is_transferable opt_cap" 443 obtains "opt_cap = None" | cap where "opt_cap = Some cap" and "is_transferable_cap cap" 444 by (rule is_transferable.cases[OF hyp];simp) 445 446lemma is_transferable_Untyped[simp]: "\<not> is_transferable (Some (UntypedCap dev ptr sz freeIndex))" 447 by (blast elim: is_transferable.cases) 448lemma is_transferable_IRQ[simp]: "\<not> is_transferable_cap IRQControlCap" 449 by (blast elim: is_transferable.cases) 450lemma is_transferable_Zombie[simp]: "\<not> is_transferable (Some (Zombie ptr sz n))" 451 by (blast elim: is_transferable.cases) 452lemma is_transferable_Ntfn[simp]: "\<not> is_transferable (Some (NotificationCap ntfn badge R))" 453 by (blast elim: is_transferable.cases) 454lemma is_transferable_Endpoint[simp]: "\<not> is_transferable (Some (EndpointCap ntfn badge R))" 455 by (blast elim: is_transferable.cases) 456 457(*FIXME MOVE *) 458lemmas descendants_incD 459 = descendants_inc_def[THEN meta_eq_to_obj_eq, THEN iffD1, rule_format] 460 461lemma acap_class_reply: 462 "(acap_class acap \<noteq> ReplyClass t)" 463 (* warning: arch split *) 464 by (cases acap; simp) 465 466lemma cap_class_reply: 467 "(cap_class cap = ReplyClass t) = (\<exists>r m. cap = ReplyCap t m r)" 468 by (cases cap; simp add: acap_class_reply) 469 470lemma reply_cap_no_children: 471 "\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk> \<Longrightarrow> cdt s p' \<noteq> Some p" 472 apply (clarsimp simp: valid_mdb_def) 473 apply (frule descendants_incD[where p=p' and p'=p]) 474 apply (rule child_descendant) 475 apply (fastforce) 476 apply clarsimp 477 apply (subgoal_tac "caps_of_state s p' \<noteq> None") 478 apply (clarsimp simp: cap_class_reply) 479 apply (simp only: reply_mdb_def reply_caps_mdb_def reply_masters_mdb_def) 480 apply (elim conjE allE[where x=p']) 481 apply simp 482 apply (drule(1) mdb_cte_atD) 483 apply (fastforce simp add: cte_wp_at_def caps_of_state_def) 484 done 485 486(*FIXME MOVE *) 487lemmas all_childrenI = all_children_def[THEN meta_eq_to_obj_eq, THEN iffD2, rule_format] 488lemmas all_childrenD = all_children_def[THEN meta_eq_to_obj_eq, THEN iffD1, rule_format] 489 490(*FIXME MOVE *) 491lemma valid_mdb_descendants_inc[elim!]: 492 "valid_mdb s \<Longrightarrow> descendants_inc (cdt s) (caps_of_state s)" 493 by (simp add:valid_mdb_def) 494 495(*FIXME MOVE *) 496lemma valid_mdb_mdb_cte_at [elim!]: 497 "valid_mdb s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s)" 498 by (simp add:valid_mdb_def) 499 500(*FIXME MOVE *) 501lemma descendants_inc_cap_classD: 502 "\<lbrakk> descendants_inc m caps; p \<in> descendants_of p' m; caps p = Some cap ; caps p' = Some cap'\<rbrakk> 503 \<Longrightarrow> cap_class cap = cap_class cap'" 504 by (fastforce dest:descendants_incD) 505 506lemma is_transferable_all_children: 507 "valid_mdb s \<Longrightarrow> all_children (\<lambda>slot . is_transferable (caps_of_state s slot)) (cdt s)" 508 apply (rule all_childrenI) 509 apply (erule is_transferable.cases) 510 apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at 511 simp: mdb_cte_at_def cte_wp_at_def caps_of_state_def) 512 apply (fastforce dest: mdb_cte_atD valid_mdb_mdb_cte_at 513 simp: mdb_cte_at_def cte_wp_at_def caps_of_state_def) 514 apply (blast dest:reply_cap_no_children) 515done 516 517 518 519 520subsection \<open>Generating a policy from the current cap, ASID and IRQs distribution\<close> 521 522(* TODO split that section between stba sata and sita and move a maximun 523 of accesor functions back to AInvs *) 524 525 526text \<open> 527 sbta_caps/sbta_asid imply that a thread and it's vspace are labelled 528 the same -- caps_of_state (tcb, vspace_index) will be the PD cap. 529 Thus, a thread is completely managed or completely self-managed. 530 We can (possibly) weaken this by only talking about addressable caps 531 (i.e., only cspace in a tcb). This would also mean that we should use 532 the current cspace for the current label ... a bit strange, though. 533 534 The set of all objects affected by a capability. We cheat a bit and 535 say that a DomainCap contains references to everything, as it 536 intuitively grants its owners that sort of access. This allows us to 537 reuse sbta for DomainCaps. 538 539 The sbta definition is non-inductive. We use the "inductive" 540 construct for convenience, i.e. to get a nice set of intro rules, 541 cases, etc. 542 543\<close> 544 545primrec aobj_ref' :: "arch_cap \<Rightarrow> obj_ref set" 546where 547 "aobj_ref' (arch_cap.ASIDPoolCap p as) = {p}" 548| "aobj_ref' arch_cap.ASIDControlCap = {}" 549| "aobj_ref' (arch_cap.PageCap isdev x rs sz as4) = ptr_range x (pageBitsForSize sz)" 550| "aobj_ref' (arch_cap.PageDirectoryCap x as2) = {x}" 551| "aobj_ref' (arch_cap.PageTableCap x as3) = {x}" 552 553primrec obj_refs :: "cap \<Rightarrow> obj_ref set" 554where 555 "obj_refs cap.NullCap = {}" 556| "obj_refs (cap.ReplyCap r m cr) = {r}" 557| "obj_refs cap.IRQControlCap = {}" 558| "obj_refs (cap.IRQHandlerCap irq) = {}" 559| "obj_refs (cap.UntypedCap d r s f) = {}" 560| "obj_refs (cap.CNodeCap r bits guard) = {r}" 561| "obj_refs (cap.EndpointCap r b cr) = {r}" 562| "obj_refs (cap.NotificationCap r b cr) = {r}" 563| "obj_refs (cap.ThreadCap r) = {r}" 564| "obj_refs (cap.Zombie ptr b n) = {ptr}" 565| "obj_refs (cap.ArchObjectCap x) = aobj_ref' x" 566| "obj_refs cap.DomainCap = UNIV" (* hack, see above *) 567 568inductive_set state_bits_to_policy for caps thread_sts thread_bas cdt vrefs 569where 570 sbta_caps: "\<lbrakk> caps ptr = Some cap; oref \<in> obj_refs cap; 571 auth \<in> cap_auth_conferred cap \<rbrakk> 572 \<Longrightarrow> (fst ptr, auth, oref) \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 573| sbta_untyped: "\<lbrakk> caps ptr = Some cap; oref \<in> untyped_range cap \<rbrakk> 574 \<Longrightarrow> (fst ptr, Control, oref) \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 575| sbta_ts: "\<lbrakk> (oref', auth) \<in> thread_sts oref \<rbrakk> 576 \<Longrightarrow> (oref, auth, oref') \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 577| sbta_bounds: "\<lbrakk>thread_bas oref = Some oref'; auth \<in> {Receive, Reset} \<rbrakk> 578 \<Longrightarrow> (oref, auth, oref') \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 579| sbta_cdt: "\<lbrakk> cdt slot' = Some slot ; \<not>is_transferable (caps slot') \<rbrakk> 580 \<Longrightarrow> (fst slot, Control, fst slot') 581 \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 582| sbta_cdt_transferable: "\<lbrakk>cdt slot' = Some slot\<rbrakk> 583 \<Longrightarrow> (fst slot, DeleteDerived, fst slot') 584 \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 585| sbta_vref: "\<lbrakk> (ptr', ref, auth) \<in> vrefs ptr \<rbrakk> 586 \<Longrightarrow> (ptr, auth, ptr') \<in> state_bits_to_policy caps thread_sts thread_bas cdt vrefs" 587 588fun cap_asid' :: "cap \<Rightarrow> asid set" 589where 590 "cap_asid' (ArchObjectCap (PageCap _ _ _ _ mapping)) 591 = fst ` set_option mapping" 592 | "cap_asid' (ArchObjectCap (PageTableCap _ mapping)) 593 = fst ` set_option mapping" 594 | "cap_asid' (ArchObjectCap (PageDirectoryCap _ asid_opt)) 595 = set_option asid_opt" 596 | "cap_asid' (ArchObjectCap (ASIDPoolCap _ asid)) 597 = {x. asid_high_bits_of x = asid_high_bits_of asid \<and> x \<noteq> 0}" 598 | "cap_asid' (ArchObjectCap ASIDControlCap) = UNIV" 599 | "cap_asid' _ = {}" 600 601inductive_set state_asids_to_policy_aux for aag caps asid_tab vrefs 602where 603 sata_asid: "\<lbrakk> caps ptr = Some cap; asid \<in> cap_asid' cap \<rbrakk> 604 \<Longrightarrow> ( pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) 605 \<in> state_asids_to_policy_aux aag caps asid_tab vrefs" 606 | sata_asid_lookup: "\<lbrakk> asid_tab (asid_high_bits_of asid) = Some poolptr; 607 (pdptr, VSRef (asid && mask asid_low_bits) 608 (Some AASIDPool), a) \<in> vrefs poolptr \<rbrakk> 609 \<Longrightarrow> (pasASIDAbs aag asid, a, pasObjectAbs aag pdptr) 610 \<in> state_asids_to_policy_aux aag caps asid_tab vrefs" 611 | sata_asidpool: "\<lbrakk> asid_tab (asid_high_bits_of asid) = Some poolptr; asid \<noteq> 0 \<rbrakk> \<Longrightarrow> 612 (pasObjectAbs aag poolptr, ASIDPoolMapsASID, pasASIDAbs aag asid) 613 \<in> state_asids_to_policy_aux aag caps asid_tab vrefs" 614 615fun cap_irqs_controlled :: "cap \<Rightarrow> irq set" 616where 617 "cap_irqs_controlled cap.IRQControlCap = UNIV" 618 | "cap_irqs_controlled (cap.IRQHandlerCap irq) = {irq}" 619 | "cap_irqs_controlled _ = {}" 620 621inductive_set state_irqs_to_policy_aux for aag caps 622where 623 sita_controlled: "\<lbrakk> caps ptr = Some cap; irq \<in> cap_irqs_controlled cap \<rbrakk> 624 \<Longrightarrow> (pasObjectAbs aag (fst ptr), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy_aux aag caps" 625 626abbreviation state_irqs_to_policy 627where 628 "state_irqs_to_policy aag s \<equiv> state_irqs_to_policy_aux aag (caps_of_state s)" 629 630definition irq_map_wellformed_aux 631where 632 "irq_map_wellformed_aux aag irqs \<equiv> \<forall>irq. pasObjectAbs aag (irqs irq) = pasIRQAbs aag irq" 633 634abbreviation irq_map_wellformed 635where 636 "irq_map_wellformed aag s \<equiv> irq_map_wellformed_aux aag (interrupt_irq_node s)" 637 638definition state_vrefs 639where 640 "state_vrefs s = case_option {} vs_refs_no_global_pts o kheap s" 641 642abbreviation state_asids_to_policy 643where 644 "state_asids_to_policy aag s \<equiv> state_asids_to_policy_aux aag (caps_of_state s) 645 (arm_asid_table (arch_state s)) (state_vrefs s)" 646 647definition tcb_states_of_state 648where 649 "tcb_states_of_state s \<equiv> \<lambda>p. option_map tcb_state (get_tcb p s)" 650 651(* FIXME: RENAME: should be named something thread_st_auth. thread_states is confusing as 652 it outputs autorities *) 653definition thread_states 654where 655 "thread_states s \<equiv> case_option {} tcb_st_to_auth \<circ> tcb_states_of_state s" 656 657definition thread_bound_ntfns 658where 659 "thread_bound_ntfns s \<equiv> \<lambda>p. case (get_tcb p s) of None \<Rightarrow> None 660 | Some tcb \<Rightarrow> tcb_bound_notification tcb" 661 662definition state_objs_to_policy 663where 664 "state_objs_to_policy s = 665 state_bits_to_policy (caps_of_state s) (thread_states s) (thread_bound_ntfns s) 666 (cdt s) (state_vrefs s)" 667 668lemmas state_objs_to_policy_mem = eqset_imp_iff[OF state_objs_to_policy_def] 669 670lemmas state_objs_to_policy_intros 671 = state_bits_to_policy.intros[THEN state_objs_to_policy_mem[THEN iffD2]] 672 673(* FIXME this is non resilient at all to adding or removing rules to or from state_bits_to_policy *) 674lemmas sta_caps = state_objs_to_policy_intros(1) 675 and sta_untyped = state_objs_to_policy_intros(2) 676 and sta_ts = state_objs_to_policy_intros(3) 677 and sta_bas = state_objs_to_policy_intros(4) 678 and sta_cdt = state_objs_to_policy_intros(5) 679 and sta_cdt_transferable = state_objs_to_policy_intros(6) 680 and sta_vref = state_objs_to_policy_intros(7) 681 682lemmas state_objs_to_policy_cases 683 = state_bits_to_policy.cases[OF state_objs_to_policy_mem[THEN iffD1]] 684 685end 686 687context pspace_update_eq begin 688 689interpretation Arch . (*FIXME: arch_split*) 690 691lemma state_vrefs[iff]: "state_vrefs (f s) = state_vrefs s" 692 by (simp add: state_vrefs_def pspace) 693 694lemma thread_states[iff]: "thread_states (f s) = thread_states s" 695 by (simp add: thread_states_def pspace get_tcb_def swp_def tcb_states_of_state_def) 696 697lemma thread_bound_ntfns[iff]: "thread_bound_ntfns (f s) = thread_bound_ntfns s" 698 by (simp add: thread_bound_ntfns_def pspace get_tcb_def swp_def split: option.splits) 699 700(* 701 lemma ipc_buffers_of_state[iff]: "ipc_buffers_of_state (f s) = ipc_buffers_of_state s" 702 by (simp add: ipc_buffers_of_state_def pspace get_tcb_def swp_def) 703*) 704 705end 706 707context begin interpretation Arch . (*FIXME: arch_split*) 708 709lemma tcb_states_of_state_preserved: 710 "\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk> 711 \<Longrightarrow> tcb_states_of_state (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = tcb_states_of_state s" 712 apply rule 713 apply (auto split: option.splits simp: tcb_states_of_state_def get_tcb_def) 714 done 715 716lemma thread_states_preserved: 717 "\<lbrakk> get_tcb thread s = Some tcb; tcb_state tcb' = tcb_state tcb \<rbrakk> 718 \<Longrightarrow> thread_states (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = thread_states s" 719 by (simp add: tcb_states_of_state_preserved thread_states_def) 720 721lemma thread_bound_ntfns_preserved: 722 "\<lbrakk> get_tcb thread s = Some tcb; tcb_bound_notification tcb' = tcb_bound_notification tcb \<rbrakk> 723 \<Longrightarrow> thread_bound_ntfns (s\<lparr>kheap := kheap s(thread \<mapsto> TCB tcb')\<rparr>) = thread_bound_ntfns s" 724 by (auto simp: thread_bound_ntfns_def get_tcb_def split: option.splits) 725 726(* FIXME: move all three *) 727lemma null_filterI: 728 "\<lbrakk> cs p = Some cap; cap \<noteq> cap.NullCap \<rbrakk> \<Longrightarrow> null_filter cs p = Some cap" 729 unfolding null_filter_def by auto 730lemma null_filterI2: 731 "\<lbrakk> cs p = None \<rbrakk> \<Longrightarrow> null_filter cs p = None" 732 unfolding null_filter_def by auto 733 734lemma null_filterE2: 735 "\<lbrakk> null_filter cps x = None; 736 \<lbrakk> cps x = Some NullCap \<rbrakk> \<Longrightarrow> R ; \<lbrakk> cps x = None \<rbrakk> \<Longrightarrow> R \<rbrakk> 737 \<Longrightarrow> R" 738 by (simp add: null_filter_def split: if_split_asm) 739 740lemma is_transferable_null_filter[simp]: 741 "is_transferable (null_filter caps ptr) = is_transferable (caps ptr)" 742 by (auto simp: is_transferable.simps null_filter_def) 743 744lemma sbta_null_filter: 745 "state_bits_to_policy (null_filter cs) sr bar cd vr = state_bits_to_policy cs sr bar cd vr" 746 apply (rule subset_antisym) 747 apply clarsimp 748 apply (erule state_bits_to_policy.induct, 749 (fastforce intro: state_bits_to_policy.intros 750 elim: null_filterE null_filterE2 split: option.splits)+)[1] 751 apply clarsimp 752 apply (erule state_bits_to_policy.induct) 753 by (fastforce intro: state_bits_to_policy.intros null_filterI split:option.splits)+ 754 755lemma sata_null_filter: 756 "state_asids_to_policy_aux aag (null_filter cs) asid_tab vrefs 757 = state_asids_to_policy_aux aag cs asid_tab vrefs" 758 by (auto elim!: state_asids_to_policy_aux.induct null_filterE 759 intro: state_asids_to_policy_aux.intros sata_asid[OF null_filterI]) 760 761subsection \<open>Policy Refinement\<close> 762 763 764text\<open> 765 766We map scheduler domains to labels. This asserts that the labels on 767tcbs are consistent with the labels on the domains they run in. 768 769We need this to show that the ready queues are not reordered by 770unauthorised subjects (see integrity_ready_queues). 771 772\<close> 773 774inductive_set domains_of_state_aux for ekheap 775where 776 domtcbs: "\<lbrakk> ekheap ptr = Some etcb; d = tcb_domain etcb \<rbrakk> 777 \<Longrightarrow> (ptr, d) \<in> domains_of_state_aux ekheap" 778 779abbreviation domains_of_state 780where 781 "domains_of_state s \<equiv> domains_of_state_aux (ekheap s)" 782 783definition tcb_domain_map_wellformed_aux 784where 785 "tcb_domain_map_wellformed_aux aag etcbs_doms \<equiv> 786 \<forall>(ptr, d) \<in> etcbs_doms. pasObjectAbs aag ptr \<in> pasDomainAbs aag d" 787 788abbreviation tcb_domain_map_wellformed 789where 790 "tcb_domain_map_wellformed aag s \<equiv> tcb_domain_map_wellformed_aux aag (domains_of_state s)" 791 792lemma tcb_domain_map_wellformed_mono: 793 "\<lbrakk> domains_of_state s' \<subseteq> domains_of_state s; tcb_domain_map_wellformed pas s \<rbrakk> \<Longrightarrow> tcb_domain_map_wellformed pas s'" 794by (auto simp: tcb_domain_map_wellformed_aux_def get_etcb_def) 795 796text\<open> 797 798We sometimes need to know that our current subject may run in the current domain. 799 800\<close> 801 802abbreviation 803 "pas_cur_domain aag s \<equiv> pasSubject aag \<in> pasDomainAbs aag (cur_domain s)" 804 805text\<open> 806 807The relation we want to hold between the current state and 808the policy: 809\begin{itemize} 810 811\item The policy should be well-formed. 812 813\item The abstraction of the state should respect the policy. 814 815\end{itemize} 816 817\<close> 818abbreviation state_objs_in_policy :: "'a PAS \<Rightarrow> det_ext state \<Rightarrow> bool" 819where 820 "state_objs_in_policy aag s \<equiv> 821 auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s) \<subseteq> pasPolicy aag" 822 823 824definition pas_refined :: "'a PAS \<Rightarrow> det_ext state \<Rightarrow> bool" 825where 826 "pas_refined aag \<equiv> \<lambda>s. 827 pas_wellformed aag 828 \<and> irq_map_wellformed aag s 829 \<and> tcb_domain_map_wellformed aag s 830 \<and> state_objs_in_policy aag s 831 \<and> state_asids_to_policy aag s \<subseteq> pasPolicy aag 832 \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag" 833 834lemma pas_refined_mem: 835 "\<lbrakk> (x, auth, y) \<in> state_objs_to_policy s; pas_refined aag s \<rbrakk> 836 \<Longrightarrow> (pasObjectAbs aag x, auth, pasObjectAbs aag y) \<in> pasPolicy aag" 837 by (auto simp: pas_refined_def intro: auth_graph_map_memI) 838 839lemma pas_refined_wellformed[elim!]: 840 "pas_refined aag s \<Longrightarrow> pas_wellformed aag" 841 unfolding pas_refined_def by simp 842 843lemmas pas_refined_Control 844 = aag_wellformed_Control[OF _ pas_refined_wellformed] 845 and pas_refined_refl = aag_wellformed_refl [OF pas_refined_wellformed] 846 847lemma caps_of_state_pasObjectAbs_eq: 848 "\<lbrakk> caps_of_state s p = Some cap; Control \<in> cap_auth_conferred cap; 849 is_subject aag (fst p); pas_refined aag s; 850 x \<in> obj_refs cap \<rbrakk> 851 \<Longrightarrow> is_subject aag x" 852 apply (frule sta_caps, simp+) 853 apply (drule pas_refined_mem, simp+) 854 apply (drule pas_refined_Control, simp+) 855 done 856 857lemma pas_refined_state_objs_to_policy_subset: 858 "\<lbrakk> pas_refined aag s; 859 state_objs_to_policy s' \<subseteq> state_objs_to_policy s; 860 state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s; 861 state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s; 862 domains_of_state s' \<subseteq> domains_of_state s; 863 interrupt_irq_node s' = interrupt_irq_node s 864 \<rbrakk> 865 \<Longrightarrow> pas_refined aag s'" 866by (simp add: pas_refined_def) (blast dest: tcb_domain_map_wellformed_mono dest: auth_graph_map_mono[where G="pasObjectAbs aag"]) 867 868lemma aag_wellformed_all_auth_is_owns': 869 "\<lbrakk> Control \<in> S; pas_wellformed aag \<rbrakk> \<Longrightarrow> (\<forall>auth \<in> S. aag_has_auth_to aag auth x) = (is_subject aag x)" 870 apply (rule iffI) 871 apply (drule (1) bspec) 872 apply (frule (1) aag_wellformed_Control ) 873 apply fastforce 874 apply (clarsimp simp: aag_wellformed_refl) 875 done 876 877lemmas aag_wellformed_all_auth_is_owns 878 = aag_wellformed_all_auth_is_owns'[where S=UNIV, simplified] 879 aag_wellformed_all_auth_is_owns'[where S="{Control}", simplified] 880 881lemmas aag_wellformed_control_is_owns 882 = aag_wellformed_all_auth_is_owns'[where S="{Control}", simplified] 883 884lemmas pas_refined_all_auth_is_owns = aag_wellformed_all_auth_is_owns[OF pas_refined_wellformed] 885 886lemma pas_refined_sita_mem: 887 "\<lbrakk> (x, auth, y) \<in> state_irqs_to_policy aag s; pas_refined aag s \<rbrakk> 888 \<Longrightarrow> (x, auth, y) \<in> pasPolicy aag" 889 by (auto simp: pas_refined_def) 890 891 892 893 894section \<open>Integrity definition\<close> 895 896subsection \<open>How kernel objects can change\<close> 897 898fun blocked_on :: "obj_ref \<Rightarrow> Structures_A.thread_state \<Rightarrow> bool" 899where 900 "blocked_on ref (Structures_A.BlockedOnReceive ref' _) = (ref = ref')" 901 | "blocked_on ref (Structures_A.BlockedOnSend ref' _) = (ref = ref')" 902 | "blocked_on ref (Structures_A.BlockedOnNotification ref') = (ref = ref')" 903 | "blocked_on _ _ = False" 904 905lemma blocked_on_def2: 906 "blocked_on ref ts = (ref \<in> fst ` tcb_st_to_auth ts)" 907 by (cases ts, simp_all) 908 909fun receive_blocked_on :: "obj_ref \<Rightarrow> Structures_A.thread_state \<Rightarrow> bool" 910where 911 "receive_blocked_on ref (Structures_A.BlockedOnReceive ref' _) = (ref = ref')" 912 | "receive_blocked_on ref (Structures_A.BlockedOnNotification ref') = (ref = ref')" 913 | "receive_blocked_on _ _ = False" 914 915lemma receive_blocked_on_def2: 916 "receive_blocked_on ref ts = ((ref, Receive) \<in> tcb_st_to_auth ts)" 917 by (cases ts, simp_all) 918 919fun can_receive_ipc :: "Structures_A.thread_state \<Rightarrow> bool" 920where 921 "can_receive_ipc (Structures_A.BlockedOnReceive _ _) = True" 922 | "can_receive_ipc (Structures_A.BlockedOnSend _ pl) = 923 (sender_is_call pl \<and> (sender_can_grant pl \<or> sender_can_grant_reply pl))" 924 | "can_receive_ipc (Structures_A.BlockedOnNotification _) = True" 925 | "can_receive_ipc Structures_A.BlockedOnReply = True" 926 | "can_receive_ipc _ = False" 927 928lemma receive_blocked_on_can_receive_ipc[elim!,simp]: 929 "receive_blocked_on ref ts \<Longrightarrow>can_receive_ipc ts" 930 by (cases ts;simp) 931 932lemma receive_blocked_on_can_receive_ipc'[elim!,simp]: 933 "case_option False (receive_blocked_on ref) tsopt \<Longrightarrow> case_option False can_receive_ipc tsopt" 934 by (cases tsopt;simp) 935 936 937fun send_blocked_on :: "obj_ref \<Rightarrow> Structures_A.thread_state \<Rightarrow> bool" 938where 939 "send_blocked_on ref (Structures_A.BlockedOnSend ref' _) = (ref = ref')" 940 | "send_blocked_on _ _ = False" 941 942lemma send_blocked_on_def2: 943 "send_blocked_on ref ts = ((ref, SyncSend) \<in> tcb_st_to_auth ts)" 944 by (cases ts, simp_all) 945 946lemma send_blocked_on_def3: 947 "send_blocked_on ref ts = (\<exists> pl. ts = BlockedOnSend ref pl)" 948 by (cases ts; force) 949 950fun send_is_call :: "Structures_A.thread_state \<Rightarrow> bool" 951where 952 "send_is_call (Structures_A.BlockedOnSend _ payl) = sender_is_call payl" 953| "send_is_call _ = False" 954 955 956 957definition tcb_bound_notification_reset_integrity 958 :: "obj_ref option \<Rightarrow> obj_ref option \<Rightarrow> 'a set \<Rightarrow> 'a PAS \<Rightarrow> bool" 959where 960 "tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag 961 = ((ntfn = ntfn') \<comment> \<open>no change to bound ntfn\<close> 962 \<or> (ntfn' = None \<and> aag_subjects_have_auth_to subjects aag Reset (the ntfn)) 963 \<comment> \<open>ntfn is unbound\<close>)" 964 965lemma tcb_bound_notification_reset_integrity_refl[simp]: 966 "tcb_bound_notification_reset_integrity ntfn ntfn subjects aag" 967 by (simp add: tcb_bound_notification_reset_integrity_def) 968 969 970definition direct_send :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> obj_ref \<Rightarrow> tcb \<Rightarrow> bool" 971where 972 "direct_send subjects aag ep tcb \<equiv> receive_blocked_on ep (tcb_state tcb) \<and> 973 (aag_subjects_have_auth_to subjects aag SyncSend ep 974 \<or> aag_subjects_have_auth_to subjects aag Notify ep)" 975 976abbreviation ep_recv_blocked :: "obj_ref \<Rightarrow> thread_state \<Rightarrow> bool" 977where 978 "ep_recv_blocked ep ts \<equiv> case ts of BlockedOnReceive w _ \<Rightarrow> w = ep 979 | _ \<Rightarrow> False" 980 981definition direct_call :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> obj_ref \<Rightarrow> thread_state \<Rightarrow> bool" 982where 983 "direct_call subjects aag ep tcbst \<equiv> ep_recv_blocked ep (tcbst) \<and> 984 aag_subjects_have_auth_to subjects aag Call ep" 985 986definition indirect_send :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> tcb \<Rightarrow> bool" 987where 988 "indirect_send subjects aag ntfn recv_ep tcb \<equiv> ep_recv_blocked recv_ep (tcb_state tcb) 989 \<comment> \<open>tcb is blocked on sync ep\<close> 990 \<and> (tcb_bound_notification tcb = Some ntfn) 991 \<and> aag_subjects_have_auth_to subjects aag Notify ntfn" 992 993 994definition call_blocked :: "obj_ref \<Rightarrow> thread_state \<Rightarrow> bool" 995where 996 "call_blocked ep tst \<equiv> \<exists> pl. tst = BlockedOnSend ep pl \<and> sender_is_call pl" 997 998definition allowed_call_blocked :: "obj_ref \<Rightarrow> thread_state \<Rightarrow> bool" 999where 1000 "allowed_call_blocked ep tst \<equiv> \<exists> pl. tst = BlockedOnSend ep pl \<and> sender_is_call pl \<and> 1001 (sender_can_grant pl \<or> sender_can_grant_reply pl)" 1002 1003lemma allowed_call_blocked_call_blocked[elim!]: 1004 "allowed_call_blocked ep tst \<Longrightarrow> call_blocked ep tst" 1005 unfolding allowed_call_blocked_def call_blocked_def by fastforce 1006 1007definition direct_reply :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> 'a \<Rightarrow> tcb \<Rightarrow> bool" 1008where 1009 "direct_reply subjects aag tcb_owner tcb \<equiv> 1010 (awaiting_reply (tcb_state tcb) 1011 \<or> (\<exists>ep. allowed_call_blocked ep (tcb_state tcb) 1012 \<and> aag_subjects_have_auth_to subjects aag Receive ep)) 1013 \<and> aag_subjects_have_auth_to_label subjects aag Reply tcb_owner" 1014 1015definition reply_cap_deletion_integrity :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool" 1016where 1017 "reply_cap_deletion_integrity subjects aag cap cap' \<equiv> 1018 (cap = cap') \<or> (\<exists> caller R. cap = ReplyCap caller False R \<and> 1019 cap' = NullCap \<and> 1020 pasObjectAbs aag caller \<in> subjects)" 1021 1022lemmas reply_cap_deletion_integrityI1 = 1023 reply_cap_deletion_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2,OF disjI1] 1024lemmas reply_cap_deletion_integrityI2 = 1025 reply_cap_deletion_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2, OF disjI2, OF exI, 1026 OF exI, OF conjI [OF _ conjI], rule_format] 1027lemmas reply_cap_deletion_integrity_intros = 1028 reply_cap_deletion_integrityI1 reply_cap_deletion_integrityI2 1029 1030lemma reply_cap_deletion_integrityE: 1031 assumes hyp:"reply_cap_deletion_integrity subjects aag cap cap'" 1032 obtains "cap = cap'" | caller R where "cap = ReplyCap caller False R" 1033 and "cap' = NullCap" and "pasObjectAbs aag caller \<in> subjects" 1034 using hyp reply_cap_deletion_integrity_def by blast 1035 1036lemma reply_cap_deletion_integrity_refl[simp]: 1037 "reply_cap_deletion_integrity subjects aag cap cap" 1038 by (rule reply_cap_deletion_integrityI1) simp 1039 1040 1041(* WARNING if some one want to add a cap to is_transferable, it must appear here *) 1042definition cnode_integrity :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> cnode_contents \<Rightarrow> cnode_contents \<Rightarrow> bool" 1043 where 1044 "cnode_integrity subjects aag content content' \<equiv> 1045 \<forall> l. content l = content' l \<or> (\<exists> cap cap'. content l = Some cap \<and> content' l = Some cap' \<and> 1046 reply_cap_deletion_integrity subjects aag cap cap')" 1047 1048lemmas cnode_integrityI = cnode_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD2,rule_format] 1049lemmas cnode_integrityD = cnode_integrity_def[THEN meta_eq_to_obj_eq,THEN iffD1,rule_format] 1050lemma cnode_integrityE: 1051 assumes hyp:"cnode_integrity subjects aag content content'" 1052 obtains "content l = content' l" | cap cap' where "content l = Some cap" 1053 and "content' l = Some cap'" and "reply_cap_deletion_integrity subjects aag cap cap'" 1054 using hyp cnode_integrityD by blast 1055 1056definition asid_pool_integrity :: 1057 "'a set \<Rightarrow> 'a PAS \<Rightarrow> (10 word \<rightharpoonup> obj_ref) \<Rightarrow> (10 word \<rightharpoonup> obj_ref) \<Rightarrow> bool" 1058 where 1059 "asid_pool_integrity subjects aag pool pool' \<equiv> 1060 \<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None 1061 \<and> aag_subjects_have_auth_to subjects aag Control (the (pool x))" 1062 1063 1064subsubsection \<open>Definition of object integrity\<close> 1065text \<open> 1066 The object integrity relation describes which modification to kernel objects are allowed by the 1067 policy aag when the system is controlled by subjects. 1068 1069 ko and ko' are the initial and final version of the particular kernel object 1070 on which we are reasoning. 1071 The corresponding memory emplacement must belong to l. 1072 1073 The activate boolean allows reactivation of a thread in a @{term Restart} state. 1074 1075 Creation and destruction or retyping of kernel objects are not allowed unless l \<in> subjects 1076\<close> 1077(* FIXME it would be nice if there was an arch_tcb_context_update with all the required lemmas*) 1078inductive integrity_obj_atomic for aag activate subjects l ko ko' 1079 where 1080 (* l can modify any object it owns *) 1081 troa_lrefl: 1082 "\<lbrakk>l \<in> subjects \<rbrakk> \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1083 (* l can modify an Notification object state if it has rights to interact with it *) 1084| troa_ntfn: 1085 "\<lbrakk>ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); 1086 auth \<in> {Receive, Notify, Reset}; s \<in> subjects; 1087 (s, auth, l) \<in> pasPolicy aag\<rbrakk> 1088 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1089 (* l can modify an Endpoint object state if it has rights to interact with it *) 1090| troa_ep: 1091 "\<lbrakk> ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); 1092 auth \<in> {Receive, SyncSend, Reset}; s \<in> subjects; 1093 (s, auth, l) \<in> pasPolicy aag\<rbrakk> 1094 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1095 (* If a tcb is waiting on receiving on an Endpoint but could be bound to a notification ntfn. 1096 Then if we can Notify ntfn, we could modify the endpoint *) 1097| troa_ep_unblock: 1098 "\<lbrakk>ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); 1099 (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag; 1100 (tcb, Receive, l) \<in> pasPolicy aag; 1101 aag_subjects_have_auth_to subjects aag Notify ntfn\<rbrakk> 1102 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1103 (* If the subjects can send to an Endpoint or its bound notification, they can also 1104 modify any thread that is waiting on it *) 1105| troa_tcb_send: 1106 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1107 tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running\<rparr>; 1108 direct_send subjects aag ep tcb 1109 \<or> indirect_send subjects aag (the (tcb_bound_notification tcb)) ep tcb\<rbrakk> 1110 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1111 (* If a tcb is waiting on an Endpoint that the subjects can Call, they are allowed 1112 to do that call, and insert a ReplyCap back towards a subject*) 1113| troa_tcb_call: 1114 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1115 tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), tcb_state := Running, 1116 tcb_caller := ReplyCap caller False R\<rparr>; 1117 pasObjectAbs aag caller \<in> subjects; 1118 direct_call subjects aag ep (tcb_state tcb)\<rbrakk> 1119 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1120 (* Subjects can reply to a tcb waiting for a Reply, if they have authority to do that Reply 1121 In case of a fault Reply, the new state of the thread can be Restart or Inactive depending on 1122 the fault handler*) 1123| troa_tcb_reply: 1124 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1125 tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1126 tcb_state := new_st, tcb_fault := None\<rparr>; 1127 new_st = Running \<or> (tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> new_st = Inactive)); 1128 awaiting_reply (tcb_state tcb); 1129 aag_subjects_have_auth_to_label subjects aag Reply l\<rbrakk> 1130 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1131 (* Subjects can receive a message from an Endpoint. The sender state will then be set to 1132 Running if it is a normal send and to Inactive or BlockedOnReply if it is a call. 1133 TODO split that rule *) 1134| troa_tcb_receive: 1135 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1136 tcb' = tcb \<lparr>tcb_state := new_st\<rparr>; 1137 new_st = Running 1138 \<or> (inactive new_st \<and> call_blocked ep (tcb_state tcb)) 1139 \<or> (awaiting_reply new_st \<and> allowed_call_blocked ep (tcb_state tcb)); 1140 send_blocked_on ep (tcb_state tcb); 1141 aag_subjects_have_auth_to subjects aag Receive ep \<rbrakk> 1142 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1143 (* Subjects can Reset an Endpoint/Notification they have Reset authority to, and thus 1144 all TCBs blocked on it need to be restarted *) 1145| troa_tcb_restart: 1146 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1147 tcb' = tcb\<lparr>tcb_state := Restart\<rparr>; 1148 blocked_on ep (tcb_state tcb); 1149 aag_subjects_have_auth_to subjects aag Reset ep\<rbrakk> 1150 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1151 (* Subjects can Reset a bound Notification which then need to be unbound*) 1152| troa_tcb_unbind: 1153 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1154 tcb' = tcb\<lparr>tcb_bound_notification := None\<rparr>; 1155 aag_subjects_have_auth_to subjects aag Reset (the (tcb_bound_notification tcb))\<rbrakk> 1156 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1157 (* Allow subjects to delete their reply caps in other subjects' threads. 1158 * Note that we need to account for the reply cap being in tcb_ctable, 1159 * because recursive deletion of the root CNode may temporarily place any 1160 * contained cap (in particular, a copied reply cap) in that location. *) 1161| troa_tcb_empty_ctable: 1162 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1163 tcb' = tcb\<lparr>tcb_ctable := cap'\<rparr>; 1164 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) cap'\<rbrakk> 1165 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1166| troa_tcb_empty_caller: 1167 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1168 tcb' = tcb\<lparr>tcb_caller := cap'\<rparr>; 1169 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'\<rbrakk> 1170 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1171 (* If the activate flag is on, any thread in Restart state can be restarted *) 1172| troa_tcb_activate: 1173 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1174 tcb' = tcb\<lparr>tcb_arch := arch_tcb_context_set 1175 ((arch_tcb_context_get (tcb_arch tcb))(NextIP := 1176 (arch_tcb_context_get (tcb_arch tcb)) FaultIP) 1177 ) (tcb_arch tcb), 1178 tcb_state := Running\<rparr>; 1179 tcb_state tcb = Restart; 1180 activate\<rbrakk> \<comment> \<open>Anyone can do this\<close> 1181 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1182 (* Subjects can clear ASIDs that they control *) 1183| troa_asidpool_clear: 1184 "\<lbrakk>ko = Some (ArchObj (ASIDPool pool)); ko' = Some (ArchObj (ASIDPool pool')); 1185 asid_pool_integrity subjects aag pool pool' \<rbrakk> 1186 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1187 (* If there is a deletable_cap in a CNode, it must be allowed to be deleted *) 1188| troa_cnode: 1189 "\<lbrakk>ko = Some (CNode n content); ko' = Some (CNode n content'); 1190 cnode_integrity subjects aag content content' \<rbrakk> 1191 \<Longrightarrow> integrity_obj_atomic aag activate subjects l ko ko'" 1192 1193definition integrity_obj 1194 where 1195 "integrity_obj aag activate subjects l \<equiv> (integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>*" 1196 1197subsubsection \<open>Introduction rules for object integrity\<close> 1198 1199lemma troa_tro: 1200 "integrity_obj_atomic aag activate subjects l ko ko' 1201 \<Longrightarrow> integrity_obj aag activate subjects l ko ko'" 1202 unfolding integrity_obj_def by (rule r_into_rtranclp) 1203 1204lemmas tro_lrefl = troa_lrefl[THEN troa_tro] 1205lemma tro_orefl: 1206 "\<lbrakk> ko = ko' \<rbrakk> \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" 1207 unfolding integrity_obj_def by simp 1208lemmas tro_ntfn = troa_ntfn[THEN troa_tro] 1209lemmas tro_ep = troa_ep[THEN troa_tro] 1210lemmas tro_ep_unblock = troa_ep_unblock[THEN troa_tro] 1211lemmas tro_tcb_send = troa_tcb_send[THEN troa_tro] 1212lemmas tro_tcb_call = troa_tcb_call[THEN troa_tro] 1213lemmas tro_tcb_reply = troa_tcb_reply[THEN troa_tro] 1214lemmas tro_tcb_receive = troa_tcb_receive[THEN troa_tro] 1215lemmas tro_tcb_restart = troa_tcb_restart[THEN troa_tro] 1216lemmas tro_tcb_unbind = troa_tcb_unbind[THEN troa_tro] 1217lemmas tro_tcb_empty_ctable = troa_tcb_empty_ctable[THEN troa_tro] 1218lemmas tro_tcb_empty_caller = troa_tcb_empty_caller[THEN troa_tro] 1219lemmas tro_tcb_activate = troa_tcb_activate[THEN troa_tro] 1220lemmas tro_asidpool_clear = troa_asidpool_clear[THEN troa_tro] 1221lemmas tro_cnode = troa_cnode[THEN troa_tro] 1222 1223lemmas tro_intros = tro_lrefl tro_orefl tro_ntfn tro_ep tro_ep_unblock tro_tcb_send tro_tcb_call 1224 tro_tcb_reply tro_tcb_receive tro_tcb_restart tro_tcb_unbind tro_tcb_empty_ctable 1225 tro_tcb_empty_caller tro_tcb_activate tro_asidpool_clear tro_cnode 1226 1227lemma tro_tcb_unbind': 1228 "\<lbrakk> ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1229 tcb' = tcb\<lparr>tcb_bound_notification := ntfn'\<rparr>; 1230 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag\<rbrakk> 1231 \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" 1232 apply (clarsimp simp:tcb_bound_notification_reset_integrity_def) 1233 apply (elim disjE) 1234 apply (rule tro_orefl;fastforce) 1235 apply (rule tro_tcb_unbind;fastforce) 1236 done 1237 1238lemmas rtranclp_transp[intro!] = transp_rtranclp 1239 1240lemma tro_transp[intro!]: 1241 "transp (integrity_obj aag activate es subjects)" 1242 unfolding integrity_obj_def by simp 1243 1244lemmas tro_trans_spec = tro_transp[THEN transpD] 1245 1246lemma tro_tcb_generic': 1247 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1248 tcb' = tcb \<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; 1249 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag ; 1250 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1251 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap' \<rbrakk> 1252 \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" 1253 apply clarsimp 1254 apply (rule tro_trans_spec) 1255 apply (rule tro_tcb_empty_caller[OF refl refl refl];simp) 1256 apply (rule tro_trans_spec) 1257 apply (rule tro_tcb_empty_ctable[OF refl refl refl];simp) 1258 apply (rule tro_trans_spec) 1259 apply (rule tro_tcb_unbind'[OF refl refl refl];simp) 1260 apply (fastforce intro!: tro_orefl tcb.equality) 1261 done 1262 1263lemma tro_tcb_reply': 1264 "\<lbrakk>ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1265 tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1266 tcb_state := new_st, tcb_fault := None\<rparr>; 1267 new_st = Running \<or> (tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> new_st = Inactive)); 1268 direct_reply subjects aag l' tcb \<rbrakk> 1269 \<Longrightarrow> integrity_obj aag activate subjects l' ko ko'" 1270 apply (clarsimp simp:direct_reply_def simp del:not_None_eq) 1271 apply (erule disjE, (rule tro_tcb_reply[OF refl refl], force; force)) (* Warning: schematics *) 1272 apply (clarsimp simp del:not_None_eq) 1273 apply (rule tro_trans_spec) 1274 apply (frule allowed_call_blocked_def[THEN meta_eq_to_obj_eq,THEN iffD1],clarsimp) 1275 apply (rule tro_tcb_receive[OF refl refl refl, where new_st=BlockedOnReply];force) 1276 apply (rule tro_trans_spec) 1277 apply (rule tro_tcb_reply[OF refl refl refl, where new_st=new_st];force) 1278 by (fastforce intro!: tro_orefl tcb.equality) 1279 1280abbreviation integrity_obj_state 1281where 1282 "integrity_obj_state aag activate subjects s s' \<equiv> 1283 (\<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x))" 1284 1285 1286 1287subsubsection \<open>Alternative tagged formulation of object integrity\<close> 1288 1289datatype Tro_rules = LRefl | ORefl | RNtfn | REp | EpUnblock | TCBSend | TCBCall | 1290 TCBReply | TCBReceive | TCBRestart | TCBGeneric | RASID | TCBActivate | RCNode 1291 1292definition tro_tag :: "Tro_rules \<Rightarrow> bool" 1293where 1294 "tro_tag t \<equiv> True" 1295 1296(* do not put that one in the simpset unless you know what you are doing *) 1297lemma tro_tagI[intro!]: 1298 "tro_tag t" 1299 unfolding tro_tag_def .. 1300 1301definition tro_tag' :: "Tro_rules \<Rightarrow> bool" 1302where 1303 "tro_tag' t \<equiv> True" 1304 1305(* do not put that one in the simpset unless you know what you are doing *) 1306lemma tro_tag'_intro[intro!]: 1307 "tro_tag' t" 1308 unfolding tro_tag'_def .. 1309 1310lemma tro_tag_to_prime: 1311 "tro_tag t = tro_tag' t" 1312 unfolding tro_tag_def tro_tag'_def by simp 1313 1314 1315text \<open> 1316 This is the old definition of @{const integrity_obj}, corresponding 1317 to @{const integrity_obj_atomic} but with certain atomic steps 1318 combined (notably TCB updates). 1319 1320 We keep this here because it is used by many of the existing proofs, 1321 and having common combinations of steps is sometimes useful. 1322 1323 The @{const tro_tag}s are used to tag each rule, for use in the 1324 transitivity proof. The transitivity property is, in turn, needed to 1325 prove that these steps are included in @{const integrity_obj} 1326 (which is the transitive closure of @{const integrity_obj_atomic}). 1327 1328 NB: we do not try to prove the converse, i.e. integrity_obj_alt 1329 implying @{const integrity_obj}. It is not quite true, and we 1330 do not need it in any case. 1331\<close> 1332inductive integrity_obj_alt for aag activate subjects l' ko ko' 1333where 1334 tro_alt_lrefl: 1335 "\<lbrakk> tro_tag LRefl ; l' \<in> subjects \<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1336| tro_alt_orefl: 1337 "\<lbrakk> tro_tag ORefl; ko = ko' \<rbrakk> \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1338| tro_alt_ntfn: 1339 "\<lbrakk>tro_tag RNtfn; ko = Some (Notification ntfn); ko' = Some (Notification ntfn'); 1340 auth \<in> {Receive, Notify, Reset}; 1341 \<exists>s \<in> subjects. (s, auth, l') \<in> pasPolicy aag \<rbrakk> 1342 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1343| tro_alt_ep: 1344 "\<lbrakk>tro_tag REp; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); 1345 auth \<in> {Receive, SyncSend, Reset}; 1346 (\<exists>s \<in> subjects. (s, auth, l') \<in> pasPolicy aag) \<rbrakk> 1347 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1348| tro_alt_ep_unblock: 1349 "\<lbrakk>tro_tag EpUnblock; ko = Some (Endpoint ep); ko' = Some (Endpoint ep'); 1350 \<exists>tcb ntfn. (tcb, Receive, pasObjectAbs aag ntfn) \<in> pasPolicy aag \<and> 1351 (tcb, Receive, l') \<in> pasPolicy aag \<and> 1352 aag_subjects_have_auth_to subjects aag Notify ntfn \<rbrakk> 1353 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1354 1355| tro_alt_tcb_send: 1356 "\<lbrakk>tro_tag TCBSend; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1357 \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1358 tcb_state := Running, 1359 tcb_bound_notification := ntfn', tcb_caller := cap', 1360 tcb_ctable := ccap'\<rparr>; 1361 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; 1362 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1363 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; 1364 direct_send subjects aag ep tcb \<or> indirect_send subjects aag (the (tcb_bound_notification tcb)) ep tcb \<rbrakk> 1365 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1366| tro_alt_tcb_call: 1367 "\<lbrakk>tro_tag TCBCall; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1368 \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1369 tcb_state := Running, 1370 tcb_bound_notification := ntfn', tcb_caller := cap', 1371 tcb_ctable := ccap'\<rparr>; 1372 pasObjectAbs aag caller \<in> subjects; 1373 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; 1374 reply_cap_deletion_integrity subjects aag (ReplyCap caller False R) cap'; 1375 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; 1376 direct_call subjects aag ep (tcb_state tcb) \<rbrakk> 1377 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1378| tro_alt_tcb_reply: 1379 "\<lbrakk>tro_tag TCBReply; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1380 \<exists>ctxt'. tcb' = tcb \<lparr>tcb_arch := arch_tcb_context_set ctxt' (tcb_arch tcb), 1381 tcb_state := new_st, tcb_fault := None, 1382 tcb_bound_notification := ntfn', tcb_caller := cap', 1383 tcb_ctable := ccap'\<rparr>; 1384 new_st = Running \<or> (tcb_fault tcb \<noteq> None \<and> (new_st = Restart \<or> new_st = Inactive)); 1385 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; 1386 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1387 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; 1388 direct_reply subjects aag l' tcb \<rbrakk> 1389 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1390| tro_alt_tcb_receive: 1391 "\<lbrakk>tro_tag TCBReceive; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1392 tcb' = tcb \<lparr>tcb_state := new_st, tcb_bound_notification := ntfn', tcb_caller := cap', 1393 tcb_ctable := ccap'\<rparr>; 1394 new_st = Running \<or> (((new_st = Inactive \<and> call_blocked ep (tcb_state tcb)) \<or> (new_st = BlockedOnReply \<and> (allowed_call_blocked ep (tcb_state tcb))))); 1395 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; 1396 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1397 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; 1398 send_blocked_on ep (tcb_state tcb); 1399 aag_subjects_have_auth_to subjects aag Receive ep \<rbrakk> 1400 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1401| tro_alt_tcb_restart: 1402 "\<lbrakk>tro_tag TCBRestart; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1403 tcb' = tcb\<lparr> tcb_arch := arch_tcb_context_set 1404 (arch_tcb_context_get (tcb_arch tcb')) (tcb_arch tcb), 1405 tcb_state := tcb_state tcb', tcb_bound_notification := ntfn', 1406 tcb_caller := cap',tcb_ctable := ccap'\<rparr>; 1407 (tcb_state tcb' = Restart \<and> 1408 arch_tcb_context_get (tcb_arch tcb') = arch_tcb_context_get (tcb_arch tcb)) \<or> 1409 (tcb_state tcb' = Running \<and> 1410 arch_tcb_context_get (tcb_arch tcb') 1411 = (arch_tcb_context_get (tcb_arch tcb)) 1412 (NextIP := arch_tcb_context_get (tcb_arch tcb) FaultIP)); 1413 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; 1414 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1415 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; 1416 blocked_on ep (tcb_state tcb); 1417 aag_subjects_have_auth_to subjects aag Reset ep \<rbrakk> 1418 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1419| tro_alt_tcb_generic: 1420 "\<lbrakk>tro_tag TCBGeneric; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1421 tcb' = tcb \<lparr>tcb_bound_notification := ntfn', tcb_caller := cap', tcb_ctable := ccap'\<rparr>; 1422 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag ; 1423 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1424 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap' \<rbrakk> 1425 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1426| tro_alt_asidpool_clear: 1427 "\<lbrakk>tro_tag RASID; ko = Some (ArchObj (ASIDPool pool)); ko' = Some (ArchObj (ASIDPool pool')); 1428 asid_pool_integrity subjects aag pool pool'\<rbrakk> 1429 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1430| tro_alt_tcb_activate: 1431 "\<lbrakk>tro_tag TCBActivate; ko = Some (TCB tcb); ko' = Some (TCB tcb'); 1432 tcb' = tcb \<lparr> tcb_arch := arch_tcb_context_set 1433 ((arch_tcb_context_get (tcb_arch tcb))(NextIP := 1434 (arch_tcb_context_get (tcb_arch tcb)) FaultIP) 1435 ) (tcb_arch tcb), 1436 tcb_caller := cap', tcb_ctable := ccap', 1437 tcb_state := Running, tcb_bound_notification := ntfn'\<rparr>; 1438 tcb_state tcb = Restart; 1439 reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap'; 1440 reply_cap_deletion_integrity subjects aag (tcb_ctable tcb) ccap'; 1441 tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag; 1442 activate \<rbrakk> \<comment> \<open>Anyone can do this\<close> 1443 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1444| tro_alt_cnode: 1445 "\<lbrakk>tro_tag RCNode; ko = Some (CNode n content); ko' = Some (CNode n content'); 1446 cnode_integrity subjects aag content content' \<rbrakk> 1447 \<Longrightarrow> integrity_obj_alt aag activate subjects l' ko ko'" 1448 1449lemmas disj_cong' = arg_cong2[where f="(\<or>)"] 1450 1451 1452lemma troa_tro_alt[elim!]: 1453 "integrity_obj_atomic aag activate subjects l ko ko' 1454 \<Longrightarrow> integrity_obj_alt aag activate subjects l ko ko'" 1455 apply (erule integrity_obj_atomic.cases) 1456 1457 text \<open>Single out TCB cases for special handling. We manually simplify 1458 the TCB updates in the tro_alt rules using @{thm tcb.equality}.\<close> 1459 (* somewhat slow 10s *) 1460 apply (find_goal \<open>match premises in "ko = Some (TCB _)" \<Rightarrow> succeed\<close>, 1461 ((erule(1) integrity_obj_alt.intros[OF tro_tagI], 1462 (intro exI tcb.equality; solves \<open>simp\<close>)); 1463 fastforce simp: reply_cap_deletion_integrity_def 1464 tcb_bound_notification_reset_integrity_def 1465 direct_reply_def))+ 1466 1467 text \<open>Remaining cases.\<close> 1468 apply (fastforce intro: integrity_obj_alt.intros[OF tro_tagI])+ 1469 done 1470 1471 1472 1473subsubsection \<open>ekheap and ready queues\<close> 1474 1475text\<open> 1476 1477 Assume two subjects can't interact. Then AINVS already implies that 1478 the ready queues of one won't change when the other is running. 1479 1480 Assume two subjects can interact via an endpoint. (Probably an 1481 notification object for infoflow purposes.) Then the following says 1482 that the ready queues for the non-running subject can be extended by 1483 the running subject, e.g. by sending a message. Note these threads are 1484 added to the start of the queue. 1485 1486\<close> 1487 1488definition integrity_ready_queues 1489where 1490 "integrity_ready_queues aag subjects queue_labels rq rq' \<equiv> 1491 pasMayEditReadyQueues aag \<or> (queue_labels \<inter> subjects = {} \<longrightarrow> (\<exists>threads. threads @ rq = rq'))" 1492 1493lemma integrity_ready_queues_refl[simp]: "integrity_ready_queues aag subjects ptr s s" 1494unfolding integrity_ready_queues_def by simp 1495 1496inductive integrity_eobj for aag subjects l' eko eko' 1497where 1498 tre_lrefl: "\<lbrakk> l' \<in> subjects \<rbrakk> \<Longrightarrow> integrity_eobj aag subjects l' eko eko'" 1499| tre_orefl: "\<lbrakk> eko = eko' \<rbrakk> \<Longrightarrow> integrity_eobj aag subjects l' eko eko'" 1500 1501subsubsection \<open>generic stuff : FIXME MOVE\<close> 1502 1503lemma integrity_obj_activate: 1504 "integrity_obj aag False subjects l' ko ko' \<Longrightarrow> 1505 integrity_obj aag activate subjects l' ko ko'" 1506 unfolding integrity_obj_def 1507 apply (erule rtranclp_mono[THEN predicate2D, rotated]) 1508 apply (rule predicate2I) 1509 by (erule integrity_obj_atomic.cases; (intro integrity_obj_atomic.intros; assumption | simp)) 1510 1511abbreviation object_integrity 1512where 1513 "object_integrity aag \<equiv> integrity_obj (aag :: 'a PAS) (pasMayActivate aag) {pasSubject aag}" 1514 1515 1516subsection \<open>auth_ipc_buffer\<close> 1517 1518definition auth_ipc_buffers :: "'z::state_ext state \<Rightarrow> word32 \<Rightarrow> word32 set" 1519where 1520 "auth_ipc_buffers s \<equiv> 1521 \<lambda>p. case (get_tcb p s) of 1522 None \<Rightarrow> {} 1523 | Some tcb \<Rightarrow> 1524 (case tcb_ipcframe tcb of 1525 cap.ArchObjectCap (arch_cap.PageCap False p' R vms _) \<Rightarrow> 1526 if AllowWrite \<in> R 1527 then (ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) 1528 msg_align_bits) 1529 else {} 1530 | _ \<Rightarrow> {})" 1531 1532(* MOVE *) 1533lemma caps_of_state_tcb': 1534 "\<lbrakk> get_tcb p s = Some tcb; option_map fst (tcb_cap_cases idx) = Some getF \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some (getF tcb)" 1535 apply (drule get_tcb_SomeD) 1536 apply clarsimp 1537 apply (drule (1) cte_wp_at_tcbI [where t = "(p, idx)" and P = "(=) (getF tcb)", simplified]) 1538 apply simp 1539 apply (clarsimp simp: cte_wp_at_caps_of_state) 1540 done 1541 1542(* MOVE *) 1543lemma caps_of_state_tcb_cap_cases: 1544 "\<lbrakk> get_tcb p s = Some tcb; idx \<in> dom tcb_cap_cases \<rbrakk> \<Longrightarrow> caps_of_state s (p, idx) = Some ((the (option_map fst (tcb_cap_cases idx))) tcb)" 1545 apply (clarsimp simp: dom_def) 1546 apply (erule caps_of_state_tcb') 1547 apply simp 1548 done 1549 1550lemma auth_ipc_buffers_member_def: 1551 "x \<in> auth_ipc_buffers s p = 1552 (\<exists>tcb p' R vms xx. get_tcb p s = Some tcb 1553 \<and> tcb_ipcframe tcb = (cap.ArchObjectCap (arch_cap.PageCap False p' R vms xx)) 1554 \<and> caps_of_state s (p, tcb_cnode_index 4) = 1555 Some (cap.ArchObjectCap (arch_cap.PageCap False p' R vms xx)) 1556 \<and> AllowWrite \<in> R 1557 \<and> x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) 1558 msg_align_bits)" 1559 unfolding auth_ipc_buffers_def 1560 by (clarsimp simp: caps_of_state_tcb' split: option.splits cap.splits arch_cap.splits bool.splits) 1561 1562subsection \<open>How User and device memory can change\<close> 1563 1564text \<open> 1565 The memory integrity relation describes which modification to user memory are allowed by the 1566 policy aag when the system is controlled by subjects. 1567 1568 p is the physical pointer to the concerned memory. 1569 ts and ts' are the @{term tcb_states_of_state} of both states 1570 icp_buf is the @{term auth_ipc_buffers} of the initial state 1571 globals is a deprecated parameter that is used in InfoFlow with the value {} 1572 TODO: It would be nice if someone made it disappear. 1573 w and w' are the data in the initial and final state. 1574 1575 The possible reason allowing for a write are : 1576 \begin{itemize} 1577 \item owning the memory 1578 \item being explicitly allowed to write by the policy 1579 \item The pointer is in the "globals" set. This is an obsolete concept and will be removed 1580 \item The thread is receiving an IPC, and we write to its IPC buffer 1581 We indirectly use the constraints of tro (@{term integrity_obj}) 1582 to decide when to allow that in order to avoid duplicating the definitions. 1583 1584 Inductive for now, we should add something about user memory/transitions. 1585\<close> 1586 1587inductive integrity_mem for aag subjects p ts ts' ipcbufs globals w w' 1588where 1589 trm_lrefl: "\<lbrakk> pasObjectAbs aag p \<in> subjects \<rbrakk> 1590 \<Longrightarrow> integrity_mem aag subjects p ts ts' ipcbufs globals w w'" (* implied by wf and write *) 1591 | trm_orefl: "\<lbrakk> w = w' \<rbrakk> \<Longrightarrow> integrity_mem aag subjects p ts ts' ipcbufs globals w w'" 1592 | trm_write: "\<lbrakk> aag_subjects_have_auth_to subjects aag Write p \<rbrakk> \<Longrightarrow> integrity_mem aag subjects p ts ts' ipcbufs globals w w'" 1593 | trm_globals: "\<lbrakk> p \<in> globals \<rbrakk> \<Longrightarrow> integrity_mem aag subjects p ts ts' ipcbufs globals w w'" 1594 | trm_ipc: "\<lbrakk> case_option False can_receive_ipc (ts p'); ts' p' = Some Structures_A.Running; 1595 p \<in> ipcbufs p'; pasObjectAbs aag p' \<notin> subjects 1596 \<rbrakk> \<Longrightarrow> integrity_mem aag subjects p ts ts' ipcbufs globals w w'" 1597 1598 1599abbreviation memory_integrity 1600where 1601 "memory_integrity X aag x t1 t2 ipc == integrity_mem (aag :: 'a PAS) {pasSubject aag} x t1 t2 ipc X" 1602 1603inductive integrity_device for aag subjects p ts ts' w w' 1604where 1605 trd_lrefl: "\<lbrakk> pasObjectAbs aag p \<in> subjects \<rbrakk> 1606 \<Longrightarrow> integrity_device aag subjects p ts ts' w w'" (* implied by wf and write *) 1607 | trd_orefl: "\<lbrakk> w = w' \<rbrakk> \<Longrightarrow> integrity_device aag subjects p ts ts' w w'" 1608 | trd_write: "\<lbrakk> aag_subjects_have_auth_to subjects aag Write p \<rbrakk> \<Longrightarrow> integrity_device aag subjects p ts ts' w w'" 1609 1610lemmas integrity_obj_simps [simp] = tro_orefl[OF refl] 1611 tro_lrefl[OF singletonI] 1612 trm_orefl[OF refl] 1613 trd_orefl[OF refl] 1614 tre_lrefl[OF singletonI] 1615 tre_orefl[OF refl] 1616 1617 1618 1619 1620subsection \<open>How the CDT can change\<close> 1621 1622text \<open> 1623 The CDT and CDT_list integrity relations describe which modification to the CDT (@{term cdt}) 1624 , @{term is_original_cap} and @{term cdt_list}) 1625 are allowed by the policy aag when the system is controlled by subjects. 1626 1627 A modification to the CDT at a specific slot can happen for different reasons : 1628 \begin{itemize} 1629 \item we own directly or indirectly the slot. The "indirectly" means that 1630 if an ancestor of a slot is owned by the subject, the slot is indirectly own by the subject 1631 \item we are allowed explicitly to take ownership of the slot, for now this only happens when 1632 we call someone: we are allowed to put a reply cap in its caller slot (slot number 3) 1633\<close> 1634 1635(* FIXME MOVE*) 1636notation parent_of_rtrancl ("_ \<Turnstile> _ \<rightarrow>* _" [60,0,60] 60) 1637 1638inductive cdt_direct_change_allowed for aag subjects tcbsts ptr 1639 where 1640 cdca_owned: 1641 "pasObjectAbs aag (fst ptr) \<in> subjects \<Longrightarrow> cdt_direct_change_allowed aag subjects tcbsts ptr" 1642| cdca_reply: 1643 "\<lbrakk>tcbsts (fst ptr) = Some tcbst; direct_call subjects aag ep tcbst; (snd ptr) = tcb_cnode_index 3\<rbrakk> 1644 \<Longrightarrow> cdt_direct_change_allowed aag subjects tcbsts ptr" 1645 1646(* for the moment the only caps that can be affected by that indirect control are reply caps *) 1647definition cdt_change_allowed 1648 where 1649 "cdt_change_allowed aag subjects m tcbsts ptr \<equiv> 1650 \<exists> pptr. m \<Turnstile> pptr \<rightarrow>* ptr \<and> cdt_direct_change_allowed aag subjects tcbsts pptr" 1651 1652lemma cdt_change_allowedI: 1653 "\<lbrakk>m \<Turnstile> pptr \<rightarrow>* ptr; cdt_direct_change_allowed aag subjects tcbsts pptr\<rbrakk> 1654 \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr" 1655 by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex) 1656 1657lemma cdt_change_allowedE: 1658 assumes "cdt_change_allowed aag subjects m tcbsts ptr" 1659 obtains pptr where "m \<Turnstile> pptr \<rightarrow>* ptr" "cdt_direct_change_allowed aag subjects tcbsts pptr" 1660 using assms by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex) 1661 1662lemma cdca_ccaI: 1663 "\<lbrakk>cdt_direct_change_allowed aag subjects tcbsts ptr\<rbrakk> 1664 \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr" 1665 by (fastforce simp: cdt_change_allowed_def simp del: split_paired_Ex) 1666 1667lemmas cca_owned = cdt_change_allowedI[OF _ cdca_owned] 1668lemmas cca_reply' = cdt_change_allowedI[OF _ cdca_owned] 1669lemmas cca_direct[intro] = cdca_ccaI[OF cdca_owned] 1670lemmas cca_reply = cdca_ccaI[OF cdca_reply] 1671 1672lemma cca_direct_single[intro]: 1673 "is_subject aag (fst ptr) \<Longrightarrow> cdt_change_allowed aag {pasSubject aag} m kh ptr" 1674 apply (rule cca_direct) by blast 1675 1676(* FIXME get a coherent naming scheme *) 1677abbreviation cdt_change_allowed' 1678where 1679 "cdt_change_allowed' aag ptr s \<equiv> cdt_change_allowed aag {pasSubject aag} (cdt s) 1680(tcb_states_of_state s) ptr" 1681 1682 1683 1684text\<open> 1685 ptr is the slot we currently looking at 1686 s is the initial state (v should be coherent with s) 1687 v = (initial parent of ptr, initial "originality" of ptr) 1688 v' = (final parent of ptr, final "originality" of ptr) 1689\<close> 1690definition integrity_cdt 1691 :: "'a PAS \<Rightarrow> 'a set \<Rightarrow> cdt \<Rightarrow> (32 word \<Rightarrow> thread_state option) 1692 \<Rightarrow> cslot_ptr \<Rightarrow> (cslot_ptr option \<times> bool) \<Rightarrow> (cslot_ptr option \<times> bool) \<Rightarrow> bool" 1693where 1694 "integrity_cdt aag subjects m tcbsts ptr v v' 1695 \<equiv> v = v' \<or> cdt_change_allowed aag subjects m tcbsts ptr" 1696 1697lemma integrity_cdtE: 1698 assumes hyp:"integrity_cdt aag subjects m tcbsts ptr v v'" 1699 obtains "v = v'" | "cdt_change_allowed aag subjects m tcbsts ptr" 1700 using hyp integrity_cdt_def by blast 1701 1702abbreviation integrity_cdt_state 1703where 1704 "integrity_cdt_state aag subjects s s' \<equiv> 1705 (\<forall>x. integrity_cdt aag subjects (cdt s) (tcb_states_of_state s) x 1706 (cdt s x,is_original_cap s x) (cdt s' x, is_original_cap s' x))" 1707 1708abbreviation cdt_integrity 1709where 1710 "cdt_integrity aag \<equiv> integrity_cdt (aag :: 'a PAS) {pasSubject aag} " 1711 1712abbreviation cdt_integrity_state 1713where 1714 "cdt_integrity_state aag s s' \<equiv> 1715 (\<forall>x. integrity_cdt (aag :: 'a PAS) {pasSubject aag} (cdt s) (tcb_states_of_state s) x 1716 (cdt s x,is_original_cap s x) (cdt s' x, is_original_cap s' x))" 1717 1718lemma integrity_cdt_refl[simp]: "integrity_cdt aag subjects m kh ptr v v" 1719 by (simp add: integrity_cdt_def) 1720 1721lemma integrity_cdt_change_allowed[simp,intro]: 1722 "cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt aag subjects m kh ptr v v'" 1723 by (simp add: integrity_cdt_def) 1724 1725lemmas integrity_cdt_intros = integrity_cdt_refl integrity_cdt_change_allowed 1726 1727lemmas integrity_cdt_direct = cca_direct[THEN integrity_cdt_change_allowed] 1728 1729 1730 1731text\<open> 1732 m is the cdt of the initial state 1733 tcbsts are tcb_states_of_state of the initial state 1734 ptr is the slot we currently looking at 1735 l and l' are the initial and final list of children of ptr 1736\<close> 1737definition integrity_cdt_list 1738 :: "'a PAS \<Rightarrow> 'a set \<Rightarrow> cdt \<Rightarrow> (32 word \<Rightarrow> thread_state option) \<Rightarrow> cslot_ptr \<Rightarrow> 1739 (cslot_ptr list) \<Rightarrow> (cslot_ptr list) \<Rightarrow> bool" 1740where 1741 "integrity_cdt_list aag subjects m tcbsts ptr l l' 1742 \<equiv> (filtered_eq (cdt_change_allowed aag subjects m tcbsts) l l') \<or> 1743 cdt_change_allowed aag subjects m tcbsts ptr" 1744 1745abbreviation integrity_cdt_list_state 1746where 1747 "integrity_cdt_list_state aag subjects s s' \<equiv> 1748 (\<forall>x. integrity_cdt_list aag subjects (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x))" 1749 1750abbreviation cdt_list_integrity 1751where 1752 "cdt_list_integrity aag == integrity_cdt_list (aag :: 'a PAS) {pasSubject aag}" 1753 1754abbreviation cdt_list_integrity_state 1755where 1756 "cdt_list_integrity_state aag s s' \<equiv> 1757 (\<forall>x. integrity_cdt_list (aag :: 'a PAS) {pasSubject aag} (cdt s) (tcb_states_of_state s) x 1758 (cdt_list s x) (cdt_list s' x))" 1759 1760lemma integrity_cdt_list_refl[simp]: "integrity_cdt_list aag subjects m kh ptr v v" 1761 by (simp add: integrity_cdt_list_def) 1762 1763lemma integrity_cdt_list_filt: 1764 "filtered_eq (cdt_change_allowed aag subjects m kh) l l' \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'" 1765 by (simp add: integrity_cdt_list_def) 1766lemma integrity_cdt_list_change_allowed: 1767 "cdt_change_allowed aag subjects m kh ptr \<Longrightarrow> integrity_cdt_list aag subjects m kh ptr l l'" 1768 by (simp add: integrity_cdt_list_def) 1769 1770lemmas integrity_cdt_list_intros = integrity_cdt_list_filt integrity_cdt_list_change_allowed 1771 1772lemma integrity_cdt_listE: 1773 assumes hyp:"integrity_cdt_list aag subjects m kh ptr l l'" 1774 obtains "filtered_eq (cdt_change_allowed aag subjects m kh) l l'" | 1775 "cdt_change_allowed aag subjects m kh ptr" 1776 using hyp integrity_cdt_list_def by blast 1777 1778 1779 1780subsection \<open>How other stuff can change\<close> 1781 1782definition integrity_interrupts 1783 :: "'a PAS \<Rightarrow> 'a set \<Rightarrow> irq \<Rightarrow> (obj_ref \<times> irq_state) \<Rightarrow> (obj_ref \<times> irq_state) \<Rightarrow> bool" 1784where 1785 "integrity_interrupts aag subjects irq v v' 1786 \<equiv> v = v' \<or> pasIRQAbs aag irq \<in> subjects" 1787 1788lemma integrity_interrupts_refl[simp]: "integrity_interrupts aag subjects ptr v v" 1789 by (simp add: integrity_interrupts_def) 1790 1791definition integrity_asids :: "'a PAS \<Rightarrow> 'a set \<Rightarrow> asid \<Rightarrow> word32 option \<Rightarrow> word32 option \<Rightarrow> bool" 1792where 1793 "integrity_asids aag subjects asid pp_opt pp_opt' 1794 \<equiv> pp_opt = pp_opt' \<or> (\<forall> asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> pasASIDAbs aag asid' \<in> subjects)" 1795 1796lemma integrity_asids_refl[simp]: "integrity_asids aag subjects ptr s s" 1797 by (simp add: integrity_asids_def) 1798 1799subsection \<open>General integrity\<close> 1800 1801text\<open> 1802 1803Half of what we ultimately want to say: that the parts of the 1804system state that change are allowed to by the labelling @{term 1805"aag"}. 1806 1807The other half involves showing that @{term "aag"} concords with the 1808policy. See @{term "state_objs_to_policy s"} and @{term "pas_refined aag s"}. 1809 1810\<close> 1811 1812definition integrity_subjects 1813 :: "'a set \<Rightarrow> 'a PAS \<Rightarrow> bool \<Rightarrow> obj_ref set \<Rightarrow> det_ext state \<Rightarrow> det_ext state \<Rightarrow> bool" 1814where 1815 "integrity_subjects subjects aag activate X s s' \<equiv> 1816 (\<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x)) \<and> 1817 (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> 1818 (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') 1819 (auth_ipc_buffers s) X 1820 (underlying_memory (machine_state s) x) 1821 (underlying_memory (machine_state s') x)) \<and> 1822 (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') 1823 (device_state (machine_state s) x) 1824 (device_state (machine_state s') x)) \<and> 1825 integrity_cdt_state aag subjects s s'\<and> 1826 integrity_cdt_list_state aag subjects s s' \<and> 1827 (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) 1828 (interrupt_irq_node s' x, interrupt_states s' x)) \<and> 1829 (\<forall>x. integrity_asids aag subjects x (arm_asid_table (arch_state s) (asid_high_bits_of x)) 1830 (arm_asid_table (arch_state s') (asid_high_bits_of x))) \<and> 1831 (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) 1832 (ready_queues s' d p))" 1833 1834abbreviation integrity 1835where 1836 "integrity pas \<equiv> integrity_subjects {pasSubject pas} pas (pasMayActivate pas)" 1837 1838 1839 1840section \<open>Integrity transitivity\<close> 1841 1842subsection \<open>Object integrity transitivity\<close> 1843 1844lemma clear_asidpool_trans[elim]: 1845 "\<lbrakk>asid_pool_integrity subjects aag pool pool'; 1846 asid_pool_integrity subjects aag pool' pool''\<rbrakk> 1847 \<Longrightarrow> asid_pool_integrity subjects aag pool pool''" 1848 unfolding asid_pool_integrity_def 1849 apply clarsimp 1850 apply (drule_tac x=x in spec)+ 1851 apply auto 1852 done 1853 1854lemma tcb_bound_notification_reset_integrity_trans[elim]: 1855 "\<lbrakk> tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag; 1856 tcb_bound_notification_reset_integrity ntfn' ntfn'' subjects aag \<rbrakk> 1857 \<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn'' subjects aag" 1858 by (auto simp: tcb_bound_notification_reset_integrity_def) 1859 1860lemma reply_cap_deletion_integrity_trans[elim]: 1861 "\<lbrakk> reply_cap_deletion_integrity subjects aag cap cap'; 1862 reply_cap_deletion_integrity subjects aag cap' cap'' \<rbrakk> 1863 \<Longrightarrow> reply_cap_deletion_integrity subjects aag cap cap''" 1864 by (auto simp: reply_cap_deletion_integrity_def) 1865 1866 1867lemma cnode_integrity_trans[elim]: 1868 "\<lbrakk> cnode_integrity subjects aag cont cont'; 1869 cnode_integrity subjects aag cont' cont'' \<rbrakk> 1870 \<Longrightarrow> cnode_integrity subjects aag cont cont''" 1871 unfolding cnode_integrity_def 1872 apply (intro allI) 1873 apply (drule_tac x=l in spec)+ 1874 by fastforce 1875 1876lemma tcb_bound_notification_reset_eq_or_none: 1877 "tcb_bound_notification_reset_integrity ntfn ntfn' subjects aag \<Longrightarrow> ntfn = ntfn' \<or> ntfn' = None" 1878 by (auto simp: tcb_bound_notification_reset_integrity_def) 1879 1880 1881lemma tro_alt_trans_spec: (* this takes a long time to process *) 1882 "\<lbrakk>integrity_obj_alt aag activate es subjects ko ko'; 1883 integrity_obj_alt aag activate es subjects ko' ko'' \<rbrakk> \<Longrightarrow> 1884 integrity_obj_alt aag activate es subjects ko ko''" 1885 (* We need to consider nearly 200 cases, one for each possible pair 1886 of integrity steps. We use the tro_tags to select subsets of goals 1887 that can be solved by the same method. *) 1888 1889 (* Expand the first integrity step *) 1890 apply (erule integrity_obj_alt.cases[where ko=ko and ko'=ko']) 1891 1892 (* LRefl and ORefl trivially collapse into the second integrity step *) 1893 apply (find_goal \<open>match premises in "tro_tag LRefl" \<Rightarrow> -\<close>) 1894 subgoal by (rule tro_alt_lrefl, simp) 1895 1896 apply (find_goal \<open>match premises in "tro_tag ORefl" \<Rightarrow> -\<close>) 1897 subgoal by simp 1898 1899 (* Now re-tag the first step with tro_tag' *) 1900 apply (all \<open>simp only:tro_tag_to_prime\<close>) 1901 (* Expand the second integrity step, which will be tagged with tro_tag *) 1902 apply (all \<open>erule integrity_obj_alt.cases\<close>) 1903 1904 (* There are some special cases that would be too slow or unsolvable by the bulk tactics. 1905 We move them up here and solve manually *) 1906 apply (find_goal \<open>match premises in "tro_tag' TCBReply" and "tro_tag TCBActivate" \<Rightarrow> -\<close>) 1907 apply (clarsimp, rule tro_alt_tcb_reply[OF tro_tagI refl refl], 1908 (rule exI; rule tcb.equality; simp add: arch_tcb_context_set_def); fastforce) 1909 1910 apply (find_goal \<open>match premises in "tro_tag' TCBReceive" and "tro_tag TCBReply" \<Rightarrow> -\<close>) 1911 apply (clarsimp, rule tro_alt_tcb_reply[OF tro_tagI refl refl], 1912 (rule exI; rule tcb.equality; 1913 simp add: arch_tcb_context_set_def); 1914 fastforce simp: indirect_send_def direct_send_def direct_reply_def 1915 allowed_call_blocked_def) 1916 1917 apply (find_goal \<open>match premises in "tro_tag TCBGeneric" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>) 1918 subgoal 1919 apply (erule integrity_obj_alt.intros[simplified tro_tag_to_prime]) 1920 apply (rule refl | assumption 1921 | fastforce intro: tcb.equality 1922 | (erule tcb_bound_notification_reset_integrity_trans 1923 reply_cap_deletion_integrity_trans; 1924 fastforce))+ 1925 done 1926 1927 apply (find_goal \<open>match premises in "tro_tag TCBActivate" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>) 1928 apply (rule tro_alt_tcb_restart[OF tro_tagI], 1929 rule refl, 1930 assumption, 1931 (* somehow works better than tcb.equality *) 1932 (simp only: tcb.splits; simp), 1933 force+)[1] 1934 1935 apply (find_goal \<open>match premises in "tro_tag REp" and "tro_tag' REp" \<Rightarrow> -\<close>) 1936 subgoal by (erule integrity_obj_alt.intros, (rule refl | assumption)+) 1937 1938 (* Select groups of subgoals by tag, then solve with the given methods *) 1939 apply (all \<open>fails \<open>erule thin_rl[of "tro_tag LRefl"]\<close> 1940 | time_methods \<open>solves \<open> 1941 fastforce intro: tro_alt_lrefl\<close>\<close>\<close>) 1942 1943 apply (all \<open>fails \<open>erule thin_rl[of "tro_tag ORefl"]\<close> 1944 | time_methods \<open>solves \<open> 1945 drule sym[where t="ko''"]; 1946 erule integrity_obj_alt.intros[simplified tro_tag_to_prime]; 1947 solves \<open>simp\<close>\<close>\<close>\<close>) 1948 1949 apply (all \<open>fails \<open>erule thin_rl[of "tro_tag RNtfn"] thin_rl[of "tro_tag' RNtfn"]\<close> 1950 | time_methods \<open>solves \<open> 1951 fastforce intro: tro_alt_ntfn\<close>\<close>\<close>) 1952 1953 apply (all \<open>fails \<open>erule thin_rl[of "tro_tag REp"] 1954 | erule thin_rl[of "tro_tag' REp"] 1955 | erule thin_rl[of "tro_tag RASID"] 1956 | erule thin_rl[of "tro_tag' RASID"] 1957 | erule thin_rl[of "tro_tag EpUnblock"] 1958 | erule thin_rl[of "tro_tag' EpUnblock"] 1959 | erule thin_rl[of "tro_tag RCNode"] 1960 | erule thin_rl[of "tro_tag' RCNode"]\<close> 1961 | time_methods \<open>solves \<open> 1962 fastforce intro: integrity_obj_alt.intros tcb.equality 1963 simp: indirect_send_def direct_send_def\<close>\<close>\<close>) 1964 1965 (* TCB-TCB steps, somewhat slow *) 1966 apply (all \<open>fails \<open>erule thin_rl[of "tro_tag TCBGeneric"]\<close> 1967 | time_methods \<open>solves \<open> 1968 erule integrity_obj_alt.intros[simplified tro_tag_to_prime], 1969 (assumption | rule refl 1970 | ((erule exE)+)?, (rule exI)?, force intro: tcb.equality)+\<close>\<close>\<close>) 1971 1972 apply (all \<open>fails \<open>erule thin_rl[of "tro_tag' TCBGeneric"]\<close> 1973 | time_methods \<open>solves \<open> 1974 erule integrity_obj_alt.intros, 1975 (assumption | rule refl 1976 | (elim exE)?, (intro exI)?, fastforce intro: tcb.equality 1977 | fastforce simp: indirect_send_def direct_send_def direct_call_def direct_reply_def 1978 dest: tcb_bound_notification_reset_eq_or_none)+\<close>\<close>\<close>) 1979 1980 apply (time_methods \<open> 1981 succeeds \<open>match premises in T: "tro_tag _" and T': "tro_tag' _" \<Rightarrow> 1982 \<open>print_fact T, print_fact T'\<close>\<close>, 1983 fastforce intro: integrity_obj_alt.intros tcb.equality 1984 simp: indirect_send_def direct_send_def direct_call_def direct_reply_def 1985 send_blocked_on_def3 call_blocked_def allowed_call_blocked_def\<close>)+ 1986 done 1987 1988lemma tro_alt_reflp[intro!]: 1989 "reflp (integrity_obj_alt aag activate es subjects)" 1990 by (rule reflpI) (rule tro_alt_orefl; blast) 1991 1992lemma tro_alt_transp[intro!]: 1993 "transp (integrity_obj_alt aag activate es subjects)" 1994 by (rule transpI) (rule tro_alt_trans_spec) 1995 1996 1997 1998lemma tro_tro_alt[elim!]: 1999 "integrity_obj aag activate es subjects ko ko' 2000 \<Longrightarrow> integrity_obj_alt aag activate es subjects ko ko'" 2001 unfolding integrity_obj_def 2002 by (subst rtranclp_id[symmetric]; fastforce elim: rtranclp_mono[THEN predicate2D,rotated]) 2003 2004lemmas integrity_objE = tro_tro_alt[THEN integrity_obj_alt.cases 2005 [simplified tro_tag_def True_implies_equals]] 2006 2007 2008 2009lemma tro_trans: 2010 "\<lbrakk>integrity_obj_state aag activate es s s'; integrity_obj_state aag activate es s' s''\<rbrakk> 2011 \<Longrightarrow> integrity_obj_state aag activate es s s''" 2012 unfolding integrity_obj_def 2013 apply clarsimp 2014 apply (drule_tac x = x in spec)+ 2015 by force 2016 2017lemma tre_trans: 2018 "\<lbrakk>(\<forall>x. integrity_eobj aag es (pasObjectAbs aag x) (ekh x) (ekh' x)); 2019 (\<forall>x. integrity_eobj aag es (pasObjectAbs aag x) (ekh' x) (ekh'' x)) \<rbrakk> \<Longrightarrow> 2020 (\<forall>x. integrity_eobj aag es (pasObjectAbs aag x) (ekh x) (ekh'' x))" 2021by (fastforce elim!: integrity_eobj.cases 2022 intro: integrity_eobj.intros) 2023 2024 2025 2026subsection \<open>CDT integrity transitivity\<close> 2027 2028lemma tcb_caller_slot_empty_on_recieve: 2029 "\<lbrakk> valid_mdb s ; valid_objs s; kheap s tcb_ptr = Some (TCB tcb); ep_recv_blocked ep (tcb_state tcb) \<rbrakk> \<Longrightarrow> 2030 tcb_caller tcb = NullCap \<and> cdt s (tcb_ptr,(tcb_cnode_index 3)) = None \<and> 2031 descendants_of (tcb_ptr,(tcb_cnode_index 3)) (cdt s) = {}" 2032 apply (simp only:valid_objs_def) 2033 apply (drule bspec,fastforce) 2034 apply (simp add:valid_obj_def) 2035 apply (simp only:valid_tcb_def) 2036 apply (drule conjunct1) 2037 apply (drule_tac x="the (tcb_cap_cases (tcb_cnode_index 3))" in bspec) 2038 apply (fastforce simp:tcb_cap_cases_def) 2039 apply (simp add:tcb_cap_cases_def split: thread_state.splits) 2040 apply (subgoal_tac "caps_of_state s (tcb_ptr, tcb_cnode_index 3) = Some NullCap") 2041 apply (simp only: valid_mdb_def2, drule conjunct1) 2042 apply (intro conjI) 2043 apply (simp add: mdb_cte_at_def) 2044 apply (rule classical) 2045 apply fastforce 2046 apply (rule mdb_cte_at_no_descendants, fastforce+)[1] 2047 apply (fastforce simp add: tcb_cnode_map_def caps_of_state_tcb_index_trans[OF get_tcb_rev]) 2048done 2049 2050 2051(* FIXME MOVE next to tcb_states_of_state definition *) 2052lemma tcb_states_of_state_kheap: 2053 "\<lbrakk>kheap s slot = Some (TCB tcb)\<rbrakk> 2054 \<Longrightarrow> tcb_states_of_state s slot = Some (tcb_state tcb)" 2055 by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits) 2056 2057lemma tcb_states_of_state_kheapI: 2058 "\<lbrakk>kheap s slot = Some (TCB tcb); tcb_state tcb = tcbst\<rbrakk> 2059 \<Longrightarrow> tcb_states_of_state s slot = Some tcbst" 2060 by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits) 2061 2062lemma tcb_states_of_state_kheapD: 2063 "tcb_states_of_state s slot = Some tcbst \<Longrightarrow> 2064 \<exists> tcb. kheap s slot = Some (TCB tcb) \<and> tcb_state tcb = tcbst" 2065 by (simp add:tcb_states_of_state_def get_tcb_def split: option.splits kernel_object.splits) 2066 2067lemma tcb_states_of_state_kheapE: 2068 assumes "tcb_states_of_state s slot = Some tcbst" 2069 obtains tcb where "kheap s slot = Some (TCB tcb)" "tcb_state tcb = tcbst" 2070 using assms tcb_states_of_state_kheapD by blast 2071 2072lemma cdt_direct_change_allowed_backward: 2073 "\<lbrakk>integrity_obj_state aag activate subjects s s'; 2074 cdt_direct_change_allowed aag subjects (tcb_states_of_state s') ptr\<rbrakk> \<Longrightarrow> 2075 cdt_direct_change_allowed aag subjects (tcb_states_of_state s) ptr" 2076 apply (erule cdt_direct_change_allowed.cases) 2077 subgoal by (rule cdca_owned) 2078 apply (erule tcb_states_of_state_kheapE) 2079 by (drule spec, 2080 erule integrity_objE, erule cdca_owned; 2081 (elim exE)?; 2082 simp; 2083 rule cdca_reply[rotated], assumption, assumption, 2084 fastforce elim:tcb_states_of_state_kheapI simp:direct_call_def) 2085 2086lemma cdt_change_allowed_to_child: 2087 "cdt_change_allowed aag subjects m tcbsts pptr \<Longrightarrow> m ptr = Some pptr 2088 \<Longrightarrow> cdt_change_allowed aag subjects m tcbsts ptr" 2089 apply (elim cdt_change_allowedE) 2090 apply (erule cdt_change_allowedI[rotated]) 2091 by(fastforce intro: rtrancl_into_rtrancl simp: cdt_parent_of_def) 2092 2093lemma cdt_change_allowed_backward: 2094 "\<lbrakk>integrity_obj_state aag activate subjects s s'; 2095 integrity_cdt_state aag subjects s s'; 2096 cdt_change_allowed aag subjects (cdt s') (tcb_states_of_state s') ptr\<rbrakk> \<Longrightarrow> 2097 cdt_change_allowed aag subjects (cdt s) (tcb_states_of_state s) ptr" 2098 apply (elim cdt_change_allowedE) 2099 apply (drule(1) cdt_direct_change_allowed_backward) 2100 apply (erule rtrancl_induct) 2101 subgoal by (rule cdca_ccaI) 2102 apply (rename_tac pptr0 ptr) 2103 apply (frule_tac x=ptr in spec) 2104 apply (elim integrity_cdtE; simp; elim conjE) 2105 apply (erule cdt_change_allowed_to_child) 2106 by(simp add: cdt_parent_of_def) 2107 2108lemma trcdt_trans: 2109 "\<lbrakk>integrity_cdt_state aag subjects s s' ; 2110 integrity_obj_state aag activate subjects s s' ; 2111 integrity_cdt_state aag subjects s' s'' \<rbrakk> 2112 \<Longrightarrow> integrity_cdt_state aag subjects s s''" 2113 apply (intro allI) 2114 apply (frule_tac x=x in spec) 2115 apply (frule_tac x=x in spec[where P = "\<lambda>x. integrity_cdt _ _ (cdt s') _ x (_ x) (_ x)"]) 2116 apply (erule integrity_cdtE)+ 2117 apply simp 2118 by (blast dest: cdt_change_allowed_backward)+ 2119 2120lemma trcdtlist_trans: 2121 "\<lbrakk>integrity_cdt_list_state aag subjects s s' ; 2122 integrity_obj_state aag activate subjects s s' ; 2123 integrity_cdt_state aag subjects s s' ; 2124 integrity_cdt_list_state aag subjects s' s'' \<rbrakk> 2125 \<Longrightarrow> integrity_cdt_list_state aag subjects s s''" 2126 apply (intro allI) 2127 apply (drule_tac x=x in spec [where P="\<lambda>ptr. integrity_cdt_list _ _ _ _ ptr (_ ptr) (_ ptr)"] )+ 2128 apply (erule integrity_cdt_listE)+ 2129 apply (rule integrity_cdt_list_filt) 2130 apply (simp del: split_paired_All split_paired_Ex) 2131 apply (erule weaken_filter_eq') 2132 by (blast intro: integrity_cdt_list_intros dest: cdt_change_allowed_backward)+ 2133 2134 2135subsection \<open>Main integrity transitivity\<close> 2136 2137 2138lemma trinterrupts_trans: 2139 "\<lbrakk> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)); 2140 (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<rbrakk> 2141 \<Longrightarrow> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x))" 2142 apply (simp add: integrity_interrupts_def 2143 del: split_paired_All) 2144 apply metis 2145 done 2146 2147lemma trasids_trans: 2148 "\<lbrakk> (\<forall>x. integrity_asids aag subjects x (arm_asid_table (arch_state s) (asid_high_bits_of x)) (arm_asid_table (arch_state s') (asid_high_bits_of x))); 2149 (\<forall>x. integrity_asids aag subjects x (arm_asid_table (arch_state s') (asid_high_bits_of x)) (arm_asid_table (arch_state s'') (asid_high_bits_of x)))\<rbrakk> 2150 \<Longrightarrow> 2151 (\<forall>x. integrity_asids aag subjects x (arm_asid_table (arch_state s) (asid_high_bits_of x)) (arm_asid_table (arch_state s'') (asid_high_bits_of x)))" 2152 apply (clarsimp simp: integrity_asids_def) 2153 apply metis 2154 done 2155 2156lemma trrqs_trans: 2157 "\<lbrakk> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)); 2158 (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p)) \<rbrakk> 2159 \<Longrightarrow> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p))" 2160apply (clarsimp simp: integrity_ready_queues_def) 2161apply (metis append_assoc) 2162done 2163 2164(* FIXME RENAME *) 2165lemma tsos_tro: 2166 "\<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a; 2167 receive_blocked_on ep a; pasObjectAbs aag p \<notin> subjects \<rbrakk> \<Longrightarrow> tcb_states_of_state s p = Some a" 2168 apply (drule_tac x = p in spec) 2169 apply (erule integrity_objE, simp_all add: tcb_states_of_state_def get_tcb_def) 2170 by fastforce+ 2171 2172lemma can_receive_ipc_backward: 2173 "\<lbrakk>integrity_obj_state aag activate subjects s s'; tcb_states_of_state s' p = Some a; 2174 can_receive_ipc a; pasObjectAbs aag p \<notin> subjects \<rbrakk> 2175 \<Longrightarrow> case tcb_states_of_state s p of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x" 2176 apply (drule_tac x = p in spec) 2177 apply (erule integrity_objE; 2178 (fastforce simp: tcb_states_of_state_def get_tcb_def 2179 call_blocked_def allowed_call_blocked_def 2180 split: option.splits kernel_object.splits 2181 | cases a \<comment> \<open>only split when needed\<close>)+) 2182 done 2183 2184 2185 2186lemma auth_ipc_buffers_tro: 2187 "\<lbrakk>integrity_obj_state aag activate subjects s s'; x \<in> auth_ipc_buffers s' p; 2188 pasObjectAbs aag p \<notin> subjects \<rbrakk> 2189 \<Longrightarrow> x \<in> auth_ipc_buffers s p " 2190 by (drule_tac x = p in spec) 2191 (erule integrity_objE; 2192 fastforce simp: tcb_states_of_state_def get_tcb_def auth_ipc_buffers_def 2193 split: cap.split_asm arch_cap.split_asm if_split_asm bool.splits) 2194 2195 2196lemma auth_ipc_buffers_tro_fwd: 2197 "\<lbrakk>integrity_obj_state aag activate subjects s s'; x \<in> auth_ipc_buffers s p; 2198 pasObjectAbs aag p \<notin> subjects \<rbrakk> 2199 \<Longrightarrow> x \<in> auth_ipc_buffers s' p " 2200 by (drule_tac x = p in spec) 2201 (erule integrity_objE; 2202 fastforce simp: tcb_states_of_state_def get_tcb_def auth_ipc_buffers_def 2203 split: cap.split_asm arch_cap.split_asm if_split_asm bool.splits) 2204 2205 2206lemma tsos_tro_running: 2207 "\<lbrakk>\<forall>x. integrity_obj aag activate subjects (pasObjectAbs aag x) (kheap s x) (kheap s' x); 2208 tcb_states_of_state s p = Some Structures_A.Running; 2209 pasObjectAbs aag p \<notin> subjects \<rbrakk> 2210 \<Longrightarrow> tcb_states_of_state s' p = Some Structures_A.Running" 2211 by (drule_tac x = p in spec) 2212 (erule integrity_objE, 2213 simp_all add: tcb_states_of_state_def get_tcb_def indirect_send_def 2214 direct_send_def direct_call_def direct_reply_def call_blocked_def allowed_call_blocked_def) 2215 2216 2217lemma integrity_trans: 2218 assumes t1: "integrity_subjects subjects aag activate X s s'" 2219 and t2: "integrity_subjects subjects aag activate X s' s''" 2220 shows "integrity_subjects subjects aag activate X s s''" 2221proof - 2222 from t1 have tro1: "integrity_obj_state aag activate subjects s s'" 2223 unfolding integrity_subjects_def by simp 2224 from t2 have tro2: "integrity_obj_state aag activate subjects s' s''" 2225 unfolding integrity_subjects_def by simp 2226 2227 have intm: "\<forall>x. integrity_mem aag subjects x 2228 (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X 2229 (underlying_memory (machine_state s) x) 2230 (underlying_memory (machine_state s'') x)" (is "\<forall>x. ?P x s s''") 2231 proof 2232 fix x 2233 from t1 t2 have m1: "?P x s s'" and m2: "?P x s' s''" unfolding integrity_subjects_def by auto 2234 2235 from m1 show "?P x s s''" 2236 proof cases 2237 case trm_lrefl thus ?thesis by (rule integrity_mem.intros) 2238 next 2239 case trm_globals thus ?thesis by (rule integrity_mem.intros) 2240 next 2241 case trm_orefl 2242 from m2 show ?thesis 2243 proof cases 2244 case (trm_ipc p') 2245 2246 show ?thesis 2247 proof (rule integrity_mem.trm_ipc) 2248 from trm_ipc show "case_option False can_receive_ipc (tcb_states_of_state s p')" 2249 by (fastforce split: option.splits dest: can_receive_ipc_backward [OF tro1]) 2250 2251 from trm_ipc show "x \<in> auth_ipc_buffers s p'" 2252 by (fastforce split: option.splits intro: auth_ipc_buffers_tro [OF tro1]) 2253 qed (simp_all add: trm_ipc) 2254 qed (auto simp add: trm_orefl intro: integrity_mem.intros) 2255 next 2256 case trm_write thus ?thesis by (rule integrity_mem.intros) 2257 next 2258 case (trm_ipc p') 2259 note trm_ipc1 = trm_ipc 2260 2261 from m2 show ?thesis 2262 proof cases 2263 case trm_orefl 2264 thus ?thesis using trm_ipc1 2265 by (auto intro!: integrity_mem.trm_ipc simp add: restrict_map_Some_iff elim!: tsos_tro_running [OF tro2, rotated]) 2266 next 2267 case (trm_ipc p'') 2268 show ?thesis 2269 proof (cases "p' = p''") 2270 case True thus ?thesis using trm_ipc trm_ipc1 by (simp add: restrict_map_Some_iff) 2271 next 2272 (* 2 tcbs sharing same IPC buffer, we can appeal to either t1 or t2 *) 2273 case False 2274 thus ?thesis using trm_ipc1 2275 by (auto intro!: integrity_mem.trm_ipc simp add: restrict_map_Some_iff elim!: tsos_tro_running [OF tro2, rotated]) 2276 qed 2277 qed (auto simp add: trm_ipc intro: integrity_mem.intros) 2278 qed 2279 qed 2280 2281 moreover have "\<forall>x. integrity_device aag subjects x 2282 (tcb_states_of_state s) (tcb_states_of_state s'') 2283 (device_state (machine_state s) x) 2284 (device_state (machine_state s'') x)" (is "\<forall>x. ?P x s s''") 2285 proof 2286 fix x 2287 from t1 t2 have m1: "?P x s s'" and m2: "?P x s' s''" unfolding integrity_subjects_def by auto 2288 2289 from m1 show "?P x s s''" 2290 proof cases 2291 case trd_lrefl thus ?thesis by (rule integrity_device.intros) 2292 next 2293 case torel1: trd_orefl 2294 from m2 show ?thesis 2295 proof cases 2296 case (trd_lrefl) thus ?thesis by (rule integrity_device.trd_lrefl) 2297 next 2298 case trd_orefl thus ?thesis 2299 by (simp add:torel1) 2300 next 2301 case trd_write thus ?thesis by (rule integrity_device.trd_write) 2302 qed 2303 next 2304 case trd_write thus ?thesis by (rule integrity_device.intros) 2305 qed 2306 qed 2307 thus ?thesis using tro_trans[OF tro1 tro2] t1 t2 intm 2308 apply (clarsimp simp add: integrity_subjects_def simp del: split_paired_All) 2309 apply (frule(2) trcdt_trans) 2310 apply (frule(3) trcdtlist_trans) 2311 apply (frule(1) trinterrupts_trans[simplified]) 2312 apply (frule(1) trasids_trans[simplified]) 2313 apply (frule(1) tre_trans[simplified]) 2314 apply (frule(1) trrqs_trans[simplified]) 2315 by blast 2316qed 2317 2318lemma integrity_refl [simp]: 2319 "integrity_subjects S aag activate X s s" 2320unfolding integrity_subjects_def 2321by simp 2322 2323section \<open>Generic AC stuff\<close> 2324 2325subsection \<open>Basic integrity lemmas\<close> 2326 2327(* Tom says that Gene Wolfe says that autarchy \<equiv> self authority. *) 2328 2329lemma integrity_update_autarch: 2330 "\<lbrakk> integrity aag X st s; is_subject aag ptr \<rbrakk> 2331 \<Longrightarrow> integrity aag X st (s\<lparr>kheap := kheap s(ptr \<mapsto> obj)\<rparr>)" 2332 unfolding integrity_subjects_def 2333 apply (intro conjI,simp_all) 2334 apply clarsimp 2335 apply (drule_tac x = x in spec, erule integrity_mem.cases) 2336 apply ((auto intro: integrity_mem.intros)+)[4] 2337 apply (erule trm_ipc, simp_all) 2338 apply (clarsimp simp: restrict_map_Some_iff tcb_states_of_state_def get_tcb_def) 2339 apply clarsimp 2340 apply (drule_tac x = x in spec, erule integrity_device.cases) 2341 apply (erule integrity_device.trd_lrefl) 2342 apply (erule integrity_device.trd_orefl) 2343 apply (erule integrity_device.trd_write) 2344 done 2345 2346lemma set_object_integrity_autarch: 2347 "\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace> 2348 set_object ptr obj 2349 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 2350 apply (wpsimp wp: set_object_wp) 2351 apply (rule integrity_update_autarch, simp_all) 2352 done 2353 2354lemma tcb_states_of_state_trans_state[simp]: 2355 "tcb_states_of_state (trans_state f s) = tcb_states_of_state s" 2356 by (simp add: tcb_states_of_state_def get_tcb_exst_update) 2357 2358lemma eintegrity_sa_update[simp]: 2359 "integrity aag X st (scheduler_action_update f s) = integrity aag X st s" 2360 by (simp add: integrity_subjects_def trans_state_update'[symmetric]) 2361 2362lemma trans_state_back[simp]: 2363 "trans_state (\<lambda>_. exst s) s = s" 2364 by simp 2365 2366declare wrap_ext_op_det_ext_ext_def[simp] 2367 2368crunch integrity[wp]: set_thread_state_ext "integrity aag X st" 2369 2370crunch integrity_autarch: set_thread_state "integrity aag X st" 2371 2372lemmas integrity_def = integrity_subjects_def 2373 2374subsection \<open>Out of subject cap manipulation\<close> 2375 2376(* FIXME MOVE *) 2377lemma all_children_descendants_of: 2378 "\<lbrakk> all_children P m ; p \<in> descendants_of q m ; P q \<rbrakk> \<Longrightarrow> P p " 2379 apply (simp add: descendants_of_def) 2380 apply (erule trancl_induct[where P=P]) 2381 unfolding cdt_parent_of_def 2382 apply (erule(2) all_childrenD)+ 2383 done 2384 2385lemmas all_children_parent_of_trancl = 2386 all_children_descendants_of[simplified descendants_of_def,simplified] 2387 2388lemma all_children_parent_of_rtrancl: 2389 "\<lbrakk> all_children P m ; m \<Turnstile> q \<rightarrow>* p ; P q \<rbrakk> \<Longrightarrow> P p " 2390 by (drule rtranclD,elim conjE disjE; blast dest:all_children_parent_of_trancl) 2391 2392lemma pas_refined_all_children': 2393 "\<lbrakk>valid_mdb s ; pas_refined aag s ; m = (cdt s) \<rbrakk> \<Longrightarrow> 2394 all_children (\<lambda>x. is_subject aag (fst x) \<or> is_transferable (caps_of_state s x)) m" 2395 apply (rule all_childrenI) 2396 apply (erule disjE) 2397 apply (simp add: pas_refined_def,elim conjE) 2398 apply (rule disjCI) 2399 apply (subgoal_tac 2400 "(pasObjectAbs aag (fst p), Control, pasObjectAbs aag (fst c)) \<in> pasPolicy aag") 2401 apply (fastforce elim: aag_wellformed_control_is_owns[THEN iffD1]) 2402 apply (simp add: state_objs_to_policy_def auth_graph_map_def) 2403 apply (erule set_mp) 2404 apply (frule(1) sbta_cdt) 2405 apply force 2406 apply (rule disjI2) 2407 by (rule is_transferable_all_children[THEN all_childrenD]; solves \<open>simp\<close>) 2408 2409lemmas pas_refined_all_children = pas_refined_all_children'[OF _ _ refl] 2410 2411(* FIXME MOVE just after cte_wp_at_cases2 *) 2412lemma caps_of_state_def': 2413 "caps_of_state s slot = 2414 (case kheap s (fst slot) of 2415 Some (TCB tcb) \<Rightarrow> tcb_cnode_map tcb (snd slot) 2416 | Some (CNode sz content) \<Rightarrow> (if well_formed_cnode_n sz content then content (snd slot) else None) 2417 | _ \<Rightarrow> None)" 2418 by (fastforce simp: caps_of_state_cte_wp_at cte_wp_at_cases2 2419 split: option.splits kernel_object.splits) 2420 2421lemma caps_of_state_cnode: 2422 "\<lbrakk>kheap s pos = Some (CNode sz content); well_formed_cnode_n sz content\<rbrakk> \<Longrightarrow> 2423 caps_of_state s (pos,addr) = content addr" 2424 by (simp add:caps_of_state_def') 2425 2426lemma caps_of_state_tcb: 2427 "\<lbrakk>kheap s pos = Some (TCB tcb)\<rbrakk> \<Longrightarrow> 2428 caps_of_state s (pos,addr) = tcb_cnode_map tcb addr" 2429 by (simp add:caps_of_state_def') 2430 2431(* FIXME MOVE next to tcb_cnode_cases_simps *) 2432lemma tcb_cnode_map_simps[simp]: 2433 "tcb_cnode_map tcb (tcb_cnode_index 0) = Some (tcb_ctable tcb)" 2434 "tcb_cnode_map tcb (tcb_cnode_index (Suc 0)) = Some (tcb_vtable tcb)" 2435 "tcb_cnode_map tcb (tcb_cnode_index 2) = Some (tcb_reply tcb)" 2436 "tcb_cnode_map tcb (tcb_cnode_index 3) = Some (tcb_caller tcb)" 2437 "tcb_cnode_map tcb (tcb_cnode_index 4) = Some (tcb_ipcframe tcb)" 2438 by (simp_all add: tcb_cnode_map_def) 2439 2440(* FIXME MOVE *) 2441lemma valid_mdb_reply_mdb[elim!]: 2442 "valid_mdb s \<Longrightarrow> reply_mdb (cdt s) (caps_of_state s)" 2443 by (simp add:valid_mdb_def) 2444 2445(* FIXME MOVE *) 2446lemma invs_reply_mdb[elim!]: "invs s \<Longrightarrow> reply_mdb (cdt s) (caps_of_state s)" 2447 by (simp add:invs_def valid_state_def valid_mdb_def) 2448 2449lemma parent_of_rtrancl_no_descendant: 2450 "\<lbrakk>m \<Turnstile> pptr \<rightarrow>* ptr; descendants_of pptr m = {}\<rbrakk> \<Longrightarrow> pptr = ptr" 2451 by (fastforce simp add:rtrancl_eq_or_trancl descendants_of_def) 2452 2453(* FIXME MOVE *) 2454lemma tcb_atD: 2455 "tcb_at ptr s \<Longrightarrow> \<exists>tcb. kheap s ptr = Some (TCB tcb)" 2456 by (cases "the (kheap s ptr)";fastforce simp:obj_at_def is_tcb_def) 2457 2458(* FIXME MOVE *) 2459lemma tcb_atE: 2460 assumes hyp: "tcb_at ptr s" 2461 obtains tcb where "kheap s ptr = Some (TCB tcb)" 2462 using hyp[THEN tcb_atD] by blast 2463 2464(*FIXME MOVE *) 2465lemma tcb_atI: 2466 "kheap s ptr = Some (TCB tcb) \<Longrightarrow> tcb_at ptr s" 2467 by (simp add:obj_at_def is_tcb_def) 2468 2469 2470 2471lemma descendant_of_caller_slot: 2472 "\<lbrakk>valid_mdb s; valid_objs s; tcb_at t s\<rbrakk> \<Longrightarrow> descendants_of (t, tcb_cnode_index 3) (cdt s) = {}" 2473 apply (frule(1) tcb_caller_cap) 2474 apply (clarsimp simp add:cte_wp_at_caps_of_state is_cap_simps; elim disjE ;clarsimp) 2475 subgoal by (intro allI no_children_empty_desc[THEN iffD1] reply_cap_no_children) 2476 apply (drule valid_mdb_mdb_cte_at) 2477 apply (erule mdb_cte_at_no_descendants) 2478 apply (simp add:cte_wp_at_caps_of_state) 2479 done 2480 2481lemma cca_to_transferable_or_subject: 2482 "\<lbrakk>valid_objs s; valid_mdb s; pas_refined aag s; cdt_change_allowed' aag ptr s \<rbrakk> 2483 \<Longrightarrow> is_subject aag (fst ptr) \<or> is_transferable (caps_of_state s ptr)" 2484 apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) 2485 apply (rule all_children_parent_of_rtrancl[OF pas_refined_all_children]; blast) 2486 apply (simp add:rtrancl_eq_or_trancl,elim disjE conjE) 2487 apply (simp add:direct_call_def, elim conjE) 2488 apply (drule tcb_states_of_state_kheapD, elim exE conjE) 2489 apply (frule(2) tcb_caller_slot_empty_on_recieve ,simp) 2490 apply (cases ptr,simp) 2491 apply (simp add:caps_of_state_tcb) 2492 apply (elim tcb_states_of_state_kheapE) 2493 apply (drule(2) descendant_of_caller_slot[OF _ _ tcb_atI]) 2494 by (force simp add: descendants_of_def simp del:split_paired_All) 2495 2496lemma is_transferable_weak_derived: 2497 "weak_derived cap cap' \<Longrightarrow> is_transferable_cap cap = is_transferable_cap cap'" 2498 unfolding is_transferable.simps weak_derived_def copy_of_def same_object_as_def 2499 by (fastforce simp: is_cap_simps split:cap.splits) 2500 2501lemma aag_cdt_link_Control: 2502 "\<lbrakk> cdt s x = Some y; \<not> is_transferable(caps_of_state s x); pas_refined aag s \<rbrakk> 2503 \<Longrightarrow> (pasObjectAbs aag (fst y), Control, pasObjectAbs aag (fst x)) \<in> pasPolicy aag" 2504 by (fastforce elim: pas_refined_mem[rotated] sta_cdt) 2505 2506lemma aag_cdt_link_DeleteDerived: 2507 "\<lbrakk> cdt s x = Some y; pas_refined aag s \<rbrakk> 2508 \<Longrightarrow> (pasObjectAbs aag (fst y), DeleteDerived, pasObjectAbs aag (fst x)) \<in> pasPolicy aag" 2509 by (fastforce elim: pas_refined_mem[rotated] sta_cdt_transferable) 2510 2511lemma tcb_states_of_state_to_auth: 2512 "\<lbrakk>tcb_states_of_state s thread = Some tcbst; pas_refined aag s \<rbrakk> 2513 \<Longrightarrow> \<forall> (obj,auth) \<in> tcb_st_to_auth tcbst. 2514 (pasObjectAbs aag thread, auth, pasObjectAbs aag obj) \<in> pasPolicy aag" 2515 2516 apply clarsimp 2517 apply (erule pas_refined_mem[rotated]) 2518 apply (rule sta_ts) 2519 apply (simp add:thread_states_def) 2520 done 2521 2522lemma tcb_states_of_state_to_auth': 2523 "\<lbrakk>tcb_states_of_state s thread = Some tcbst; pas_refined aag s; 2524 (obj,auth) \<in> tcb_st_to_auth tcbst \<rbrakk> 2525 \<Longrightarrow> (pasObjectAbs aag thread, auth, pasObjectAbs aag obj) \<in> pasPolicy aag" 2526 using tcb_states_of_state_to_auth by blast 2527 2528lemma ep_recv_blocked_def: 2529 "ep_recv_blocked ep st \<longleftrightarrow> (\<exists>pl. st = BlockedOnReceive ep pl)" 2530 by (simp split: thread_state.split) 2531 2532lemma cdt_change_allowed_delete_derived: 2533 "valid_objs s \<Longrightarrow> valid_mdb s \<Longrightarrow> pas_refined aag s \<Longrightarrow> cdt_change_allowed' aag slot s 2534 \<Longrightarrow> aag_has_auth_to aag DeleteDerived (fst slot)" 2535 apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) 2536 apply (erule rtrancl_induct) 2537 apply (solves\<open>simp add: pas_refined_refl\<close>) 2538 apply (fastforce simp: cdt_parent_of_def 2539 dest: aag_cdt_link_DeleteDerived 2540 intro: aag_wellformed_delete_derived_trans) 2541 apply (clarsimp simp: direct_call_def ep_recv_blocked_def) 2542 apply (frule(1)tcb_states_of_state_to_auth) 2543 apply (elim tcb_states_of_state_kheapE) 2544 apply (frule(2) descendant_of_caller_slot[OF _ _ tcb_atI]) 2545 apply (frule(1) parent_of_rtrancl_no_descendant) 2546 apply clarsimp 2547 by (rule aag_wellformed_delete_derived'[OF _ _ pas_refined_wellformed]) 2548 2549end 2550 2551context pspace_update_eq begin 2552 2553interpretation Arch . (*FIXME: arch_split*) 2554 2555lemma integrity_update_eq[iff]: 2556 "tcb_states_of_state (f s) = tcb_states_of_state s" 2557 by (simp add: pspace tcb_states_of_state_def get_tcb_def) 2558 2559end 2560 2561subsection \<open>Various abbreviations\<close> 2562 2563context begin interpretation Arch . (*FIXME: arch_split*) 2564 2565definition label_owns_asid_slot :: "'a PAS \<Rightarrow> 'a \<Rightarrow> asid \<Rightarrow> bool" 2566where 2567 "label_owns_asid_slot aag l asid \<equiv> 2568 (l, Control, pasASIDAbs aag asid) \<in> pasPolicy aag" 2569 2570definition cap_links_asid_slot :: "'a PAS \<Rightarrow> 'a \<Rightarrow> cap \<Rightarrow> bool" 2571where 2572 "cap_links_asid_slot aag l cap \<equiv> (\<forall>asid \<in> cap_asid' cap. 2573 label_owns_asid_slot aag l asid)" 2574 2575abbreviation is_subject_asid :: "'a PAS \<Rightarrow> asid \<Rightarrow> bool" 2576where 2577 "is_subject_asid aag asid \<equiv> pasASIDAbs aag asid = pasSubject aag" 2578 2579lemma clas_no_asid: 2580 "cap_asid' cap = {} \<Longrightarrow> cap_links_asid_slot aag l cap" 2581 unfolding cap_links_asid_slot_def by simp 2582 2583definition cap_links_irq 2584where 2585 "cap_links_irq aag l cap \<equiv> 2586 \<forall>irq \<in> cap_irqs_controlled cap. (l, Control, pasIRQAbs aag irq) \<in> pasPolicy aag" 2587 2588lemma cli_no_irqs: 2589 "cap_irqs_controlled cap = {} \<Longrightarrow> cap_links_irq aag l cap" 2590 unfolding cap_links_irq_def by simp 2591 2592abbreviation is_subject_irq :: "'a PAS \<Rightarrow> irq \<Rightarrow> bool" 2593where 2594 "is_subject_irq aag irq \<equiv> pasIRQAbs aag irq = pasSubject aag" 2595 2596definition aag_cap_auth :: "'a PAS \<Rightarrow> 'a \<Rightarrow> cap \<Rightarrow> bool" 2597where 2598 "aag_cap_auth aag l cap \<equiv> 2599 (\<forall>x \<in> obj_refs cap. \<forall>auth \<in> cap_auth_conferred cap. (l, auth, pasObjectAbs aag x) \<in> pasPolicy aag) 2600 \<and> (\<forall>x \<in> untyped_range cap. (l, Control, pasObjectAbs aag x) \<in> pasPolicy aag) 2601 \<and> cap_links_asid_slot aag l cap \<and> cap_links_irq aag l cap" 2602 2603abbreviation pas_cap_cur_auth :: "'a PAS \<Rightarrow> cap \<Rightarrow> bool" 2604where 2605 "pas_cap_cur_auth aag cap \<equiv> aag_cap_auth aag (pasSubject aag) cap" 2606 2607subsection \<open>Random lemmas that belong here\<close> 2608 2609crunch integrity_autarch: as_user "integrity aag X st" 2610 2611lemma owns_thread_owns_cspace: 2612 "\<lbrakk> is_subject aag thread; pas_refined aag s; get_tcb thread s = Some tcb; is_cnode_cap (tcb_ctable tcb); x \<in> obj_refs (tcb_ctable tcb)\<rbrakk> 2613 \<Longrightarrow> is_subject aag x" 2614 apply (drule get_tcb_SomeD) 2615 apply (drule cte_wp_at_tcbI[where t="(thread, tcb_cnode_index 0)" and P="\<lambda>cap. cap = tcb_ctable tcb", simplified]) 2616 apply (auto simp: cte_wp_at_caps_of_state is_cap_simps cap_auth_conferred_def 2617 elim: caps_of_state_pasObjectAbs_eq [where p = "(thread, tcb_cnode_index 0)"]) 2618 done 2619 2620 2621 2622lemma is_subject_into_is_subject_asid: 2623 "\<lbrakk> cap_links_asid_slot aag (pasObjectAbs aag p) cap; is_subject aag p; pas_refined aag s; 2624 asid \<in> cap_asid' cap \<rbrakk> 2625 \<Longrightarrow> is_subject_asid aag asid" 2626 apply (clarsimp simp add: cap_links_asid_slot_def label_owns_asid_slot_def) 2627 apply (drule (1) bspec) 2628 apply (drule (1) pas_refined_Control) 2629 apply simp 2630 done 2631 2632(* MOVE *) 2633lemma clas_caps_of_state: 2634 "\<lbrakk> caps_of_state s slot = Some cap; pas_refined aag s \<rbrakk> \<Longrightarrow> cap_links_asid_slot aag (pasObjectAbs aag (fst slot)) cap" 2635apply (clarsimp simp add: cap_links_asid_slot_def label_owns_asid_slot_def pas_refined_def) 2636apply (blast dest: state_asids_to_policy_aux.intros) 2637done 2638 2639lemma as_user_state_vrefs[wp]: 2640 "\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> as_user t f \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>" 2641 apply (simp add: as_user_def) 2642 apply (wpsimp wp: set_object_wp) 2643 apply (clarsimp simp: state_vrefs_def vs_refs_no_global_pts_def get_tcb_def 2644 elim!: rsubst[where P=P, OF _ ext] 2645 split: option.split_asm Structures_A.kernel_object.split) 2646 done 2647 2648lemma as_user_tcb_states[wp]: 2649 "\<lbrace>\<lambda>s. P (tcb_states_of_state s)\<rbrace> as_user t f \<lbrace>\<lambda>rv s. P (tcb_states_of_state s)\<rbrace>" 2650 apply (simp add: as_user_def) 2651 apply (wpsimp wp: set_object_wp) 2652 apply (clarsimp simp: thread_states_def get_tcb_def tcb_states_of_state_def 2653 elim!: rsubst[where P=P, OF _ ext] split: option.split) 2654 done 2655 2656lemma as_user_thread_state[wp]: 2657 "\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> as_user t f \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>" 2658 apply (simp add: thread_states_def) 2659 apply wp 2660 done 2661 2662lemma as_user_thread_bound_ntfn[wp]: 2663 "\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> as_user t f \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>" 2664 apply (simp add: as_user_def set_object_def split_def thread_bound_ntfns_def) 2665 apply (wp get_object_wp) 2666 apply (clarsimp simp: thread_states_def get_tcb_def 2667 elim!: rsubst[where P=P, OF _ ext] split: option.split) 2668 done 2669 2670lemma tcb_domain_map_wellformed_lift: 2671 assumes 1: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>" 2672 shows "\<lbrace>tcb_domain_map_wellformed aag\<rbrace> f \<lbrace>\<lambda>rv. tcb_domain_map_wellformed aag\<rbrace>" 2673 by (rule 1) 2674 2675lemma as_user_pas_refined[wp]: 2676 "\<lbrace>pas_refined aag\<rbrace> as_user t f \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 2677apply (simp add: pas_refined_def state_objs_to_policy_def) 2678apply (rule hoare_pre) 2679 apply wps 2680 apply wp 2681apply simp 2682done 2683 2684(* **************************************** *) 2685 2686subsection\<open>Random lemmas that belong elsewhere.\<close> 2687 2688(* FIXME: move *) 2689lemma bang_0_in_set: 2690 "xs \<noteq> [] \<Longrightarrow> xs ! 0 \<in> set xs" 2691 apply(fastforce simp: in_set_conv_nth) 2692 done 2693 2694(* FIXME: move *) 2695lemma update_one_strg: 2696 "((b \<longrightarrow> P c v) \<and> (\<not> b \<longrightarrow> (\<forall>v'. f c' = Some v' \<longrightarrow> P c v'))) 2697 \<longrightarrow> 2698 ((f(c := if b then Some v else f c')) x = Some y \<and> f x \<noteq> Some y \<longrightarrow> P x y)" 2699 by auto 2700 2701(* FIXME: move *) 2702lemma hoare_gen_asm2: 2703 assumes a: "P \<Longrightarrow> \<lbrace>\<top>\<rbrace> f \<lbrace>Q\<rbrace>" 2704 shows "\<lbrace>K P\<rbrace> f \<lbrace>Q\<rbrace>" 2705 using a by (fastforce simp: valid_def) 2706 2707(* FIXME: move *) 2708lemma hoare_vcg_all_liftE: 2709 "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, \<lbrace>Q' x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, \<lbrace>\<lambda>rv s. \<forall>x. Q' x rv s\<rbrace>" 2710 unfolding validE_def 2711 apply (rule hoare_post_imp [where Q = "\<lambda>v s. \<forall>x. case v of Inl e \<Rightarrow> Q' x e s | Inr r \<Rightarrow> Q x r s"]) 2712 apply (clarsimp split: sum.splits) 2713 apply (erule hoare_vcg_all_lift) 2714 done 2715 2716(* FIXME: eliminate *) 2717lemma hoare_weak_lift_impE: 2718 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. R \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. R \<longrightarrow> Q rv s\<rbrace>, \<lbrace>\<lambda>rv s. R \<longrightarrow> Q' rv s\<rbrace>" 2719 by (rule wp_throw_const_impE) 2720 2721(* FIXME: move *) 2722lemma hoare_use_ex_R: 2723 "(\<And>x. \<lbrace>P x and Q \<rbrace> f \<lbrace>R\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> Q s \<rbrace> f \<lbrace>R\<rbrace>, -" 2724 unfolding validE_R_def validE_def valid_def by fastforce 2725 2726(* FIXME: move *) 2727lemma mapM_x_and_const_wp: 2728 assumes f: "\<And>v. \<lbrace>P and K (Q v)\<rbrace> f v \<lbrace>\<lambda>rv. P\<rbrace>" 2729 shows "\<lbrace>P and K (\<forall>v \<in> set vs. Q v)\<rbrace> mapM_x f vs \<lbrace>\<lambda>rv. P\<rbrace>" 2730 apply (induct vs) 2731 apply (simp add: mapM_x_Nil) 2732 apply (simp add: mapM_x_Cons) 2733 apply (wp f | assumption | simp)+ 2734 done 2735 2736(* stronger *) 2737(* FIXME: MOVE *) 2738lemma ep_queued_st_tcb_at': 2739 "\<And>P. \<lbrakk>ko_at (Endpoint ep) ptr s; (t, rt) \<in> ep_q_refs_of ep; 2740 valid_objs s; sym_refs (state_refs_of s); 2741 \<And>pl pl'. P (Structures_A.BlockedOnSend ptr pl) \<and> P (Structures_A.BlockedOnReceive ptr pl') \<rbrakk> 2742 \<Longrightarrow> st_tcb_at P t s" 2743 apply (case_tac ep, simp_all) 2744 apply (frule(1) sym_refs_ko_atD, clarsimp, erule (1) my_BallE, 2745 clarsimp simp: st_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ 2746 done 2747 2748(* Sometimes we only care about one of the queues. *) 2749(* FIXME: move *) 2750lemma ep_rcv_queued_st_tcb_at: 2751 "\<And>P. \<lbrakk>ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep; 2752 valid_objs s; sym_refs (state_refs_of s); 2753 \<And>pl. P (Structures_A.BlockedOnReceive epptr pl); 2754 kheap s' t = kheap s t\<rbrakk> 2755 \<Longrightarrow> st_tcb_at P t s'" 2756 apply (case_tac ep, simp_all) 2757 apply (subgoal_tac "st_tcb_at P t s") 2758 apply (simp add: st_tcb_at_def obj_at_def) 2759 apply (frule(1) sym_refs_ko_atD, clarsimp, erule (1) my_BallE, 2760 clarsimp simp: st_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ 2761 done 2762 2763(* FIXME: move. *) 2764lemma ntfn_queued_st_tcb_at': 2765 "\<And>P. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; (t, rt) \<in> ntfn_q_refs_of (ntfn_obj ntfn); 2766 valid_objs s; sym_refs (state_refs_of s); 2767 P (Structures_A.BlockedOnNotification ntfnptr) \<rbrakk> 2768 \<Longrightarrow> st_tcb_at P t s" 2769 apply (case_tac "ntfn_obj ntfn", simp_all) 2770 apply (frule(1) sym_refs_ko_atD) 2771 apply (clarsimp) 2772 apply (erule_tac y="(t, NTFNSignal)" in my_BallE, clarsimp) 2773 apply (clarsimp simp: pred_tcb_at_def refs_of_rev elim!: obj_at_weakenE)+ 2774 done 2775 2776(* FIXME: move *) 2777lemma case_prod_wp: 2778 "(\<And>a b. x = (a, b) \<Longrightarrow> \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>) 2779 \<Longrightarrow> \<lbrace>P (fst x) (snd x)\<rbrace> case_prod f x \<lbrace>Q\<rbrace>" 2780 by (cases x, simp) 2781 2782(* FIXME: move *) 2783lemma case_sum_wp: 2784 "\<lbrakk> (\<And>a. x = Inl a \<Longrightarrow> \<lbrace>P a\<rbrace> f a \<lbrace>Q\<rbrace>); 2785 (\<And>a. x = Inr a \<Longrightarrow> \<lbrace>P' a\<rbrace> g a \<lbrace>Q\<rbrace>) \<rbrakk> 2786 \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>a. x = Inl a \<longrightarrow> P a s) \<and> (\<forall>a. x = Inr a \<longrightarrow> P' a s)\<rbrace> case_sum f g x \<lbrace>Q\<rbrace>" 2787 by (cases x, simp_all) 2788 2789(* MOVE *) 2790crunch arm_asid_table_inv [wp]: store_pte "\<lambda>s. P (arm_asid_table (arch_state s))" 2791 2792lemma st_tcb_at_to_thread_states: 2793 "st_tcb_at P t s \<Longrightarrow> \<exists>st. P st \<and> thread_states s t = tcb_st_to_auth st" 2794 by (fastforce simp: st_tcb_def2 thread_states_def tcb_states_of_state_def) 2795 2796lemma aag_Control_into_owns: 2797 "\<lbrakk> aag_has_auth_to aag Control p; pas_refined aag s \<rbrakk> \<Longrightarrow> is_subject aag p" 2798 apply (drule (1) pas_refined_Control) 2799 apply simp 2800 done 2801 2802lemma aag_has_Control_iff_owns: 2803 "pas_refined aag s \<Longrightarrow> (aag_has_auth_to aag Control x) = (is_subject aag x)" 2804 apply (rule iffI) 2805 apply (erule (1) aag_Control_into_owns) 2806 apply (simp add: pas_refined_refl) 2807 done 2808 2809lemma aag_Control_owns_strg: 2810 "pas_wellformed aag \<and> is_subject aag v \<longrightarrow> aag_has_auth_to aag Control v" 2811 by (clarsimp simp: aag_wellformed_refl) 2812 2813(* **************************************** *) 2814 2815subsection \<open>Policy entailments\<close> 2816 2817lemma owns_ep_owns_receivers: 2818 "\<lbrakk>\<forall>auth. aag_has_auth_to aag auth epptr; pas_refined aag s; invs s; 2819 ko_at (Endpoint ep) epptr s; (t, EPRecv) \<in> ep_q_refs_of ep\<rbrakk> 2820 \<Longrightarrow> is_subject aag t" 2821 apply (drule (1) ep_rcv_queued_st_tcb_at [where P = "receive_blocked_on epptr"]) 2822 apply clarsimp 2823 apply clarsimp 2824 apply clarsimp 2825 apply (rule refl) 2826 apply (drule st_tcb_at_to_thread_states) 2827 apply (clarsimp simp: receive_blocked_on_def2) 2828 apply (drule spec [where x = Grant]) 2829 apply (frule aag_wellformed_grant_Control_to_recv 2830 [OF _ _ pas_refined_wellformed]) 2831 apply (rule pas_refined_mem [OF sta_ts]) 2832 apply fastforce 2833 apply assumption+ 2834 apply (erule (1) aag_Control_into_owns) 2835 done 2836 2837(* MOVE *) 2838lemma cli_caps_of_state: 2839 "\<lbrakk> caps_of_state s slot = Some cap; pas_refined aag s \<rbrakk> \<Longrightarrow> cap_links_irq aag (pasObjectAbs aag (fst slot)) cap" 2840apply (clarsimp simp add: cap_links_irq_def pas_refined_def) 2841apply (blast dest: state_irqs_to_policy_aux.intros) 2842done 2843 2844(* MOVE *) 2845lemma cap_auth_caps_of_state: 2846 "\<lbrakk> caps_of_state s p = Some cap; pas_refined aag s \<rbrakk> 2847 \<Longrightarrow> aag_cap_auth aag (pasObjectAbs aag (fst p)) cap" 2848 unfolding aag_cap_auth_def 2849 apply (intro conjI) 2850 apply clarsimp 2851 apply (drule (2) sta_caps) 2852 apply (drule_tac f="pasObjectAbs aag" in auth_graph_map_memI[OF _ refl refl]) 2853 apply (fastforce simp: pas_refined_def) 2854 apply clarsimp 2855 apply (drule (2) sta_untyped [THEN pas_refined_mem] ) 2856 apply simp 2857 apply (drule (1) clas_caps_of_state) 2858 apply simp 2859 apply (drule (1) cli_caps_of_state) 2860 apply simp 2861 done 2862 2863lemma cap_cur_auth_caps_of_state: 2864 "\<lbrakk> caps_of_state s p = Some cap; pas_refined aag s; is_subject aag (fst p) \<rbrakk> 2865 \<Longrightarrow> pas_cap_cur_auth aag cap" 2866 by (metis cap_auth_caps_of_state) 2867 2868subsection \<open>Integrity monotony over subjects\<close> 2869 2870lemmas new_range_subset' = aligned_range_offset_subset 2871lemmas ptr_range_subset = new_range_subset' [folded ptr_range_def] 2872 2873lemma pbfs_less_wb: 2874 "pageBitsForSize x < word_bits" 2875 by (cases x, simp_all add: word_bits_def) 2876 2877lemma ipcframe_subset_page: 2878 "\<lbrakk>valid_objs s; get_tcb p s = Some tcb; 2879 tcb_ipcframe tcb = cap.ArchObjectCap (arch_cap.PageCap d p' R vms xx); 2880 x \<in> ptr_range (p' + (tcb_ipc_buffer tcb && mask (pageBitsForSize vms))) msg_align_bits \<rbrakk> 2881 \<Longrightarrow> x \<in> ptr_range p' (pageBitsForSize vms)" 2882 apply (frule (1) valid_tcb_objs) 2883 apply (clarsimp simp add: valid_tcb_def ran_tcb_cap_cases) 2884 apply (erule set_mp[rotated]) 2885 apply (rule ptr_range_subset) 2886 apply (simp add: valid_cap_def cap_aligned_def) 2887 apply (simp add: valid_tcb_def valid_ipc_buffer_cap_def is_aligned_andI1 split:bool.splits) 2888 apply (rule order_trans [OF _ pbfs_atleast_pageBits]) 2889 apply (simp add: msg_align_bits pageBits_def) 2890 apply (rule and_mask_less') 2891 apply (simp add: pbfs_less_wb [unfolded word_bits_conv]) 2892 done 2893 2894lemma trm_ipc': 2895 "\<lbrakk> pas_refined aag s; valid_objs s; case_option False can_receive_ipc (tcb_states_of_state s p'); 2896 (tcb_states_of_state s' p') = Some Structures_A.Running; 2897 p \<in> auth_ipc_buffers s p' \<rbrakk> \<Longrightarrow> 2898 integrity_mem aag subjects p 2899 (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X 2900 (underlying_memory (machine_state s) p) 2901 (underlying_memory (machine_state s') p)" 2902 apply (cases "pasObjectAbs aag p' \<in> subjects") 2903 apply (rule trm_write) 2904 apply (clarsimp simp: auth_ipc_buffers_member_def) 2905 apply (frule pas_refined_mem[rotated]) 2906 apply (erule sta_caps, simp) 2907 apply (erule(3) ipcframe_subset_page) 2908 apply (simp add: cap_auth_conferred_def vspace_cap_rights_to_auth_def 2909 is_page_cap_def) 2910 apply fastforce 2911 apply fastforce 2912 by (rule trm_ipc) 2913 2914 2915lemma tcb_bound_notification_reset_integrity_mono: 2916 "\<lbrakk> tcb_bound_notification_reset_integrity ntfn ntfn' S aag ; S \<subseteq> T\<rbrakk> 2917 \<Longrightarrow> tcb_bound_notification_reset_integrity ntfn ntfn' T aag" 2918 unfolding tcb_bound_notification_reset_integrity_def by blast 2919 2920lemma reply_cap_deletion_integrity_mono: 2921 "\<lbrakk> reply_cap_deletion_integrity S aag cap cap' ; S \<subseteq> T\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity T aag cap cap'" 2922 by (blast intro: reply_cap_deletion_integrity_intros elim: reply_cap_deletion_integrityE) 2923 2924lemma cnode_integrity_mono: 2925 "\<lbrakk> cnode_integrity S aag cont cont' ; S \<subseteq> T\<rbrakk> \<Longrightarrow> cnode_integrity T aag cont cont'" 2926 by (blast intro!: cnode_integrityI elim: cnode_integrityE dest:reply_cap_deletion_integrity_mono) 2927 2928lemma asid_pool_integrity_mono: 2929 "\<lbrakk> asid_pool_integrity S aag cont cont' ; S \<subseteq> T\<rbrakk> \<Longrightarrow> asid_pool_integrity T aag cont cont'" 2930 unfolding asid_pool_integrity_def by fastforce 2931 2932lemma cdt_change_allowed_mono: 2933 "\<lbrakk>cdt_change_allowed aag S (cdt s) (tcb_states_of_state s) ptr; S \<subseteq> T \<rbrakk> \<Longrightarrow> 2934 cdt_change_allowed aag T (cdt s) (tcb_states_of_state s) ptr" 2935 unfolding cdt_change_allowed_def cdt_direct_change_allowed.simps direct_call_def by blast 2936 2937 2938 2939lemmas rtranclp_monoE = rtranclp_mono[THEN predicate2D,rotated,OF _ predicate2I] 2940 2941lemma integrity_mono: 2942 "\<lbrakk> integrity_subjects S aag activate X s s'; S \<subseteq> T; 2943 pas_refined aag s; valid_objs s \<rbrakk> 2944 \<Longrightarrow> integrity_subjects T aag activate X s s'" 2945 apply (clarsimp simp: integrity_subjects_def simp del:split_paired_All) 2946 apply (rule conjI) 2947 apply clarsimp 2948 apply (drule_tac x=x in spec)+ 2949 apply (simp only: integrity_obj_def) 2950 apply (erule rtranclp_monoE) 2951 apply (erule integrity_obj_atomic.cases[OF _ integrity_obj_atomic.intros]; 2952 auto simp: indirect_send_def direct_send_def direct_call_def direct_reply_def 2953 elim: asid_pool_integrity_mono reply_cap_deletion_integrity_mono 2954 cnode_integrity_mono) 2955 apply (rule conjI) 2956 apply clarsimp 2957 apply (drule_tac x=x in spec)+ 2958 apply (erule integrity_eobj.cases; auto intro: integrity_eobj.intros) 2959 apply (rule conjI) 2960 apply clarsimp 2961 apply (drule_tac x=x in spec, erule integrity_mem.cases; 2962 blast intro: integrity_mem.intros trm_ipc') 2963 apply (rule conjI) 2964 apply clarsimp 2965 apply (drule_tac x=x in spec, erule integrity_device.cases; 2966 blast intro: integrity_device.intros) 2967 apply (rule conjI) 2968 apply (intro allI) 2969 apply (drule_tac x=x in spec)+ 2970 apply (erule integrity_cdtE; auto elim: cdt_change_allowed_mono) 2971 apply (rule conjI) 2972 apply (intro allI) 2973 apply (drule_tac x=x in spec)+ 2974 apply (erule integrity_cdt_listE; 2975 auto elim!: weaken_filter_eq' intro: integrity_cdt_list_intros 2976 elim: cdt_change_allowed_mono) 2977 apply (rule conjI) 2978 apply (fastforce simp: integrity_interrupts_def) 2979 apply (rule conjI) 2980 apply (fastforce simp: integrity_asids_def) 2981 apply (clarsimp simp: integrity_ready_queues_def) 2982 apply blast 2983 done 2984 2985subsection\<open>Access control do not care about machine_state\<close> 2986 2987lemma integrity_irq_state_independent[intro!, simp]: 2988 "integrity x y z (s\<lparr>machine_state := 2989 machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) 2990 = integrity x y z s" 2991 by (simp add: integrity_def) 2992 2993lemma state_objs_to_policy_irq_state_independent[intro!, simp]: 2994 "state_objs_to_policy (s\<lparr>machine_state := 2995 machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) 2996 = state_objs_to_policy s" 2997 by (simp add: state_objs_to_policy_def) 2998 2999lemma tcb_domain_map_wellformed_independent[intro!, simp]: 3000 "tcb_domain_map_wellformed aag (s\<lparr>machine_state := 3001 machine_state s\<lparr>irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>) 3002 = tcb_domain_map_wellformed aag s" 3003 by (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def) 3004 3005lemma pas_refined_irq_state_independent[intro!, simp]: 3006 "pas_refined x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) 3007 = pas_refined x s" 3008 by (simp add: pas_refined_def) 3009 3010 3011subsection\<open>Transitivity of integrity lemmas and tactics\<close> 3012 3013lemma integrity_trans_start: 3014 "(\<And> s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. integrity aag X s\<rbrace>) 3015 \<Longrightarrow> \<lbrace>integrity aag X st and P\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 3016 unfolding spec_valid_def valid_def using integrity_trans 3017 by simp blast 3018 3019method integrity_trans_start 3020 = ((simp only: and_assoc[symmetric])?, rule integrity_trans_start[rotated]) 3021 3022(* Q should be explicitly supplied, if not, use wp_integrity_clean' *) 3023lemma wp_integrity_clean: 3024 "\<lbrakk>\<And>s. Q s \<Longrightarrow> integrity aag X s (g s); 3025 \<lbrace> P \<rbrace> f \<lbrace>\<lambda>_. integrity aag X st and Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>_ s. integrity aag X st (g s) \<rbrace> " 3026 by (rule hoare_post_imp[of "\<lambda>_. integrity aag X st and Q"]) 3027 (fastforce elim: integrity_trans) 3028 3029lemmas wp_integrity_clean'= wp_integrity_clean[of \<top>, simplified] 3030 3031 3032end 3033 3034end 3035