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

SELFOUR-444: Repair InfoFlow.

This commit is contained in:
Thomas Sewell 2016-10-18 00:56:47 +11:00
parent f1d546db85
commit 0fa247199b
5 changed files with 44 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/infoflow/ADT_IF.thy
View File

@ -3061,7 +3061,7 @@ lemma reset_untyped_cap_irq_state_inv:
preemption_point_irq_state_inv'[where irq=irq]
get_cap_wp
| rule irq_state_inv_triv
| simp
| simp add: unless_def
| wp_once dmo_wp)+
done

21
proof/infoflow/Example_Valid_StateH.thy
View File

@ -1107,6 +1107,7 @@ where
High_cnode_ptr \<mapsto> 10,
Silc_cnode_ptr \<mapsto> 10,
irq_cnode_ptr \<mapsto> 0),
gsUntypedZeroRanges = ran (map_comp untypedZeroRange (option_map cteCap o map_to_ctes kh0H)),
gsMaxObjectSize = card (UNIV :: word32 set),
ksDomScheduleIdx = 0,
ksDomSchedule = [(0 ,10), (1, 10)],
@ -1547,6 +1548,11 @@ lemma map_to_ctes_kh0H:
((clarsimp simp: kh0H_dom_sets_distinct[THEN orthD1] not_in_range_cte_None irq_node_offs_in_range |
clarsimp simp: kh0H_dom_sets_distinct[THEN orthD2] not_in_range_cte_None)+)[1])+
lemma option_update_range_map_comp:
"option_update_range m m' = map_add m' m"
by (simp add: fun_eq_iff option_update_range_def map_comp_def map_add_def
split: option.split)
lemma tcb_offs_in_rangeI:
"\<lbrakk>ptr \<le> ptr + x; ptr + x \<le> ptr + 2 ^ 9 - 1\<rbrakk> \<Longrightarrow> ptr + x \<in> tcb_offs_range ptr"
by (simp add: tcb_offs_range_def)
@ -3034,16 +3040,11 @@ lemma s0H_invs:
apply (clarsimp split: split_if_asm)
apply (rule conjI)
apply (clarsimp simp: kdr_pspace_domain_valid) (* use axiomatization for now *)
apply (rule conjI)
apply (clarsimp simp: s0H_internal_def)
apply (rule conjI)
apply (clarsimp simp: s0H_internal_def)
apply (rule conjI)
apply (clarsimp simp: s0H_internal_def maxDomain_def numDomains_def dschDomain_def dschLength_def)
apply (rule conjI)
apply (clarsimp simp: s0H_internal_def newKernelState_def newKSDomSched)
apply (rule conjI)
apply (clarsimp simp: s0H_internal_def newKernelState_def newKSDomSched)
(* unfold s0H_internal for remaining goals *)
apply (clarsimp simp: s0H_internal_def cteCaps_of_def
untyped_ranges_zero_inv_def
maxDomain_def numDomains_def dschDomain_def dschLength_def)
apply (clarsimp simp: newKernelState_def newKSDomSched)
apply (clarsimp simp: cur_tcb'_def obj_at'_def projectKO_eq project_inject s0H_internal_def objBitsKO_def s0_ptrs_aligned)
apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified s0H_internal_def])
apply (simp add: objBitsKO_def kh0H_simps[simplified cte_level_bits_def])

2
proof/infoflow/FinalCaps.thy
View File

