CamkesCdlRefine, Lib: add debug tag for integrity policy
This tags each generated policy goal with the object and cap that led to that goal. We create a new constant `generic_tag` in Lib for this purpose.
This commit is contained in:
parent
31d5c1c70e
commit
2c3b4c24fc
|
@ -17,6 +17,7 @@ imports
|
||||||
"Lib.FastMap"
|
"Lib.FastMap"
|
||||||
"Lib.RangeMap"
|
"Lib.RangeMap"
|
||||||
"Lib.FP_Eval"
|
"Lib.FP_Eval"
|
||||||
|
"Lib.GenericTag"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
text \<open>
|
text \<open>
|
||||||
|
@ -244,14 +245,16 @@ lemma helper_pcs_refined_policy__eval:
|
||||||
\<forall>auth \<in> cdl_cap_auth_conferred cap.
|
\<forall>auth \<in> cdl_cap_auth_conferred cap.
|
||||||
\<forall>oref \<in> cdl_obj_refs cap.
|
\<forall>oref \<in> cdl_obj_refs cap.
|
||||||
(case label_spec oref of
|
(case label_spec oref of
|
||||||
Some orefl \<Rightarrow> (pl, auth, orefl) \<in> policy_spec
|
Some orefl \<Rightarrow> generic_tag ''obj policy'' (p, cap, cdl_obj_refs cap)
|
||||||
|
((pl, auth, orefl) \<in> policy_spec)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
| _ \<Rightarrow> False)"
|
| _ \<Rightarrow> False)"
|
||||||
shows "auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> (pasPolicy aag)"
|
shows "auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> (pasPolicy aag)"
|
||||||
apply (rule helper_pcs_refined_policyI)
|
apply (rule helper_pcs_refined_policyI)
|
||||||
apply (blast intro: cdt_policy)
|
apply (blast intro: cdt_policy)
|
||||||
apply (blast intro: delete_derived_policy)
|
apply (blast intro: delete_derived_policy)
|
||||||
apply (fastforce intro: subsetD[OF policy_spec]
|
apply (fastforce simp: remove_generic_tag
|
||||||
|
intro: subsetD[OF policy_spec]
|
||||||
dest: label_spec obj_policy[simplified graph_of_def, simplified, rule_format]
|
dest: label_spec obj_policy[simplified graph_of_def, simplified, rule_format]
|
||||||
split: option.splits)
|
split: option.splits)
|
||||||
done
|
done
|
||||||
|
@ -398,13 +401,14 @@ lemma cdl_state_irqs_to_policy__eval:
|
||||||
\<forall>(p_idx, cap) \<in> graph_of (object_slots p_obj).
|
\<forall>(p_idx, cap) \<in> graph_of (object_slots p_obj).
|
||||||
\<forall>irq \<in> cdl_cap_irqs_controlled cap.
|
\<forall>irq \<in> cdl_cap_irqs_controlled cap.
|
||||||
(case irq_label_spec irq of
|
(case irq_label_spec irq of
|
||||||
Some irql \<Rightarrow> (pl, Control, irql) \<in> policy_spec
|
Some irql \<Rightarrow> generic_tag ''irq policy'' (p, cap, irq)
|
||||||
|
((pl, Control, irql) \<in> policy_spec)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
\<Longrightarrow> cdl_state_irqs_to_policy aag s \<subseteq> pasPolicy aag"
|
\<Longrightarrow> cdl_state_irqs_to_policy aag s \<subseteq> pasPolicy aag"
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (erule cdl_state_irqs_to_policy_aux.cases)
|
apply (erule cdl_state_irqs_to_policy_aux.cases)
|
||||||
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def
|
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def remove_generic_tag
|
||||||
split: option.splits
|
split: option.splits
|
||||||
dest: obj_label_spec irq_label_spec
|
dest: obj_label_spec irq_label_spec
|
||||||
intro: subsetD[OF policy_spec])
|
intro: subsetD[OF policy_spec])
|
||||||
|
@ -422,7 +426,8 @@ lemma cdl_state_asids_to_policy__eval:
|
||||||
\<forall>(p_idx, cap) \<in> graph_of (object_slots p_obj).
|
\<forall>(p_idx, cap) \<in> graph_of (object_slots p_obj).
|
||||||
\<forall>asid \<in> asid_high_bits_of ` cdl_cap_asid' cap.
|
\<forall>asid \<in> asid_high_bits_of ` cdl_cap_asid' cap.
|
||||||
(case asid_label_spec asid of
|
(case asid_label_spec asid of
|
||||||
Some irql \<Rightarrow> (pl, Control, irql) \<in> policy_spec
|
Some asidl \<Rightarrow> generic_tag ''asid policy'' (p, cap, asid)
|
||||||
|
((pl, Control, asidl) \<in> policy_spec)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
| _ \<Rightarrow> False)"
|
| _ \<Rightarrow> False)"
|
||||||
and asid_table_lookups:
|
and asid_table_lookups:
|
||||||
|
@ -435,29 +440,31 @@ lemma cdl_state_asids_to_policy__eval:
|
||||||
\<forall>(asid_low, pd_cap) \<in> graph_of (object_slots asid_pool).
|
\<forall>(asid_low, pd_cap) \<in> graph_of (object_slots asid_pool).
|
||||||
if is_null_cap pd_cap then True else
|
if is_null_cap pd_cap then True else
|
||||||
(case obj_label_spec (cap_object pd_cap) of
|
(case obj_label_spec (cap_object pd_cap) of
|
||||||
Some pdl \<Rightarrow> (asidl, Control, pdl) \<in> policy_spec
|
Some pdl \<Rightarrow> generic_tag ''asid PD policy'' (asid_high, pd_cap)
|
||||||
|
((asidl, Control, pdl) \<in> policy_spec)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
\<and> (case obj_label_spec (cap_object asid_pool_cap) of
|
\<and> (case obj_label_spec (cap_object asid_pool_cap) of
|
||||||
Some asid_pool_l \<Rightarrow>
|
Some asid_pool_l \<Rightarrow>
|
||||||
(asid_pool_l, ASIDPoolMapsASID, asidl) \<in> policy_spec
|
generic_tag ''asid pool policy'' (asid_high, asid_pool_cap)
|
||||||
|
((asid_pool_l, ASIDPoolMapsASID, asidl) \<in> policy_spec)
|
||||||
| _ \<Rightarrow> False)
|
| _ \<Rightarrow> False)
|
||||||
| _ \<Rightarrow> False)"
|
| _ \<Rightarrow> False)"
|
||||||
|
|
||||||
shows "cdl_state_asids_to_policy aag s \<subseteq> pasPolicy aag"
|
shows "cdl_state_asids_to_policy aag s \<subseteq> pasPolicy aag"
|
||||||
apply clarsimp
|
apply clarsimp
|
||||||
apply (erule cdl_state_asids_to_policy_aux.cases)
|
apply (erule cdl_state_asids_to_policy_aux.cases)
|
||||||
using cap_asids
|
using cap_asids[unfolded remove_generic_tag]
|
||||||
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def
|
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def
|
||||||
dest: obj_label_spec asid_label_spec
|
dest: obj_label_spec asid_label_spec
|
||||||
intro: subsetD[OF policy_spec]
|
intro: subsetD[OF policy_spec]
|
||||||
split: option.splits)
|
split: option.splits)
|
||||||
using asid_table_lookups
|
using asid_table_lookups[unfolded remove_generic_tag]
|
||||||
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def transform_asid_def
|
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def transform_asid_def
|
||||||
dest: obj_label_spec asid_label_spec
|
dest: obj_label_spec asid_label_spec
|
||||||
intro: subsetD[OF policy_spec]
|
intro: subsetD[OF policy_spec]
|
||||||
split: option.splits)
|
split: option.splits)
|
||||||
using asid_table_lookups
|
using asid_table_lookups[unfolded remove_generic_tag]
|
||||||
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def transform_asid_def
|
apply (fastforce simp: opt_cap_def slots_of_def graph_of_def transform_asid_def
|
||||||
dest: obj_label_spec asid_label_spec
|
dest: obj_label_spec asid_label_spec
|
||||||
intro: subsetD[OF policy_spec]
|
intro: subsetD[OF policy_spec]
|
||||||
|
|
|
@ -0,0 +1,44 @@
|
||||||
|
(*
|
||||||
|
* Copyright 2019, Data61
|
||||||
|
* Commonwealth Scientific and Industrial Research Organisation (CSIRO)
|
||||||
|
* ABN 41 687 119 230.
|
||||||
|
|
||||||
|
* This software may be distributed and modified according to the terms of
|
||||||
|
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
|
||||||
|
* See "LICENSE_BSD2.txt" for details.
|
||||||
|
|
||||||
|
* @TAG(DATA61_BSD)
|
||||||
|
*)
|
||||||
|
|
||||||
|
theory GenericTag
|
||||||
|
imports
|
||||||
|
HOL.HOL
|
||||||
|
begin
|
||||||
|
|
||||||
|
text \<open>
|
||||||
|
Generic annotation constant.
|
||||||
|
|
||||||
|
@{typ 'ns} is a namespace parameter and should be a different
|
||||||
|
type or constant for each distinct use of this constant.
|
||||||
|
|
||||||
|
@{typ 'tag} is an arbitrary annotation associated with the actual
|
||||||
|
value @{term x}.
|
||||||
|
\<close>
|
||||||
|
definition generic_tag :: "'ns \<Rightarrow> 'tag \<Rightarrow> 'a \<Rightarrow> 'a"
|
||||||
|
where remove_generic_tag[code del]: "generic_tag _ _ x \<equiv> x"
|
||||||
|
|
||||||
|
text \<open>Often the tagged value is a proposition to be proved.\<close>
|
||||||
|
lemma generic_tagP_I:
|
||||||
|
"P \<Longrightarrow> generic_tag ns tag P"
|
||||||
|
by (simp add: remove_generic_tag)
|
||||||
|
|
||||||
|
lemma generic_tag_True:
|
||||||
|
"generic_tag ns tag True"
|
||||||
|
by (simp add: remove_generic_tag)
|
||||||
|
|
||||||
|
text \<open>We often want to avoid rewriting under annotations.\<close>
|
||||||
|
lemma generic_tag_cong:
|
||||||
|
"x = x' \<Longrightarrow> generic_tag ns tag x = generic_tag ns tag x'"
|
||||||
|
by simp
|
||||||
|
|
||||||
|
end
|
1
lib/ROOT
1
lib/ROOT
|
@ -78,6 +78,7 @@ session Lib (lib) = Word_Lib +
|
||||||
Conjuncts
|
Conjuncts
|
||||||
DetWPLib
|
DetWPLib
|
||||||
Guess_ExI
|
Guess_ExI
|
||||||
|
GenericTag
|
||||||
|
|
||||||
(* should really be a separate session, but too entangled atm: *)
|
(* should really be a separate session, but too entangled atm: *)
|
||||||
NonDetMonadLemmaBucket
|
NonDetMonadLemmaBucket
|
||||||
|
|
Loading…
Reference in New Issue