aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--xacml-proofs/compiler/.gitignore1
-rw-r--r--xacml-proofs/compiler/bin/dune5
-rw-r--r--xacml-proofs/compiler/bin/main.ml139
-rw-r--r--xacml-proofs/compiler/compiler.opam31
-rw-r--r--xacml-proofs/compiler/dune-project26
-rw-r--r--xacml-proofs/compiler/lib/dune2
-rw-r--r--xacml-proofs/compiler/main.scm83
-rw-r--r--xacml-proofs/compiler/test/compiler.ml0
-rw-r--r--xacml-proofs/compiler/test/dune2
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))

© 2015 - 2026 Jakob L. Kreuze