@ -2116,7 +2116,7 @@ lemma reset_untyped_cap_silc_inv:
apply (rule hoare_gen_asm)
apply (simp add: reset_untyped_cap_def cong: if_cong)
apply (rule validE_valid, rule hoare_pre)
apply (wp set_cap_silc_inv_simple | simp)+
apply (wp set_cap_silc_inv_simple | simp add: unless_def)+
apply (rule valid_validE, rule_tac Q="\<lambda>_. cte_wp_at is_untyped_cap slot
and silc_inv aag st" in hoare_strengthen_post)
apply (rule validE_valid, rule mapME_x_inv_wp, rule hoare_pre)

35
proof/infoflow/Noninterference.thy
View File

@ -2548,12 +2548,19 @@ lemma partitionIntegrity_irq_state_update[simp]:
apply(cut_tac s=y and aag=aag in partitionIntegrity_refl)
apply(clarsimp simp: partitionIntegrity_def integrity_subjects_def domain_fields_equiv_def globals_equiv_scheduler_def silc_dom_equiv_def equiv_for_def)
done
lemma invs_if_Invs:
"invs_if s
\<Longrightarrow> Invs (internal_state_if s)
\<and> det_inv (sys_mode_of s) (cur_thread_context_of s) (internal_state_if s)"
by (simp add: invs_if_def)
lemma do_user_op_A_if_confidentiality:
notes
read_respects_irq =
use_ev[OF check_active_irq_if_reads_respects_f_g[
where st=s0_internal and st'=s0_internal and irq=timer_irq]] and
where st=s0_internal and st'=s0_internal and irq=timer_irq
and aag="current_aag (internal_state_if s)"]] and
read_respects_user_op =
use_ev[OF do_user_op_if_reads_respects_f_g[
where aag="current_aag (internal_state_if s)" and st="s0_internal"]]
@ -2577,10 +2584,9 @@ lemma do_user_op_A_if_confidentiality:
H: "(_,_) \<in> fst (check_active_irq_if _ p)"
for p q \<Rightarrow> \<open>rule revcut_rl[OF read_respects_irq[where t=q, OF H]]\<close>)
apply assumption
apply (clarsimp simp: invs_if_def Invs_def)
apply assumption
apply(clarsimp simp: invs_if_def Invs_def)
apply(drule uwr_PSched_cur_domain)
apply (clarsimp dest!: invs_if_Invs simp: Invs_def)
apply (drule uwr_PSched_cur_domain)
apply (clarsimp dest!: invs_if_Invs simp: Invs_def)
apply(clarsimp simp: current_aag_def)
apply simp
apply fastforce
@ -2591,7 +2597,8 @@ lemma do_user_op_A_if_confidentiality:
apply assumption
apply (match premises in "s = ((_,p),_)" and H: "(_,_) \<in> fst (check_active_irq_if _ p)"
for p \<Rightarrow> \<open>rule revcut_rl[OF use_valid[OF H check_active_irq_if_User_det_inv]]\<close>)
apply (clarsimp simp: invs_if_def Invs_def cur_thread_context_of_def)
apply (simp(no_asm_use) add: invs_if_def Invs_def cur_thread_context_of_def)
apply (clarsimp simp only: simp_thms)
apply simp
apply (erule use_valid)
apply(wp check_active_irq_if_wp)
@ -2601,7 +2608,8 @@ lemma do_user_op_A_if_confidentiality:
apply (simp add: active_from_running)+
apply (match premises in "t_aux = (_,q)" and H: "(_,q) \<in> fst (check_active_irq_if _ _)"
for q \<Rightarrow> \<open>rule revcut_rl[OF use_valid[OF H check_active_irq_if_User_det_inv]]\<close>)
apply (clarsimp simp: invs_if_def Invs_def cur_thread_context_of_def)
apply (simp(no_asm_use) add: invs_if_def Invs_def cur_thread_context_of_def)
apply (clarsimp simp only: simp_thms)
apply simp
apply(erule_tac s'=yc in use_valid)
apply(wp check_active_irq_if_wp)
@ -2615,19 +2623,21 @@ lemma do_user_op_A_if_confidentiality:
apply (match premises in "t = ((_,q),_)" for q \<Rightarrow>
\<open>rule revcut_rl[OF current_aag_def[where t=q]]\<close>)
apply (rule guarded_pas_is_subject_current_aag[rule_format])
apply (simp add: active_from_running)+
apply (simp only: active_from_running)+
apply(drule uwr_PSched_cur_domain, simp add: current_aag_def)
apply simp
apply simp
apply simp
apply(rule reads_equiv_f_g_affects_equiv_uwr)
apply (simp add: invs_if_def Invs_def)+
apply ((clarsimp simp: Invs_def dest!: invs_if_Invs; rule TrueI)+)
apply (simp add: invs_if_def Invs_def)+
apply(erule use_valid[OF _ do_user_op_if_partitionIntegrity])
apply(erule use_valid[OF _ check_active_irq_if_wp])
apply(clarsimp)
apply(frule (1) ct_running_cur_thread_not_idle_thread[OF invs_valid_idle])
apply (rule guarded_pas_is_subject_current_aag[rule_format])
apply (simp add: active_from_running)+
apply (simp only: active_from_running)+
apply simp
apply(erule_tac s'=s'aa in use_valid[OF _ do_user_op_if_partitionIntegrity])
apply(erule_tac s'=yc in use_valid[OF _ check_active_irq_if_wp])
apply(clarsimp)
@ -2636,11 +2646,10 @@ lemma do_user_op_A_if_confidentiality:
\<open>rule revcut_rl[OF ct_running_cur_thread_not_idle_thread[OF invs_valid_idle[OF H]]]\<close>)
apply assumption
apply (rule guarded_pas_is_subject_current_aag[rule_format])
apply (simp add: active_from_running)+
apply (simp only: active_from_running)+
apply(simp add: sys_mode_of_def)
apply(simp add: user_context_of_def)
done
lemma do_user_op_A_if_confidentiality':
"\<lbrakk>(XX, YY) \<in> uwr PSched; XX = s; YY = t; (s, t) \<in> uwr (part s); (s, t) \<in> uwr u;

12
proof/infoflow/Retype_IF.thy
View File

@ -1045,6 +1045,10 @@ lemma delete_objects_pspace_no_overlap_again:
apply(simp add: valid_cap_simps cap_aligned_def is_aligned_neg_mask_eq field_simps)
done
lemma ex_tupleI:
"P (fst t) (snd t) \<Longrightarrow> \<exists>a b. P a b"
by blast
lemma reset_untyped_cap_reads_respects_g:
"reads_equiv_valid_g_inv (affects_equiv aag l) aag
(\<lambda>s. cte_wp_at is_untyped_cap slot s \<and> invs s \<and> ct_active s
@ -1052,7 +1056,7 @@ lemma reset_untyped_cap_reads_respects_g:
\<and> is_subject aag (fst slot)
\<and> (descendants_of slot (cdt s) = {}))
(reset_untyped_cap slot)"
apply (simp add: reset_untyped_cap_def)
apply (simp add: reset_untyped_cap_def cong: if_cong)
apply (rule equiv_valid_guard_imp)
apply (wp set_cap_reads_respects_g dmo_clearMemory_reads_respects_g
| simp add: unless_def when_def split del: split_if)+
@ -1128,12 +1132,14 @@ lemma reset_untyped_cap_reads_respects_g:
apply (clarsimp simp: ptr_range_def[symmetric] global_refs_def
descendants_range_def2)
apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+)
apply (strengthen empty_descendants_range_in)
apply (strengthen refl[where t=True] refl ex_tupleI[where t=slot]
empty_descendants_range_in
| clarsimp)+
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 (cases slot, fastforce)
apply fastforce
done
lemma equiv_valid_obtain: