theory ArchNoninterference

lemma partitionIntegrity_subjectAffects_aobj':
  "\<lbrakk> kheap s x = Some (ArchObj ao); ao \<noteq> ao'; pas_refined aag s;
     silc_inv aag st s; pas_wellformed_noninterference aag;
     arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
                               {pasSubject aag} (pasObjectAbs aag x) ao ao' \<rbrakk>
     \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x)" unfolding arch_integrity_obj_atomic.simps asid_pool_integrity_def apply clarsimp apply (rule ccontr) apply (drule fun_noteqD) apply (erule exE, rename_tac r) apply (drule_tac x=r in spec) apply (clarsimp dest!: not_sym[where t=None]) apply (subgoal_tac "is_subject aag x", force intro: affects_lrefl) apply (frule (1) aag_Control_into_owns) apply (frule (2) asid_pool_into_aag) apply simp apply (frule (1) pas_wellformed_noninterference_control_to_eq) by (fastforce elim!: silc_inv_cnode_onlyE obj_atE simp: is_cap_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (ArchObj ao); ao \<noteq> ao'; pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) {pasSubject aag} (pasObjectAbs aag x) ao ao'\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s x = Some (ArchObj ao); ao \<noteq> ao'; pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; \<exists>pool pool'. ao = ASIDPool pool \<and> ao' = ASIDPool pool' \<and> (\<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None \<and> aag_subjects_have_auth_to {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) Control (the (pool x)))\<rbrakk> \<Longrightarrow> subject_can_affect_label_directly aag (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. \<And>pool pool'. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; \<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (pool x))) \<in> pasPolicy aag; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag)\<rbrakk> \<Longrightarrow> pool = pool' proof (prove)
goal (1 subgoal):
 1. \<And>pool pool'. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; \<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (pool x))) \<in> pasPolicy aag; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool \<noteq> pool'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>pool pool'. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; \<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (pool x))) \<in> pasPolicy aag; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); \<exists>a. pool a \<noteq> pool' a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; \<forall>x. pool' x \<noteq> pool x \<longrightarrow> pool' x = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (pool x))) \<in> pasPolicy aag; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r \<noteq> pool' r\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r \<noteq> pool' r; pool' r \<noteq> pool r \<longrightarrow> pool' r = None \<and> (pasSubject aag, Control, pasObjectAbs aag (the (pool r))) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag; is_subject aag y\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasObjectAbs aag y) \<in> pasPolicy aag; is_subject aag y; (pasObjectAbs aag x, Control, pasObjectAbs aag y) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (1 subgoal):
 1. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag; is_subject aag y; (pasObjectAbs aag x, Control, pasSubject aag) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject aag x proof (prove)
goal (2 subgoals):
 1. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag; is_subject aag y; (pasObjectAbs aag x, Control, pasSubject aag) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<noteq> SilcLabel
 2. \<And>pool pool' r y. \<lbrakk>kheap s x = Some (ArchObj (ASIDPool pool)); pas_refined aag s; silc_inv aag st s; pas_wellformed_noninterference aag; ao = ASIDPool pool; ao' = ASIDPool pool'; pasObjectAbs aag x \<notin> subjectAffects (pasPolicy aag) (pasSubject aag); pool r = Some y; pool' r = None; (pasSubject aag, Control, pasSubject aag) \<in> pasPolicy aag; is_subject aag y; (pasObjectAbs aag x, Control, pasSubject aag) \<in> pasPolicy aag; is_subject aag x\<rbrakk> \<Longrightarrow> is_subject aag x