AArch64 Information Flow

proof/ROOT

@@ -159,8 +159,7 @@ session InfoFlowC in "infoflow/refine" = InfoFlowCBase +
   directories
     "$L4V_ARCH"
   theories
-    "Noninterference_Refinement"
-    "Example_Valid_StateH"
+    "InfoFlowC_Image_Toplevel"
 
 (*
  * capDL

proof/access-control/AARCH64/ArchAccess.thy

@@ -133,8 +133,8 @@ where
      | (Some vcpu, None) \<Rightarrow> Some (vcpu_mask n vcpu) \<comment> \<open>No current VCPU\<close>
      | (Some vcpu, Some enabled) \<Rightarrow> Some (vcpu_mask n
          (vcpu\<lparr>vcpu_regs := \<lambda>reg. if vcpuRegSavedWhenDisabled reg \<and> \<not>enabled
-                                       then vcpu_regs vcpu reg \<comment> \<open>Register saved when VCPU disabled\<close>
-                                       else vcpu_regs vst reg,
+                                  then vcpu_regs vcpu reg \<comment> \<open>Register saved when VCPU disabled\<close>
+                                  else vcpu_regs vst reg,
                     vcpu_vgic := (vcpu_vgic vcpu)
                       \<lparr>vgic_hcr := if \<not>enabled
                                    then vgic_hcr (vcpu_vgic vcpu) \<comment> \<open>Saved when VCPU disabled\<close>
@@ -143,8 +143,18 @@ where
                        vgic_apr := vgic_apr (vcpu_vgic vst),
                        vgic_lr := vgic_lr (vcpu_vgic vst)\<rparr>\<rparr>))"
 
+(* A vcpu's vgic_lr field is a total function from nats to virqs, with the domain restricted only
+   in practice via the arm_gicvcpu_numlistregs parameter. To establish true equivalence between
+   vcpus in the InfoFlow proofs, we prove here that these out-of-bounds registers aren't touched. *)
+definition vcpu_extra_lrs :: "nat \<Rightarrow> vcpu option \<rightharpoonup> (nat \<Rightarrow> virq)" where
+  "vcpu_extra_lrs n vopt \<equiv>
+     case vopt of
+       None \<Rightarrow> None
+     | Some vcpu \<Rightarrow> Some (\<lambda>r. if r \<ge> n then vgic_lr (vcpu_vgic vcpu) r else undefined)"
+
 definition vcpu_integrity where
    "vcpu_integrity hv hv' cv cv' n n' vopt vopt' \<equiv>
+      vcpu_extra_lrs n vopt = vcpu_extra_lrs n' vopt' \<and>
       vcpu_of_state hv cv n vopt = vcpu_of_state hv' cv' n' vopt'"
 
 definition integrity_hyp_2 ::

proof/access-control/AARCH64/ArchAccess_AC.thy

@@ -333,7 +333,7 @@ lemma integrity_hyp_ao_upd:
   "\<lbrakk> ao p = Some ako; vcpu_of ako = None; vcpu_of ako' = None;
      integrity_hyp_2 aag subjects x ms ms' as as' ao ao' \<rbrakk>
      \<Longrightarrow> integrity_hyp_2 aag subjects x ms ms' as as' ao (ao'(p \<mapsto> ako')) "
-  unfolding integrity_hyp_def vcpu_integrity_def vcpu_of_state_def opt_map_def
+  unfolding integrity_hyp_def vcpu_integrity_def vcpu_extra_lrs_def vcpu_of_state_def opt_map_def
   by (case_tac "x = p"; clarsimp; auto split: option.splits)+
 
 end

proof/access-control/AARCH64/ArchArch_AC.thy

@@ -2164,13 +2164,57 @@ lemma vcpu_proj_arch_state_update[simp]:
 crunch vcpu_switch
   for arm_gicvcpu_numlistregs[wp]: "\<lambda>s. P (arm_gicvcpu_numlistregs (arch_state s))"
 
+lemma vcpu_update_extra_lrs[wp]:
+  "\<lbrace>\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x)) \<and>
+          (\<forall>v r. arm_gicvcpu_numlistregs (arch_state s) \<le> r
+                 \<longrightarrow> vgic_lr (vcpu_vgic (f v)) r = vgic_lr (vcpu_vgic v) r)\<rbrace>
+   vcpu_update vr f
+   \<lbrace>\<lambda>_ s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x))\<rbrace>"
+  unfolding vcpu_update_def
+  apply (wpsimp wp: set_vcpu_wp get_vcpu_wp)
+  apply (erule_tac x=v in allE)
+  apply (erule_tac P=P in rsubst)
+  apply (auto intro!: ext simp: vcpu_extra_lrs_def)
+  done
+
+crunch vcpu_save_reg, vcpu_save_reg_range, save_virt_timer
+  for extra_lrs[wp]: "\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x))"
+  (wp: mapM_x_wp)
+
+lemma vgic_update_extra_lrs[wp]:
+  "\<lbrace>\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x)) \<and>
+        (\<forall>v r. arm_gicvcpu_numlistregs (arch_state s) \<le> r \<longrightarrow> vgic_lr (f v) r = vgic_lr v r)\<rbrace>
+   vgic_update vr f
+   \<lbrace>\<lambda>_ s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x))\<rbrace>"
+  unfolding vgic_update_def by wpsimp
+
+lemma vgic_update_lr_extra_lrs[wp]:
+  "\<lbrace>\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x)) \<and>
+        r < arm_gicvcpu_numlistregs (arch_state s)\<rbrace>
+   vgic_update_lr vr r irq
+   \<lbrace>\<lambda>_ s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x))\<rbrace>"
+  unfolding vgic_update_lr_def by wpsimp
+
+lemma vcpu_save_extra_lrs[wp]:
+  "vcpu_save vr \<lbrace>\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x))\<rbrace>"
+  by (wpsimp simp: vcpu_save_def
+      | rule hoare_strengthen_post,
+        rule_tac P="\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x)) \<and>
+                        num_list_regs = arm_gicvcpu_numlistregs (arch_state s)"
+             and Q="\<lambda>r s. r < num_list_regs" and xs="[0..<num_list_regs]" for num_list_regs
+              in mapM_set_inv)+
+
+crunch vcpu_restore, vcpu_enable, vcpu_disable, vcpu_invalidate_active
+  for extra_lrs[wp]: "\<lambda>s. P (vcpu_extra_lrs (arm_gicvcpu_numlistregs (arch_state s)) (vcpus_of s x))"
+  (wp: mapM_x_wp)
+
 lemma vcpu_switch_integrity_hyp[wp]:
   "\<lbrace>integrity_hyp aag subjects x st and valid_arch_state\<rbrace>
    vcpu_switch vr
    \<lbrace>\<lambda>_. integrity_hyp aag subjects x st\<rbrace>"
   unfolding integrity_hyp_def vcpu_integrity_def vcpu_switch_def vcpu_proj_of_state
   supply if_split[split del] if_split[where P="\<lambda>v. _ = v", simp]
