Policy evaluation

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)