path: root/xacml-proofs/lean/Xacml.lean

------------------------------------------------------------------------
---- Atoms -------------------------------------------------------------
------------------------------------------------------------------------
--
-- # References
--
-- - 7.6 Match evaluation
--
------------------------------------------------------------------------

inductive MatchResult where
  | is_match      : MatchResult
  | no_match      : MatchResult
  | indeterminate : MatchResult
deriving BEq, Repr

inductive Decision where
  | permit           : Decision
  | deny             : Decision
  | indeterminate    : Decision
  | not_applicable   : Decision
deriving 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 BEq, Repr

instance : Coe Decision' Decision where
  coe b :=
    match b with
      | 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

inductive EffectType where
  | permit : EffectType
  | deny   : EffectType
deriving 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 BEq, Repr

def Primitive : Type := XmlType × String
deriving 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  => #<XmlType.boolean, "True">
      | false => #<XmlType.boolean, "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   => #<XmlType.boolean, "Indeterminate">
      | Option.some a => a

structure Bag where
  contents: List Primitive
deriving Repr

def List.count [BEq α] (xs : List α) (x : α) : Int :=
  (xs.filter (fun y => y == x)).length

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 BEq, Repr

instance : Coe (Option Value) Value where
  coe b :=
    match b with
      | Option.none   => Value.primitive (#<XmlType.boolean, "Indeterminate">)
      | Option.some a => a

------------------------------------------------------------------------
---- Attributes---------------------------------------------------------
------------------------------------------------------------------------
--
-- # References
--
-- - 5.46 Element <Attribute>
-- - 5.42 Element <Request>
--
-- Attributes are categories into <Attributes> elements. In this
-- implementation, categories are rolled up - every attribute carries
-- the category of its enclosing <Attributes> element.
--
------------------------------------------------------------------------

structure Attribute where
  category   : String
  identifier : String
  issuer     : Option String
  value      : Primitive
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

---

def Identifier : Type := String
deriving BEq, Repr

inductive CombinatorAlgorithm where
  | deny_overrides                  : CombinatorAlgorithm
  | ordered_deny_overrides          : CombinatorAlgorithm
  | permit_overrides                : CombinatorAlgorithm
  | ordered_permit_overrides        : CombinatorAlgorithm
  | deny_unless_permit              : CombinatorAlgorithm
  | permit_unless_deny              : CombinatorAlgorithm
  | first_applicable                : CombinatorAlgorithm
  | only_one_applicable             : CombinatorAlgorithm
  | legacy_deny_overrides           : CombinatorAlgorithm
  | legacy_ordered_deny_overrides   : CombinatorAlgorithm
  | legacy_permit_overrides         : CombinatorAlgorithm
  | legacy_ordered_permit_overrides : CombinatorAlgorithm

structure AttributeDesignator where
  category        : String
  identifier      : String
  type            : XmlType
  issuer          : Option String
  must_be_present : Bool
deriving BEq, Repr

namespace AttributeDesignator
  def eval (designator : AttributeDesignator) (context : List Attribute) : Option 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
            | _ => Value.bag (Bag.mk found)
        else 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 BEq, Repr

-- "The <Expression> element is not used directly in a policy. The <Expression>
-- element signifies that an element that extends the ExpressionType and is a
-- member of the <Expression> element substitution group SHALL appear in its
-- place."
--
-- We omit the `<xacml:AttributeSelector>` case because this model of XACML does
-- not include it, and we exclude the `<xacml:VariableReference>` 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 BEq, Repr

namespace Expression
  def apply_eval (name : FunctionID) (args : List Value) : Option Value :=
    if name == "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match" then
      match args with
        | [Value.primitive (XmlType.string,     lhs),
           Value.primitive (XmlType.rfc822Name, rhs)] =>
           Value.primitive (lhs == rhs)
        | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
    else Option.none

  def eval (expression : Expression) (context : Request) : Option Value :=
    -- The return type of `<Apply>` 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:
    --
    -- - <xacml:AttributeValue>
    -- - <xacml:AttributeDesignator>
    -- - <xacml:AttributeSelector>
    -- - <xacml:Apply>
    -- - <xacml:Function>
    -- - <xacml:VariableReference>
    match expression with
      | Expression.apply name args            => apply_eval name args
      | Expression.attribute_designator inner => inner.eval context
      | Expression.attribute_value inner      => some inner
      | _                                     => Option.none
end Expression

structure Match where
  function   : Identifier
  designator : AttributeDesignator
  value      : Value
deriving BEq, Repr
def AllOf  : Type := List Match
deriving BEq, Repr
def AnyOf  : Type := List AllOf
deriving BEq, Repr
def Target : Type := List AnyOf
deriving BEq, Repr

namespace Match
  def eval (m : Match) (context : Request) : Option Value :=
    match m with
      | Match.mk fn designator value =>
        do
          let result <- designator.eval context
          let results := match result with
          | (Value.bag (Bag.mk attrs)) =>
            attrs.map
            fun attr =>
              let args := [value, Value.primitive attr]
              (Expression.apply fn args).eval context
          | (Value.primitive attr) =>
            let args := [value, Value.primitive attr]
            [(Expression.apply fn args).eval context]

          let results := results.map (fun (x : Option Value) => (x : Value))
          if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then
            (Value.primitive (#<XmlType.boolean, "True">))
          else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then
            (Value.primitive (#<XmlType.boolean, "Indeterminate">))
          else Value.primitive (#<XmlType.boolean, "False">)
end Match

structure AttributeAssignment where
  category        : String
  identifier      : String
  issuer          : Option String
deriving BEq, Repr

structure Obligation where
  assignments : List AttributeAssignment
  identifier : String
deriving BEq, Repr

structure Advice where
  assignments : List AttributeAssignment
  identifier : String
deriving BEq, Repr

structure AttributeAssignmentExpression where
  category        : String
  identifier      : String
  issuer          : Option String
  expression      : Expression
deriving BEq, Repr

structure ObligationExpression where
  assignments : List AttributeAssignmentExpression
  identifier : String
  fulfill_on : Decision
deriving BEq, Repr

structure AdviceExpression where
  assignments : List AttributeAssignmentExpression
  identifier : String
  applies_to : Decision
deriving BEq, Repr

-- n.b. "The <Condition> contains one <Expression> element"
structure Rule where
  target      : Target
  condition   : Expression
  effect      : EffectType
  obligations : List ObligationExpression
  advice      : List AdviceExpression

structure PolicySet where
  combinator  : CombinatorAlgorithm
  target      : Target
  children    : List PolicySetChild
  obligations : List ObligationExpression
  advice      : List AdviceExpression

inductive PolicySetChild where
  | policy_set (inner : PolicySet) : PolicySetChild
  | policy     (inner : Policy)    : PolicySetChild

structure Policy where
  combinator  : CombinatorAlgorithm
  target      : Target
  rules       : List Rule
  obligations : List ObligationExpression
  advice      : List AdviceExpression

inductive StatusCode
  | ok                : StatusCode
  | missing_attribute : StatusCode
  | syntax_error      : StatusCode
  | processing_error  : StatusCode
deriving BEq, Repr

structure ResultAuxiliary where
  status      : Option (List StatusCode)
  obligations : List Obligation
  advice      : List Advice
deriving BEq, Repr

structure MissingAttributeDetail where
  category   : String
  identifier : String
  issuer     : Option String
  value      : Option Value
  type       : XmlType
deriving BEq, Repr

def Result : Type := Decision × (Option ResultAuxiliary)

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 status₂ obligations₂ advice₂) =>
      ResultAuxiliary.mk
        status₁
        (obligations₁ ++ obligations₂)
        (advice₁ ++ advice₂)

def Choice : Type := List (Decision × ResultAuxiliary)
deriving BEq, Repr

---
-- 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_all_of (all_of : AllOf) (context : Request) : MatchResult :=
--   let result := all_of.map (fun x => x.eval 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
--   else MatchResult.no_match

-- def evaluate_any_of (any_of : AnyOf) (context : Request) : MatchResult :=
--   match any_of with
--     | [] => MatchResult.is_match
--     | List.cons x xs => match evaluate_all_of x context with
--       | MatchResult.is_match => MatchResult.is_match
--       | MatchResult.no_match =>
--         let rest := evaluate_any_of xs context
--         if rest == MatchResult.is_match then MatchResult.no_match else rest
--       | MatchResult.indeterminate =>
--         let rest := evaluate_any_of xs context
--         if rest == MatchResult.no_match then MatchResult.indeterminate else rest

-- def evaluate_target (target : Target) (context : Request) : MatchResult :=
--   match target with
--     | [] => MatchResult.is_match
--     | List.cons x xs => match evaluate_any_of x context with
--       | MatchResult.is_match => evaluate_target xs context
--       | MatchResult.no_match => MatchResult.no_match
--       | MatchResult.indeterminate =>
--         let rest := evaluate_target xs context
--         if rest == MatchResult.no_match then rest else MatchResult.indeterminate

-- def evaluate_assignments (assignments : List AttributeAssignmentExpression) : List AttributeAssignment :=
--   assignments.map (fun assignment =>
--                        match assignment with
--                        | AttributeAssignmentExpression.mk category identifier issuer _ =>
--                          AttributeAssignment.mk category identifier issuer)


-- def evaluate_rule (rule : Rule) (context : Request) : Decision' × ResultAuxiliary :=
--   let decision :=
--     if rule.target == [] then (rule.effect).to_decision'
--     else match evaluate_target rule.target context with
--       | MatchResult.is_match =>
--         match ((rule.condition).eval context : Value) with
--           | (XmlType.string, "True") => (rule.effect).to_decision'
--           | (XmlType.string, "False") => Decision'.not_applicable
--           | (_, _) =>
--             if (rule.effect).to_decision' == Decision'.permit then
--               Decision'.indeterminate_p else
--               Decision'.indeterminate_d
--       | MatchResult.no_match      => Decision'.not_applicable
--       | MatchResult.indeterminate => Decision'.not_applicable
--   let obligations := rule.obligations.filter (fun obl => obl.fulfill_on == (decision : Decision))
--   let advice      := rule.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
--   (
--     decision,
--     ResultAuxiliary.mk
--       Option.none
--       (obligations.map (fun expr => Obligation.mk
--                                       (evaluate_assignments expr.assignments)
--                                       expr.identifier))
--       (advice.map      (fun expr => Advice.mk
--                                       (evaluate_assignments expr.assignments)
--                                       expr.identifier)))

-- 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_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)
--   let obligations := policy.obligations.filter (fun obl => obl.fulfill_on == (decision : Decision))
--   let advice      := policy.advice.filter      (fun obl => obl.applies_to == (decision : Decision))
--   -- TODO: How do we combine advice/obligations?
--   [(
--     decision,
--     ResultAuxiliary.mk
--       Option.none
--       (obligations.map (fun expr => Obligation.mk
--                                       (evaluate_assignments expr.assignments)
--                                       expr.identifier))
--       (advice.map      (fun expr => Advice.mk
--                                       (evaluate_assignments expr.assignments)
--                                       expr.identifier))
--   )]