------------------------------------------------------------------------ ---- Atoms ------------------------------------------------------------- ------------------------------------------------------------------------ -- -- # References -- -- - 7.6 Match evaluation -- ------------------------------------------------------------------------ inductive MatchResult where | is_match : MatchResult | no_match : MatchResult | indeterminate : MatchResult deriving DecidableEq, BEq, Repr inductive Decision where | permit : Decision | deny : Decision | indeterminate : Decision | not_applicable : Decision deriving DecidableEq, BEq, Repr -- This type is used to implement the semantics described in § 7.10 (Extended -- Indeterminate). It is only relevant to combining algorithms. inductive Decision' where | permit : Decision' | deny : Decision' | indeterminate : Decision' | indeterminate_d : Decision' | indeterminate_p : Decision' | indeterminate_dp : Decision' | not_applicable : Decision' deriving DecidableEq, BEq, Repr def Decision'.downcast : Decision' → Decision | Decision'.permit => Decision.permit | Decision'.deny => Decision.deny | Decision'.indeterminate => Decision.indeterminate | Decision'.indeterminate_d => Decision.indeterminate | Decision'.indeterminate_p => Decision.indeterminate | Decision'.indeterminate_dp => Decision.indeterminate | Decision'.not_applicable => Decision.not_applicable instance : Coe Decision' Decision where coe := Decision'.downcast inductive EffectType where | permit : EffectType | deny : EffectType deriving DecidableEq, BEq, Repr namespace EffectType def to_decision (e : EffectType) : Decision := match e with | EffectType.permit => Decision.permit | EffectType.deny => Decision.deny def to_decision' (e : EffectType) : Decision' := match e with | EffectType.permit => Decision'.permit | EffectType.deny => Decision'.deny end EffectType ------------------------------------------------------------------------ ---- Values ------------------------------------------------------------ ------------------------------------------------------------------------ -- -- From A.2 Data-types: "Although XML instances represent all data-types -- as strings, an XACML PDP must operate on types of data that, while -- they have string representations, are not just strings. Types such as -- Boolean, integer, and double MUST be converted from their XML string -- representations to values that can be compared with values in their -- domain of discourse, such as numbers." -- -- The standard enumerates the types that must be supported by any -- conforming implementaiton. This is represented in `XmlType`, and -- `Value` is the representation of a value payload with its associated -- type. -- ------------------------------------------------------------------------ inductive XmlType | string : XmlType | boolean : XmlType | integer : XmlType | double : XmlType | time : XmlType | date : XmlType | dateTime : XmlType | anyURI : XmlType | hexBinary : XmlType | base64Binary : XmlType | dayTimeDuration : XmlType | yearMonthDuration : XmlType | x500Name : XmlType | rfc822Name : XmlType | ipAddress : XmlType | dnsName : XmlType deriving DecidableEq, BEq, Repr def Primitive : Type := XmlType × String deriving DecidableEq, BEq, Repr def Primitive.mk (type : XmlType) (inner : String) : Primitive := (type, inner) notation:65 "#<" lhs:65 "," rhs:66 ">" => Primitive.mk lhs rhs instance : Coe Bool Primitive where coe b := match b with | true => # | false => # -- 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 Primitive) Primitive where coe b := match b with | Option.none => # | Option.some a => a structure Bag where contents: List Primitive deriving BEq, DecidableEq, Repr -- def Bag.beq (b₁ b₂ : Bag) : Bool := -- b₁.contents.all (fun x => b₂.contents.count x == b₁.contents.count x) -- instance : BEq Bag where -- beq := Bag.beq inductive Value where | primitive (p : Primitive) : Value | bag (b : Bag) : Value deriving DecidableEq, Repr def Value.beq (v₁ v₂ : Value) : Bool := match v₁ with | Value.primitive p₁ => match v₂ with | Value.primitive p₂ => p₁ == p₂ | Value.bag _ => false | Value.bag b₁ => match v₂ with | Value.primitive _ => false | Value.bag b₂ => b₁ == b₂ instance : BEq Value where beq := Value.beq instance : Coe (Option Value) Value where coe b := match b with | Option.none => Value.primitive (#) | Option.some a => a instance : Coe (Option Value) MatchResult where coe b := match b with | Option.some (Value.primitive (XmlType.boolean, "True")) => MatchResult.is_match | Option.some (Value.primitive (XmlType.boolean, "False")) => MatchResult.no_match | _ => MatchResult.indeterminate ------------------------------------------------------------------------ ---- Attributes--------------------------------------------------------- ------------------------------------------------------------------------ -- -- # References -- -- - 5.46 Element -- - 5.42 Element -- -- Attributes are categories into elements. In this -- implementation, categories are rolled up - every attribute carries -- the category of its enclosing element. -- ------------------------------------------------------------------------ structure Attribute where category : String identifier : String issuer : Option String value : Primitive deriving DecidableEq, Repr def Attribute.beq (a₁ a₂ : Attribute) : Bool := match a₁ with | { category := category₁, identifier := identifier₁, issuer := issuer₁, value := value₁ } => match a₂ with | { category := category₂, identifier := identifier₂, issuer := issuer₂, value := value₂ } => category₁ == category₂ && identifier₁ == identifier₂ && issuer₁ == issuer₂ && value₁ == value₂ instance : BEq Attribute where beq := Attribute.beq -- 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 --- def Identifier : Type := String deriving DecidableEq, BEq, Repr inductive RuleCombinatorAlgorithm where | deny_overrides : RuleCombinatorAlgorithm | ordered_deny_overrides : RuleCombinatorAlgorithm | permit_overrides : RuleCombinatorAlgorithm | ordered_permit_overrides : RuleCombinatorAlgorithm | deny_unless_permit : RuleCombinatorAlgorithm | permit_unless_deny : RuleCombinatorAlgorithm | first_applicable : RuleCombinatorAlgorithm | legacy_deny_overrides : RuleCombinatorAlgorithm | legacy_ordered_deny_overrides : RuleCombinatorAlgorithm | legacy_permit_overrides : RuleCombinatorAlgorithm | legacy_ordered_permit_overrides : RuleCombinatorAlgorithm namespace RuleCombinatorAlgorithm -- 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 (results : List Decision') : Decision' := match (results.filter (fun d => d != Decision'.not_applicable)).get? 0 with | some a => a | none => Decision'.not_applicable def eval_legacy_deny_overrides (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 : List Decision' -> Decision' := eval_legacy_deny_overrides -- See the comment for `eval_legacy_deny_overrides_rule`. def eval_legacy_permit_overrides (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 : List Decision' -> Decision' := eval_legacy_permit_overrides end RuleCombinatorAlgorithm inductive PolicyCombinatorAlgorithm where | deny_overrides : PolicyCombinatorAlgorithm | ordered_deny_overrides : PolicyCombinatorAlgorithm | permit_overrides : PolicyCombinatorAlgorithm | ordered_permit_overrides : PolicyCombinatorAlgorithm | deny_unless_permit : PolicyCombinatorAlgorithm | permit_unless_deny : PolicyCombinatorAlgorithm | first_applicable : PolicyCombinatorAlgorithm | only_one_applicable : PolicyCombinatorAlgorithm | legacy_deny_overrides : PolicyCombinatorAlgorithm | legacy_ordered_deny_overrides : PolicyCombinatorAlgorithm | legacy_permit_overrides : PolicyCombinatorAlgorithm | legacy_ordered_permit_overrides : PolicyCombinatorAlgorithm namespace PolicyCombinatorAlgorithm def eval_deny_overrides := RuleCombinatorAlgorithm.eval_deny_overrides def eval_ordered_deny_overrides := RuleCombinatorAlgorithm.eval_ordered_deny_overrides def eval_permit_overrides := RuleCombinatorAlgorithm.eval_permit_overrides def eval_ordered_permit_overrides := RuleCombinatorAlgorithm.eval_ordered_permit_overrides def eval_deny_unless_permit := RuleCombinatorAlgorithm.eval_deny_unless_permit def eval_permit_unless_deny := RuleCombinatorAlgorithm.eval_permit_unless_deny def eval_first_applicable := RuleCombinatorAlgorithm.eval_first_applicable -- 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_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 (results : List Decision') : Decision' := if results.elem Decision'.deny then Decision'.deny else if results.elem Decision'.indeterminate then Decision'.deny else if results.elem Decision'.permit then Decision'.permit else Decision'.not_applicable def eval_legacy_ordered_deny_overrides : List Decision' -> Decision' := eval_legacy_deny_overrides -- See the comment for `eval_legacy_deny_overrides`. def eval_legacy_permit_overrides (results : List Decision') : Decision' := if results.elem Decision'.permit then Decision'.permit else if results.elem Decision'.deny then Decision'.deny else if results.elem Decision'.indeterminate then Decision'.indeterminate else Decision'.not_applicable def eval_legacy_ordered_permit_overrides : List Decision' -> Decision' := eval_legacy_permit_overrides end PolicyCombinatorAlgorithm inductive StatusCode | ok : StatusCode | missing_attribute : StatusCode | syntax_error : StatusCode | processing_error : StatusCode deriving DecidableEq, BEq, Repr structure AttributeDesignator where category : String identifier : String type : XmlType issuer : Option String must_be_present : Bool deriving DecidableEq, BEq, Repr namespace AttributeDesignator -- 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 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. def matches? (designator : AttributeDesignator) (attr : Attribute) : Bool := attr.category == designator.category && attr.identifier == designator.identifier && attr.value.fst == designator.type && (attr.issuer == Option.none ∨ attr.issuer == designator.issuer) def eval (designator : AttributeDesignator) (context : List Attribute) : Sum Value (List StatusCode) := let found := context.filter designator.matches? let found := found.map (fun x => x.value) if designator.must_be_present then match found with | [] => Sum.inr $ [StatusCode.missing_attribute] | _ => Sum.inl $ Value.bag (Bag.mk found) else Sum.inl $ Value.bag (Bag.mk found) end AttributeDesignator def matches? (designator : AttributeDesignator) (attr : Attribute) : Prop := designator.category == attr.category ∧ designator.identifier == attr.identifier ∧ designator.type == attr.value.fst ∧ match (designator.issuer, attr.issuer) with | (none, _) => True | (some issuer₁, some issuer₂) => issuer₁ == issuer₂ | _ => False def FunctionID : Type := String deriving DecidableEq, BEq, Repr -- "The element is not used directly in a policy. The -- element signifies that an element that extends the ExpressionType and is a -- member of the element substitution group SHALL appear in its -- place." -- -- We omit the `` case because this model of XACML does -- not include it, and we exclude the `` case because -- we erase variable references in the compiler. inductive Expression where -- Note well that `apply` accepts a list of Values, not a list of Expressions, -- as its arguments. The compiler is responsible for ensuring that the -- arguments in a function call are fully evaluated. -- -- Lean is quite strict about recursion being bounded, which is a little hard -- to prove in our case! Fortunately, we can punt the job of proving that to -- the compiler. | apply (function : FunctionID) (args: List Value) : Expression | attribute_designator (inner : AttributeDesignator) : Expression | attribute_value (inner : Value) : Expression | function (function : FunctionID) : Expression deriving DecidableEq, BEq, Repr namespace Expression def apply_eval (name : FunctionID) (args : List Value) : Option Value := if name == "urn:oasis:names:tc:xacml:1.0:function:string-equal" then match args with | [Value.primitive (XmlType.string, lhs), Value.primitive (XmlType.string, rhs)] => Value.primitive (lhs == rhs) | _ => Value.primitive (#) else if name == "urn:oasis:names:tc:xacml:1.0:function:anyURI-equal" then match args with | [Value.primitive (XmlType.anyURI, lhs), Value.primitive (XmlType.anyURI, rhs)] => Value.primitive (lhs == rhs) | _ => Value.primitive (#) else if name == "urn:oasis:names:tc:xacml:1.0:function:integer-equal" then match args with | [Value.primitive (XmlType.integer, lhs), Value.primitive (XmlType.integer, rhs)] => Value.primitive (lhs == rhs) | _ => Value.primitive (#) else Option.none def eval (expression : Expression) (context : Request) : Option Value := -- The return type of `` may be made more specific by type unification. -- -- The evaluation result can be specified to be "Indeterminate"; we encode -- this as `Option.none` here for ergonomics, but we do give an instance for -- `Coe (Option Value) Value`. -- -- § 7.6 enumerates but does not describe the semantics for: -- -- - -- - -- - -- - -- - -- - match expression with | Expression.apply name args => apply_eval name args | Expression.attribute_designator inner => match inner.eval context with | Sum.inl res => res | Sum.inr _ => Option.none | Expression.attribute_value inner => some inner | _ => Option.none end Expression structure Match where function : Identifier designator : AttributeDesignator value : Value deriving DecidableEq, BEq, Repr def AllOf : Type := List Match deriving DecidableEq, BEq, Repr def AnyOf : Type := List AllOf deriving DecidableEq, BEq, Repr def Target : Type := List AnyOf deriving DecidableEq, BEq, Repr instance : Membership AllOf AnyOf where mem := fun x y => y.contains x namespace Match -- The evaluation semantics for a matching element is as follows. -- -- 1. If an operational error were to occur while evaluating the -- or element, then the -- result of the entire expression SHALL be "Indeterminate". -- -- 2. If the or 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 -- and each element of the bag returned from the -- or 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 eval (m : Match) (context : Request) : Option Value := match m with | Match.mk fn designator value => match designator.eval context with | Sum.inl result => let results := match result with -- Otherwise, the MatchId function SHALL be applied between the -- and each element of the bag returned from the -- or element. | (Value.bag (Bag.mk attrs)) => attrs.map fun attr => let args := [value, Value.primitive attr] (Expression.apply fn args).eval context | (Value.primitive attr) => -- TODO: Prove that this case is impossible. let args := [value, Value.primitive attr] [(Expression.apply fn args).eval context] let results := results.map (fun (x : Option Value) => (x : Value)) -- If at least one of those function applications were to evaluate to -- "True", then the result of the entire expression SHALL be "True". if results.elem (Value.primitive (#)) then (Value.primitive (#)) -- Otherwise, if at least one of the function applications results in -- "Indeterminate", then the result SHALL be "Indeterminate". else if results.elem (Value.primitive (#)) then (Value.primitive (#)) -- The `else` arm handles the following cases: -- -- If the or element were to -- evaluate to an empty bag, then the result of the expression SHALL -- be "False". -- -- Finally, if all function applications evaluate to "False", then the -- result of the entire expression SHALL be "False". else Value.primitive (#) -- If an operational error were to occur while evaluating the -- or element, then the result -- of the entire expression SHALL be "Indeterminate". | Sum.inr _ => Option.none end Match namespace AllOf def eval (conj : AllOf) (context : Request) : MatchResult := let result := conj.map (fun x => x.eval context) let result := result.map (fun (x : Option Value) => (x : Value)) if result.all (fun x => x == Value.primitive (XmlType.boolean, "True")) then MatchResult.is_match else if result.all (fun x => x != Value.primitive (XmlType.boolean, "False")) ∧ result.elem (Value.primitive (XmlType.boolean, "Indeterminate")) then MatchResult.indeterminate else MatchResult.no_match end AllOf namespace AnyOf def eval (disj : AnyOf) (context : Request) : MatchResult := -- match disj with -- | [] => MatchResult.is_match -- | List.cons x xs => match x.eval context with -- | MatchResult.is_match => MatchResult.is_match -- | MatchResult.no_match => -- let rest := AnyOf.eval xs context -- if rest == MatchResult.no_match then MatchResult.no_match else rest -- | MatchResult.indeterminate => -- let rest := AnyOf.eval xs context -- if rest == MatchResult.no_match then MatchResult.indeterminate else rest if disj.isEmpty then MatchResult.is_match else let result := disj.map (fun x => x.eval context) if result.any (fun x => x == MatchResult.is_match) then MatchResult.is_match else if result.elem MatchResult.indeterminate then MatchResult.indeterminate else MatchResult.no_match end AnyOf namespace Target def eval (target : Target) (context : Request) : MatchResult := match target with -- An empty target matches any request. | [] => MatchResult.is_match | xs => let results := xs.map (fun disj => disj.eval context) -- Otherwise the target value SHALL be "Match" if all the AnyOf -- specified in the target match values in the request context. if results.all (fun result => result == MatchResult.is_match) then MatchResult.is_match -- Otherwise, if any one of the AnyOf specified in the target is “No -- Match”, then the target SHALL be “No Match”. else if results.any (fun result => result == MatchResult.no_match) then MatchResult.no_match -- Otherwise, the target SHALL be “Indeterminate”. else MatchResult.indeterminate end Target structure Obligation where assignments : List Attribute identifier : String deriving DecidableEq, BEq, Repr structure Advice where assignments : List Attribute identifier : String deriving DecidableEq, BEq, Repr structure AttributeAssignmentExpression where category : String identifier : String issuer : Option String expression : Expression deriving DecidableEq, BEq, Repr namespace AttributeAssignmentExpression def eval (assignment : AttributeAssignmentExpression) (context : Request) : Option Attribute := match assignment.expression.eval context with | some (Value.primitive inner) => Attribute.mk assignment.category assignment.identifier assignment.issuer inner | _ => none end AttributeAssignmentExpression structure ObligationExpression where assignments : List AttributeAssignmentExpression identifier : String fulfill_on : Decision deriving DecidableEq, BEq, Repr namespace ObligationExpression def eval (obligation : ObligationExpression) (context : Request) : Option Obligation := let assignments := obligation.assignments.map (fun x => AttributeAssignmentExpression.eval x context) if assignments.all Option.isSome then Obligation.mk (List.filterMap id assignments) obligation.identifier else none end ObligationExpression structure AdviceExpression where assignments : List AttributeAssignmentExpression identifier : String applies_to : Decision deriving DecidableEq, BEq, Repr namespace AdviceExpression def eval (advice : AdviceExpression) (context : Request) : Option Advice := let assignments := advice.assignments.map (fun x => AttributeAssignmentExpression.eval x context) if assignments.all Option.isSome then Advice.mk (List.filterMap id assignments) advice.identifier else none end AdviceExpression structure ResultAuxiliary where status : Option (List StatusCode) obligations : List Obligation advice : List Advice deriving DecidableEq, BEq, Repr structure ResultAuxiliary' where status : Option (List StatusCode) obligations : List ObligationExpression advice : List AdviceExpression deriving DecidableEq, BEq, Repr def collect_option {α : Type} (xs : List (Option α)) : Option (List α) := match xs with | [] => some [] | some x :: xs' => match collect_option xs' with | some xs' => some (x :: xs') | none => none | none :: _ => none namespace ResultAuxiliary' def eval (result : ResultAuxiliary') (context : Request) : Option ResultAuxiliary := let advice := collect_option (List.map (fun x => AdviceExpression.eval x context) result.advice) let obligations := collect_option (List.map (fun x => ObligationExpression.eval x context) result.obligations) match (obligations, advice) with | (some obligations, some advice) => some { status := result.status, obligations, advice } | _ => none end ResultAuxiliary' structure MissingAttributeDetail where category : String identifier : String issuer : Option String value : Option Value type : XmlType deriving DecidableEq, BEq, Repr def Result : Type := Decision' × (Option ResultAuxiliary) def Result' : Type := Decision' × (Option ResultAuxiliary') namespace Result' def eval (result : Result') (context : Request) : Result := match result.snd with | some aux => let advices := aux.advice.map (fun advice => AdviceExpression.eval advice context) let obligations := aux.obligations.map (fun x => ObligationExpression.eval x context) if advices.any Option.isNone || obligations.any Option.isNone then (Decision'.indeterminate, none) else ( result.fst, ResultAuxiliary.mk aux.status (List.filterMap id obligations) (List.filterMap id advices) ) | none => (result.fst, none) end Result' structure Rule where target : Target condition : Option Expression effect : EffectType obligations : List ObligationExpression advice : List AdviceExpression namespace Rule def eval (rule : Rule) (context : Request) : Result' := let (decision : Decision') := -- The "no target" case is handled within `Target.eval`, returning -- `MatchResult.is_match` when the target is empty. match rule.target.eval context with | MatchResult.is_match => let condition := match rule.condition with | some condition => -- The condition value SHALL be "True" if the element -- evaluates to "True". let result := condition.eval context if result == some (Value.primitive (#)) then result -- Its value SHALL be "False" if the element evaluates to -- "False". else if result == some (Value.primitive (#)) then result -- The condition value SHALL be "Indeterminate", if the expression -- contained in the element evaluates to "Indeterminate." else Value.primitive (#) -- The condition value SHALL be "True" if the element is absent. | none => Value.primitive (#) match condition with | some (Value.primitive (XmlType.boolean, "False")) => Decision'.not_applicable | some (Value.primitive (XmlType.boolean, "True")) => match rule.effect with | EffectType.permit => Decision'.permit | EffectType.deny => Decision'.deny -- | (#) => | _ => if rule.effect == EffectType.permit then Decision'.indeterminate_p else Decision'.indeterminate_d | MatchResult.no_match => Decision'.not_applicable | MatchResult.indeterminate => if rule.effect == EffectType.permit then Decision'.indeterminate_p else Decision'.indeterminate_d let advices := rule.advice.filter (fun advice => advice.applies_to == (decision : Decision)) let obligations := rule.obligations.filter (fun obligation => obligation.fulfill_on == (decision : Decision)) ( decision, ResultAuxiliary'.mk none obligations advices ) end Rule structure Policy where combinator : RuleCombinatorAlgorithm target : Target obligations : List ObligationExpression advice : List AdviceExpression namespace Policy def eval (policy : Policy) (child_results : List Result') (context : Request) : Result' := let combinator := match policy.combinator with | RuleCombinatorAlgorithm.deny_overrides => RuleCombinatorAlgorithm.eval_deny_overrides | RuleCombinatorAlgorithm.ordered_deny_overrides => RuleCombinatorAlgorithm.eval_ordered_deny_overrides | RuleCombinatorAlgorithm.permit_overrides => RuleCombinatorAlgorithm.eval_permit_overrides | RuleCombinatorAlgorithm.ordered_permit_overrides => RuleCombinatorAlgorithm.eval_ordered_permit_overrides | RuleCombinatorAlgorithm.deny_unless_permit => RuleCombinatorAlgorithm.eval_deny_unless_permit | RuleCombinatorAlgorithm.permit_unless_deny => RuleCombinatorAlgorithm.eval_permit_unless_deny | RuleCombinatorAlgorithm.first_applicable => RuleCombinatorAlgorithm.eval_first_applicable | RuleCombinatorAlgorithm.legacy_deny_overrides => RuleCombinatorAlgorithm.eval_legacy_deny_overrides | RuleCombinatorAlgorithm.legacy_ordered_deny_overrides => RuleCombinatorAlgorithm.eval_legacy_ordered_deny_overrides | RuleCombinatorAlgorithm.legacy_permit_overrides => RuleCombinatorAlgorithm.eval_legacy_permit_overrides | RuleCombinatorAlgorithm.legacy_ordered_permit_overrides => RuleCombinatorAlgorithm.eval_legacy_ordered_permit_overrides let (decision : Decision') := combinator (List.map Prod.fst child_results) let (decision : Decision') := 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 let advices := policy.advice.filter (fun advice => advice.applies_to == (decision : Decision)) ++ List.join (child_results.filterMap (fun x => match x.snd with | some y => y.advice | none => none)) let obligations := policy.obligations.filter (fun obligation => obligation.fulfill_on == (decision : Decision)) ++ List.join (child_results.filterMap (fun x => match x.snd with | some y => y.obligations | none => none)) ( decision, ResultAuxiliary'.mk none obligations advices ) end Policy structure PolicySet where combinator : PolicyCombinatorAlgorithm target : Target obligations : List ObligationExpression advice : List AdviceExpression namespace PolicySet def eval (policyset : PolicySet) (child_results : List Result') (context : Request) : Result' := let combinator := match policyset.combinator with | PolicyCombinatorAlgorithm.deny_overrides => PolicyCombinatorAlgorithm.eval_deny_overrides | PolicyCombinatorAlgorithm.ordered_deny_overrides => PolicyCombinatorAlgorithm.eval_ordered_deny_overrides | PolicyCombinatorAlgorithm.permit_overrides => PolicyCombinatorAlgorithm.eval_permit_overrides | PolicyCombinatorAlgorithm.ordered_permit_overrides => PolicyCombinatorAlgorithm.eval_ordered_permit_overrides | PolicyCombinatorAlgorithm.deny_unless_permit => PolicyCombinatorAlgorithm.eval_deny_unless_permit | PolicyCombinatorAlgorithm.permit_unless_deny => PolicyCombinatorAlgorithm.eval_permit_unless_deny | PolicyCombinatorAlgorithm.first_applicable => PolicyCombinatorAlgorithm.eval_first_applicable | PolicyCombinatorAlgorithm.only_one_applicable => PolicyCombinatorAlgorithm.eval_only_one_applicable | PolicyCombinatorAlgorithm.legacy_deny_overrides => PolicyCombinatorAlgorithm.eval_legacy_deny_overrides | PolicyCombinatorAlgorithm.legacy_ordered_deny_overrides => PolicyCombinatorAlgorithm.eval_legacy_ordered_deny_overrides | PolicyCombinatorAlgorithm.legacy_permit_overrides => PolicyCombinatorAlgorithm.eval_legacy_permit_overrides | PolicyCombinatorAlgorithm.legacy_ordered_permit_overrides => PolicyCombinatorAlgorithm.eval_legacy_ordered_permit_overrides let (decision : Decision') := combinator (List.map Prod.fst child_results) let (decision : Decision') := match policyset.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 let advices := policyset.advice.filter (fun advice => advice.applies_to == (decision : Decision)) ++ List.join (child_results.filterMap (fun x => match x.snd with | some y => y.advice | none => none)) let obligations := policyset.obligations.filter (fun obligation => obligation.fulfill_on == (decision : Decision)) ++ List.join (child_results.filterMap (fun x => match x.snd with | some y => y.obligations | none => none)) ( decision, ResultAuxiliary'.mk none obligations advices ) end PolicySet inductive PolicyElement where | PolicySet (ps : PolicySet) | Policy (p : Policy) | Rule (r : Rule) def PolicyElement.eval (context : Request) : PolicyElement -> List Result' -> Result' | PolicySet ps, results => ps.eval results context | Policy p, results => p.eval results context | Rule r, _ => r.eval context inductive ElementTree where | Node (e : PolicyElement) (xs : List ElementTree) def ElementTree.eval' (context : Request) : ElementTree -> List Result' -> Result' | ElementTree.Node e [], results => PolicyElement.eval context e results | ElementTree.Node e (x :: xs), results => ElementTree.eval' context (ElementTree.Node e xs) ((ElementTree.eval' context x []) :: results) def ElementTree.eval (context : Request) (et : ElementTree) : Result' := ElementTree.eval' context et [] -- let results := policy.rules.map (fun rule => rule.eval context) def is_indeterminate (x : Expression) : Bool := match x with | Expression.attribute_value (Value.primitive (XmlType.boolean, "Indeterminate")) => true | _ => false def make_response (decision : Decision) (status : Option (List StatusCode)) (obligations : List Obligation) (advice : List Advice) : Decision × ResultAuxiliary := let obligations := obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier) let advice := advice.map (fun expr => Advice.mk expr.assignments expr.identifier) -- If any of the attribute assignment expressions in an obligation or -- advice expression with a matching FulfillOn or AppliesTo attribute -- evaluates to “Indeterminate”, then the whole rule, policy, or -- policy set SHALL be “Indeterminate”. If the FulfillOn or AppliesTo -- attribute does not match the result of the combining algorithm or -- the rule evaluation, then any indeterminate in an obligation or -- advice expression has no effect. -- if obligations. let decision := -- if obligations.any -- (fun obligation => obligation.assignments.any -- (fun assignment => is_indeterminate assignment.expression)) ∨ -- advice.any -- (fun advice => advice.assignments.any -- (fun assignment => is_indeterminate assignment.expression)) -- then -- Decision.indeterminate -- else decision ( decision, ResultAuxiliary.mk status (obligations.map (fun expr => Obligation.mk expr.assignments expr.identifier)) (advice.map (fun expr => Advice.mk expr.assignments expr.identifier)) ) def combine_response_aux (x y : ResultAuxiliary) : ResultAuxiliary := match (x, y) with | (ResultAuxiliary.mk status₁ obligations₁ advice₁, ResultAuxiliary.mk _ obligations₂ advice₂) => ResultAuxiliary.mk status₁ (obligations₁ ++ obligations₂) (advice₁ ++ advice₂) def Choice : Type := List (Decision × ResultAuxiliary) deriving DecidableEq, BEq, Repr def xml_of_decision (decision : Decision) := match decision with | Decision.permit => "Permit" | Decision.deny => "Deny" | Decision.indeterminate => "Indeterminate" | Decision.not_applicable => "NotApplicable" def string_of_status_code (code : StatusCode) := match code with | StatusCode.ok => "urn:oasis:names:tc:xacml:1.0:status:ok" | StatusCode.missing_attribute => "urn:oasis:names:tc:xacml:1.0:status:missing-attribute" | StatusCode.syntax_error => "urn:oasis:names:tc:xacml:1.0:status:syntax-error" | StatusCode.processing_error => "urn:oasis:names:tc:xacml:1.0:status:processing-error" def xml_of_status_code (status : List StatusCode) := match status with | primary :: [] => String.join [ ""] | primary :: rest => String.join [ "", xml_of_status_code rest, ""] | _ => "" def xml_of_status (status : List StatusCode) := match status with | [] => "" | codes => String.join ["", xml_of_status_code codes, ""] def xml_of_xmltype : XmlType -> String | XmlType.string => "http://www.w3.org/2001/XMLSchema#string" | XmlType.boolean => "http://www.w3.org/2001/XMLSchema#boolean" | XmlType.integer => "http://www.w3.org/2001/XMLSchema#integer" | XmlType.double => "http://www.w3.org/2001/XMLSchema#double" | XmlType.time => "http://www.w3.org/2001/XMLSchema#time" | XmlType.date => "http://www.w3.org/2001/XMLSchema#date" | XmlType.dateTime => "http://www.w3.org/2001/XMLSchema#dateTime" | XmlType.dayTimeDuration => "http://www.w3.org/2001/XMLSchema#dayTimeDuration" | XmlType.yearMonthDuration => "http://www.w3.org/2001/XMLSchema#yearMonthDuration" | XmlType.anyURI => "http://www.w3.org/2001/XMLSchema#anyURI" | XmlType.hexBinary => "http://www.w3.org/2001/XMLSchema#hexBinary" | XmlType.base64Binary => "http://www.w3.org/2001/XMLSchema#base64Binary" | XmlType.rfc822Name => "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name" | XmlType.x500Name => "urn:oasis:names:tc:xacml:1.0:data-type:x500Name" | XmlType.ipAddress => "urn:oasis:names:tc:xacml:2.0:data-type:ipAddress" | XmlType.dnsName => "urn:oasis:names:tc:xacml:2.0:data-type:dnsName" def xml_of_attribute_assignment (assignment : Attribute) := String.join [ " String.join ["\" Issuer=\"", issuer] | none => ""), "\"/>" ] def xml_of_obligation (obligation : Obligation) := String.join [ "", String.join (List.map xml_of_attribute_assignment obligation.assignments), "" ] def xml_of_obligations (obligations : List Obligation) := String.join ["", String.join (List.map xml_of_obligation obligations), ""] def xml_of_advice (advice : Advice) := String.join [ "", String.join (List.map xml_of_attribute_assignment advice.assignments), "" ] def xml_of_advices (advices : List Advice) := String.join ["", String.join (List.map xml_of_advice advices), ""] def xml_of_response (response : Result) := String.join [ "", "", "", xml_of_decision response.fst, (match response.snd with | some {status, obligations, advice} => String.join [ (match status with | some status => xml_of_status status | none => ""), (match obligations with | [] => "" | _ => xml_of_obligations obligations), (match advice with | [] => "" | _ => xml_of_advices advice) ] | none => ""), "", "" ]