Define roadmap for symbolic compiler/smt analyzer

[B-Lorentz]

Category

Other

Describe the feature you'd like to request

Analyzability (the ability to query about logical properties of a given schema + policy set) is a major goal of cedar, to the point of it being a hard requirement for any proposed language feature. https://www.cedarpolicy.com/blog/whats-analyzable
Yet, looking around the cedar-policy github org, no 'analyzer' or 'symbolic compiler' is available.

I presume this is an intentional strategy, since this is available in a proprietary form in Amazon Verified Permissions. (Nothing wrong with that, cedar is not for charity after all, and what is open-sourced already is very valuable)

I think it would be helpful however to clarify in the documentation:

• if these capabilities are ever planned to be open sourced
• if so, at what roadmap and timeline.

Describe alternatives you've considered

Someone could write an open-source 'unofficial' one, based on the paper.

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

[D-McAdams]

Apologies for the delayed response! Much of the team was out for the holidays.
While there is no implementation of analysis yet (not even in Amazon Verified Permissions), we are looking to set that roadmap. Feedback from the community is especially helpful in setting priorities. If willing to chat further about the interest in analysis and the types of problems you'd like to solve, it would be great to do a quick video call and/or Slack conversation to get into details. If you're open to that, you can reach me directly at darinm@amazon.com or via the Cedar Slack community where I can be found under the same email (https://communityinviter.com/apps/cedar-policy/cedar-policy-language).