path: root/xacml-proofs/compiler/bin/main.ml

open Base

let policy = {|<?xml version="1.0" encoding="UTF-8"?>
<Policy
  xmlns="urn:oasis:names:tc:xacml:3.0:core:schema:wd-17"
  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
  xsi:schemaLocation="urn:oasis:names:tc:xacml:3.0:core:schema:wd-17
  http://docs.oasis-open.org/xacml/3.0/xacml-core-v3-schema-wd-17.xsd"
  PolicyId="urn:oasis:names:tc:xacml:3.0:example:SimplePolicy1"
  Version="1.0"
  RuleCombiningAlgId="urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-overrides">
  <Description>
    Medi Corp access control policy
  </Description>
  <Target/>
  <Rule
    RuleId= "urn:oasis:names:tc:xacml:3.0:example:SimpleRule1"
    Effect="Permit">
    <Description>
      Any subject with an e-mail name in the med.example.com domain
      can perform any action on any resource.
    </Description>
    <Target>
      <AnyOf>
        <AllOf>
          <Match
            MatchId="urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match">
          <AttributeValue
            DataType="http://www.w3.org/2001/XMLSchema#string"
              >med.example.com</AttributeValue>
          <AttributeDesignator
            MustBePresent="false"
            Category="urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
            AttributeId="urn:oasis:names:tc:xacml:1.0:subject:subject-id"
            DataType="urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name"/>
          </Match>
        </AllOf>
      </AnyOf>
    </Target>
  </Rule>
</Policy>
|}



type xml_element = (string * (string * string) list * Xml.xml list)

type lean_expression = Identifier of string
                     | Bool of bool
                     | String of string
                     | Number of int
                     | List of lean_expression list
                     | Tuple of lean_expression list
                     | Application of lean_expression * lean_expression list
                     | Define of string * lean_expression

let rec fmt_lean_expression : lean_expression -> string = function
  | Identifier s -> s
  | Bool b -> if b then "True" else "False"
  | String s -> Printf.sprintf "\"%s\"" s
  | Number n -> Int.to_string n
  | List xs -> Printf.sprintf "[%s]" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
  | Tuple xs -> Printf.sprintf "(%s)" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
  | Application (head, args) -> Printf.sprintf "(%s %s)" (fmt_lean_expression head) (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args))
  | Define (ident, expr) -> Printf.sprintf "def %s := (%s)" ident (fmt_lean_expression expr)

let get_exn opt message =
  match opt with
  | Some x -> x
  | _ -> failwith message

let rec get_attr (needle : string) : (string * string) list -> string option = function
  | (k, v) :: xs -> if String.equal k needle then Some v else get_attr needle xs
  | _ -> None

let get_attr_exn needle attrs : string =
  get_exn (get_attr needle attrs) "missing attribute"

let rec get_children (kind : string) : Xml.xml list -> xml_element list = function
  | (Element ((tag_name, _, _) as x)) :: xs ->
     if String.equal tag_name kind
     then x :: get_children kind xs
     else get_children kind xs
  | PCData s :: xs -> get_children kind xs
  | _ -> []

let get_child kind xs = List.nth (get_children kind xs) 0
let get_child_exn kind xs =
  get_exn (get_child kind xs) "no such child"

let xml_element_of_children (children : Xml.xml list) : xml_element list =
  List.map children ~f:(function
      | Element x -> x
      | _ -> failwith "called on element with non-element children")

let compile_rule_combinator_algorithm : string -> lean_expression = function
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.ordered_permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-unless-permit" ->
     (Identifier "RuleCombinatorAlgorithm.deny_unless_permit")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:permit-unless-deny" ->
     (Identifier "RuleCombinatorAlgorithm.permit_unless_deny")
  | "urn:oasis:names:tc:xacml:1.0:rule-combining-algorithm:first-applicable" ->
     (Identifier "RuleCombinatorAlgorithm.first_applicable")
  | "urn:oasis:names:tc:xacml:1.0:rule-combining-algorithm:deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.1:rule-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.0:rule-combining-algorithm:permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_permit_overrides")
  | "urn:oasis:names:tc:xacml:1.1:rule-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_ordered_permit_overrides")
  | _ -> failwith "unknown rule combinator"

