This file contains the top-level interface to optimized SymCC.
Returns none iff p does not error on any well-formed input in the εnv it
was compiled for.
Otherwise returns an input some env on which p errors.
Equations
Instances For
Returns none iff p matches all well-formed inputs in εnv. That is,
if p is a permit policy, it allows all inputs in εnv, or if p is a
forbid policy, it denies all inputs in εnv.
Otherwise returns an input some env that is not-matched by p.
Compare with alwaysAllowsOpt?, which takes a policyset (which could consist of a
single policy, or more) and determines whether it allows all well-formed
inputs in an εnv. This function differs from alwaysAllowsOpt on a singleton
policyset in how it treats forbid policies -- while alwaysAllowsOpt trivially
doesn't hold for any policyset containing only forbid policies,
alwaysMatchesOpt does hold if the forbid policy explicitly denies all inputs in
the εnv.
Equations
Instances For
Returns none iff p matches no well-formed inputs in εnv.
Otherwise returns an input some env that is matched by p.
Compare with alwaysDeniesOpt, which takes a policyset (which could consist of a
single policy, or more) and determines whether it denies all well-formed
inputs in an εnv. This function differs from alwaysDeniesOpt on a singleton
policyset in how it treats forbid policies -- while alwaysDeniesOpt trivially
holds for any policyset containing only forbid policies, neverMatchesOpt only
holds if the forbid policy explicitly denies no inputs in the εnv.
Equations
Instances For
Returns none iff p₁ and p₂ match exactly the same set of well-formed
inputs in the εnv they were compiled for.
(Caller guarantees that p₁ and p₂ were compiled for the same εnv.)
Otherwise returns an input some env on which p₁ and p₂
have different matching behavior (one matches and the other does not).
Compare with equivalentOpt?, which takes two policysets (which could consist of a
single policy, or more) and determines whether the authorization behavior of
those policysets is equivalent for well-formed inputs in εnv. This function
differs from equivalentOpt? on singleton policysets in how it treats forbid
policies -- while equivalentOpt? trivially holds for any pair of forbid policies
(as they both always-deny), matchesEquivalentOpt? only holds if the two policies
match exactly the same set of inputs. Also, a nontrivial permit and nontrivial
forbid policy can be matchesEquivalentOpt?, but can never be equivalentOpt?.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Returns none iff p₁ matching implies that p₂ matches, for every
well-formed input in the εnv they were compiled for.
(Caller guarantees that p₁ and p₂ were compiled for the same εnv.)
That is, for every request where p₁ matches, p₂ also matches.
Otherwise returns an input some env that is matched by p₁ but
not-matched by p₂.
Compare with impliesOpt?, which takes two policysets (which could consist of a
single policy, or more) and determines whether the authorization decision of
the first implies that of the second. This function differs from impliesOpt? on
singleton policysets in how it treats forbid policies -- while for impliesOpt?,
any forbid policy trivially implies any permit policy (as always-deny always
implies any policy), for matchesImpliesOpt?, a forbid policy may or may not
imply a permit policy, and a permit policy may or may not imply a forbid
policy.
Equations
Instances For
Returns none iff there is no well-formed input in the εnv they were compiled
for that is matched by both p₁ and p₂.
(Caller guarantees that p₁ and p₂ were compiled for the same εnv.)
Otherwise returns an input some env that is matched by both p₁ and p₂.
This checks that the sets of inputs matched by p₁ and p₂ are disjoint.
Compare with disjointOpt?, which takes two policysets (which could consist of a
single policy, or more) and determines whether the authorization behavior of
those policysets are disjoint. This function differs from disjointOpt? on
singleton policysets in how it treats forbid policies -- while for
disjointOpt?, any forbid policy is trivially disjoint from any other policy (as
it allows nothing), matchesDisjointOpt? considers whether the forbid policy may
match (rather than allow) any input that is matched by the other policy.
Equations
Instances For
Returns none iff the authorization decision of ps₁ implies that of ps₂ for
every well-formed input in the εnv that the policysets were compiled for.
(Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)
That is, every input allowed by ps₁ is allowed by ps₂; ps₂ is either more
permissive than, or equivalent to, ps₁.
Otherwise returns an input some env that is allowed by ps₁ but denied by ps₂.
Equations
Instances For
Returns none iff ps allows all well-formed inputs in the εnv it was
compiled for.
Otherwise returns an input some env that is denied by ps.
Equations
Instances For
Returns none iff ps denies all well-formed inputs in the εnv it was
compiled for.
Otherwise returns an input some env that is allowed by ps.
Equations
Instances For
Returns none iff ps₁ and ps₂ produce the same authorization decision on
all well-formed inputs in the εnv that the policysets were compiled for.
(Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)
Otherwise returns an input some env on which ps₁ and ps₂ produce different
authorization decisions.
Equations
Instances For
Returns none iff there is no well-formed input in εnv that the policysets were
compiled for, that is allowed by both ps₁ and ps₂.
(Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)
Otherwise returns an input some env that is allowed by both ps₁ and ps₂.
This checks that the authorization semantics of ps₁ and ps₂ are disjoint.
Equations
Instances For
Returns true iff p does not error on any well-formed input in the εnv it was
compiled for.
Equations
Instances For
Returns none iff p matches all well-formed inputs in εnv. That is,
if p is a permit policy, it allows all inputs in εnv, or if p is a
forbid policy, it denies all inputs in εnv.
Otherwise returns an input some env that is not-matched by p.
Compare with checkAlwaysAllowsOpt, which takes a policyset (which could
consist of a single policy, or more) and determines whether it allows all
well-formed inputs in an εnv. This function differs from
checkAlwaysAllowsOpt on a singleton policyset in how it treats forbid
policies -- while checkAlwaysAllowsOpt trivially doesn't hold for any
policyset containing only forbid policies, checkAlwaysMatchesOpt does hold
if the forbid policy explicitly denies all inputs in the εnv.
Equations
Instances For
Returns none iff p matches no well-formed inputs in εnv.
Otherwise returns an input some env that is matched by p.
Compare with checkAlwaysDeniesOpt, which takes a policyset (which could
consist of a single policy, or more) and determines whether it denies all
well-formed inputs in an εnv. This function differs from
checkAlwaysDeniesOpt on a singleton policyset in how it treats forbid
policies -- while checkAlwaysDeniesOpt trivially holds for any policyset
containing only forbid policies, checkNeverMatchesOpt only holds if the
forbid policy explicitly denies no inputs in the εnv.
Equations
Instances For
Returns true iff p₁ and p₂ match exactly the same set of well-formed
inputs in the εnv they were compiled for.
(Caller guarantees that p₁ and p₂ were compiled for the same εnv.)
Compare with checkEquivalentOpt, which takes two policysets (which could consist of a
single policy, or more) and determines whether the authorization behavior of
those policysets is equivalent for well-formed inputs in εnv. This function
differs from checkEquivalentOpt on singleton policysets in how it treats forbid
policies -- while checkEquivalentOpt trivially holds for any pair of forbid policies
(as they both always-deny), checkMatchesEquivalentOpt only holds if the two policies
match exactly the same set of inputs. Also, a nontrivial permit and nontrivial
forbid policy can be checkMatchesEquivalentOpt, but can never be checkEquivalentOpt.
Equations
Instances For
Returns true iff p₁ matching implies that p₂ matches, for every
well-formed input in the εnv they were compiled for.
(Caller guarantees that p₁ and p₂ were compiled for the same εnv.)
That is, for every request where p₁ matches, p₂ also matches.
Compare with checkImpliesOpt, which takes two policysets (which could consist of
a single policy, or more) and determines whether the authorization decision of
the first implies that of the second. This function differs from checkImpliesOpt
on singleton policysets in how it treats forbid policies -- while for
checkImpliesOpt, any forbid policy trivially implies any permit policy (as
always-deny always implies any policy), for checkMatchesImpliesOpt, a forbid
policy may or may not imply a permit policy, and a permit policy may or may
not imply a forbid policy.
Equations
Instances For
Returns true iff there is no well-formed input in the εnv they were compiled
for that is matched by both p₁ and p₂.
(Caller guarantees that p₁ and p₂ were compiled for the same εnv.)
This checks that the sets of inputs matched by p₁ and p₂ are disjoint.
Compare with checkDisjointOpt, which takes two policysets (which could consist of
a single policy, or more) and determines whether the authorization behavior of
those policysets are disjoint. This function differs from checkDisjointOpt on
singleton policysets in how it treats forbid policies -- while for
checkDisjointOpt, any forbid policy is trivially disjoint from any other policy
(as it allows nothing), checkMatchesDisjointOpt considers whether the forbid
policy may match (rather than allow) any input that is matched by the other
policy.
Equations
Instances For
Returns true iff the authorization decision of ps₁ implies that of ps₂ for
every well-formed input in εnv that the policysets were compiled for.
(Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)
That is, every input allowed by ps₁ is allowed by ps₂; ps₂ is either more
permissive than, or equivalent to, ps₁.
Equations
- Cedar.SymCC.checkImpliesOpt ps₁ ps₂ = Cedar.SymCC.checkUnsatAsserts (Cedar.SymCC.verifyImpliesOpt ps₁ ps₂) ps₁.εnv
Instances For
Returns true iff ps allows all well-formed inputs in the εnv it was compiled
for.
Equations
Instances For
Returns true iff ps denies all well-formed inputs in the εnv it was compiled
for.
Equations
Instances For
Returns true iff ps₁ and ps₂ produce the same authorization decision on all
well-formed inputs in the εnv that the policysets were compiled for.
Equations
- Cedar.SymCC.checkEquivalentOpt ps₁ ps₂ = Cedar.SymCC.checkUnsatAsserts (Cedar.SymCC.verifyEquivalentOpt ps₁ ps₂) ps₁.εnv
Instances For
Returns true iff there is no well-formed input in εnv that is allowed by both
ps₁ and ps₂.
(Caller guarantees that ps₁ and ps₂ were compiled for the same εnv.)
This checks that the authorization semantics of ps₁ and ps₂ are disjoint. If
this query is satisfiable, then there is at least one well-formed input that is
allowed by both ps₁ and ps₂.
Equations
- Cedar.SymCC.checkDisjointOpt ps₁ ps₂ = Cedar.SymCC.checkUnsatAsserts (Cedar.SymCC.verifyDisjointOpt ps₁ ps₂) ps₁.εnv