diff options
| -rw-r--r-- | xacml-proofs/compiler/bin/dune | 3 | ||||
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 681 | ||||
| -rw-r--r-- | xacml-proofs/compiler/lib/compiler.ml | 636 | ||||
| -rw-r--r-- | xacml-proofs/compiler/lib/compiler.mli | 1 | ||||
| -rw-r--r-- | xacml-proofs/compiler/lib/dune | 4 |
5 files changed, 647 insertions, 678 deletions
diff --git a/xacml-proofs/compiler/bin/dune b/xacml-proofs/compiler/bin/dune index 239df43..3d787bf 100644 --- a/xacml-proofs/compiler/bin/dune +++ b/xacml-proofs/compiler/bin/dune @@ -1,5 +1,4 @@ (executable (public_name compiler) (name main) - (libraries base compiler str topological_sort xml-light) - (preprocess (pps ppx_let ppx_jane))) + (libraries core compiler)) diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml index d797e47..3a2073e 100644 --- a/xacml-proofs/compiler/bin/main.ml +++ b/xacml-proofs/compiler/bin/main.ml @@ -1,676 +1,7 @@ -open Base +open Core +open Compiler -let version_regex = Str.regexp "^\\([0-9]+\\.\\)*[0-9]+$" -let version_match_type_regex = Str.regexp "^\\(\\(\\d+|\\*\\)\\.\\)*\\(\\d+|\\*|\\+\\)$" - -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.(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.(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.(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.(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.(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.(tag_name = "AllOf")); - assert (not Int.((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.(tag_name = "AnyOf")); - assert (not Int.((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.(tag_name = "Target")); - List (List.map ~f:compile_any_of (xml_element_of_children children)) - - - -let rec compile_expression - (env : (string * lean_expression) list) - (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 env 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" -> - let identifier = get_attr_exn "VariableId" attrs in - (match List.Assoc.find ~equal:String.equal env identifier with - | Some value -> value - | _ -> failwith "unbound variable") - | _ -> failwith "unknown expression type" - -let compile_condition - (env : (string * lean_expression) list) - (elt : xml_element) - : lean_expression = - let (tag_name, _, children) = elt in - assert (String.(tag_name = "Condition")); - match children with - | [Element elt] -> compile_expression env elt - | _ -> failwith "invalid <Condition> form" - -let compile_attribute_assignment_expression - (env : (string * lean_expression) list) - (elt : xml_element) - : lean_expression = - let (tag_name, attrs, children) = elt in - assert (String.(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 env expression]) - -let compile_obligation_expression - (env : (string * lean_expression) list) - (elt : xml_element) - : lean_expression = - let (tag_name, attrs, children) = elt in - assert (String.(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 env)); - String identifier; - fulfill_on]) - -let compile_advice_expression - (env : (string * lean_expression) list) - (elt : xml_element) - : lean_expression = - let (tag_name, attrs, children) = elt in - assert (String.(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 env)); - 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 metadata_identifier_of ?(version = None) (ident : string) : string = - canonicalize_identifier ~version:version ident ^ "_metadata" - -let element_identifier_of ?(version = None) (ident : string) : string = - canonicalize_identifier ~version:version ident ^ "_element" - -type compilation_intermediate = - { metadata_definitions : lean_expression list; - element_definitions : lean_expression list; - root_identifier : string; - edges : (int * int) list - } -[@@deriving fields] - -let compile_rule - (env : (string * lean_expression) list) - (elt : xml_element) - : compilation_intermediate = - let (tag_name, attrs, children) = elt in - assert (String.(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 env cond - | None -> Identifier "none" in - let metadata = - Application - ((Identifier "Rule.mk"), - [target; - condition; - effect; - List (List.map ~f:(compile_obligation_expression env) - obligation_expressions); - List (List.map ~f:(compile_advice_expression env) - advice_expressions);]) in - let metadata_identifier = metadata_identifier_of identifier in - let element_identifier = element_identifier_of identifier in - { metadata_definitions = - [Define - (metadata_identifier, - Application - ((Identifier "PolicyElement.Rule"), [metadata]))]; - element_definitions = - [Define - (element_identifier, - Application - ((Identifier "ElementTree.Node"), - [Identifier metadata_identifier; List []]))]; - root_identifier = element_identifier; - edges = [] - } - -let compile_variable_definition - (env : (string * lean_expression) list) - (elt : xml_element) - : string * lean_expression = - let (tag_name, attrs, children) = elt in - assert (String.(tag_name = "VariableDefinition")); - let identifier = get_attr_exn "VariableId" attrs in - let value = get_child_exn "Expression" children in - (identifier, compile_expression env value) - -let order_variable_definitions elts = - let rec find_variable_references identifier : Xml.xml -> (string * string) list = - function - | Element ("VariableReference", attrs, _) -> - let referenced_identifier = get_attr_exn "VariableId" attrs in - [(identifier, referenced_identifier)] - | Element (_, _, children) -> - List.map ~f:(find_variable_references identifier) - children - |> List.concat - | _ -> [] - in - let nodes = - List.map - ~f:(function - | ("VariableDefinition", attrs, _) -> get_attr_exn "VariableId" attrs - | _ -> failwith "unreachable") - elts in - let edges = - List.map - ~f:(function - | ("VariableDefinition", attrs, children) as elt -> - find_variable_references (get_attr_exn "VariableId" attrs) (Element elt) - | _ -> failwith "unreachable") - elts - |> List.concat - in - let open Topological_sort in - let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in - sort (module String) nodes edges - -let compile_policy (elt : xml_element) : compilation_intermediate = - let (tag_name, attrs, children) = elt in - assert (String.(tag_name = "Policy")); - let identifier = get_attr_exn "PolicyId" attrs in - let version = get_attr_exn "Version" attrs in - assert (Str.string_match version_regex version 0); - let variables = get_children "VariableDefinition" children in - let variables = - match order_variable_definitions variables with - | Ok ordering -> - List.map ordering - ~f:(fun needle -> - List.find_exn ~f:(function - | ("VariableDefinition", attrs, _) -> - String.(needle = (get_attr_exn "VariableId" attrs)) - | _ -> false) - variables) - | _ -> failwith "failed to order variable definitions" - in - let variables = - List.fold variables - ~init:[] - ~f:(fun x y -> - let (key, value) = compile_variable_definition x y in - (key,value) :: x) - 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 variables) - obligation_expressions); - List (List.map ~f:(compile_advice_expression variables) - advice_expressions);])in - let children = List.map ~f:(compile_rule variables) - (get_children "Rule" children) in - let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in - let element_identifier = element_identifier_of identifier ~version:(Some version) in - { metadata_definitions = - (List.map ~f:metadata_definitions children |> List.concat) - @ [Define - (metadata_identifier, - Application - ((Identifier "PolicyElement.Policy"), [metadata]))]; - element_definitions = - (List.map ~f:element_definitions children |> List.concat) - @ [Define - (element_identifier, - Application - ((Identifier "ElementTree.Node"), - [Identifier metadata_identifier; - List (List.map ~f:(fun x -> Identifier (root_identifier x)) children)]))]; - root_identifier = element_identifier; - edges = [] - } - -let rec match_policy_reference elements identifier = - match elements with - | `Policy (identifier', version) :: xs -> - if String.(identifier = identifier') - then Some (canonicalize_identifier ~version:(Some version) identifier) - else match_policy_reference xs identifier - | `PolicySet (_, _) :: xs -> match_policy_reference xs identifier - | [] -> None - -let rec match_policyset_reference elements identifier regexes = - match elements with - | `PolicySet (identifier', version) :: xs -> - if String.(identifier = identifier') && - List.for_all ~f:(fun regex -> Str.string_match regex version 0) regexes - then Some (canonicalize_identifier ~version:(Some version) identifier) - else match_policyset_reference xs identifier regexes - | `Policy (_, _) :: xs -> match_policyset_reference xs identifier regexes - | [] -> None - -let rec compile_policyset - policy_elements - (elt : xml_element) - : compilation_intermediate = - let (tag_name, attrs, children) = elt in - assert (String.(tag_name = "Rule")); - let identifier = get_attr_exn "PolicySetId" attrs in - let version = get_attr_exn "Version" attrs in - assert (Str.string_match version_regex version 0); - 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 children = - List.filter_map ~f:(function - | Element (("PolicySet", _, _) as elt) -> - Some (compile_policyset policy_elements elt) - | Element (("PolicySetIdReference", attrs, children) as elt) -> - let identifier = match children with - | [PCData identifier] -> identifier - | _ -> failwith "invalid PolicySetIdReference" - in - let regexes = - List.filter_map ~f:(fun x -> x) [ - get_attr "xacml:Version" attrs; - get_attr "xacml:EarliestVersion" attrs; - get_attr "xacml:LatestVersion" attrs - ] - in - List.iter ~f:(fun x -> assert (Str.string_match version_match_type_regex x 0)) - regexes ; - let regexes = List.map ~f:Str.regexp regexes in - (match match_policyset_reference policy_elements identifier regexes with - | Some identifier -> - Some { metadata_definitions = []; - element_definitions = []; - root_identifier = identifier; - edges = [] } - | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier)) - | Element (("Policy", _, _) as elt) -> Some (compile_policy elt) - | Element (("PolicyIdReference", _, _) as elt) -> - let identifier = match children with - | [PCData identifier] -> identifier - | _ -> failwith "invalid PolicyIdReference" - in - (match match_policy_reference policy_elements identifier with - | Some identifier -> - Some { metadata_definitions = []; - element_definitions = []; - root_identifier = identifier; - edges = [] } - | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier)) - | _ -> None) - children in - let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in - let element_identifier = element_identifier_of identifier ~version:(Some version) in - { metadata_definitions = - (List.map ~f:metadata_definitions children |> List.concat) - @ [Define - (metadata_identifier, - Application - ((Identifier "PolicyElement.PolicySet"), [metadata]))]; - element_definitions = - (List.map ~f:element_definitions children |> List.concat) - @ [Define - (element_identifier, - Application - ((Identifier "ElementTree.Node"), - [Identifier metadata_identifier; - List (List.map ~f:(fun x -> Identifier (root_identifier x)) children)]))]; - root_identifier = element_identifier; - edges = [] - } - -let rec policy_element_names (root : xml_element) = - let (tag_name, attrs, children) = root in - match tag_name with - | "PolicySet" -> - let identifier = get_attr_exn "PolicySetId" attrs in - let version = get_attr_exn "Version" attrs in - [`PolicySet (identifier, version)] - @ (List.map ~f:policy_element_names (get_children "PolicySet" children) |> List.concat) - @ (List.map ~f:policy_element_names (get_children "Policy" children) |> List.concat) - | "Policy" -> - let identifier = get_attr_exn "PolicyId" attrs in - let version = get_attr_exn "Version" attrs in - [`Policy (identifier, version)] - | _ -> [] - -let order_element_definitions elts = - let nodes = - List.map - ~f:(function - | Define (identifier, _) -> identifier - | _ -> failwith "badly formed list of expressions") - elts in - let edges = - List.map - ~f:(function - | Define (parent, Application (_, [_; List children])) -> - List.map ~f:(function - | Identifier child -> (child, parent) - | _ -> failwith "badly formed list of expressions") - children - | _ -> failwith "badly formed list of expressions") - elts - |> List.concat - in - let open Topological_sort in - let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in - sort (module String) nodes edges - -let compile : Xml.xml -> lean_expression list = function - | Element ((tag_name, attributes, children) as elt) -> - let { metadata_definitions; element_definitions; root_identifier } = - (match tag_name with - | "PolicySet" -> - let policy_elements = (policy_element_names elt) in - compile_policyset policy_elements elt - | "Policy" -> compile_policy elt - | _ -> failwith (Printf.sprintf "(%s)" tag_name)) - in - let element_definitions = - (match order_element_definitions element_definitions with - | Result.Ok ordering -> - List.map ordering - ~f:(fun needle -> - List.find_exn ~f:(function - | Define (identifier, _) -> String.(identifier = needle) - | _ -> false) - element_definitions) - | _ -> failwith "failed to order definitions") - in - metadata_definitions @ element_definitions @ [Identifier root_identifier] - | PCData s -> failwith s - -let () = policy - |> Xml.parse_string - |> compile - |> List.map ~f:fmt_lean_expression - |> List.iter ~f:Caml.print_endline +let () = + let file_name = Array.get (Sys.get_argv ()) 1 in + let policy_code = In_channel.read_all file_name in + compile' policy_code |> Stdio.print_endline diff --git a/xacml-proofs/compiler/lib/compiler.ml b/xacml-proofs/compiler/lib/compiler.ml new file mode 100644 index 0000000..8938c63 --- /dev/null +++ b/xacml-proofs/compiler/lib/compiler.ml @@ -0,0 +1,636 @@ +open Base + +let version_regex = Str.regexp "^\\([0-9]+\\.\\)*[0-9]+$" +let version_match_type_regex = Str.regexp "^\\(\\(\\d+|\\*\\)\\.\\)*\\(\\d+|\\*|\\+\\)$" + + + +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.(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.(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.(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.(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.(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.(tag_name = "AllOf")); + assert (not Int.((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.(tag_name = "AnyOf")); + assert (not Int.((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.(tag_name = "Target")); + List (List.map ~f:compile_any_of (xml_element_of_children children)) + + + +let rec compile_expression + (env : (string * lean_expression) list) + (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 env 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" -> + let identifier = get_attr_exn "VariableId" attrs in + (match List.Assoc.find ~equal:String.equal env identifier with + | Some value -> value + | _ -> failwith "unbound variable") + | _ -> failwith "unknown expression type" + +let compile_condition + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = + let (tag_name, _, children) = elt in + assert (String.(tag_name = "Condition")); + match children with + | [Element elt] -> compile_expression env elt + | _ -> failwith "invalid <Condition> form" + +let compile_attribute_assignment_expression + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = + let (tag_name, attrs, children) = elt in + assert (String.(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 env expression]) + +let compile_obligation_expression + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = + let (tag_name, attrs, children) = elt in + assert (String.(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 env)); + String identifier; + fulfill_on]) + +let compile_advice_expression + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = + let (tag_name, attrs, children) = elt in + assert (String.(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 env)); + 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 metadata_identifier_of ?(version = None) (ident : string) : string = + canonicalize_identifier ~version:version ident ^ "_metadata" + +let element_identifier_of ?(version = None) (ident : string) : string = + canonicalize_identifier ~version:version ident ^ "_element" + +type compilation_intermediate = + { metadata_definitions : lean_expression list; + element_definitions : lean_expression list; + root_identifier : string; + edges : (int * int) list + } +[@@deriving fields] + +let compile_rule + (env : (string * lean_expression) list) + (elt : xml_element) + : compilation_intermediate = + let (tag_name, attrs, children) = elt in + assert (String.(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 env cond + | None -> Identifier "none" in + let metadata = + Application + ((Identifier "Rule.mk"), + [target; + condition; + effect; + List (List.map ~f:(compile_obligation_expression env) + obligation_expressions); + List (List.map ~f:(compile_advice_expression env) + advice_expressions);]) in + let metadata_identifier = metadata_identifier_of identifier in + let element_identifier = element_identifier_of identifier in + { metadata_definitions = + [Define + (metadata_identifier, + Application + ((Identifier "PolicyElement.Rule"), [metadata]))]; + element_definitions = + [Define + (element_identifier, + Application + ((Identifier "ElementTree.Node"), + [Identifier metadata_identifier; List []]))]; + root_identifier = element_identifier; + edges = [] + } + +let compile_variable_definition + (env : (string * lean_expression) list) + (elt : xml_element) + : string * lean_expression = + let (tag_name, attrs, children) = elt in + assert (String.(tag_name = "VariableDefinition")); + let identifier = get_attr_exn "VariableId" attrs in + let value = get_child_exn "Expression" children in + (identifier, compile_expression env value) + +let order_variable_definitions elts = + let rec find_variable_references identifier : Xml.xml -> (string * string) list = + function + | Element ("VariableReference", attrs, _) -> + let referenced_identifier = get_attr_exn "VariableId" attrs in + [(identifier, referenced_identifier)] + | Element (_, _, children) -> + List.map ~f:(find_variable_references identifier) + children + |> List.concat + | _ -> [] + in + let nodes = + List.map + ~f:(function + | ("VariableDefinition", attrs, _) -> get_attr_exn "VariableId" attrs + | _ -> failwith "unreachable") + elts in + let edges = + List.map + ~f:(function + | ("VariableDefinition", attrs, _children) as elt -> + find_variable_references (get_attr_exn "VariableId" attrs) (Element elt) + | _ -> failwith "unreachable") + elts + |> List.concat + in + let open Topological_sort in + let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in + sort (module String) ~nodes:nodes ~edges:edges ~what:Topological_sort.What.Nodes + +let compile_policy (elt : xml_element) : compilation_intermediate = + let (tag_name, attrs, children) = elt in + assert (String.(tag_name = "Policy")); + let identifier = get_attr_exn "PolicyId" attrs in + let version = get_attr_exn "Version" attrs in + assert (Str.string_match version_regex version 0); + let variables = get_children "VariableDefinition" children in + let variables = + match order_variable_definitions variables with + | Ok ordering -> + List.map ordering + ~f:(fun needle -> + List.find_exn ~f:(function + | ("VariableDefinition", attrs, _) -> + String.(needle = (get_attr_exn "VariableId" attrs)) + | _ -> false) + variables) + | _ -> failwith "failed to order variable definitions" + in + let variables = + List.fold variables + ~init:[] + ~f:(fun x y -> + let (key, value) = compile_variable_definition x y in + (key,value) :: x) + 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 variables) + obligation_expressions); + List (List.map ~f:(compile_advice_expression variables) + advice_expressions);])in + let children = List.map ~f:(compile_rule variables) + (get_children "Rule" children) in + let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in + let element_identifier = element_identifier_of identifier ~version:(Some version) in + { metadata_definitions = + (List.map ~f:metadata_definitions children |> List.concat) + @ [Define + (metadata_identifier, + Application + ((Identifier "PolicyElement.Policy"), [metadata]))]; + element_definitions = + (List.map ~f:element_definitions children |> List.concat) + @ [Define + (element_identifier, + Application + ((Identifier "ElementTree.Node"), + [Identifier metadata_identifier; + List (List.map ~f:(fun x -> Identifier (root_identifier x)) children)]))]; + root_identifier = element_identifier; + edges = [] + } + +let rec match_policy_reference elements identifier = + match elements with + | `Policy (identifier', version) :: xs -> + if String.(identifier = identifier') + then Some (canonicalize_identifier ~version:(Some version) identifier) + else match_policy_reference xs identifier + | `PolicySet (_, _) :: xs -> match_policy_reference xs identifier + | [] -> None + +let rec match_policyset_reference elements identifier regexes = + match elements with + | `PolicySet (identifier', version) :: xs -> + if String.(identifier = identifier') && + List.for_all ~f:(fun regex -> Str.string_match regex version 0) regexes + then Some (canonicalize_identifier ~version:(Some version) identifier) + else match_policyset_reference xs identifier regexes + | `Policy (_, _) :: xs -> match_policyset_reference xs identifier regexes + | [] -> None + +let rec compile_policyset + policy_elements + (elt : xml_element) + : compilation_intermediate = + let (tag_name, attrs, children) = elt in + assert (String.(tag_name = "PolicySet")); + let identifier = get_attr_exn "PolicySetId" attrs in + let version = get_attr_exn "Version" attrs in + assert (Str.string_match version_regex version 0); + 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 children = + List.filter_map ~f:(function + | Element (("PolicySet", _, _) as elt) -> + Some (compile_policyset policy_elements elt) + | Element (("PolicySetIdReference", attrs, _children)) -> + let identifier = match children with + | [PCData identifier] -> identifier + | _ -> failwith "invalid PolicySetIdReference" + in + let regexes = + List.filter_map ~f:(fun x -> x) [ + get_attr "xacml:Version" attrs; + get_attr "xacml:EarliestVersion" attrs; + get_attr "xacml:LatestVersion" attrs + ] + in + List.iter ~f:(fun x -> assert (Str.string_match version_match_type_regex x 0)) + regexes ; + let regexes = List.map ~f:Str.regexp regexes in + (match match_policyset_reference policy_elements identifier regexes with + | Some identifier -> + Some { metadata_definitions = []; + element_definitions = []; + root_identifier = identifier; + edges = [] } + | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier)) + | Element (("Policy", _, _) as elt) -> Some (compile_policy elt) + | Element (("PolicyIdReference", _, _)) -> + let identifier = match children with + | [PCData identifier] -> identifier + | _ -> failwith "invalid PolicyIdReference" + in + (match match_policy_reference policy_elements identifier with + | Some identifier -> + Some { metadata_definitions = []; + element_definitions = []; + root_identifier = identifier; + edges = [] } + | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier)) + | _ -> None) + children in + let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in + let element_identifier = element_identifier_of identifier ~version:(Some version) in + { metadata_definitions = + (List.map ~f:metadata_definitions children |> List.concat) + @ [Define + (metadata_identifier, + Application + ((Identifier "PolicyElement.PolicySet"), [metadata]))]; + element_definitions = + (List.map ~f:element_definitions children |> List.concat) + @ [Define + (element_identifier, + Application + ((Identifier "ElementTree.Node"), + [Identifier metadata_identifier; + List (List.map ~f:(fun x -> Identifier (root_identifier x)) children)]))]; + root_identifier = element_identifier; + edges = [] + } + +let rec policy_element_names (root : xml_element) = + let (tag_name, attrs, children) = root in + match tag_name with + | "PolicySet" -> + let identifier = get_attr_exn "PolicySetId" attrs in + let version = get_attr_exn "Version" attrs in + [`PolicySet (identifier, version)] + @ (List.map ~f:policy_element_names (get_children "PolicySet" children) |> List.concat) + @ (List.map ~f:policy_element_names (get_children "Policy" children) |> List.concat) + | "Policy" -> + let identifier = get_attr_exn "PolicyId" attrs in + let version = get_attr_exn "Version" attrs in + [`Policy (identifier, version)] + | _ -> [] + +let order_element_definitions elts = + let nodes = + List.map + ~f:(function + | Define (identifier, _) -> identifier + | _ -> failwith "badly formed list of expressions") + elts in + let edges = + List.map + ~f:(function + | Define (parent, Application (_, [_; List children])) -> + List.map ~f:(function + | Identifier child -> (child, parent) + | _ -> failwith "badly formed list of expressions") + children + | _ -> failwith "badly formed list of expressions") + elts + |> List.concat + in + let open Topological_sort in + let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in + sort (module String) ~nodes:nodes ~edges:edges ~what:Topological_sort.What.Nodes + +let compile : Xml.xml -> lean_expression list = function + | Element ((tag_name, _attributes, _children) as elt) -> + let { metadata_definitions; element_definitions; root_identifier; _ } = + (match tag_name with + | "PolicySet" -> + let policy_elements = (policy_element_names elt) in + compile_policyset policy_elements elt + | "Policy" -> compile_policy elt + | _ -> failwith (Printf.sprintf "(%s)" tag_name)) + in + let element_definitions = + (match order_element_definitions element_definitions with + | Result.Ok ordering -> + List.map ordering + ~f:(fun needle -> + List.find_exn ~f:(function + | Define (identifier, _) -> String.(identifier = needle) + | _ -> false) + element_definitions) + | _ -> failwith "failed to order definitions") + in + metadata_definitions @ element_definitions @ [Identifier root_identifier] + | PCData s -> failwith s + +let compile' (policy : string) : string = + policy + |> Xml.parse_string + |> compile + |> List.map ~f:fmt_lean_expression + |> String.concat ~sep:"\n" diff --git a/xacml-proofs/compiler/lib/compiler.mli b/xacml-proofs/compiler/lib/compiler.mli new file mode 100644 index 0000000..09198ba --- /dev/null +++ b/xacml-proofs/compiler/lib/compiler.mli @@ -0,0 +1 @@ +val compile' : string -> string diff --git a/xacml-proofs/compiler/lib/dune b/xacml-proofs/compiler/lib/dune index 15b8510..d243c0a 100644 --- a/xacml-proofs/compiler/lib/dune +++ b/xacml-proofs/compiler/lib/dune @@ -1,2 +1,4 @@ (library - (name compiler)) + (name compiler) + (libraries base str topological_sort xml-light) + (preprocess (pps ppx_let ppx_jane))) |