access+infoflow: minimal update for ioport hiding for current arches

Currently this means ARM and RISCV64. Already, these two architectures did not consider IO ports, so were not compatible with X64, and neither was an X64 integrity proof planned. This change leans on that by requalifying/assuming some extra lemmas which pretend that valid_arch_state not relying on caps is a generic concept. Signed-off-by: Rafal Kolanski <[email protected]>
seL4 · Dec 4, 2024 · c158fbf · c158fbf
1 parent 06e189c
commit c158fbf
Show file tree

Hide file tree

Showing 13 changed files with 76 additions and 17 deletions.
diff --git a/proof/access-control/ARM/ArchIpc_AC.thy b/proof/access-control/ARM/ArchIpc_AC.thy
@@ -63,6 +63,10 @@ lemma tcb_context_no_change[Ipc_AC_assms]:
   apply (auto simp: arch_tcb_context_set_def)
   done
 
+lemma transfer_caps_loop_valid_arch[Ipc_AC_assms]:
+  "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps transfer_caps_loop_aobj_at)
+
 end
 
 

diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy
@@ -8,6 +8,19 @@ theory CNode_AC
 imports ArchAccess_AC
 begin
 
+(* Note: exporting the following diverges from AInvs interfaces where valid_arch_state is
+   permitted to depend on caps (due to supporting x64). If x64 access control is to go ahead,
+   these will need more careful management. *)
+arch_requalify_facts
+  set_cap_valid_arch_state
+  cap_insert_simple_valid_arch_state
+
+lemmas [wp] = set_cap_valid_arch_state cap_insert_simple_valid_arch_state
+
+crunch set_untyped_cap_as_full
+  for valid_arch_state[wp]: valid_arch_state
+
+
 section\<open>CNode-specific AC.\<close>
 
 
@@ -33,7 +46,6 @@ crunch cap_swap_ext,cap_move_ext,empty_slot_ext
 crunch set_untyped_cap_as_full
   for integrity_autarch: "integrity aag X st"
 
-
 locale CNode_AC_1 =
   fixes aag :: "'a PAS"
   and val_t :: "'b"
@@ -1010,8 +1022,6 @@ locale CNode_AC_3 = CNode_AC_2 +
     "arch_post_cap_deletion irqopt \<lbrace>pas_refined aag\<rbrace>"
   and aobj_ref'_same_aobject:
     "same_aobject_as ao' ao \<Longrightarrow> aobj_ref' ao = aobj_ref' ao'"
-  and set_untyped_cap_as_full_valid_arch_state[wp]:
-    "set_untyped_cap_as_full src_cap new_cap src_slot \<lbrace>\<lambda>s :: det_ext state. valid_arch_state s\<rbrace>"
 begin
 
 lemma cap_insert_pas_refined:

diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy
@@ -372,7 +372,7 @@ crunch suspend
   for pspace_aligned[wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
   and valid_vspace_objs[wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
   and valid_arch_state[wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
-  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)
+  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps simp: tcb_cap_cases_def)
 
 crunch suspend
   for pas_refined[wp]: "pas_refined aag"

diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy
@@ -172,6 +172,9 @@ locale Ipc_AC_1 =
     "\<And>P. make_fault_msg ft t \<lbrace>\<lambda>s :: det_ext state. P s\<rbrace>"
   and tcb_context_no_change:
     "\<exists>ctxt. (tcb :: tcb) = tcb\<lparr>tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\<rparr>"
+  (* This assumption excludes x64 (its valid_arch_state includes caps) *)
+  and transfer_caps_loop_valid_arch[wp]:
+    "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
 begin
 
 lemma send_upd_ctxintegrity:
@@ -914,7 +917,7 @@ crunch do_fault_transfer
   for pas_refined[wp]: "\<lambda>s :: det_ext state. pas_refined aag s"
 
 crunch transfer_caps, copy_mrs
-  for valid_arch_state[wp]: valid_arch_state
+  for valid_arch_state[wp]: "valid_arch_state :: det_ext state \<Rightarrow> _"
   (wp: crunch_wps)
 
 lemma do_normal_transfer_pas_refined:
@@ -1067,6 +1070,7 @@ lemma send_ipc_pas_refined:
                     in hoare_strengthen_post[rotated])
         apply simp
        apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined hoare_weak_lift_imp gts_wp
