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

ARM infoflow: proof update for user_context refactor

This commit is contained in:
Gerwin Klein 2018-02-28 09:42:46 +11:00
parent 84633ccb7f
commit 3f7d6e1ce9
5 changed files with 19 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
proof/infoflow/Arch_IF.thy
View File

@ -930,13 +930,6 @@ lemma modify_det:
apply(clarsimp simp: det_def modify_def get_def put_def bind_def)
done
lemma set_register_det:
"det (set_register a b)"
unfolding set_register_def
apply(rule modify_det)
done
lemma dummy_kheap_update:
"st = st\<lparr> kheap := kheap st \<rparr>"
by simp
@ -966,7 +959,7 @@ lemma get_tcb_not_asid_pool_at:
lemma as_user_set_register_ev2:
"labels_are_invisible aag l (pasObjectAbs aag ` {thread,thread'}) \<Longrightarrow>
equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (op =) \<top> \<top> (as_user thread (set_register x y)) (as_user thread' (set_register a b))"
equiv_valid_2 (reads_equiv aag) (affects_equiv aag l) (affects_equiv aag l) (op =) \<top> \<top> (as_user thread (setRegister x y)) (as_user thread' (setRegister a b))"
apply(simp add: as_user_def)
apply(rule equiv_valid_2_guard_imp)
apply(rule_tac L="{pasObjectAbs aag thread}" and L'="{pasObjectAbs aag thread'}" and Q="\<top>" and Q'="\<top>" in ev2_invisible)
@ -993,12 +986,12 @@ lemma reads_affects_equiv_get_tcb_eq:
done
lemma as_user_set_register_reads_respects':
"reads_respects aag l \<top> (as_user thread (set_register x y))"
"reads_respects aag l \<top> (as_user thread (setRegister x y))"
apply (case_tac "aag_can_read aag thread \<or> aag_can_affect aag l thread")
apply (simp add: as_user_def fun_app_def split_def)
apply (rule gen_asm_ev)
apply (wp set_object_reads_respects select_f_ev gets_the_ev)
apply (auto intro: reads_affects_equiv_get_tcb_eq set_register_det)[1]
apply (auto intro: reads_affects_equiv_get_tcb_eq det_setRegister)[1]
apply(simp add: equiv_valid_def2)
apply(rule as_user_set_register_ev2)
apply(simp add: labels_are_invisible_def)

2
proof/infoflow/InfoFlow.thy
View File

@ -1248,7 +1248,7 @@ lemma as_user_reads_respects:
lemma get_message_info_rev:
"reads_equiv_valid_inv A aag (K (is_subject aag ptr)) (get_message_info ptr)"
apply (simp add: get_message_info_def)
apply (wp as_user_rev | clarsimp simp: get_register_def)+
apply (wp as_user_rev | clarsimp simp: getRegister_def)+
done
lemma syscall_rev:

21
proof/infoflow/Ipc_IF.thy
View File

@ -1428,11 +1428,6 @@ lemma aag_has_auth_to_read_mrs:
done
lemma get_register_det:
"det (get_register x)"
apply(clarsimp simp: get_register_def)
done
abbreviation aag_can_read_or_affect where
"aag_can_read_or_affect aag l x \<equiv>
aag_can_read aag x \<or> aag_can_affect aag l x"
@ -1482,7 +1477,7 @@ lemma copy_mrs_reads_respects:
load_word_offs_reads_respects as_user_set_register_reads_respects'
as_user_reads_respects
| wpc
| simp add: set_register_det get_register_det split del: if_split)+
| simp add: det_setRegister det_getRegister split del: if_split)+
apply clarsimp
apply(rename_tac n')
apply(subgoal_tac " ptr_range (x + of_nat n' * of_nat word_size) 2
@ -1539,7 +1534,7 @@ lemma ev_irrelevant_bind:
lemma get_message_info_reads_respects:
"reads_respects aag l (K (aag_can_read_or_affect aag l ptr)) (get_message_info ptr)"
apply (simp add: get_message_info_def)
apply (wp as_user_reads_respects | clarsimp simp: get_register_def)+
apply (wp as_user_reads_respects | clarsimp simp: getRegister_def)+
done
lemma do_normal_transfer_reads_respects:
@ -1559,7 +1554,7 @@ lemma do_normal_transfer_reads_respects:
lookup_extra_caps_auth get_message_info_rev
get_mi_length' get_mi_length validE_E_wp_post_taut
| wpc
| simp add: set_register_det ball_conj_distrib)+
| simp add: det_setRegister ball_conj_distrib)+
apply (fastforce intro: aag_has_read_auth_can_read_or_affect_ipc_buffer)
apply(rule gen_asm_ev)
apply(simp add: do_normal_transfer_def transfer_caps_def)
@ -1646,7 +1641,11 @@ lemma do_fault_transfer_reads_respects:
"reads_respects aag l (K (aag_can_read_or_affect aag l sender \<and> ipc_buffer_has_auth aag receiver buf \<and>
(case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits))) (do_fault_transfer badge sender receiver buf)"
unfolding do_fault_transfer_def
apply (wp as_user_set_register_reads_respects' as_user_reads_respects set_message_info_reads_respects set_mrs_reads_respects' make_fault_msg_reads_respects thread_get_reads_respects | wpc | simp add: split_def set_register_det | wp_once hoare_drop_imps)+
apply (wp as_user_set_register_reads_respects' as_user_reads_respects set_message_info_reads_respects
set_mrs_reads_respects' make_fault_msg_reads_respects thread_get_reads_respects
| wpc
| simp add: split_def det_setRegister
| wp_once hoare_drop_imps)+
done
@ -2001,7 +2000,7 @@ lemma handle_fault_reply_reads_respects:
apply(case_tac fault)
apply (wp as_user_reads_respects thread_get_reads_respects
thread_get_wp' handle_arch_fault_reply_reads_respects[simplified K_def]
| simp add: reads_lrefl det_zipWithM_x set_register_det)+
| simp add: reads_lrefl det_zipWithM_x det_setRegister)+
done
lemma lookup_ipc_buffer_has_read_auth':
@ -2075,7 +2074,7 @@ lemma reply_from_kernel_reads_respects:
unfolding reply_from_kernel_def fun_app_def
apply (wp set_message_info_reads_respects set_mrs_reads_respects
as_user_reads_respects lookup_ipc_buffer_reads_respects
| simp add: split_def reads_lrefl set_register_det)+
| simp add: split_def reads_lrefl det_setRegister)+
done

