adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm infoflow: update proofs 

Signed-off-by: Ryan Barry <ryan.barry@unsw.edu.au>
This commit is contained in:
Ryan Barry 2021-10-15 13:35:43 +11:00 committed by Gerwin Klein
parent 82fd48d769
commit 1b1814c9b1
8 changed files with 105 additions and 41 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
proof/infoflow/ARM/ArchADT_IF.thy
View File

@ -266,26 +266,26 @@ lemma kernel_entry_if_valid_pdpt_objs[wp]:
wp: static_imp_wp thread_set_invs_trivial)+
done
lemma kernel_entry_if_valid_vspace_objs'[ADT_IF_assms, wp]:
"\<lbrace>valid_vspace_objs' and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
lemma kernel_entry_if_valid_vspace_objs_if[ADT_IF_assms, wp]:
"\<lbrace>valid_vspace_objs_if and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. valid_vspace_objs'\<rbrace>"
\<lbrace>\<lambda>_. valid_vspace_objs_if\<rbrace>"
by wpsimp
lemma handle_preemption_if_valid_pdpt_objs[ADT_IF_assms, wp]:
"\<lbrace>valid_vspace_objs'\<rbrace> handle_preemption_if a \<lbrace>\<lambda>rv s. valid_vspace_objs' s\<rbrace>"
"\<lbrace>valid_vspace_objs_if\<rbrace> handle_preemption_if a \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>"
by (simp add: handle_preemption_if_def | wp)+
lemma schedule_if_valid_pdpt_objs[ADT_IF_assms, wp]:
"\<lbrace>valid_vspace_objs'\<rbrace> schedule_if a \<lbrace>\<lambda>rv s. valid_vspace_objs' s\<rbrace>"
"\<lbrace>valid_vspace_objs_if\<rbrace> schedule_if a \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>"
by (simp add: schedule_if_def | wp)+
lemma do_user_op_if_valid_pdpt_objs[ADT_IF_assms, wp]:
"\<lbrace>valid_vspace_objs'\<rbrace> do_user_op_if a b \<lbrace>\<lambda>rv s. valid_vspace_objs' s\<rbrace>"
"\<lbrace>valid_vspace_objs_if\<rbrace> do_user_op_if a b \<lbrace>\<lambda>rv s. valid_vspace_objs_if s\<rbrace>"
by (simp add: do_user_op_if_def | wp select_wp | wpc)+
lemma valid_vspace_objs'_ms_update[ADT_IF_assms, simp]:
"valid_vspace_objs' (machine_state_update f s) = valid_vspace_objs' s"
lemma valid_vspace_objs_if_ms_update[ADT_IF_assms, simp]:
"valid_vspace_objs_if (machine_state_update f s) = valid_vspace_objs_if s"
by auto
lemma non_kernel_IRQs_empty[ADT_IF_assms]:

26
proof/infoflow/ARM/ArchArch_IF.thy
View File

