Skip to content

Commit

Permalink
arm access: proof update for det_ext refactor
Browse files Browse the repository at this point in the history
Signed-off-by: Corey Lewis <[email protected]>
  • Loading branch information
corlewis committed Dec 12, 2024
1 parent 918da15 commit 9788c54
Show file tree
Hide file tree
Showing 16 changed files with 394 additions and 569 deletions.
11 changes: 11 additions & 0 deletions proof/access-control/ARM/ArchAccess.thy
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,11 @@ lemmas state_vrefs_upd =
revokable_update.state_vrefs
machine_state_update.state_vrefs
more_update.state_vrefs
scheduler_action_update.state_vrefs
domain_index_update.state_vrefs
cur_domain_update.state_vrefs
domain_time_update.state_vrefs
ready_queues_update.state_vrefs

end

Expand Down Expand Up @@ -138,6 +143,7 @@ abbreviation integrity_asids_aux ::
pp_opt = pp_opt' \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of asid
\<longrightarrow> pasASIDAbs aag asid' \<in> subjects)"

\<comment> \<open>FIXME: could we define integrity_asids to operate on arch_state only?\<close>
definition integrity_asids ::
"'a PAS \<Rightarrow> 'a set \<Rightarrow> obj_ref \<Rightarrow> asid \<Rightarrow> 'y::state_ext state \<Rightarrow> 'z:: state_ext state \<Rightarrow> bool" where
"integrity_asids aag subjects x a s s' \<equiv>
Expand All @@ -159,6 +165,11 @@ lemmas integrity_asids_updates =
interrupt_update.integrity_asids_update
cur_thread_update.integrity_asids_update
machine_state_update.integrity_asids_update
scheduler_action_update.integrity_asids_update
domain_index_update.integrity_asids_update
cur_domain_update.integrity_asids_update
domain_time_update.integrity_asids_update
ready_queues_update.integrity_asids_update

(* The kheap isn't used in ARM's integrity_asids definition,
but we need the following lemmas in some generic contexts *)
Expand Down
13 changes: 6 additions & 7 deletions proof/access-control/ARM/ArchArch_AC.thy
Original file line number Diff line number Diff line change
Expand Up @@ -1011,21 +1011,20 @@ lemma delete_asid_respects:
by (wpsimp wp: set_asid_pool_respects_clear hoare_vcg_all_lift
simp: obj_at_def pas_refined_refl delete_asid_def asid_pool_integrity_def)

lemma authorised_arch_inv_sa_update:
lemma authorised_arch_inv_sa_update[simp]:
"authorised_arch_inv aag i (scheduler_action_update (\<lambda>_. act) s) =
authorised_arch_inv aag i s"
by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
split: arch_invocation.splits page_invocation.splits)

crunch set_thread_state_act
for authorised_arch_inv[wp]: "authorised_arch_inv aag i"

lemma set_thread_state_authorised_arch_inv[wp]:
"set_thread_state ref ts \<lbrace>authorised_arch_inv aag i\<rbrace>"
unfolding set_thread_state_def
apply (wpsimp wp: dxo_wp_weak)
apply (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
split: arch_invocation.splits page_invocation.splits)
apply (wpsimp wp: set_object_wp)+
by (clarsimp simp: authorised_arch_inv_def authorised_page_inv_def authorised_slots_def
split: arch_invocation.splits page_invocation.splits)
apply (wpsimp wp: set_object_wp)
by (clarsimp simp: authorised_arch_inv_def)

end

Expand Down
25 changes: 4 additions & 21 deletions proof/access-control/ARM/ArchCNode_AC.thy
Original file line number Diff line number Diff line change
Expand Up @@ -114,15 +114,12 @@ lemma list_integ_lift[CNode_AC_assms]:
"\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
f
\<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\<rbrace>"
assumes ekh: "\<And>P. f \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
assumes rq: "\<And>P. f \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace>"
shows "\<lbrace>integrity aag X st and Q\<rbrace> f \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
apply (rule hoare_pre)
apply (unfold integrity_def[abs_def] integrity_asids_def)
apply (simp only: integrity_cdt_list_as_list_integ)
apply (rule hoare_lift_Pf2[where f="ekheap"])
apply (simp add: tcb_states_of_state_def get_tcb_def)
apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+
apply (simp add: tcb_states_of_state_def get_tcb_def)
apply (wp li[simplified tcb_states_of_state_def get_tcb_def])+
apply (simp only: integrity_cdt_list_as_list_integ)
apply (simp add: tcb_states_of_state_def get_tcb_def)
done
Expand Down Expand Up @@ -374,16 +371,9 @@ lemma auth_graph_map_def2:
"auth_graph_map f S = (\<lambda>(x, auth, y). (f x, auth, f y)) ` S"
by (auto simp add: auth_graph_map_def image_def intro: rev_bexI)