+                 do_ipc_transfer_valid_arch
               | wpc
               | simp add: hoare_if_r_and)+
    apply (wp hoare_vcg_all_lift hoare_imp_lift_something | simp add: st_tcb_at_tcb_states_of_state_eq)+
@@ -1214,6 +1218,7 @@ lemma receive_ipc_base_pas_refined:
         apply (wp hoare_weak_lift_imp do_ipc_transfer_pas_refined set_simple_ko_pas_refined
                   set_thread_state_pas_refined get_simple_ko_wp hoare_vcg_all_lift
                   hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
+                  do_ipc_transfer_valid_arch
                | wpc
                | simp add: thread_get_def  get_thread_state_def do_nbrecv_failed_transfer_def)+
   apply (clarsimp simp: tcb_at_def [symmetric] tcb_at_st_tcb_at)
@@ -2541,9 +2546,9 @@ lemma do_reply_transfer_pas_refined:
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   apply (simp add: do_reply_transfer_def)
   apply (rule hoare_pre)
-  apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined
-            thread_set_pas_refined K_valid
-         | wpc | simp add: thread_get_def split del: if_split)+
+  apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined do_ipc_transfer_valid_arch
+            thread_set_pas_refined K_valid thread_set_valid_arch_state
+         | wpc | simp add: thread_get_def tcb_cap_cases_def split del: if_split)+
   (* otherwise simp does too much *)
   apply (rule hoare_strengthen_post, rule gts_inv)
    apply (rule impI)

diff --git a/proof/access-control/RISCV64/ArchIpc_AC.thy b/proof/access-control/RISCV64/ArchIpc_AC.thy
@@ -66,6 +66,10 @@ lemma tcb_context_no_change[Ipc_AC_assms]:
   apply (auto simp: arch_tcb_context_set_def)
   done
 
+lemma transfer_caps_loop_valid_arch[Ipc_AC_assms]:
+  "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps transfer_caps_loop_aobj_at)
+
 end
 
 

diff --git a/proof/infoflow/ARM/ArchRetype_IF.thy b/proof/infoflow/ARM/ArchRetype_IF.thy
@@ -12,6 +12,15 @@ context Arch begin global_naming ARM
 
 named_theorems Retype_IF_assms
 
+lemma do_ipc_transfer_valid_arch_no_caps[wp]:
+  "do_ipc_transfer s ep bg grt r \<lbrace>valid_arch_state\<rbrace>"
+  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps do_ipc_transfer_aobj_at)
+
+lemma create_cap_valid_arch_state_no_caps[wp]:
+  "\<lbrace>valid_arch_state \<rbrace> create_cap tp sz p dev ref
+   \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps create_cap_aobj_at)
+
 lemma cacheRangeOp_ev[wp]:
   "(\<And>a b. equiv_valid_inv I A \<top> (oper a b))
    \<Longrightarrow> equiv_valid_inv I A \<top> (cacheRangeOp oper x y z)"

diff --git a/proof/infoflow/ARM/ArchTcb_IF.thy b/proof/infoflow/ARM/ArchTcb_IF.thy
@@ -185,6 +185,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
                            cap_delete_pas_refined' itr_wps(12) itr_wps(14) cap_insert_cte_at
                            checked_insert_no_cap_to hoare_vcg_const_imp_liftE_R hoare_vcg_conj_lift
                            as_user_reads_respects_f thread_set_mdb cap_delete_invs
+                           thread_set_valid_arch_state
                       | wpc
                       | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
                                   tcb_at_st_tcb_at when_def
@@ -231,6 +232,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
              thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
              thread_set_cte_at thread_set_no_cap_to_trivial
              thread_set_tcb_fault_handler_update_only_timer_irq_inv