@ -178,12 +178,12 @@ proof goal_cases
qed
context Arch begin global_naming ARM
lemmas invs_imps =
invs_valid_vs_lookup invs_sym_refs invs_psp_aligned invs_distinct invs_arch_state
invs_valid_global_objs invs_arch_state invs_valid_objs invs_valid_global_refs tcb_at_invs
invs_cur invs_kernel_mappings
invs_sym_refs invs_psp_aligned invs_distinct invs_arch_state invs_valid_global_objs
invs_arch_state invs_valid_objs invs_valid_global_refs tcb_at_invs invs_cur invs_kernel_mappings
context Arch begin global_naming ARM
lemma cte_wp_at_page_directory_not_in_globals:
"\<lbrakk> cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap word optiona))) slot s;
@ -1571,6 +1571,20 @@ lemma arch_perform_invocation_globals_equiv:
simp: invs_def valid_state_def valid_arch_inv_def invs_valid_vs_lookup)
done
lemma arch_perform_invocation_reads_respects_g:
assumes domains_distinct: "pas_domains_distinct aag"
shows "reads_respects_g aag l (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai
and authorised_for_globals_arch_inv ai and invs
and pas_refined aag and is_subject aag \<circ> cur_thread)
(arch_perform_invocation ai)"
apply (rule equiv_valid_guard_imp)
apply (rule reads_respects_g)
apply (rule arch_perform_invocation_reads_respects[OF domains_distinct])
apply (rule doesnt_touch_globalsI)
apply (wp arch_perform_invocation_globals_equiv)
apply (simp add: invs_valid_vs_lookup invs_def valid_state_def valid_pspace_def)+
done
lemma find_pd_for_asid_authority3:
"\<lbrace>\<lambda>s. \<forall>pd. (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) \<and> (\<exists>\<rhd> pd) s
\<longrightarrow> Q pd s\<rbrace>
@ -1760,7 +1774,6 @@ requalify_facts
thread_set_globals_equiv
arch_post_modify_registers_cur_domain
arch_post_modify_registers_cur_thread
invs_imps
length_msg_lt_msg_max
set_mrs_globals_equiv
arch_perform_invocation_globals_equiv
@ -1769,6 +1782,7 @@ requalify_facts
make_arch_fault_msg_inv
check_valid_ipc_buffer_inv
arch_tcb_update_aux2
arch_perform_invocation_reads_respects_g
declare
arch_post_cap_deletion_valid_global_objs[wp]

2
proof/infoflow/ARM/ArchCNode_IF.thy
View File

@ -45,7 +45,7 @@ lemma set_cap_globals_equiv':
done
lemma set_cap_globals_equiv[CNode_IF_assms]:
"\<lbrace>globals_equiv s and valid_global_objs\<rbrace>
"\<lbrace>globals_equiv s and valid_global_objs and valid_arch_state\<rbrace>
set_cap cap p
\<lbrace>\<lambda>_. globals_equiv s\<rbrace>"
unfolding set_cap_def

3
proof/infoflow/ARM/ArchFinalise_IF.thy
View File

@ -334,8 +334,7 @@ lemma pagebitsforsize_ge_2[simp]:
by (induct vmpage_size; simp)
lemma arch_finalise_cap_globals_equiv[Finalise_IF_assms]:
"\<lbrace>globals_equiv st and valid_global_objs and valid_arch_state and pspace_aligned
and valid_vspace_objs and valid_global_refs and valid_vs_lookup\<rbrace>
"\<lbrace>globals_equiv st and invs and valid_arch_cap cap\<rbrace>
arch_finalise_cap cap b
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (induct cap; simp add: arch_finalise_cap_def)

66
proof/infoflow/ARM/ArchNoninterference.thy
View File

