diff options
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/lean/Xacml.lean | 227 |
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 |