Initial commit for Xacml translator

9 files changed, 206 insertions, 83 deletions

diff --git a/xacml-proofs/compiler/.gitignore b/xacml-proofs/compiler/.gitignore
new file mode 100644
index 0000000..69fa449
--- /dev/null
+++ b/xacml-proofs/compiler/.gitignore
@@ -0,0 +1 @@
+_build/
diff --git a/xacml-proofs/compiler/bin/dune b/xacml-proofs/compiler/bin/dune
new file mode 100644
index 0000000..c8c6569
--- /dev/null
+++ b/xacml-proofs/compiler/bin/dune
@@ -0,0 +1,5 @@
+(executable
+ (public_name compiler)
+ (name main)
+ (libraries base compiler xml-light)
+ (preprocess (pps ppx_let)))
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
new file mode 100644
index 0000000..382b99f
--- /dev/null
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -0,0 +1,139 @@
+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 lean_expression = Identifier of string
+                     | String of string
+                     | Number of int
+                     | List of lean_expression list
+                     | Tuple of lean_expression list
+                     | Application of lean_expression * lean_expression list
+
+let rec fmt_lean_expression : lean_expression -> string = function
+  | Identifier s -> s
+  | 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))
+
+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 rec get_children (kind : string) : Xml.xml list -> Xml.xml option = function
+  | (Element (tag_name, _, _) as x) :: xs ->
+     if String.equal tag_name kind
+     then Some x
+     else get_children kind xs
+  | PCData s :: xs -> get_children kind xs
+  | _ -> None
+
+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.ordered_deny_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_match (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
+  failwith "unimplemented"
+
+let compile_all_of (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
+  failwith "unimplemented"
+
+let compile_any_of (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
+  failwith "unimplemented"
+
+let compile_target (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
+  Some (List [])
+  (* failwith "unimplemented" *)
+
+let call_with (elt : Xml.xml) (f : (string * string) list -> Xml.xml list -> lean_expression option) : lean_expression option =
+  match elt with
+  | Element (tag_name, attributes, children) -> f attributes children
+  | _ -> failwith "elt is not an Element"
+
+let compile_policy (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
+  let open Option.Let_syntax in
+  let%bind alg_id = get_attr "RuleCombiningAlgId" attrs in
+  let%bind target = get_children "Target" children in
+  let%bind target = call_with target compile_target in
+  Some (Application
+     ((Identifier "Policy.mk"),
+      [(compile_rule_combinator_algorithm alg_id);
+       target]))
+
+let compile : Xml.xml -> lean_expression option = function
+  | Element (tag_name, attributes, children) ->
+     (match tag_name with
+      | "Policy" -> compile_policy attributes children
+      | _ -> failwith (Printf.sprintf "(%s)" tag_name))
+  | PCData s -> failwith s
+
+let () =
+  match compile @@ Xml.parse_string policy with
+  | Some ast ->
+     ast
+     |> fmt_lean_expression
+     |> Caml.print_endline
+  | _ -> failwith "compilation failed!"
diff --git a/xacml-proofs/compiler/compiler.opam b/xacml-proofs/compiler/compiler.opam
new file mode 100644
index 0000000..1cd1d95
--- /dev/null
+++ b/xacml-proofs/compiler/compiler.opam
@@ -0,0 +1,31 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "A short synopsis"
+description: "A longer description"
+maintainer: ["Maintainer Name"]
+authors: ["Author Name"]
+license: "LICENSE"
+tags: ["topics" "to describe" "your" "project"]
+homepage: "https://github.com/username/reponame"
+doc: "https://url/to/documentation"
+bug-reports: "https://github.com/username/reponame/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.10"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/username/reponame.git"
diff --git a/xacml-proofs/compiler/dune-project b/xacml-proofs/compiler/dune-project
new file mode 100644
index 0000000..af8c3ab
--- /dev/null
+++ b/xacml-proofs/compiler/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.10)
+
+(name compiler)
+
+(generate_opam_files true)
+
+(source
+ (github username/reponame))
+
+(authors "Author Name")
+
+(maintainers "Maintainer Name")
+
+(license LICENSE)
+
+(documentation https://url/to/documentation)
+
+(package
+ (name compiler)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (depends ocaml dune)
+ (tags
+  (topics "to describe" your project)))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project
diff --git a/xacml-proofs/compiler/lib/dune b/xacml-proofs/compiler/lib/dune
new file mode 100644
index 0000000..15b8510
--- /dev/null
+++ b/xacml-proofs/compiler/lib/dune
@@ -0,0 +1,2 @@
+(library
+ (name compiler))
diff --git a/xacml-proofs/compiler/main.scm b/xacml-proofs/compiler/main.scm
deleted file mode 100644
index 60cf76e..0000000
--- a/xacml-proofs/compiler/main.scm
+++ /dev/null
@@ -1,83 +0,0 @@
-(use-modules (ice-9 pretty-print)
-             (sxml simple))
-
-(define 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=\"identifier: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>")
-
-
-(pretty-print (cddr (xml->sxml policy
-                              #:trim-whitespace? #t
-                              #:namespaces '((xacml . "urn:oasis:names:tc:xacml:3.0:core:schema:wd-17")))))
-
-(define (xml-element? x)
-  (and (list x) (positive? (length x)) (symbol? (car x))))
-
-(define (element-kind element)
-  (if (xml-element? element)
-      (car element)
-      #f))
-
-(define (element-attributes element)
-  (if (xml-element? element)
-      (cdadr element)
-      #f))
-
-(define (element-attribute element key)
-  (car (assoc-ref (element-attributes element) key)))
-
-(define (assert prop) #t)
-
-(define (policy->ast element)
-  (assert (eqv? (element-kind element) 'xacml:Policy))
-  `(policy ,(element-attribute element 'PolicyId)
-           ,(element-attribute element 'RuleCombiningAlgId)
-           ,(map rule->ast (filter-element-children element 'xacml:Rule))))
-
-(define (rule->ast element)
-  `(Rule))
-
-(define (filter-element-children element tag)
-  (filter (lambda (child)
-            (eqv? tag (element-kind child)))
-          (cddr element)))
-
-(policy->ast (caddr (xml->sxml policy
-                               #:trim-whitespace? #t
-                               #:namespaces '((xacml . "urn:oasis:names:tc:xacml:3.0:core:schema:wd-17")))))
diff --git a/xacml-proofs/compiler/test/compiler.ml b/xacml-proofs/compiler/test/compiler.ml
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/xacml-proofs/compiler/test/compiler.ml
diff --git a/xacml-proofs/compiler/test/dune b/xacml-proofs/compiler/test/dune
new file mode 100644
index 0000000..da01376
--- /dev/null
+++ b/xacml-proofs/compiler/test/dune
@@ -0,0 +1,2 @@
+(test
+ (name compiler))