let compile_policy_combinator_algorithm : string -> lean_expression = function
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.ordered_permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:deny-unless-permit" ->
     (Identifier "PolicyCombinatorAlgorithm.deny_unless_permit")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:permit-unless-deny" ->
     (Identifier "PolicyCombinatorAlgorithm.permit_unless_deny")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:first-applicable" ->
     (Identifier "PolicyCombinatorAlgorithm.first_applicable")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:only-one-applicable" ->
     (Identifier "PolicyCombinatorAlgorithm.only_one_applicable")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.1:policy-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_permit_overrides")
  | "urn:oasis:names:tc:xacml:1.1:policy-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_ordered_permit_overrides")
  | _ -> failwith "unknown policy combinator"

(* let (tag_name, attributes, children) = elt in *)

let compile_xml_type (s : string) : lean_expression =
  let kind = match s with
    | "http://www.w3.org/2001/XMLSchema#string"                -> "string"
    | "http://www.w3.org/2001/XMLSchema#boolean"               -> "boolean"
    | "http://www.w3.org/2001/XMLSchema#integer"               -> "integer"
    | "http://www.w3.org/2001/XMLSchema#double"                -> "double"
    | "http://www.w3.org/2001/XMLSchema#time"                  -> "time"
    | "http://www.w3.org/2001/XMLSchema#date"                  -> "date"
    | "http://www.w3.org/2001/XMLSchema#dateTime"              -> "dateTime"
    | "http://www.w3.org/2001/XMLSchema#anyURI"                -> "anyURI"
    | "http://www.w3.org/2001/XMLSchema#hexBinary"             -> "hexBinary"
    | "http://www.w3.org/2001/XMLSchema#base64Binary"          -> "base64Binary"
    | "http://www.w3.org/2001/XMLSchema#dayTimeDuration"       -> "dayTimeDuration"
    | "http://www.w3.org/2001/XMLSchema#yearMonthDuration"     -> "yearMonthDuration"
    | "urn:oasis:names:tc:xacml:1.0:data-type:x500Name"        -> "x500Name"
    | "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name"      -> "rfc822Name"
    | "urn:oasis:names:tc:xacml:2.0:data-type:ipAddress"       -> "ipAddress"
    | "urn:oasis:names:tc:xacml:2.0:data-type:dnsName"         -> "dnsName"
    | "urn:oasis:names:tc:xacml:3.0:data-type:xpathExpression" -> "xpathExpression"
    | _ -> failwith "unknown DataType"
  in
  Identifier ("XmlType." ^ kind)

let compile_primitive kind value : lean_expression =
  Application
    (Identifier "Value.primitive",
     [(Tuple [compile_xml_type kind; (String value)])])

let compile_attribute_value (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "AttributeValue");
  let kind = get_attr_exn "DataType" attrs in
  match List.nth_exn children 0 with
  | PCData value -> compile_primitive kind value
  | _ -> failwith "invalid value expression"

let compile_attribute_designator (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "AttributeDesignator");
  let category = get_attr_exn "Category" attrs in
  let identifier = get_attr_exn "AttributeId" attrs in
  let kind = get_attr_exn "DataType" attrs in
  let must_be_present = get_attr_exn "MustBePresent" attrs in
  let issuer =  (match get_attr "Issuer" attrs with
    | Some s -> (Application ((Identifier "some"), [(String s)]))
    | _ -> (Identifier "none"))
  in
  Application
    ((Identifier "AttributeDesignator.mk"),
     [(String category);
      (String identifier);
      (compile_xml_type kind);
      issuer;
      (Bool (Bool.of_string must_be_present))])

let compile_match (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "Match");
  let alg_id = get_attr_exn "MatchId" attrs in
  let value = get_child_exn "AttributeValue" children in
  let designator = get_child_exn "AttributeDesignator" children in
  Application
    ((Identifier "Match.mk"),
     [(String alg_id);
      compile_attribute_designator designator;
      compile_attribute_value value])

