Initial commit

5 files changed, 305 insertions, 0 deletions

diff --git a/xacml-proofs/.gitignore b/xacml-proofs/.gitignore
new file mode 100644
index 0000000..4aab16c
--- /dev/null
+++ b/xacml-proofs/.gitignore
@@ -0,0 +1 @@
+xacml-3.0-from-2.0-ct/
diff --git a/xacml-proofs/compiler/main.scm b/xacml-proofs/compiler/main.scm
new file mode 100644
index 0000000..60cf76e
--- /dev/null
+++ b/xacml-proofs/compiler/main.scm
@@ -0,0 +1,83 @@
+(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/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
new file mode 100644
index 0000000..69de8c3
--- /dev/null
+++ b/xacml-proofs/lean/Xacml.lean
@@ -0,0 +1,104 @@
+-- The following elements are in the <Expression> element substitution group:
+-- <Apply>, <AttributeSelector>, <AttributeValue>, <Function>, <VariableReference> and <AttributeDesignator>.
+
+inductive CombinatorAlgorithm where
+  | deny_overrides                  : CombinatorAlgorithm
+  | ordered_deny_overrides          : CombinatorAlgorithm
+  | permit_overrides                : CombinatorAlgorithm
+  | ordered_permit_overrides        : CombinatorAlgorithm
+  | deny_unless_permit              : CombinatorAlgorithm
+  | permit_unless_deny              : CombinatorAlgorithm
+  | first_applicable                : CombinatorAlgorithm
+  | only_one_applicable             : CombinatorAlgorithm
+  | legacy_deny_overrides           : CombinatorAlgorithm
+  | legacy_ordered_deny_overrides   : CombinatorAlgorithm
+  | legacy_permit_overrides         : CombinatorAlgorithm
+  | legacy_ordered_permit_overrides : CombinatorAlgorithm
+
+inductive MatchAlgorithm where
+  | x500Name_match          : MatchAlgorithm
+  | rfc822Name_match        : MatchAlgorithm
+  | string_regexp_match     : MatchAlgorithm
+  | anyURI_regexp_match     : MatchAlgorithm
+  | ipAddress_regexp_match  : MatchAlgorithm
+  | dnsName_regexp_match    : MatchAlgorithm
+  | rfc822Name_regexp_match : MatchAlgorithm
+  | x500Name_regexp_match   : MatchAlgorithm
+  | xpath_node_count        : MatchAlgorithm
+  | xpath_node_equal        : MatchAlgorithm
+  | xpath_node_match        : MatchAlgorithm
+
+def FunctionID : Type := String
+
+structure PolicySet where
+  combinator : CombinatorAlgorithm
+  target : Target
+  children : List PolicySetChild
+  -- TODO: ObligationExpressions
+  -- TODO: AdviceExpressions
+
+inductive PolicySetChild where
+  | policy_set (inner : PolicySet) : PolicySetChild
+  | policy     (inner : Policy)    : PolicySetChild
+
+structure Policy where
+  combinator : CombinatorAlgorithm
+  target : Target
+  children : List Rule
+  -- TODO: ObligationExpressions
+  -- TODO: AdviceExpressions
+
+structure AttributeDesignator where
+  category        : String
+  identifier      : String
+  type            : String
+  issuer          : String
+  must_be_present : Bool
+
+inductive Expression where
+  | apply                (function : FunctionID) (args: List Expression) : Expression
+  | attribute_designator (inner : AttributeDesignator)                   : Expression
+  | attribute_value      (inner : String)                                : Expression
+  | function             (function : FunctionID)                         : Expression
+
+
+structure Rule where
+  target : Target
+  -- "The <Condition> contains one <Expression> element"
+  condition : Expression
+  effect : Decision
+  -- TODO: ObligationExpressions
+  -- TODO: AdviceExpressions  
+
+structure Match where
+  function : MatchAlgorithm
+  designator: AttributeDesignator
+  value: List String
+def AllOf : Type  := List Match -- TODO: Should restrict nonempty.
+def AnyOf : Type  := List AllOf -- TODO: Should restrict nonempty.
+def Target : Type := List AnyOf
+
+---
+
+structure Attribute where
+  category : String
+  identifier: String
+  issuer : String
+  value : List String
+deriving Repr
+
+def Request : Type := List Attribute
+deriving Repr
+
+---
+
+inductive Decision where
+  | permit : Decision
+  | deny : Decision
+  | indeterminate : Decision
+  | not_applicable : Decision
+deriving Repr
+
+def Response : Type := Decision
+deriving Repr
+
diff --git a/xacml-proofs/lean/Xacml.lean.bak b/xacml-proofs/lean/Xacml.lean.bak
new file mode 100644
index 0000000..bec63e6
--- /dev/null
+++ b/xacml-proofs/lean/Xacml.lean.bak
@@ -0,0 +1,27 @@
+inductive V₃ where
+  | true          : V₃
+  | false         : V₃
+  | indeterminate : V₃
+
+inductive V₆ where
+  | true_deny : V₆
+  | true_permit : V₆
+  | indeterminate_deny : V₆
+  | indeterminate_permit : V₆
+  | indeterminate : V₆
+  | false : V₆
+
+inductive Decision where
+  | permit : Decision
+  | deny   : Decision
+deriving Repr
+
+-- structure Result where
+--   decision    : Decision
+--   obligations : Option (List String)
+--   advice      : Option (List String)
+-- deriving Repr
+
+def Result (α : Type) : Type := Decision × α
+
+#check ((Decision.permit, "Hi!") : Result String)
diff --git a/xacml-proofs/modeling-choices.org b/xacml-proofs/modeling-choices.org
new file mode 100644
index 0000000..80c2968
--- /dev/null
+++ b/xacml-proofs/modeling-choices.org
@@ -0,0 +1,90 @@
+* Not Relevant
+
+- [ ] Element <Description> (no semantic meaning)
+- [ ] Element <PolicyIssuer> (XMLAdmin)
+- [ ] Element <PolicySetDefaults> (optional)
+- [ ] Element <XPathVersion> (optional)
+- [ ] Element <PolicySetIdReference> (dissolved by compiler translation)
+- [ ] Element <PolicyIdReference> (dissolved by compiler translation)
+- [ ] Simple type VersionType (dissolved by compiler translation)
+- [ ] Simple type VersionMatchType (dissolved by compiler translation)
+- [ ] Element <PolicyDefaults> (optional)
+- [ ] Element <CombinerParameters> (optional)
+- [ ] Element <CombinerParameter> (optional)
+- [ ] Element <RuleCombinerParameters> (optional)
+- [ ] Element <PolicyCombinerParameters> (optional)
+- [ ] Element <PolicySetCombinerParameters> (optional)
+- [ ] Element <AttributeSelector> (dissolved by compiler translation)
+- [ ] Element <RequestDefaults> (optional)
+- [ ] Element <PolicyIdentifierList> (optional)
+- [ ] Element <MultiRequests> (optional)
+- [ ] Element <RequestReference> (optional)
+- [ ] Element <AttributesReference> (optional)
+- [ ] Element <StatusMessage> (optional)
+- [ ] Element <StatusDetail> (optional)
+- [ ] Element <VariableDefinition> (dissolved by compiler translation)
+- [ ] Element <VariableReference> (dissolved by compiler translation)
+- [ ] Element <Content> (dissolved by compiler translation)
+  
+* Modeled
+
+- [X] Element <PolicySet>
+- [X] Element <Target>
+- [X] Element <AnyOf>
+- [X] Element <AllOf>
+- [X] Element <Match>
+- [X] Element <Policy>
+- [X] Element <Rule>
+- [ ] Simple type EffectType
+  - Same as Decision in Lean
+- [ ] Element <Expression>
+- [X] Element <Condition>
+  - Just an Expression per 5.26
+- [X] Element <Apply>
+- [X] Element <Function>
+- [ ] Element <AttributeDesignator>
+- [ ] Element <AttributeValue>
+- [X] Element <Request>
+- [X] Element <Attributes>
+  - Category subsumed by individual attributes
+- [ ] Element <Attribute>
+- [X] Element <Response>
+- [X] Element <Result>
+- [X] Element <Decision>
+- [ ] Element <Obligations>
+- [ ] Element <AssociatedAdvice>
+- [ ] Element <Obligation>
+- [ ] Element <Advice>
+- [ ] Element <AttributeAssignment>
+- [ ] Element <ObligationExpressions>
+- [ ] Element <AdviceExpressions>
+- [ ] Element <ObligationExpression>
+- [ ] Element <AdviceExpression>
+- [ ] Element <AttributeAssignmentExpression>
+- [ ] Element <Status>
+- [ ] Element <StatusCode>
+- [ ] Element <MissingAttributeDetail>
+
+* Doesn't Line Up with ACES
+
+- Does use PolicySetDefaults and XPathVersion but it's just XPath 1.0. Probably safe to ignore and have our XPath implementation follow 1.0.
+
+* Policy Schema
+
+- PolicySetId isn't explicitly encoded in the PolicySet, that's just the name we'll give to it in the embedding.
+- Not modeling MaxDelegationDepth (XACMLAdmin extension)
+- No =CombinerParameters= because no combination algorithm uses them.
+- No =PolicySetDefaults=, =PolicyDefaults= because they're optional
+
+Assume =PolicySetIdReference=, =PolicyIdReference= are turned into =PolicySet= and =Policy= respectively.
+Same assumption about PolicySelector as logic paper.
+
+* Request
+- RequestDefaults is excluded because it is specified by the standard to be optional.
+- MultiRequests is excluded because it is specified by the standard to be optional.
+- Always assume ReturnPolicyIdList is true
+
+** Attribute
+
+- Assume Attribute->Issuer has no effect on access control decision
+- TODO What about Attribute->IncludeInResult?