diff options
Diffstat (limited to 'xacml-proofs/modeling-choices.org')
| -rw-r--r-- | xacml-proofs/modeling-choices.org | 118 |
1 files changed, 0 insertions, 118 deletions
diff --git a/xacml-proofs/modeling-choices.org b/xacml-proofs/modeling-choices.org deleted file mode 100644 index 8d88c61..0000000 --- a/xacml-proofs/modeling-choices.org +++ /dev/null @@ -1,118 +0,0 @@ -XACML makes use of URIs and strings as identifiers. When such identifiers are compared for equality, the comparison MUST be done so that the identifiers are equal if they have the same length and the characters in the two identifiers are equal codepoint by codepoint. - -(This is equivalent to string equality in Lean.) - -* Modeling Exceptions - -7.19 Exception handling specifies that an indeterminate decision is returned and a statuscode is set. - StatusCode is, however, optional. - -* In Scope vs Out of Scope - -"We would like to be as complete as possible, so as to ensure that this can be leveraged to prove a refinement of a policy down to the status codes, obligations, and advice it returns." - -** 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? - -* 7.3.3 Multivalued attributes - -If a single <Attribute> element in a request context contains multiple <AttributeValue> child elements, then the bag of values resulting from evaluation of the <Attribute> element MUST be identical to the bag of values that results from evaluating a context in which each <AttributeValue> element appears in a separate <Attribute> element, each carrying identical meta-data. - -This is handled by the compiler. - -* Variable Substitution - -Functions SHALL NOT have side effects, as evaluation order cannot be guaranteed in a standard way. - -* Compiler Versus Embedding Decisions - -Example: =<AllOf>= and =<AnyOf>= are specified to be nonempty. -We could encode this in Lean's type system but it's more convenient to assume that an empty =AllOf= or =AnyOf= will never be constructed by the trusted compiler base. |