let compile_all_of (elt : xml_element) : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.equal tag_name "AllOf");
  assert (not @@ phys_equal (List.length children) 0); (* "empty <AllOf>" *)
  List (List.map ~f:compile_match (get_children "Match" children))

let compile_any_of (elt : xml_element) : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.equal tag_name "AnyOf");
  assert (not @@ phys_equal (List.length children) 0); (* "empty <AnyOf>" *)
  List (List.map ~f:compile_all_of (get_children "AllOf" children))

let compile_target (elt : xml_element) : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.equal tag_name "Target");
  List (List.map ~f:compile_any_of (xml_element_of_children children))



let rec compile_expression (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  match tag_name with
  | "Apply" ->
     let args = List.filter_map children ~f:(function
                    | Element ("Description", _, _) -> None
                    | Element elt -> Some (compile_expression elt)
                    | _ -> None) in
     Application (Identifier "Expression.apply", args)
  | "Function" ->
     let name = get_attr_exn "FunctionID" attrs in
     Application (Identifier "Expression.function", [String name])
  | "AttributeDesignator" ->
     Application
       (Identifier "Expression.attribute_designator",
        [compile_attribute_designator elt])
  | "AttributeValue" ->
     Application
       (Identifier "Expression.attribute_value",
        [compile_attribute_value elt])
  | "VariableReference" -> failwith "unimplemented"
  | _ -> failwith "unknown expression type"

let compile_condition (elt : xml_element) : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.equal tag_name "Condition");
  match children with
  | [Element elt] -> compile_expression elt
  | _ -> failwith "invalid <Condition> form"

let compile_attribute_assignment_expression (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "AdviceExpression");
  let category = get_attr_exn "Category" attrs in
  let identifier = get_attr_exn "Identifier" attrs in
  let expression = get_child_exn "Expression" children in
  let issuer = (match get_attr "Identifier" attrs with
                | Some issuer -> Application (Identifier "some", [String issuer])
                | None -> Application (Identifier "none", [])) in
  Application
    (Identifier "AttributeAssignmentExpression.mk",
     [String category;
      String identifier;
      issuer;
      compile_expression expression])

let compile_obligation_expression (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "ObligationExpression");
  let identifier = get_attr_exn "ObligationId" attrs in
  let assignments = get_children "AttributeAssignmentExpression" children in
  let fulfill_on = match get_attr_exn "FullfillOn" attrs with
    | "Permit" -> Identifier "EffectType.permit"
    | "Deny" -> Identifier "EffectType.deny"
    | _ -> failwith "invalid <EffectType>"
  in
  Application
    (Identifier "ObligationExpression.mk",
     [List (List.map assignments ~f:compile_attribute_assignment_expression);
      String identifier;
      fulfill_on])

let compile_advice_expression (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "AdviceExpression");
  let identifier = get_attr_exn "AdviceId" attrs in
  let assignments = get_children "AttributeAssignmentExpression" children in
  let applies_to = match get_attr_exn "AppliesTo" attrs with
    | "Permit" -> Identifier "EffectType.permit"
    | "Deny" -> Identifier "EffectType.deny"
    | _ -> failwith "invalid <EffectType>"
  in
  Application
    (Identifier "ObligationExpression.mk",
     [List (List.map assignments ~f:compile_attribute_assignment_expression);
      String identifier;
      applies_to])

let canonicalize_identifier ?(version = None) (ident : string) : string =
  let is_alphanumeric = function
      'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' -> true
      | _ -> false in
  let filtered = match version with
    | Some version -> List.filter ~f:is_alphanumeric
                        (String.to_list (ident ^ "_" ^ version))
    | None -> List.filter ~f:is_alphanumeric (String.to_list ident)
  in
  "compiled_" ^ (String.of_char_list filtered)