@ -118,7 +118,7 @@ lemma owns_mapping_owns_asidpool:
apply simp
done
lemma partitionIntegrity_subjectAffects_aobj[Noninterference_assms]:
lemma partitionIntegrity_subjectAffects_aobj':
"\<lbrakk> kheap s x = Some (ArchObj ao); ao \<noteq> ao'; pas_refined aag s;
silc_inv aag st s; pas_wellformed_noninterference aag;
arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
@ -138,6 +138,65 @@ lemma partitionIntegrity_subjectAffects_aobj[Noninterference_assms]:
apply (frule (1) pas_wellformed_noninterference_control_to_eq)
by (fastforce elim!: silc_inv_cnode_onlyE obj_atE simp: is_cap_table_def)
lemma inte_obj_arch:
assumes inte_obj: "(integrity_obj_atomic aag activate subjects l)\<^sup>*\<^sup>* ko ko'"
assumes "ko = Some (ArchObj ao)"
assumes "ko \<noteq> ko'"
shows "integrity_obj_atomic aag activate subjects l ko ko'"
proof (cases "l \<in> subjects")
case True
then show ?thesis by (fastforce intro: integrity_obj_atomic.intros)
next
case False
note l = this
have "\<forall>ao'. ko = Some (ArchObj ao) \<longrightarrow>
ko \<noteq> ko' \<longrightarrow>
integrity_obj_atomic aag activate subjects l ko ko'"
using inte_obj
proof (induct rule: rtranclp_induct)
case base
then show ?case by clarsimp
next
case (step y z)
have "\<exists>ao'. ko' = Some (ArchObj ao')"
using False inte_obj assms
by (auto elim!: rtranclp_induct integrity_obj_atomic.cases)
then show ?case using step.hyps
by (fastforce intro: troa_arch arch_troa_asidpool_clear integrity_obj_atomic.intros
elim!: integrity_obj_atomic.cases arch_integrity_obj_atomic.cases)
qed
then show ?thesis
using assms by fastforce
qed
lemma partitionIntegrity_subjectAffects_aobj[Noninterference_assms]:
assumes par_inte: "partitionIntegrity aag s s'"
and "kheap s x = Some (ArchObj ao)"
"kheap s x \<noteq> kheap s' x"
"silc_inv aag st s"
"pas_refined aag s"
"pas_wellformed_noninterference aag"
notes inte_obj = par_inte[THEN partitionIntegrity_integrity, THEN integrity_subjects_obj,
THEN spec[where x=x], simplified integrity_obj_def, simplified]
shows "subject_can_affect_label_directly aag (pasObjectAbs aag x)"
proof (cases "pasObjectAbs aag x = pasSubject aag")
case True
then show ?thesis by (simp add: subjectAffects.intros(1))
next
case False
obtain ao' where ao': "kheap s' x = Some (ArchObj ao')"
using assms False inte_obj_arch[OF inte_obj]
by (auto elim: integrity_obj_atomic.cases)
have arch_tro:
"arch_integrity_obj_atomic (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>)
{pasSubject aag} (pasObjectAbs aag x) ao ao'"
using assms False ao' inte_obj_arch[OF inte_obj]
by (auto elim: integrity_obj_atomic.cases)
show ?thesis
using assms ao' arch_tro
by (fastforce dest: partitionIntegrity_subjectAffects_aobj')
qed
lemma partitionIntegrity_subjectAffects_asid[Noninterference_assms]:
"\<lbrakk> partitionIntegrity aag s s'; pas_refined aag s; valid_objs s;
valid_arch_state s; valid_arch_state s'; pas_wellformed_noninterference aag;
@ -314,6 +373,11 @@ lemma dmo_getActive_IRQ_reads_respect_scheduler[Noninterference_assms]:
apply (simp add: scheduler_equiv_def)
done
lemma integrity_asids_update_reference_state[Noninterference_assms]:
"is_subject aag t
\<Longrightarrow> integrity_asids aag {pasSubject aag} x asid s (s\<lparr>kheap := kheap s(t \<mapsto> blah)\<rparr>)"
by clarsimp
end
context begin interpretation Arch .

9
proof/infoflow/ARM/ArchRetype_IF.thy
View File

@ -489,6 +489,7 @@ lemma reset_untyped_cap_reads_respects_g:
apply (strengthen invs_valid_global_objs)
apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
delete_objects_pspace_no_overlap_again
delete_objects_valid_arch_state
only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
del: Untyped_AI.delete_objects_pspace_no_overlap
| simp)+
@ -506,7 +507,7 @@ lemma reset_untyped_cap_reads_respects_g:
apply (drule ex_cte_cap_protects[OF _ _ _ _ order_refl], erule caps_of_state_cteD)
apply (clarsimp simp: descendants_range_def2 empty_descendants_range_in)
apply clarsimp+
apply (fastforce simp: untyped_min_bits_def)
apply (fastforce simp: untyped_min_bits_def ptr_range_def)
done
lemma retype_region_ret_pd_aligned:
@ -596,7 +597,7 @@ lemma invoke_untyped_reads_respects_g_wcap[Retype_IF_assms]:
split del: if_split)
apply (frule(1) valid_global_refsD2[OF _ invs_valid_global_refs])
apply (strengthen refl)
apply (strengthen invs_valid_global_objs)
apply (strengthen invs_valid_global_objs invs_arch_state)
apply (clarsimp simp: authorised_untyped_inv_def conj_comms invoke_untyped_proofs.simps)
apply (simp add: arg_cong[OF mask_out_sub_mask, where f="\<lambda>y. x - y" for x]
field_simps invoke_untyped_proofs.idx_le_new_offs
@ -654,7 +655,7 @@ lemma reset_untyped_cap_globals_equiv:
preemption_point_inv | simp add: unless_def)+
apply (rule valid_validE)
apply (rule_tac P="cap_aligned cap \<and> is_untyped_cap cap" in hoare_gen_asm)
apply (rule_tac Q="\<lambda>_ s. valid_global_objs s \<and> globals_equiv st s"
apply (rule_tac Q="\<lambda>_ s. valid_global_objs s \<and> valid_arch_state s \<and> globals_equiv st s"
in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_wp')
apply (rule hoare_pre)
@ -664,7 +665,7 @@ lemma reset_untyped_cap_globals_equiv:
cap_aligned_def bits_of_def
free_index_of_def)
apply (clarsimp simp: reset_chunk_bits_def)
apply (strengthen invs_valid_global_objs)
apply (strengthen invs_valid_global_objs invs_arch_state)
apply (wp delete_objects_invs_ex hoare_vcg_const_imp_lift get_cap_wp)+
apply (clarsimp simp: cte_wp_at_caps_of_state descendants_range_def2 is_cap_simps bits_of_def
split del: if_split)

14
proof/infoflow/ARM/ArchSyscall_IF.thy
View File

@ -29,20 +29,6 @@ lemma thread_set_globals_equiv'[Syscall_IF_assms]:
apply (fastforce simp: obj_at_def get_tcb_def valid_arch_state_def)+
done
lemma arch_perform_invocation_reads_respects_g[Syscall_IF_assms]:
assumes domains_distinct: "pas_domains_distinct aag"
shows "reads_respects_g aag l (ct_active and authorised_arch_inv aag ai and valid_arch_inv ai
and authorised_for_globals_arch_inv ai and invs
and pas_refined aag and is_subject aag \<circ> cur_thread)
(arch_perform_invocation ai)"
apply (rule equiv_valid_guard_imp)
apply (rule reads_respects_g)
apply (rule arch_perform_invocation_reads_respects[OF domains_distinct])
apply (rule doesnt_touch_globalsI)
apply (wp arch_perform_invocation_globals_equiv)
apply (simp add: invs_valid_vs_lookup invs_def valid_state_def valid_pspace_def)+
done
lemma sts_authorised_for_globals_inv[Syscall_IF_assms]:
"set_thread_state d f \<lbrace>authorised_for_globals_inv oper\<rbrace>"
unfolding authorised_for_globals_inv_def authorised_for_globals_arch_inv_def

