diff options
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 117 |
1 files changed, 108 insertions, 9 deletions
diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean index 9950b1a..15a5d4b 100644 --- a/xacml-proofs/lean/Xacml.lean +++ b/xacml-proofs/lean/Xacml.lean @@ -215,6 +215,82 @@ inductive CombinatorAlgorithm where | legacy_permit_overrides : CombinatorAlgorithm | legacy_ordered_permit_overrides : CombinatorAlgorithm +namespace CombinatorAlgorithm + -- The output of a combining algorithm which does not track the extended set + -- of “Indeterminate” values MUST be treated as “Indeterminate{DP}” for the + -- value “Indeterminate” by a combining algorithm which tracks the extended + -- set of “Indeterminate” values. A combining algorithm which does not track + -- the extended set of “Indeterminate” values MUST treat the output of a + -- combining algorithm which tracks the extended set of “Indeterminate” values + -- as an “Indeterminate” for any of the possible values of the extended set of + -- “Indeterminate”. + + def eval_deny_overrides (results : List Decision') : Decision' := + if results.elem Decision'.deny then Decision'.deny else + if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else + if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else + if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else + if results.elem Decision'.permit then Decision'.permit else + if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else + Decision'.not_applicable + def eval_ordered_deny_overrides : List Decision' -> Decision' := eval_deny_overrides + + def eval_permit_overrides (results : List Decision') : Decision' := + if results.elem Decision'.permit then Decision'.permit else + if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else + if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else + if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else + if results.elem Decision'.deny then Decision'.deny else + if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else + Decision'.not_applicable + def eval_ordered_permit_overrides : List Decision' -> Decision' := eval_permit_overrides + + def eval_deny_unless_permit (results : List Decision') : Decision' := + if results.elem Decision'.permit then Decision'.permit else Decision'.deny + + def eval_permit_unless_deny (results : List Decision') : Decision' := + if results.elem Decision'.deny then Decision'.deny else Decision'.permit + + -- The non-normative part of the specification asserts that "If an error + -- occurs while evaluating the target or condition of a rule, then the + -- evaluation SHALL halt, and the policy shall evaluate to "Indeterminate", + -- with the appropriate error status." + -- + -- This behavior isn't spelled out in the normative part, because errors are + -- represented as an Indeterminate. + def eval_first_applicable_rule (results : List Decision') : Decision' := + match (results.filter (fun d => d != Decision'.not_applicable)).get? 0 with + | some a => a + | none => Decision'.not_applicable + + -- See the comment for `eval_first_applicable_rule`. + def eval_only_one_applicable (results : List Decision') : Decision' := + match results.filter (fun d => d != Decision'.not_applicable) with + | [] => Decision'.not_applicable + | [a] => a + | _ => Decision'.indeterminate + + def eval_legacy_deny_overrides_rule (results : List Decision') : Decision' := + -- Note that "any rule having Effect=Deny evaluates to Indeterminate" + -- corresponds to indeterminate_d, and "any rule having Effect=Permit + -- evaluates to Indeterminate" corresponds to indeterminate_p. + if results.elem Decision'.deny then Decision'.deny else + if results.elem Decision'.indeterminate_d then Decision'.indeterminate else + if results.elem Decision'.permit then Decision'.permit else + if results.elem Decision'.indeterminate_p then Decision'.indeterminate else + Decision'.not_applicable + def eval_legacy_ordered_deny_overrides_rule : List Decision' -> Decision' := eval_legacy_deny_overrides_rule + + -- See the comment for `eval_legacy_deny_overrides_rule`. + def eval_legacy_permit_overrides_rule (results : List Decision') : Decision' := + if results.elem Decision'.permit then Decision'.permit else + if results.elem Decision'.indeterminate_p then Decision'.indeterminate else + if results.elem Decision'.deny then Decision'.deny else + if results.elem Decision'.indeterminate_d then Decision'.indeterminate else + Decision'.not_applicable + def eval_legacy_ordered_permit_overrides_rule : List Decision' -> Decision' := eval_legacy_permit_overrides_rule +end CombinatorAlgorithm + structure AttributeDesignator where category : String identifier : String @@ -517,6 +593,38 @@ structure Policy where obligations : List ObligationExpression advice : List AdviceExpression +namespace Policy + def eval (policy : Policy) (context : Request) : Decision' := + let results := policy.rules.map (fun rule => rule.eval context) + let combinator := + match policy.combinator with + | CombinatorAlgorithm.deny_overrides => CombinatorAlgorithm.eval_deny_overrides + | CombinatorAlgorithm.ordered_deny_overrides => CombinatorAlgorithm.eval_ordered_deny_overrides + | CombinatorAlgorithm.permit_overrides => CombinatorAlgorithm.eval_permit_overrides + | CombinatorAlgorithm.ordered_permit_overrides => CombinatorAlgorithm.eval_ordered_permit_overrides + | CombinatorAlgorithm.deny_unless_permit => CombinatorAlgorithm.eval_deny_unless_permit + | CombinatorAlgorithm.permit_unless_deny => CombinatorAlgorithm.eval_permit_unless_deny + | CombinatorAlgorithm.first_applicable => CombinatorAlgorithm.eval_first_applicable_rule + | CombinatorAlgorithm.only_one_applicable => CombinatorAlgorithm.eval_only_one_applicable + | CombinatorAlgorithm.legacy_deny_overrides => CombinatorAlgorithm.eval_legacy_deny_overrides_rule + | CombinatorAlgorithm.legacy_ordered_deny_overrides => CombinatorAlgorithm.eval_legacy_ordered_deny_overrides_rule + | CombinatorAlgorithm.legacy_permit_overrides => CombinatorAlgorithm.eval_legacy_permit_overrides_rule + | CombinatorAlgorithm.legacy_ordered_permit_overrides => CombinatorAlgorithm.eval_legacy_ordered_permit_overrides_rule + let decision := combinator results + match policy.target.eval context with + | MatchResult.is_match => decision + | MatchResult.no_match => Decision'.not_applicable + | MatchResult.indeterminate => + match decision with + | Decision'.not_applicable => Decision'.not_applicable + | Decision'.permit => Decision'.indeterminate_p + | Decision'.deny => Decision'.indeterminate_d + | Decision'.indeterminate => Decision'.indeterminate_dp + | Decision'.indeterminate_dp => Decision'.indeterminate_dp + | Decision'.indeterminate_p => Decision'.indeterminate_p + | Decision'.indeterminate_d => Decision'.indeterminate_d +end Policy + inductive StatusCode | ok : StatusCode | missing_attribute : StatusCode @@ -695,15 +803,6 @@ deriving BEq, Repr -- simp [h_condition_eval] } -- { simp } --- def evaluate_deny_overrides (results : List Decision') : Decision' := --- if results.elem Decision'.deny then Decision'.deny else --- if results.elem Decision'.indeterminate_dp then Decision'.indeterminate_dp else --- if results.elem Decision'.indeterminate_d ∧ results.elem Decision'.indeterminate_p then Decision'.indeterminate_dp else --- if results.elem Decision'.indeterminate_d then Decision'.indeterminate_d else --- if results.elem Decision'.permit then Decision'.permit else --- if results.elem Decision'.indeterminate_p then Decision'.indeterminate_p else --- Decision'.not_applicable - -- def evaluate_policy (policy : Policy) (context : Request) : Choice := -- let results := policy.rules.map (fun x => evaluate_rule x context) -- let decision := evaluate_deny_overrides (results.map Prod.fst) |