-  apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift' | wp dmo_lift_vcpu_proj)+
+  apply (wpsimp wp: dmo_lift_vcpu_proj hoare_vcg_all_lift hoare_vcg_imp_lift')
   apply (auto simp: insert_commute cur_vcpu_of_def split: if_splits)
   done
 
@@ -2221,11 +2265,15 @@ lemma vcpu_flush_integrity_hyp[wp]:
    vcpu_flush
    \<lbrace>\<lambda>_. integrity_hyp aag subjects x st\<rbrace>"
   unfolding integrity_hyp_def vcpu_integrity_def vcpu_flush_def vcpu_proj_of_state
+  apply (rule hoare_weaken_pre)
+   apply (rule hoare_vcg_conj_lift, solves wpsimp)
+   apply (rule hoare_vcg_imp_lift, solves wpsimp)
+   apply (rule hoare_vcg_conj_lift, solves wpsimp)
   supply if_split[split del] if_split[where P="\<lambda>v. _ = v", simp]
   apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift'
                     hoare_pre_cont[where f=vcpu_invalidate_active and P="\<lambda>_ s. cur_vcpu_of s x = Some _"]
          | strengthen None_Some_strg)+
-  apply (fastforce simp: cur_vcpu_of_def split: if_splits)
+  apply (auto simp: insert_commute cur_vcpu_of_def split: if_splits)
   done
 
 crunch vcpu_flush

proof/access-control/Access.thy

@@ -669,6 +669,8 @@ inductive integrity_obj_alt for aag activate subjects l' ko ko' where
     "\<lbrakk> tro_tag TCBGeneric; ko = Some (TCB tcb); ko' = Some (TCB tcb');
        tcb' = tcb \<lparr>tcb_arch := new_arch, tcb_bound_notification := ntfn',
                    tcb_caller := cap', tcb_ctable := ccap'\<rparr>;
+       tcb_ctable tcb = ccap' \<and> tcb_caller tcb = cap' \<and> tcb_bound_notification tcb = ntfn'
+       \<longrightarrow> arch_tcb_get_registers new_arch = arch_tcb_get_registers (tcb_arch tcb);
        tcb_hyp_refs new_arch = tcb_hyp_refs (tcb_arch tcb);
        tcb_bound_notification_reset_integrity (tcb_bound_notification tcb) ntfn' subjects aag ;
        reply_cap_deletion_integrity subjects aag (tcb_caller tcb) cap';

proof/access-control/Access_AC.thy