10
proof/infoflow/ARM/ArchUserOp_IF.thy
View File

@ -927,10 +927,10 @@ lemma getExMonitor_wp[wp]:
by (simp add: getExMonitor_def | wp)+
definition valid_vspace_objs' where
"valid_vspace_objs' \<equiv> valid_pdpt_objs"
definition valid_vspace_objs_if where
"valid_vspace_objs_if \<equiv> valid_pdpt_objs"
declare valid_vspace_objs'_def[simp]
declare valid_vspace_objs_if_def[simp]
lemma do_user_op_reads_respects_g:
@ -938,7 +938,7 @@ lemma do_user_op_reads_respects_g:
shows
"(\<forall>pl pr pxn tc ms s. P tc s \<and> context_matches_state pl pr pxn ms s
\<longrightarrow> (\<exists>x. uop (cur_thread s) pl pr pxn (tc, ms) = {x}))
\<Longrightarrow> reads_respects_g aag l (pas_refined aag and invs and valid_vspace_objs'
\<Longrightarrow> reads_respects_g aag l (pas_refined aag and invs and valid_vspace_objs_if
and is_subject aag \<circ> cur_thread
and (\<lambda>s. cur_thread s \<noteq> idle_thread s) and P tc)
(do_user_op_if uop tc)"
@ -1000,7 +1000,7 @@ context begin interpretation Arch .
requalify_consts
do_user_op_if
valid_vspace_objs'
valid_vspace_objs_if
context_matches_state
requalify_facts