Implement PolicySetIdReference, PolicyIdReference

1 files changed, 116 insertions, 31 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 5df7864..36ca738 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -1,6 +1,7 @@
 open Base
 
 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
@@ -346,10 +347,16 @@ let canonicalize_identifier ?(version = None) (ident : string) : string =
   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"
+
 let compile_rule
       (env : (string * lean_expression) list)
       (elt : xml_element)
-    : (lean_expression list) * lean_expression =
+    : (lean_expression list) * string =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "RuleId" attrs in
@@ -376,13 +383,18 @@ let compile_rule
                 obligation_expressions);
         List (List.map ~f:(compile_advice_expression env)
                 advice_expressions);]) in
-  let identifier = canonicalize_identifier identifier in
+  let metadata_identifier = metadata_identifier_of identifier in
+  let element_identifier = element_identifier_of identifier in
   ([Define
-      (identifier,
+      (metadata_identifier,
        Application
-         ((Identifier "PolicyElement.Rule"), [metadata]))],
-   Application
-     ((Identifier "ElementTree.Node"), [Identifier identifier; List []]))
+         ((Identifier "PolicyElement.Rule"), [metadata]));
+    Define
+      (element_identifier,
+       Application
+         ((Identifier "ElementTree.Node"),
+          [Identifier metadata_identifier; List []]))],
+   element_identifier)
 
 let compile_variable_definition
       (env : (string * lean_expression) list)
@@ -394,7 +406,7 @@ let compile_variable_definition
   let value = get_child_exn "Expression" children in
   (identifier, compile_expression env value)
 
-let compile_policy (elt : xml_element) : (lean_expression list) * lean_expression =
+let compile_policy (elt : xml_element) : (lean_expression list) * string =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Policy");
   let identifier = get_attr_exn "PolicyId" attrs in
@@ -420,20 +432,46 @@ let compile_policy (elt : xml_element) : (lean_expression list) * lean_expressio
                 obligation_expressions);
         List (List.map ~f:(compile_advice_expression variables)
                 advice_expressions);])in
-  let identifier = canonicalize_identifier identifier ~version:(Some version) in
   let children = List.map ~f:(compile_rule variables)
                    (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 metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in
+  let element_identifier = element_identifier_of identifier ~version:(Some version) in
+  ((List.map ~f:fst children |> List.concat)
+   @ [Define
+        (metadata_identifier,
+         Application
+           ((Identifier "PolicyElement.Policy"), [metadata]));
+      Define
+        (element_identifier,
+         Application
+           ((Identifier "ElementTree.Node"),
+            [Identifier metadata_identifier;
+             List (List.map ~f:(fun x -> Identifier (snd x)) children)]))],
+   element_identifier)
+
+let rec match_policy_reference elements identifier =
+  match elements with
+  | `Policy (identifier', version) :: xs ->
+     if String.equal 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.equal 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 (elt : xml_element) : (lean_expression list) * lean_expression =
+let rec compile_policyset
+          policy_elements
+          (elt : xml_element)
+        : (lean_expression list) * string =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "PolicySetId" attrs in
@@ -450,30 +488,77 @@ let rec compile_policyset (elt : xml_element) : (lean_expression list) * lean_ex
         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 (("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)) ;
+                        let regexes = List.map ~f:Str.regexp regexes in
+                        (match match_policyset_reference policy_elements identifier regexes with
+                         | Some identifier -> Some ([], identifier)
+                         | _ -> 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 ([], identifier)
+                         | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier))
                      | _ -> None)
                    children in
-  ([Define
-      (identifier,
+  let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in
+  let element_identifier = element_identifier_of identifier ~version:(Some version) in
+  ((List.map ~f:fst children |> List.concat)
+   @ [Define
+      (metadata_identifier,
+       Application
+         ((Identifier "PolicyElement.PolicySet"), [metadata]));
+    Define
+      (element_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)]))
+         ((Identifier "ElementTree.Node"),
+          [Identifier metadata_identifier;
+           List (List.map ~f:(fun x -> Identifier (snd x)) children)]))],
+   element_identifier)
+
+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 compile : Xml.xml -> lean_expression list = function
   | Element ((tag_name, attributes, children) as elt) ->
-     let (defns, tree) =
+     let (defns, tree_root_identifier) =
        (match tag_name with
-        | "PolicySet" -> compile_policyset elt
+        | "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 defns @ [tree]
+     in defns @ [Identifier tree_root_identifier]
   | PCData s -> failwith s
 
 let () = policy