4
proof/infoflow/Syscall_IF.thy
View File

@ -593,7 +593,7 @@ lemma handle_invocation_reads_respects_g:
)+
apply (rule conjI)
apply (clarsimp simp: requiv_g_cur_thread_eq simp: reads_equiv_f_g_conj)
apply (clarsimp simp: get_register_def invs_sym_refs invs_def valid_state_def valid_arch_state_ko_at_arm valid_pspace_vo valid_pspace_distinct)
apply (clarsimp simp: getRegister_def invs_sym_refs invs_def valid_state_def valid_arch_state_ko_at_arm valid_pspace_vo valid_pspace_distinct)
apply (rule context_conjI)
apply (simp add: ct_active_not_idle')
apply (clarsimp simp: valid_pspace_def ct_in_state_def)
@ -718,7 +718,7 @@ lemma handle_recv_reads_respects_f:
apply (wp reads_respects_f[OF as_user_reads_respects,where st=st and Q=\<top>])
apply simp
apply (wp as_user_silc_inv[where st=st] | simp)+
apply (simp add: get_register_det invs_valid_objs tcb_at_invs)
apply (simp add: det_getRegister invs_valid_objs tcb_at_invs)
done
lemma handle_recv_globals_equiv:

14
proof/infoflow/Tcb_IF.thy
View File

@ -74,15 +74,7 @@ crunch globals_equiv[wp]: restart "globals_equiv st"
(wp: cancel_ipc_valid_ko_at_arm hoare_vcg_if_lift2 dxo_wp_weak hoare_drop_imps
ignore: reschedule_required possible_switch_to)
lemma as_user_globals_equiv[wp]:
"\<lbrace> globals_equiv st and valid_ko_at_arm and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>
as_user thread f
\<lbrace> \<lambda>_. globals_equiv st \<rbrace>"
unfolding as_user_def fun_app_def
apply (wp set_object_globals_equiv | simp add: split_def)+
apply (simp add: valid_ko_at_arm_def)
apply (clarsimp simp: get_tcb_def obj_at_def)
done
declare as_user_globals_equiv[wp]
lemma cap_ne_global_pd : "ex_nonz_cap_to word s \<Longrightarrow> valid_global_refs s \<Longrightarrow> word \<noteq> arm_global_pd (arch_state s)"
unfolding ex_nonz_cap_to_def
@ -330,7 +322,7 @@ lemma invoke_tcb_thread_preservation:
assumes thread_set_P: "\<And>f ptr. \<lbrace>invs and P\<rbrace> thread_set (tcb_ipc_buffer_update f) ptr \<lbrace>\<lambda>_.P\<rbrace>"
assumes thread_set_P': "\<And>f ptr. \<lbrace>invs and P\<rbrace> thread_set (tcb_fault_handler_update f) ptr \<lbrace>\<lambda>_.P\<rbrace>"
assumes set_mcpriority_P: "\<And>mcp ptr. \<lbrace>invs and P\<rbrace> set_mcpriority ptr mcp \<lbrace>\<lambda>_.P\<rbrace>"
assumes set_register_P[wp]: "\<And>d. \<lbrace>P and invs and (\<lambda>s. t \<noteq> idle_thread s)\<rbrace> as_user t (set_register TPIDRURW d) \<lbrace>\<lambda>_. P\<rbrace>"
assumes set_register_P[wp]: "\<And>d. \<lbrace>P and invs and (\<lambda>s. t \<noteq> idle_thread s)\<rbrace> as_user t (setRegister TPIDRURW d) \<lbrace>\<lambda>_. P\<rbrace>"
assumes P_trans[simp]: "\<And>f s. P (trans_state f s) = P s"
shows "
\<lbrace>P and invs and Tcb_AI.tcb_inv_wf (tcb_invocation.ThreadControl t sl ep mcp prio croot vroot buf)\<rbrace>
@ -730,7 +722,7 @@ lemma invoke_tcb_reads_respects_f:
| simp add: tcb_cap_cases_def | wpc)+
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
set_register_det
det_setRegister
| intro impI
| rule conjI)+
(*Extra slow*)