Implement evaluate_designator

1 files changed, 157 insertions, 70 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index ff4e78d..060a2c2 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -88,12 +88,16 @@ notation:65 "#<" lhs:65 "," rhs:66 ">" => Value.mk lhs rhs
 ------------------------------------------------------------------------
 
 structure Attribute where
-  category : String
-  identifier: String
-  issuer : Option String
-  value : List Value
+  category   : String
+  identifier : String
+  issuer     : Option String
+  value      : Value
 deriving Repr
 
+-- More than one attribute with a particular (category, identifier, issuer) can
+-- exist in a `Request`. Indeed, this is how poly-valued attributes are
+-- represented.
+
 def Request : Type := List Attribute
 deriving Repr
 
@@ -125,17 +129,19 @@ structure AttributeDesignator where
 deriving BEq
 
 def FunctionID : Type := String
+deriving BEq
 
 inductive Expression where
   | apply                (function : FunctionID) (args: List Expression) : Expression
   | attribute_designator (inner : AttributeDesignator)                   : Expression
   | attribute_value      (inner : Value)                                 : Expression
   | function             (function : FunctionID)                         : Expression
+deriving BEq
 
 structure Match where
-  function : Identifier
-  designator: AttributeDesignator
-  value: List Value
+  function   : Identifier
+  designator : AttributeDesignator
+  value      : Value
 deriving BEq
 def AllOf  : Type := List Match -- TODO: Should restrict nonempty.
 deriving BEq
