Ability to add safely add custom assertions to Cedar Analysis

[luxas]

Category

User level API features/changes

Describe the feature you'd like to request

Sometimes it would be useful to give the symbolic environment knowledge about authorization-related semantics when analyzing the policies.

For example, in upbound/kubernetes-cedar-authorizer#24, the authorizer is built such that:

• when action == Action::"create", then resource has request == true && resource has stored == false,
• when action == Action::"update", then resource has request == true && resource has stored == true
• else resource has request == false && resource has stored == false

Under these assumptions, the following policy is always false:

permit(principal == User::"lucas", action == Action::"create", resource)
when {
  resource has stored && resource.stored.foo == "bar"
}

(this specific example actually happened when preparing for the KubeCon talk, and took a while to debug until I realized there was a copy-paste error resource.stored => resource.request).

There is compile_with_custom_symenv today, but it requires the user to know about some internal invariants, and at a quick glance I did not see a method to add custom (assert ...) blocks to the SMT. I think that for the specific use-case I provided above, I could encode the invariant as a deny(...) unless {...} policy, bundle that "invariant policy" with the one I actually want to analyze, and use verify_always_denies instead of verify_never_matches that would otherwise be used for single-policy analysis.

The user shouldn't need to think about internal invariants, and ideally, not be required to write invariants in SMT format, but Cedar itself (where possible), and through an API that is easy to understand and does not conflate "invariants" with policies to analyze. In addition, if there are lots of policies to analyze this way, one could maybe consider incremental SMT solving, where the invariants are always there, and just individual policy terms are pushed/popped.

This could provide a pretty nice framework for the user to "unit test" their policies, given that this feature would be straightforward enough to use (that is, without the need to learn about Cedar internals).

Describe alternatives you've considered

One workaround covered above, another workaround could be "simply" writing composite Solver implementation that adds some extra assert lines, but this may require the user to do a lot of extra work to understand the current symbolic environment.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change