A
policy is a sequence of
rules. A
given
subject,
object,
and
action
are matched against each of the rules of the policy in order
to determine whether the given action should be permitted or denied.
Evaluation of a policy is expressed as a total function from a policy
to an
access
value.
Evaluating a rule may cause evaluation of subsequent rules to be cancelled.
Evaluating a rule has two possible outcomes; the rule
matches and
returns a
halt
and
access value,
or the rule fails to match. This is described by the following inductive type:
The evaluateRule function describes how
a single rule is evaluated:
The evaluateRulesInF function describes how
a list of rules is recursively evaluated:
Informally, the body of the evaluateRulesInF
maintains a notion of the current access value. If no rule has been evaluated
yet, the current access value is a value set by the caller. In this specification,
the only caller is the evaluateRules function,
which assumes a starting value of AccessDenied.
The function checks if the current rule matches. If the current rule does match,
the function effectively sets the current access value to that returned by
the rule. If the current rule specifies that evaluation should halt, the
current access value is returned immediately. If the current rule specifies
that evaluation should continue, the rest of the rules are evaluated with
the newly set access value. Otherwise, if the rule does not match, the rest
of the rules are evaluated with the current access value left unchanged.
Subsequently, the evaluateRules and
evaluatePolicy functions describe how
an entire policy is evaluated.
In order to succinctly describe various properties of policy evaluation, numerous
shorthand propositions are used. These propositions do not actually define any new
information; they are simply used to make the various theorems and proofs shorter
to read.
The proposition ruleAllows r states that
r has a conclusion that would result in
an action being permitted.
The proposition ruleDenies r states that
r has a conclusion that would result in
an action being denied.
The proposition ruleHaltsOnMatch r states that
r has a conclusion that would result in
evaluation being halted if the rule was to match.
The proposition ruleDoesNotHaltOnMatch r states that
r has a conclusion that would result in
evaluation being continued if the rule was to match.
The proposition ruleDoesNotMatch ... r states that
r does not match against the given inputs.
The proposition ruleMatchesWithConclusion ... r c states that
r matches against the given inputs and has the
conclusion c.
If no rules in a policy match, the default is to deny access.
If a policy consists of a possibly-empty sequence of rules r_pre that do not
halt on matching, followed by a rule r that does match, followed by a
possibly-empty sequence of rules r_post that do not match, then
evaluation is equivalent to evaluating r on its own.
If a policy consists of a possibly-empty sequence of rules r_pre,
followed by a possibly-empty sequence of rules r_post that do not match, then
evaluation is equivalent to evaluating r_pre.
If a policy consists of a possibly-empty sequence of rules r_pre that do not
match, followed by a possibly-empty sequence of rules r_post, then
evaluation is equivalent to evaluating r_post.