@@ -180,15 +186,21 @@ def example_4_1_policy :=
     CombinatorAlgorithm.deny_overrides
     []
     [Rule.mk
-      [[[Match.mk
-          "rfc822Name_match"
-          (AttributeDesignator.mk
-            "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
-            "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
-            XmlType.rfc822Name
-            Option.none
-            false)
-          [#<XmlType.string, "med.example.com">]]]]
+      [
+        [ -- <AnyOf>
+          [ -- <AllOf>
+            Match.mk
+              "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match"
+              (AttributeDesignator.mk
+                "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
+                "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
+                XmlType.rfc822Name
+                Option.none
+                false)
+              (#<XmlType.string, "med.example.com">)
+          ] -- </AllOf>
+        ] -- </AnyOf>
+      ]
       (Expression.attribute_value (#<XmlType.boolean, "True">))
       Decision.permit]
 
@@ -196,15 +208,15 @@ def example_4_1_request :=
   [Attribute.mk "urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
                 "urn:oasis:names:tc:xacml:1.0:subject:subject-id"
                 Option.none
-                [#<XmlType.rfc822Name, "bs@simpsons.com">],
+                (#<XmlType.rfc822Name, "bs@simpsons.com">),
    Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:resource"
                 "urn:oasis:names:tc:xacml:1.0:resource:resource-id"
                 Option.none
-                [#<XmlType.anyURI, "file://example/med/record/patient/BartSimpson">],
+                (#<XmlType.anyURI, "file://example/med/record/patient/BartSimpson">),
    Attribute.mk "urn:oasis:names:tc:xacml:3.0:attribute-category:action"
                 "urn:oasis:names:tc:xacml:1.0:action:action-id"
                 Option.none
-                [#<XmlType.string, "read">]]
+                (#<XmlType.string, "read">)]
 
 def example_4_1_response := Decision.not_applicable
 
@@ -223,7 +235,7 @@ def example_4_2_policy_rule_1 :=
             XmlType.rfc822Name
             Option.none
             false)
-          [#<XmlType.anyURI, "urn:example:med:schemas:record">],
+          (#<XmlType.anyURI, "urn:example:med:schemas:record">),
         Match.mk
           "xpath_node_match"
           (AttributeDesignator.mk
@@ -232,7 +244,7 @@ def example_4_2_policy_rule_1 :=
             XmlType.xpathExpression
             Option.none
             false)
-          [#<XmlType.xpathExpression, "md:record">]],
+          (#<XmlType.xpathExpression, "md:record">)],
         [Match.mk
           "string_equal"
           (AttributeDesignator.mk
@@ -241,7 +253,7 @@ def example_4_2_policy_rule_1 :=
             XmlType.string
             Option.none
             false)
-          [#<XmlType.string, "read">]]]]
+          (#<XmlType.string, "read">)]]]
       (Expression.apply
         "urn:oasis:names:tc:xacml:1.0:function:string-equal"
         [Expression.apply
@@ -277,7 +289,7 @@ def example_4_2_policy_rule_2 :=
             XmlType.anyURI
             Option.none
             false)
-          [#<XmlType.anyURI, "urn:example:med:schemas:record">],
+          (#<XmlType.anyURI, "urn:example:med:schemas:record">),
          Match.mk
            "xpath-node-match"
            (AttributeDesignator.mk
@@ -286,7 +298,7 @@ def example_4_2_policy_rule_2 :=
             XmlType.xpathExpression
             Option.none
             false)
-           [#<XmlType.xpathExpression, "md:record">]]],
+          (#<XmlType.xpathExpression, "md:record">)]],
         [[Match.mk
           "string-equal"
           (AttributeDesignator.mk
@@ -295,7 +307,7 @@ def example_4_2_policy_rule_2 :=
             XmlType.string
             Option.none
             false)
-          [#<XmlType.string, "read">]]]]
+          (#<XmlType.string, "read">)]]]
       (Expression.apply
         "urn:oasis:names:tc:xacml:1.0:function:and"
         [Expression.apply
@@ -331,7 +343,7 @@ def example_4_2_policy_rule_3 :=
           XmlType.anyURI
           Option.none
           false)
-        [#<XmlType.anyURI, "urn:example:med:schemas:record">]]]]
+        (#<XmlType.anyURI, "urn:example:med:schemas:record">)]]]
     [Rule.mk
       [[[Match.mk
           "string-equal"
@@ -341,7 +353,7 @@ def example_4_2_policy_rule_3 :=
             XmlType.string
             Option.none
             false)
-          [#<XmlType.string, "physician">]]],
+          (#<XmlType.string, "physician">)]],
        [[Match.mk
            "xpath-node-match"
            (AttributeDesignator.mk
@@ -350,7 +362,7 @@ def example_4_2_policy_rule_3 :=
             XmlType.xpathExpression
             Option.none
             false)
-           [#<XmlType.xpathExpression, "md:record">]]],
+          (#<XmlType.xpathExpression, "md:record">)]],
         [[Match.mk
           "string-equal"
           (AttributeDesignator.mk
@@ -359,7 +371,7 @@ def example_4_2_policy_rule_3 :=
             XmlType.string
             Option.none
             false)
-          [#<XmlType.string, "write">]]]]
+          (#<XmlType.string, "write">)]]]
       (Expression.apply
         "urn:oasis:names:tc:xacml:1.0:function:string-equal"
         [Expression.apply
@@ -395,7 +407,7 @@ def example_4_2_policy_rule_4 :=
           XmlType.string
           Option.none
           false)
-        [#<XmlType.string, "administrator">]]],
+        (#<XmlType.string, "administrator">)]],
       [[Match.mk
         "anyURI-equal"
         (AttributeDesignator.mk
@@ -404,7 +416,7 @@ def example_4_2_policy_rule_4 :=
           XmlType.anyURI
           Option.none
           false)
-        [#<XmlType.anyURI, "urn:example:med:schemas:record">],
+        (#<XmlType.anyURI, "urn:example:med:schemas:record">),
         Match.mk
         "xpath-node-match"
         (AttributeDesignator.mk
@@ -413,7 +425,7 @@ def example_4_2_policy_rule_4 :=
           XmlType.xpathExpression
           Option.none
           false)
-        [#<XmlType.xpathExpression, "md:record/md:medical">]]],
+        (#<XmlType.xpathExpression, "md:record/md:medical">)]],
       [[Match.mk
         "string-equal"
         (AttributeDesignator.mk
@@ -422,7 +434,7 @@ def example_4_2_policy_rule_4 :=
           XmlType.string
           Option.none
           false)
-        [#<XmlType.string, "read">]]]]
+        (#<XmlType.string, "read">)]]]
       (Expression.attribute_value (#<XmlType.boolean, "True">))
       Decision.deny]
 
@@ -438,35 +450,111 @@ def example_4_2_policy :=
           XmlType.string
           Option.none
           false)
-        [#<XmlType.string, "urn:example:med:schema:records">]]]]
+        (#<XmlType.string, "urn:example:med:schema:records">)]]]
 
 ---
 
--- TODO
-def evaluate_expression (expression : Expression) : Value :=
+-- Per 7.4 Expression evaluation,
+--
+-- "XACML defines an evaluation result of "Indeterminate", which is said
+-- to be the result of an invalid expression, or an operational error
+-- occurring during the evaluation of the expression."
+
+instance : Coe (Option Value) Value where
+  coe b :=
+    match b with
+      | Option.none   => #<XmlType.boolean, "Indeterminate">
+      | Option.some a => a
+
+def evaluate_apply (name : FunctionID) (args : List Expression) : Option Value :=
+  if name == "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match" then
+    match args with
+      | [lhs, rhs] => if lhs == rhs
+                      then #<XmlType.boolean, "True">
+                      else #<XmlType.boolean, "False">
+      | _          => #<XmlType.boolean, "Indeterminate">
+  else Option.none
+
+def evaluate_expression (expression : Expression) : Option Value :=
   match expression with
-    | Expression.apply fn args => #<XmlType.string, "True">
-    | Expression.attribute_designator
-        (AttributeDesignator.mk category identifier type issuer must_be_present)
-      => #<XmlType.string, "True">
+    | Expression.apply name args => evaluate_apply name args
     | Expression.attribute_value inner => inner
-    | Expression.function _ => #<XmlType.string, "True">
+    | _ => Option.none
+
+def evaluate_designator (designator : AttributeDesignator)
+                        (context : List Attribute) : Option (List Value) :=
+  match designator with
+    | AttributeDesignator.mk category identifier type issuer must_be_present =>
+      let found :=
+        -- A named attribute SHALL match an attribute if the values of
+        -- their respective Category, AttributeId, DataType and Issuer
+        -- attributes match. The attribute designator’s Category MUST
+        -- match, by identifier equality, the Category of the
+        -- <Attributes> element in which the attribute is present. The
+        -- attribute designator’s AttributeId MUST match, by identifier
+        -- equality, the AttributeId of the attribute. The attribute
+        -- designator’s DataType MUST match, by identifier equality, the
+        -- DataType of the same attribute.
+        --
+        -- If the Issuer attribute is present in the attribute
+        -- designator, then it MUST match, using the
+        -- “urn:oasis:names:tc:xacml:1.0:function:string-equal”
+        -- function, the Issuer of the same attribute. If the Issuer is
+        -- not present in the attribute designator, then the matching of
+        -- the attribute to the named attribute SHALL be governed by
+        -- AttributeId and DataType attributes alone.
+        context.filter (fun (attr : Attribute) =>
+                          attr.category == category
+                        ∧ attr.identifier == identifier
+                        ∧ attr.value.fst == type
+                        ∧ (attr.issuer == Option.none ∨ attr.issuer == issuer))
+      let found := found.map (fun x => x.value)
+      if must_be_present then
+        match found with
+          | [] => Option.none
+          | _ => found
+      else found
 
--- TODO
-def evaluate_designator (designator : AttributeDesignator) (context : Request) : Value :=
-  #<XmlType.string, "True">
-  -- match designator with
-    -- | AttributeDesignator.mk category identifier type issuer must_be_present
-    --   match issuer with
-    --     | Option.some x =>
+-- The evaluation semantics for a matching element is as follows.
+--
+-- 1. If an operational error were to occur while evaluating the
+--    <AttributeDesignator> or <AttributeSelector> element, then the
+--    result of the entire expression SHALL be "Indeterminate".
+--
+-- 2. If the <AttributeDesignator> or <AttributeSelector> element were
+--    to evaluate to an empty bag, then the result of the expression
+--    SHALL be "False".
+--
+-- 3. Otherwise, the MatchId function SHALL be applied between the
+--    <AttributeValue> and each element of the bag returned from the
+--    <AttributeDesignator> or <AttributeSelector> element.
+--    a. If at least one of those function applications were to evaluate
+--       to "True", then the result of the entire expression SHALL be
+--       "True".
+--    b. Otherwise, if at least one of the function applications results
+--       in "Indeterminate", then the result SHALL be "Indeterminate".
+--    c. Finally, if all function applications evaluate to "False", then
+--       the result of the entire expression SHALL be "False".
 
-def evaluate_match (m : Match) (context : Request) : Value :=
+def evaluate_match (m : Match) (context : Request) : Option Value :=
   match m with
     | Match.mk fn designator value =>
-      evaluate_expression (Expression.apply fn (([evaluate_designator designator context].append value).map (fun x => Expression.attribute_value x)))
+      do
+        let attrs <- evaluate_designator designator context
+        let results :=
+          attrs.map
+            (fun attr =>
+              let args := [value, attr]
+              let args := args.map (fun x => Expression.attribute_value x)
+              evaluate_expression (Expression.apply fn args))
+        let results := results.map (fun (x : Option Value) => (x : Value))
+        if results.elem (#<XmlType.boolean, "True">) then (#<XmlType.boolean, "True">)
+        else if results.elem (#<XmlType.boolean, "Indeterminate">) then (#<XmlType.boolean, "Indeterminate">)
+        else (#<XmlType.boolean, "False">)
 
 def evaluate_all_of (all_of : AllOf) (context : Request) : MatchResult :=
   let result := all_of.map (fun x => evaluate_match x context)
+  let result := result.map (fun (x : Option Value) => (x : Value))
   if result.all (fun x => x == (XmlType.boolean, "True")) then MatchResult.is_match
   else if result.all (fun x => x != (XmlType.boolean, "False")) ∧
           result.elem (XmlType.boolean, "Indeterminate") then MatchResult.indeterminate
@@ -498,7 +586,7 @@ def evaluate_rule (rule : Rule) (context : Request) : Choice :=
   if rule.target == [] then [rule.effect]
   else match evaluate_target rule.target context with
     | MatchResult.is_match =>
-      match evaluate_expression rule.condition with
+      match (evaluate_expression rule.condition : Value) with
         -- TODO: coe to some strongly typed result?
         | (XmlType.string, "True") => [rule.effect]
         | (XmlType.string, "False") => [Decision.not_applicable]
@@ -509,23 +597,22 @@ def evaluate_rule (rule : Rule) (context : Request) : Choice :=
     | MatchResult.no_match      => [Decision.not_applicable]
     | MatchResult.indeterminate => [Decision.not_applicable]
 
-theorem test :
-  ∀ r: Rule,
-  ∀ c: Request,
-    evaluate_target r.target c = MatchResult.is_match
-  ∧ evaluate_expression r.condition = #<XmlType.string, "True">
-  → evaluate_rule r c = [r.effect] :=
-  by
-    intros r c
-    intro h
-    rw [evaluate_rule]
-    cases (r.target == [])
-    { simp
-      have h_target_eval : evaluate_target r.target c = MatchResult.is_match := And.left h
-      have h_condition_eval : evaluate_expression r.condition = (XmlType.string, "True") := And.right h
-      simp [h_target_eval]
-      simp [h_condition_eval] }
-    { simp }
+-- theorem test :
+--   ∀ (r : Rule) (c : Request),
+--     evaluate_target r.target c = MatchResult.is_match
+--   ∧ evaluate_expression r.condition = #<XmlType.string, "True">
+--   → evaluate_rule r c = [r.effect] :=
+--   by
+--     intros r c
+--     intro h
+--     rw [evaluate_rule]
+--     cases (r.target == [])
+--     { simp
+--       have h_target_eval : evaluate_target r.target c = MatchResult.is_match := And.left h
+--       have h_condition_eval : (evaluate_expression r.condition : Value) = (XmlType.string, "True") := And.right h
+--       simp [h_target_eval]
+--       simp [h_condition_eval] }
+--     { simp }
 
 def evaluate_policy (policy : Policy) (context : Request) : Choice :=
   match policy.rules with
@@ -534,9 +621,9 @@ def evaluate_policy (policy : Policy) (context : Request) : Choice :=
 
 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_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.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