let compile_rule (elt : xml_element) : (lean_expression list) * lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "Rule");
  let identifier = get_attr_exn "RuleId" attrs in
  let obligation_expressions = get_children "ObligationExpression" children in
  let advice_expressions = get_children "AdviceExpression"children  in
  let effect = match get_attr_exn "Effect" attrs with
    | "Permit" -> Identifier "EffectType.permit"
    | "Deny" -> Identifier "EffectType.deny"
    | _ -> failwith "invalid <EffectType>"
  in
  let target = match get_child "Target" children with
    | Some tgt -> compile_target tgt
    | None -> List [] in
  let condition = match get_child "Condition" children with
    | Some cond -> compile_condition cond
    | None -> Identifier "none" in
  let metadata =
    Application
      ((Identifier "Rule.mk"),
       [target;
        condition;
        effect;
        List (List.map ~f:compile_obligation_expression obligation_expressions);
        List (List.map ~f:compile_advice_expression advice_expressions);]) in
  let identifier = canonicalize_identifier identifier in
  ([Define
      (identifier,
       Application
         ((Identifier "PolicyElement.Rule"), [metadata]))],
   Application
     ((Identifier "ElementTree.Node"), [Identifier identifier; List []]))

let compile_policy (elt : xml_element) : (lean_expression list) * lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "Policy");
  let identifier = get_attr_exn "PolicyId" attrs in
  let version = get_attr_exn "Version" attrs in
  let obligation_expressions = get_children "ObligationExpression" children in
  let advice_expressions = get_children "AdviceExpression" children in
  let alg_id = get_attr_exn "RuleCombiningAlgId" attrs in
  let target = get_child_exn "Target" children in
  let metadata =
    Application
      ((Identifier "Policy.mk"),
       [compile_rule_combinator_algorithm alg_id;
        compile_target target;
        List (List.map ~f:compile_obligation_expression obligation_expressions);
        List (List.map ~f:compile_advice_expression advice_expressions);])in
  let identifier = canonicalize_identifier identifier ~version:(Some version) in
  let children = List.map ~f:compile_rule (get_children "Rule" children) in
  ([Define
      (identifier,
       Application
         ((Identifier "PolicyElement.Policy"), [metadata]))]
   @ (List.map ~f:fst children |> List.concat),
   Application
     ((Identifier "ElementTree.Node"),
      [Identifier identifier;
       List (List.map ~f:snd children)]))

let compile_policyset (elt : xml_element) : (lean_expression list) * lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.equal tag_name "Rule");
  let identifier = get_attr_exn "PolicySetId" attrs in
  let version = get_attr_exn "Version" attrs in
  let obligation_expressions = get_children "ObligationExpression" children in
  let advice_expressions = get_children "AdviceExpression" children in
  let alg_id = get_attr_exn "PolicyCombiningAlgId" attrs in
  let target = get_child_exn "Target" children in
  let metadata =
    Application
      ((Identifier "PolicySet.mk"),
       [compile_policy_combinator_algorithm alg_id;
        compile_target target;
        List (List.map ~f:compile_obligation_expression obligation_expressions);
        List (List.map ~f:compile_advice_expression advice_expressions);])in
  let identifier = canonicalize_identifier identifier ~version:(Some version) in
  let children = List.filter_map ~f:(function
                     | Element (("PolicySet", _, _) as elt) -> Some (compile_policyset elt)
                     | Element (("Policy", _, _) as elt) -> Some (compile_policy elt)
                     | _ -> None)
                   children in
  ([Define
      (identifier,
       Application
         ((Identifier "PolicyElement.PolicySet"), [metadata]))]
   @ (List.map ~f:fst children |> List.concat),
   Application
     ((Identifier "ElementTree.Node"),
      [Identifier identifier;
       List (List.map ~f:snd children)]))

let compile : Xml.xml -> lean_expression list = function
  | Element ((tag_name, attributes, children) as elt) ->
     let (defns, tree) =
       (match tag_name with
        | "PolicySet" -> compile_policyset elt
        | "Policy" -> compile_policy elt
        | _ -> failwith (Printf.sprintf "(%s)" tag_name))
     in defns @ [tree]
  | PCData s -> failwith s

let () = policy
         |> Xml.parse_string
         |> compile
         |> List.map ~f:fmt_lean_expression
         |> List.iter ~f:Caml.print_endline