+             thread_set_valid_arch_state
           | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imp)+
   apply (clarsimp simp: authorised_tcb_inv_def  authorised_tcb_inv_extra_def emptyable_def)
   by (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def is_valid_vtable_root_def det_setRegister

diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy
@@ -8,6 +8,14 @@ theory Arch_IF
 imports ArchRetype_IF
 begin
 
+(* Note: exporting the following diverges from AInvs interfaces where valid_arch_state is
+   permitted to depend on caps (due to supporting x64). If x64 confidentiality is to go ahead,
+   this will need more careful management. *)
+arch_requalify_facts
+  do_ipc_transfer_valid_arch_no_caps
+
+lemmas [wp] = do_ipc_transfer_valid_arch_no_caps
+
 abbreviation irq_state_of_state :: "det_state \<Rightarrow> nat" where
   "irq_state_of_state s \<equiv> irq_state (machine_state s)"
 

diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy
@@ -1489,7 +1489,8 @@ crunch deleting_irq_handler
 
 crunch cancel_ipc
   for globals_equiv[wp]: "globals_equiv st"
-  (wp: mapM_x_wp select_inv hoare_drop_imps hoare_vcg_if_lift2 simp: unless_def)
+  (wp: mapM_x_wp select_inv hoare_drop_imps hoare_vcg_if_lift2 thread_set_valid_arch_state
+   simp: unless_def tcb_cap_cases_def)
 
 lemma suspend_globals_equiv[ wp]:
   "\<lbrace>globals_equiv st and (\<lambda>s. t \<noteq> idle_thread s) and valid_arch_state\<rbrace>

diff --git a/proof/infoflow/Ipc_IF.thy b/proof/infoflow/Ipc_IF.thy
@@ -1600,9 +1600,9 @@ lemma do_reply_transfer_reads_respects_f:
             cap_delete_one_silc_inv do_ipc_transfer_silc_inv
             set_thread_state_pas_refined thread_set_fault_pas_refined'
             possible_switch_to_reads_respects[THEN reads_respects_f[where aag=aag and st=st and Q=\<top>]]
-            when_ev
+            when_ev thread_set_valid_arch_state
          | wpc
-         | simp split del: if_split
+         | simp split del: if_split add: tcb_cap_cases_def
          | wp (once) reads_respects_f[where aag=aag and st=st]
          | elim conjE
          | wp (once) hoare_drop_imps)+
@@ -1987,8 +1987,10 @@ lemma send_fault_ipc_globals_equiv:
   apply (wp)
      apply (simp add: Let_def)
      apply (wp send_ipc_globals_equiv thread_set_globals_equiv thread_set_valid_objs''
-               thread_set_fault_valid_global_refs thread_set_valid_idle_trivial thread_set_refs_trivial
-            | wpc | simp)+
+               thread_set_fault_valid_global_refs thread_set_valid_idle_trivial
+               thread_set_refs_trivial thread_set_valid_arch_state
+               thread_set_tcb_fault_update_valid_mdb
+            | wpc | simp add: tcb_cap_cases_def)+
     apply (rule_tac Q'="\<lambda>_. globals_equiv st and valid_objs and valid_arch_state and
                             valid_global_refs and pspace_distinct and pspace_aligned and
                             valid_global_objs and K (valid_fault fault) and valid_idle and
@@ -2000,8 +2002,9 @@ lemma send_fault_ipc_globals_equiv:
   done
 
 crunch send_fault_ipc
-  for valid_arch_state[wp]: valid_arch_state
-  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)
+  for valid_arch_statex[wp]: valid_arch_state
+  (wp: dxo_wp_weak hoare_drop_imps thread_set_valid_arch_state crunch_wps
+   simp: crunch_simps tcb_cap_cases_def)
 
 lemma handle_fault_globals_equiv:
   "\<lbrace>globals_equiv st and valid_objs and valid_arch_state and valid_global_refs