(* FIXME move to AInvs *)
lemma store_pte_ekheap[wp]:
"store_pte p pte \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
apply (simp add: store_pte_def set_pt_def)
apply (wp get_object_wp)
apply simp
done

crunch store_pte
for asid_table_inv[wp]: "\<lambda>s. P (asid_table s)"
for etcbs_of[wp]: "\<lambda>s. P (etcbs_of s)"
and asid_table_inv[wp]: "\<lambda>s. P (asid_table s)"

lemma store_pte_pas_refined[wp]:
"\<lbrace>pas_refined aag and
Expand Down Expand Up @@ -501,13 +491,6 @@ lemma set_asid_pool_thread_bound_ntfns[wp]:
split: kernel_object.split_asm option.split)
done

(* FIXME move to AInvs *)
lemma set_asid_pool_ekheap[wp]:
"set_asid_pool p pool \<lbrace>\<lambda>s. P (ekheap s)\<rbrace>"
apply (simp add: set_asid_pool_def)
apply (wp get_object_wp | simp)+
done

lemma set_asid_pool_pas_refined[wp]:
"\<lbrace>pas_refined aag and
(\<lambda>s. \<forall>(x, y) \<in> graph_of pool.
Expand Down
8 changes: 3 additions & 5 deletions proof/access-control/ARM/ArchIpc_AC.thy
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ declare handle_arch_fault_reply_typ_at[Ipc_AC_assms]

crunch cap_insert_ext
for integrity_asids[Ipc_AC_assms, wp]: "integrity_asids aag subjects x a st"
(ignore_del: cap_insert_ext) \<comment> \<open>FIXME: should these ext consts still be ignored in DetSched_AI files and beyond?\<close>

lemma arch_derive_cap_auth_derived[Ipc_AC_assms]:
"\<lbrace>\<top>\<rbrace> arch_derive_cap acap \<lbrace>\<lambda>rv _. rv \<noteq> NullCap \<longrightarrow> auth_derived rv (ArchObjectCap acap)\<rbrace>, -"
Expand Down Expand Up @@ -203,18 +204,15 @@ lemma list_integ_lift_in_ipc[Ipc_AC_assms]:
"\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
f
\<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\<rbrace>"
assumes ekh: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
assumes rq: "\<And>P. \<lbrace> \<lambda>s. P (ready_queues s) \<rbrace> f \<lbrace> \<lambda>rv s. P (ready_queues s) \<rbrace>"
shows "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\<rbrace>
f
\<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>"
apply (unfold integrity_tcb_in_ipc_def integrity_def[abs_def])
apply (simp del:split_paired_All)
apply (rule hoare_pre)
apply (simp only: integrity_cdt_list_as_list_integ)
apply (rule hoare_lift_Pf2[where f="ekheap"])
apply (simp add: tcb_states_of_state_def get_tcb_def)
apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+
apply (simp add: tcb_states_of_state_def get_tcb_def)
apply (wp li[simplified tcb_states_of_state_def get_tcb_def])+
apply (simp only: integrity_cdt_list_as_list_integ)
apply (simp add: tcb_states_of_state_def get_tcb_def)
done
Expand Down
33 changes: 25 additions & 8 deletions proof/access-control/ARM/ArchRetype_AC.thy
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ lemma invs_mdb_cte':
context retype_region_proofs begin interpretation Arch .

lemma vs_refs_no_global_pts_default[simp]:
"vs_refs_no_global_pts (default_object ty dev us) = {}"
"vs_refs_no_global_pts (default_object ty dev us d) = {}"
by (simp add: default_object_def default_arch_object_def tyunt
vs_refs_no_global_pts_def pde_ref2_def pte_ref_def
o_def
Expand All @@ -33,12 +33,29 @@ end

context retype_region_proofs' begin interpretation Arch .

lemma test:
"pas_refined aag s \<Longrightarrow> tcb_domain_map_wellformed aag s"
by (simp add: pas_refined_def)

\<comment> \<open>FIXME: move to pas_refined_state_objs_to_policy_subset?\<close>
lemma pas_refined_subsets_tcb_domain_map_wellformed:
"\<lbrakk> pas_refined aag s;
state_objs_to_policy s' \<subseteq> state_objs_to_policy s;
state_asids_to_policy aag s' \<subseteq> state_asids_to_policy aag s;
state_irqs_to_policy aag s' \<subseteq> state_irqs_to_policy aag s;
tcb_domain_map_wellformed aag s \<Longrightarrow> tcb_domain_map_wellformed aag s';
interrupt_irq_node s' = interrupt_irq_node s \<rbrakk>
\<Longrightarrow> pas_refined aag s'"
by (simp add: pas_refined_def)
(blast dest: auth_graph_map_mono[where G="pasObjectAbs aag"])

lemma pas_refined:
"\<lbrakk> invs s; pas_refined aag s \<rbrakk> \<Longrightarrow> pas_refined aag s'"
apply (erule pas_refined_state_objs_to_policy_subset)
apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable)
apply (rule subsetI, rename_tac x, case_tac x, simp)
apply (erule state_bits_to_policy.cases)
"\<lbrakk> invs s; pas_refined aag s; pas_cur_domain aag s; \<forall>x\<in> set (retype_addrs ptr ty n us). is_subject aag x \<rbrakk>
\<Longrightarrow> pas_refined aag s'"
apply (erule pas_refined_subsets_tcb_domain_map_wellformed)
apply (simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable)
apply (rule subsetI, rename_tac x, case_tac x, simp)
apply (erule state_bits_to_policy.cases)
apply (solves \<open>auto intro!: sbta_caps intro: caps_retype split: cap.split\<close>)
apply (solves \<open>auto intro!: sbta_untyped intro: caps_retype split: cap.split\<close>)
apply (blast intro: state_bits_to_policy.intros)
Expand All @@ -57,7 +74,7 @@ lemma pas_refined:
apply clarsimp
apply (erule state_irqs_to_policy_aux.cases)
apply (solves\<open>auto intro!: sita_controlled intro: caps_retype split: cap.split\<close>)
apply (rule domains_of_state)
apply (erule (2) tcb_domain_map_wellformed)
apply simp
done

Expand Down Expand Up @@ -427,7 +444,7 @@ lemma retype_region_integrity_asids[Retype_AC_assms]:
\<forall>x\<in>up_aligned_area ptr sz. is_subject aag x; integrity_asids aag {pasSubject aag} x a s st \<rbrakk>
\<Longrightarrow> integrity_asids aag {pasSubject aag} x a s
(st\<lparr>kheap := \<lambda>a. if a \<in> (\<lambda>x. ptr_add ptr (x * 2 ^ obj_bits_api typ o_bits)) ` {0 ..< n}
then Some (default_object typ dev o_bits)
then Some (default_object typ dev o_bits d)
else kheap s a\<rparr>)"
by clarsimp

Expand Down
5 changes: 2 additions & 3 deletions proof/access-control/ARM/ArchTcb_AC.thy
Original file line number Diff line number Diff line change
Expand Up @@ -32,14 +32,12 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
apply (rule hoare_gen_asm)+
apply (subst invoke_tcb.simps)
apply (subst option_update_thread_def)
apply (subst set_priority_extended.dxo_eq)
apply (rule hoare_weaken_pre)
apply (rule_tac P="case ep of Some v \<Rightarrow> length v = word_bits | _ \<Rightarrow> True"
in hoare_gen_asm)
apply (simp only: split_def)
apply (((simp add: conj_comms,
strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong)
| strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
| rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_liftE_R
hoare_vcg_conj_elimE hoare_vcg_const_imp_liftE_R hoare_vcg_conj_liftE_R
| wp restart_integrity_autarch set_mcpriority_integrity_autarch
Expand Down Expand Up @@ -79,7 +77,8 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
| simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
emptyable_def a_type_def partial_inv_def
| wpc
| strengthen invs_mdb use_no_cap_to_obj_asid_strg
| strengthen invs_psp_aligned invs_vspace_objs invs_arch_state
invs_mdb use_no_cap_to_obj_asid_strg
tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"]))+
apply (clarsimp simp: authorised_tcb_inv_def)
Expand Down
Loading

0 comments on commit 9788c54

Please sign in to comment.