From 08ba0c131341ed530d48576c34ca96b6c7a3be20 Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Tue, 14 Nov 2023 20:15:23 -0500
Subject: Initial encoding of XACML semantics in Rego

---
 xacml-translation/match.rego | 604 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 604 insertions(+)
 create mode 100644 xacml-translation/match.rego

diff --git a/xacml-translation/match.rego b/xacml-translation/match.rego
new file mode 100644
index 0000000..f94c6e5
--- /dev/null
+++ b/xacml-translation/match.rego
@@ -0,0 +1,604 @@
+# Assumption:
+#
+# input.request is an array or set of
+# { category: string
+#   identifier: string
+#   issuer: string or null
+#   value: { type: string, value: string } }
+
+package equivalence
+
+import future.keywords.every
+import future.keywords.if
+import future.keywords.in
+
+########################################################################
+# Data Types
+########################################################################
+
+lift_decision_indeterminate({ "decision": "not_applicable"   }) := { "decision": "not_applicable"   }
+lift_decision_indeterminate({ "decision": "permit"           }) := { "decision": "indeterminate_p"  }
+lift_decision_indeterminate({ "decision": "deny"             }) := { "decision": "indeterminate_d"  }
+lift_decision_indeterminate({ "decision": "indeterminate"    }) := { "decision": "indeterminate_dp" }
+lift_decision_indeterminate({ "decision": "indeterminate_dp" }) := { "decision": "indeterminate_dp" }
+lift_decision_indeterminate({ "decision": "indeterminate_p"  }) := { "decision": "indeterminate_p"  }
+lift_decision_indeterminate({ "decision": "indeterminate_d"  }) := { "decision": "indeterminate_d"  }
+
+########################################################################
+# Match Functions
+########################################################################
+
+## TODO
+apply_xacml_function("a", _) := true
+apply_xacml_function("b", _) := "indeterminate"
+
+########################################################################
+# AttributeDesignator
+########################################################################
+
+designator_matches(designator, attribute) if {
+    attribute.category    == designator.category
+    attribute.identifier  == designator.identifier
+    attribute.value.type  == designator.type
+    attribute.attr.issuer == null
+}
+
+designator_matches(designator, attribute) if {
+    attribute.category    == designator.category
+    attribute.identifier  == designator.identifier
+    attribute.value.type  == designator.type
+    attribute.attr.issuer == designator.issuer
+}
+
+evaluate_designator(designator) := xs if {
+    xs := [y | y := input.request[_]; designator_matches(designator, y)]
+    count(xs) > 0
+}
+
+evaluate_designator(designator) := xs if {
+    xs := [y | y := input.request[_]; designator_matches(designator, y)]
+    count(xs) == 0
+    not designator.must_be_present
+}
+
+evaluate_designator(designator) := { "error": ["missing_attribute"] } if {
+    xs := [y | y := input.request[_]; designator_matches(designator, y)]
+    count(xs) == 0
+    designator.must_be_present
+}
+
+#########################################################################
+# Match
+########################################################################
+
+evaluate_match(match) := true if {
+    designator_result := evaluate_designator(match.designator)
+
+    # Designator evaluates without error.
+    is_array(designator_result)
+
+    some x in designator_result
+    apply_xacml_function(match.fn, x) == true
+} else := "indeterminate" if {
+    designator_result := evaluate_designator(match.designator)
+
+    # Designator evaluates without error.
+    is_array(designator_result)
+
+    some x in designator_result
+    apply_xacml_function(match.fn, x) == "indeterminate"
+} else := false
+
+evaluate_all_of(conj) := { "match_result": "is_match" } if {
+    every x in conj {
+        evaluate_match(x) == true
+    }
+} else := { "match_result": "indeterminate" } if {
+    some x in conj
+    evaluate_match(x) == "indeterminate"
+} else := { "match_result": "no_match" }
+
+evaluate_any_of([]) := { "match_result": "is_match" }
+evaluate_any_of(disj) := { "match_result": "is_match" } if {
+    some x in disj
+    evaluate_all_of(x) == { "match_result": "is_match" }
+} else := { "match_result": "indeterminate" } if {
+    some x in disj
+    evaluate_all_of(x) == { "match_result": "is_match" }
+} else := { "match_result": "no_match" }
+
+
+########################################################################
+# Target
+########################################################################
+
+evaluate_target([]) := { "match_result": "is_match" }
+evaluate_target(xs) := { "match_result": "is_match" } if {
+    every disj in xs {
+        evaluate_any_of(disj) == { "match_result": "is_match" }
+    }
+} else := { "match_result": "no_match" } if {
+    some disj in xs
+    evaluate_any_of(disj) == { "match_result": "no_match" }
+} else := { "match_result": "indeterminate" }
+
+########################################################################
+# Expression
+########################################################################
+
+evaluate_expression({ "kind": "apply", "function": function_name, "args": args }) := x if {
+    x := apply_xacml_function(function_name, args)
+}
+evaluate_expression({ "kind": "attribute_designator", "inner": designator }) := x if {
+    x := evaluate_designator(designator)
+}
+evaluate_expression({ "kind": "attribute_value", "inner": value }) := x if {
+    x := value
+}
+evaluate_function({ "kind": "function", "function": name }) := x if {
+    x := name
+}
+
+########################################################################
+# Rule
+########################################################################
+
+# Condition is specified and applicable
+evaluate_rule_decision(rule) := { "decision": decision } {
+    evaluate_target(rule.target) == { "match_result": "is_match" }
+
+    is_object(rule.condition)
+    evaluate_expression(rule.condition) == true
+
+    decision := rule.effect
+}
+# Condition is specified and not applicable
+evaluate_rule_decision(rule) := { "decision": "not_applicable" } {
+    evaluate_target(rule.target) == { "match_result": "is_match" }
+    evaluate_expression(rule.condition) == false
+}
+# Condition is indeterminate
+evaluate_rule_decision(rule) := { "decision": "indeterminate_p" } {
+    evaluate_target(rule.target) == { "match_result": "is_match" }
+    condition := evaluate_expression(rule.condition)
+    is_null(condition)
+    rule.effect == "permit"
+}
+evaluate_rule_decision(rule) := { "decision": "indeterminate_d" } {
+    evaluate_target(rule.target) == { "match_result": "is_match" }
+    condition := evaluate_expression(rule.condition)
+    is_null(condition)
+    rule.effect == "deny"
+}
+# Condition is unspecified
+evaluate_rule_decision(rule) := { "decision": decision } {
+    evaluate_target(rule.target) == { "match_result": "is_match" }
+    decision := rule.effect
+}
+
+evaluate_rule_decision(rule) := { "decision": "not_applicable" } {
+    evaluate_target(rule.target) == { "match_result": "no_match" }
+}
+evaluate_rule_decision(rule) := { "decision": "indeterminate_p" } {
+    evaluate_target(rule.target) == { "match_result": "indeterminate" }
+    rule.effect == "permit"
+}
+evaluate_rule_decision(rule) := { "decision": "indeterminate_d" } {
+    evaluate_target(rule.target) == { "match_result": "indeterminate" }
+    rule.effect == "permit"
+}
+
+evaluate_rule_advices(rule) := { "advice": advice } if {
+    decision := evaluate_rule_decision(rule)
+    advice := [expr | expr := rule.advice[_]; expr.applies_to == decision ]
+}
+
+evaluate_rule_obligations(rule) := { "obligations": obligations } if {
+    decision := evaluate_rule_decision(rule)
+    obligations := [expr | expr := rule.obligations[_]; expr.fulfill_on == decision ]
+}
+
+########################################################################
+# Policy
+########################################################################
+
+evaluate_rule_combinator("deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "not_applicable" }
+
+# evaluate_rule_combinator("ordered_deny_overrides", results) := result if {
+#     result := evaluate_rule_combinator("deny_overrides", results)
+# }
+
+evaluate_rule_combinator("ordered_deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "not_applicable" }
+
+evaluate_rule_combinator("permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+evaluate_rule_combinator("ordered_permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+# evaluate_rule_combinator("ordered_permit_overrides", results) := result if {
+#     result := evaluate_rule_combinator("permit_overrides", results)
+# }
+
+evaluate_rule_combinator("deny_unless_permit", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "deny" }
+
+evaluate_rule_combinator("permit_unless_deny", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "permit" }
+
+evaluate_rule_combinator("first_applicable", results) := result if {
+    indices := [i | results[i].decision != "not_applicable"]
+    count(indices) > 0
+    result := results[max(indices)]
+    result.decision == "deny"
+} else := { "decision": "not_applicable" }
+
+evaluate_rule_combinator("legacy_deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "not_applicable" }
+
+evaluate_rule_combinator("ordered_legacy_deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "not_applicable" }
+
+# evaluate_rule_combinator("ordered_legacy_deny_overrides", results) := result if {
+#     result := evaluate_rule_combinator("legacy_deny_overrides", results)
+# }
+
+evaluate_rule_combinator("legacy_permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+evaluate_rule_combinator("ordered_legacy_permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+
+# evaluate_rule_combinator("ordered_legacy_permit_overrides", results) := result if {
+#     result := evaluate_rule_combinator("legacy_permit_overrides", results)
+# }
+
+evaluate_policy_decision(policy) := decision if {
+    evaluate_target(policy.target) == { "match_result": "is_match" }
+    child_results := [result | rule := policy.rules[_]; result := evaluate_rule_decision(rule)]
+    decision := evaluate_rule_combinator(policy.combinator, child_results)
+} else := decision if {
+    evaluate_target(policy.target) == { "match_result": "indeterminate" }
+    child_results := [result | rule := policy.rules[_]; result := evaluate_rule_decision(rule)]
+    decision := lift_decision_indeterminate(evaluate_rule_combinator(policy.combinator, child_results))
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_advices(policy) := { "advice" : advice } if {
+    decision := evaluate_policy_decision(policy)
+    policy_advice := [expr | expr := policy.advice[_]; expr.applies_to == decision ]
+    children_advice := [advice | rule := policy.rules[_]; expr := evaluate_rule_advices(rule); advice := expr[_]]
+    advice := array.concat(policy_advice, children_advice)
+}
+
+evaluate_policy_obligations(policy) := { "obligations" : obligations } if {
+    decision := evaluate_policy_decision(policy)
+    policy_obligations := [expr | expr := policy.obligations[_]; expr.applies_to == decision ]
+    children_obligations := [obligation | rule := policy.rules[_]; expr := evaluate_rule_obligations(rule); obligation := expr[_]]
+    obligations := array.concat(policy_obligations, children_obligations)
+}
+
+########################################################################
+# PolicySet
+########################################################################
+
+evaluate_policy_combinator("deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "not_applicable" }
+
+# evaluate_policy_combinator("ordered_deny_overrides", results) := result if {
+#     result := evaluate_policy_combinator("deny_overrides", results)
+# }
+
+evaluate_policy_combinator("ordered_deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_combinator("permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_combinator("ordered_permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate_dp" } if {
+    some result in results
+    result.decision == "indeterminate_dp"
+} else := { "decision": "indeterminate_dp" } if {
+    some result1 in results
+    some result2 in results
+    result1.decision == "indeterminate_d"
+    result1.decision == "indeterminate_p"
+} else := { "decision": "indeterminate_p" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate_d" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+# evaluate_policy_combinator("ordered_permit_overrides", results) := result if {
+#     result := evaluate_policy_combinator("permit_overrides", results)
+# }
+
+evaluate_policy_combinator("deny_unless_permit", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "deny" }
+
+evaluate_policy_combinator("permit_unless_deny", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "permit" }
+
+evaluate_policy_combinator("first_applicable", results) := result if {
+    indices := [i | results[i].decision != "not_applicable"]
+    count(indices) > 0
+    result := results[max(indices)]
+    result.decision == "deny"
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_combinator("only_one_applicable", results) := result if {
+    applicable := [result | result := results[i]; result.decision != "not_applicable"]
+    count(applicable) == 1
+    result := applicable[0]
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_combinator("legacy_deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "indeterminate"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_combinator("ordered_legacy_deny_overrides", results) := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "indeterminate"
+} else := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "not_applicable" }
+
+# evaluate_policy_combinator("ordered_legacy_deny_overrides", results) := result if {
+#     result := evaluate_policy_combinator("legacy_deny_overrides", results)
+# }
+
+evaluate_policy_combinator("legacy_permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate"
+} else := { "decision": "not_applicable" }
+
+evaluate_policy_combinator("ordered_legacy_permit_overrides", results) := { "decision": "permit" } if {
+    some result in results
+    result.decision == "permit"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_p"
+} else := { "decision": "deny" } if {
+    some result in results
+    result.decision == "deny"
+} else := { "decision": "indeterminate" } if {
+    some result in results
+    result.decision == "indeterminate_d"
+} else := { "decision": "not_applicable" }
+
+
+# evaluate_policy_combinator("ordered_legacy_permit_overrides", results) := result if {
+#     result := evaluate_policy_combinator("legacy_permit_overrides", results)
+# }
+
+evaluate_policyset_decision(policyset, child_results) := decision if {
+    evaluate_target(policyset.target) == { "match_result": "is_match" }
+    decision := evaluate_policy_combinator(policyset.combinator, child_results)
+} else := decision if {
+    evaluate_target(policyset.target) == { "match_result": "indeterminate" }
+    decision := lift_decision_indeterminate(evaluate_policy_combinator(policyset.combinator, child_results))
+} else := { "decision": "not_applicable" }
+
+evaluate_policyset_advices(policyset, child_results, child_advice) := { "advice" : advice } if {
+    decision := evaluate_policyset_decision(policyset, child_results)
+    policyset_advice := [expr | expr := policyset.advice[_]; expr.applies_to == decision ]
+    advice := array.concat(policyset_advice, child_advice)
+}
+
+evaluate_policyset_obligations(policyset, child_results, child_obligations) := { "obligations" : obligations } if {
+    decision := evaluate_policyset_decision(policyset, child_results)
+    policyset_obligations := [expr | expr := policyset.obligations[_]; expr.applies_to == decision ]
+    obligations := array.concat(policyset_obligations, child_obligations)
+}
-- 
cgit v1.3