@@ -2033,7 +2036,8 @@ lemma do_reply_transfer_globals_equiv:
   unfolding do_reply_transfer_def
   apply (wp set_thread_state_globals_equiv cap_delete_one_globals_equiv do_ipc_transfer_globals_equiv
             thread_set_globals_equiv handle_fault_reply_globals_equiv dxo_wp_weak
-         | wpc | simp split del: if_split)+
+            thread_set_valid_arch_state
+         | wpc | simp split del: if_split add: tcb_cap_cases_def)+
      apply (rule_tac Q'="\<lambda>_. globals_equiv st and valid_arch_state and valid_objs and valid_arch_state
                                              and valid_global_refs and pspace_distinct
                                              and pspace_aligned and valid_global_objs

diff --git a/proof/infoflow/RISCV64/ArchRetype_IF.thy b/proof/infoflow/RISCV64/ArchRetype_IF.thy
@@ -12,6 +12,15 @@ context Arch begin global_naming RISCV64
 
 named_theorems Retype_IF_assms
 
+lemma do_ipc_transfer_valid_arch_no_caps[wp]:
+  "do_ipc_transfer s ep bg grt r \<lbrace>valid_arch_state\<rbrace>"
+  by (wpsimp wp: valid_arch_state_lift_aobj_at_no_caps do_ipc_transfer_aobj_at)
+
+lemma create_cap_valid_arch_state_no_caps[wp]:
+  "\<lbrace>valid_arch_state \<rbrace> create_cap tp sz p dev ref
+   \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps create_cap_aobj_at)
+
 lemma modify_underlying_memory_update_0_ev:
   "equiv_valid_inv (equiv_machine_state P) (equiv_machine_state Q) \<top>
                    (modify (underlying_memory_update (\<lambda>m. m(x := word_rsplit 0 ! 7,

diff --git a/proof/infoflow/RISCV64/ArchTcb_IF.thy b/proof/infoflow/RISCV64/ArchTcb_IF.thy
@@ -181,6 +181,7 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
                            cap_delete_pas_refined' itr_wps(12) itr_wps(14) cap_insert_cte_at
                            checked_insert_no_cap_to hoare_vcg_const_imp_liftE_R hoare_vcg_conj_lift
                            as_user_reads_respects_f thread_set_mdb cap_delete_invs
+                           thread_set_valid_arch_state
                       | wpc
                       | simp add: emptyable_def tcb_cap_cases_def tcb_cap_valid_def
                                   tcb_at_st_tcb_at when_def
@@ -220,13 +221,15 @@ lemma tc_reads_respects_f[Tcb_IF_assms]:
     apply (simp add: option_update_thread_def tcb_cap_cases_def
            | wp hoare_weak_lift_imp hoare_weak_lift_imp_conj thread_set_pas_refined
                 reads_respects_f[OF thread_set_reads_respects, where st=st and Q="\<top>"]
+                thread_set_valid_arch_state
            | wpc)+
    apply (wp hoare_vcg_all_lift thread_set_tcb_fault_handler_update_invs
              thread_set_tcb_fault_handler_update_silc_inv
              thread_set_not_state_valid_sched
              thread_set_pas_refined thread_set_emptyable thread_set_valid_cap
              thread_set_cte_at thread_set_no_cap_to_trivial
              thread_set_tcb_fault_handler_update_only_timer_irq_inv
+             thread_set_valid_arch_state
           | simp add: tcb_cap_cases_def | wpc | wp (once) hoare_drop_imp)+
   apply (clarsimp simp: authorised_tcb_inv_def authorised_tcb_inv_extra_def emptyable_def)
   apply (clarsimp simp: invs_psp_aligned invs_vspace_objs invs_arch_state)

diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy
@@ -196,7 +196,7 @@ begin
 
 crunch cap_swap_for_delete
   for valid_arch_state[wp]: valid_arch_state
-  (wp: dxo_wp_weak)
+  (wp: dxo_wp_weak simp: crunch_simps)
 
 lemma rec_del_globals_equiv:
   "\<lbrace>\<lambda>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>