theory Noninterference

lemma reads_g_affects_equiv_sameFor:
  "\<lbrakk> reads_equiv_f_g aag s s' \<and> affects_equiv aag (OrdinaryLabel l) s s';
     pas_cur_domain aag s; silc_inv aag st' st'';
     Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag)) \<rbrakk>
     \<Longrightarrow> (((uc,s),mode),((uc,s'),mode)) \<in> same_for aag (Partition l)" apply (clarsimp simp: partsSubjectAffects_def) apply (simp add: affects_equiv_def2 sameFor_def sameFor_subject_def) apply (frule pasSubject_not_SilcLabel) apply (simp add: reads_equiv_f_g_def reads_equiv_def2 silc_dom_equiv_def) apply (erule states_equiv_for_guard_imp) apply (simp add: aag_can_affect_label_def label_can_affect_partition_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_f_g aag s s' \<and> affects_equiv aag (OrdinaryLabel l) s s'; pas_cur_domain aag s; silc_inv aag st' st''; Partition l \<in> partsSubjectAffects (pasPolicy aag) (label_of (pasSubject aag))\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc, s'), mode) \<in> same_for aag (Partition l) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag s; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) (OrdinaryLabel l); reads_equiv_f_g aag s s'; affects_equiv aag (OrdinaryLabel l) s s'\<rbrakk> \<Longrightarrow> (((uc, s), mode), (uc, s'), mode) \<in> same_for aag (Partition l) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag s; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) (OrdinaryLabel l); reads_equiv_f_g aag s s'; states_equiv_for (aag_can_affect aag (OrdinaryLabel l)) (aag_can_affect_irq aag (OrdinaryLabel l)) (aag_can_affect_asid aag (OrdinaryLabel l)) (aag_can_affect_domain aag (OrdinaryLabel l)) s s'\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) s s' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) = {} \<longrightarrow> pasDomainAbs aag (cur_domain s') \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain s = cur_domain s' \<and> globals_equiv s s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag s; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (OrdinaryLabel (label_of (pasSubject aag))) (OrdinaryLabel l); reads_equiv_f_g aag s s'; states_equiv_for (aag_can_affect aag (OrdinaryLabel l)) (aag_can_affect_irq aag (OrdinaryLabel l)) (aag_can_affect_asid aag (OrdinaryLabel l)) (aag_can_affect_domain aag (OrdinaryLabel l)) s s'; pasSubject aag \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) s s' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) = {} \<longrightarrow> pasDomainAbs aag (cur_domain s') \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) \<longrightarrow> cur_domain s = cur_domain s' \<and> globals_equiv s s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pas_cur_domain aag s'; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l); states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> globals_equiv s s' \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'; states_equiv_for (aag_can_affect aag (OrdinaryLabel l)) (aag_can_affect_irq aag (OrdinaryLabel l)) (aag_can_affect_asid aag (OrdinaryLabel l)) (aag_can_affect_domain aag (OrdinaryLabel l)) s s'; pasSubject aag \<noteq> SilcLabel\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)) (\<lambda>x. pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}) s s' proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>pas_cur_domain aag s'; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l); states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> globals_equiv s s' \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'; pasSubject aag \<noteq> SilcLabel; pasObjectAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)\<rbrakk> \<Longrightarrow> aag_can_affect aag (OrdinaryLabel l) x
 2. \<And>x. \<lbrakk>pas_cur_domain aag s'; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l); states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> globals_equiv s s' \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'; pasSubject aag \<noteq> SilcLabel; pasIRQAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)\<rbrakk> \<Longrightarrow> aag_can_affect_irq aag (OrdinaryLabel l) x
 3. \<And>x. \<lbrakk>pas_cur_domain aag s'; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l); states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> globals_equiv s s' \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'; pasSubject aag \<noteq> SilcLabel; pasASIDAbs aag x \<in> subjectReads (pasPolicy aag) (OrdinaryLabel l)\<rbrakk> \<Longrightarrow> aag_can_affect_asid aag (OrdinaryLabel l) x
 4. \<And>x. \<lbrakk>pas_cur_domain aag s'; silc_inv aag st' st''; label_can_affect_partition (pasPolicy aag) (pasSubject aag) (OrdinaryLabel l); states_equiv_for (aag_can_read aag) (aag_can_read_irq aag) (aag_can_read_asid aag) (aag_can_read_domain aag) s s' \<and> cur_thread s = cur_thread s' \<and> cur_domain s = cur_domain s' \<and> scheduler_action s = scheduler_action s' \<and> work_units_completed s = work_units_completed s' \<and> equiv_irq_state (machine_state s) (machine_state s') \<and> globals_equiv s s' \<and> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap s s'; pasSubject aag \<noteq> SilcLabel; pasDomainAbs aag x \<inter> subjectReads (pasPolicy aag) (OrdinaryLabel l) \<noteq> {}\<rbrakk> \<Longrightarrow> aag_can_affect_domain aag (OrdinaryLabel l) x proof (prove)
goal:
No subgoals!