From c158fbf9902f0be4a295f9db317d4ba6dab5add5 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Thu, 21 Nov 2024 17:42:11 +1100 Subject: [PATCH] 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 --- proof/access-control/ARM/ArchIpc_AC.thy | 4 ++++ proof/access-control/CNode_AC.thy | 16 +++++++++++++--- proof/access-control/Finalise_AC.thy | 2 +- proof/access-control/Ipc_AC.thy | 13 +++++++++---- proof/access-control/RISCV64/ArchIpc_AC.thy | 4 ++++ proof/infoflow/ARM/ArchRetype_IF.thy | 9 +++++++++ proof/infoflow/ARM/ArchTcb_IF.thy | 2 ++ proof/infoflow/Arch_IF.thy | 8 ++++++++ proof/infoflow/Finalise_IF.thy | 3 ++- proof/infoflow/Ipc_IF.thy | 18 +++++++++++------- proof/infoflow/RISCV64/ArchRetype_IF.thy | 9 +++++++++ proof/infoflow/RISCV64/ArchTcb_IF.thy | 3 +++ proof/infoflow/Tcb_IF.thy | 2 +- 13 files changed, 76 insertions(+), 17 deletions(-) diff --git a/proof/access-control/ARM/ArchIpc_AC.thy b/proof/access-control/ARM/ArchIpc_AC.thy index 4f2b49cd9d..b7d2687f13 100644 --- 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 \valid_arch_state :: det_ext state \ _\" + 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 index 383935f0bf..b79309883c 100644 --- 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\CNode-specific AC.\ @@ -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 \pas_refined aag\" and aobj_ref'_same_aobject: "same_aobject_as ao' ao \ 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 \\s :: det_ext state. valid_arch_state s\" begin lemma cap_insert_pas_refined: diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy index 465471bb1f..36f064cfa3 100644 --- a/proof/access-control/Finalise_AC.thy +++ b/proof/access-control/Finalise_AC.thy @@ -372,7 +372,7 @@ crunch suspend for pspace_aligned[wp]: "\s :: det_ext state. pspace_aligned s" and valid_vspace_objs[wp]: "\s :: det_ext state. valid_vspace_objs s" and valid_arch_state[wp]: "\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 index aec0b47790..eb7a8cc056 100644 --- a/proof/access-control/Ipc_AC.thy +++ b/proof/access-control/Ipc_AC.thy @@ -172,6 +172,9 @@ locale Ipc_AC_1 = "\P. make_fault_msg ft t \\s :: det_ext state. P s\" and tcb_context_no_change: "\ctxt. (tcb :: tcb) = tcb\tcb_arch := arch_tcb_context_set ctxt (tcb_arch tcb)\" + (* 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 \valid_arch_state :: det_ext state \ _\" begin lemma send_upd_ctxintegrity: @@ -914,7 +917,7 @@ crunch do_fault_transfer for pas_refined[wp]: "\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 \ _" (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: \\_. pas_refined aag\" 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 index 7be518e246..211262fde4 100644 --- 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 \valid_arch_state :: det_ext state \ _\" + 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 index 8a8060dc9d..d30122f709 100644 --- 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 \valid_arch_state\" + 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]: + "\valid_arch_state \ create_cap tp sz p dev ref + \\rv. valid_arch_state\" + by (wp valid_arch_state_lift_aobj_at_no_caps create_cap_aobj_at) + lemma cacheRangeOp_ev[wp]: "(\a b. equiv_valid_inv I A \ (oper a b)) \ equiv_valid_inv I A \ (cacheRangeOp oper x y z)" diff --git a/proof/infoflow/ARM/ArchTcb_IF.thy b/proof/infoflow/ARM/ArchTcb_IF.thy index 44dd1df9c1..c84b03c1fd 100644 --- 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 index 98d64ca9d7..ea1c2388a8 100644 --- 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 \ nat" where "irq_state_of_state s \ irq_state (machine_state s)" diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy index 476a7a8062..259a182e72 100644 --- 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]: "\globals_equiv st and (\s. t \ idle_thread s) and valid_arch_state\ diff --git a/proof/infoflow/Ipc_IF.thy b/proof/infoflow/Ipc_IF.thy index 11865a8ea3..049644dedb 100644 --- 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=\]] - 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'="\_. 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: "\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'="\_. 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 index 194bdbbf0d..3f23f73912 100644 --- 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 \valid_arch_state\" + 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]: + "\valid_arch_state \ create_cap tp sz p dev ref + \\rv. valid_arch_state\" + 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) \ (modify (underlying_memory_update (\m. m(x := word_rsplit 0 ! 7, diff --git a/proof/infoflow/RISCV64/ArchTcb_IF.thy b/proof/infoflow/RISCV64/ArchTcb_IF.thy index 56830a0004..999bc04b2c 100644 --- 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,6 +221,7 @@ 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="\"] + 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 @@ -227,6 +229,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) 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 index 16cfd1f855..fcdcb12975 100644 --- 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: "\\s. invs s \ globals_equiv st s \ emptyable (slot_rdcall call) s \ valid_rec_del_call call s\