@@ -603,6 +603,7 @@ lemma tro_alt_trans_spec: (* this takes a long time to process *)
 
   apply (find_goal \<open>match premises in "tro_tag TCBGeneric" and "tro_tag' TCBRestart" \<Rightarrow> -\<close>)
   subgoal
+    apply (thin_tac "_ \<longrightarrow> _")
     apply (erule integrity_obj_alt.intros[simplified tro_tag_to_prime])
             apply (simp | rule tcb.equality | fastforce)+
     done
@@ -638,14 +639,33 @@ lemma tro_alt_trans_spec: (* this takes a long time to process *)
                                         simp: arch_tro_alt_trans_spec\<close>\<close>)
 
   (* TCB-TCB steps, somewhat slow *)
+  apply (all \<open>fails \<open>erule thin_rl[of "tro_tag TCBGeneric"],
+                     erule thin_rl[of "tro_tag' TCBGeneric"]\<close>
+             | time_methods \<open>solves \<open>
+                        erule integrity_obj_alt.intros[simplified tro_tag_to_prime],
+                        (assumption | rule refl
+                        | ((erule exE)+)?, (rule exI)?,
+                          force intro: tcb.equality
+                                 simp: reply_cap_deletion_integrity_def
+                                       tcb_bound_notification_reset_integrity_def)+\<close>\<close>\<close>)
+
+  apply (all \<open>fails \<open>erule thin_rl[of "tro_tag TCBGeneric"]\<close>
+             | time_methods \<open>solves \<open>
+                    (thin_tac \<open>_ \<longrightarrow> _\<close>)?,
+                    erule integrity_obj_alt.intros[simplified tro_tag_to_prime],
+                    (assumption | rule refl
+                    | ((erule exE)+)?, (rule exI)?, force intro: tcb.equality)+\<close>\<close>\<close>)
+
   apply (all \<open>fails \<open>erule thin_rl[of "tro_tag TCBGeneric"]\<close>
              | time_methods \<open>solves \<open>
+                    thin_tac \<open>_ \<longrightarrow> _\<close>,
                     erule integrity_obj_alt.intros[simplified tro_tag_to_prime],
                     (assumption | rule refl
                     | ((erule exE)+)?, (rule exI)?, force intro: tcb.equality)+\<close>\<close>\<close>)
 
   apply (all \<open>fails \<open>erule thin_rl[of "tro_tag' TCBGeneric"]\<close>
              | time_methods \<open>solves \<open>
+                    (thin_tac \<open>_ \<longrightarrow> _\<close>)?,
                     erule integrity_obj_alt.intros,
                     (assumption | rule refl
                     | (elim exE)?, (intro exI)?, fastforce intro: tcb.equality
@@ -777,6 +797,7 @@ lemma cdt_direct_change_allowed_backward:
   by (drule spec,
       erule integrity_objE, erule cdca_owned;
       (elim exE)?;
+      (thin_tac "_ \<longrightarrow> _")?;
       simp;
       rule cdca_reply[rotated], assumption, assumption,
       fastforce elim:tcb_states_of_state_kheapI simp:direct_call_def)

proof/access-control/DomainSepInv.thy

@@ -30,6 +30,7 @@ definition domain_sep_inv :: "bool \<Rightarrow> 'a :: state_ext state \<Rightar
                       \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) slot s
                       \<and> interrupt_states s irq \<noteq> IRQSignal
                       \<and> interrupt_states s irq \<noteq> IRQReserved
+                      \<and> (irq \<in> non_kernel_IRQs \<longrightarrow> interrupt_states s irq = IRQInactive)
                       \<and> interrupt_states s = interrupt_states st))"
 
 definition domain_sep_inv_cap where
@@ -59,6 +60,7 @@ lemma domain_sep_inv_def2:
                        \<and> \<not> cte_wp_at ((=) (IRQHandlerCap irq)) slot s)) \<and>
      (irqs \<or> (\<forall>irq. interrupt_states s irq \<noteq> IRQSignal
                   \<and> interrupt_states s irq \<noteq> IRQReserved
+                  \<and> (irq \<in> non_kernel_IRQs \<longrightarrow> interrupt_states s irq = IRQInactive)
                   \<and> interrupt_states s = interrupt_states st)))"
   by (fastforce simp: domain_sep_inv_def)
 
@@ -90,7 +92,9 @@ lemma domain_sep_inv_wp:
   apply (rule disjI2)
   apply simp
   apply (intro allI conjI)
-    apply (erule_tac P1="\<lambda>x. x irq \<noteq> IRQSignal" in use_valid[OF _ irq_pres], assumption)
+     apply (erule_tac P1="\<lambda>x. x irq \<noteq> IRQSignal" in use_valid[OF _ irq_pres], assumption)
+     apply blast
+    apply (erule use_valid[OF _ irq_pres], assumption)
     apply blast
    apply (erule use_valid[OF _ irq_pres], assumption)
    apply blast