`cedar-lean-cli analyze compare` maybe does not need to consider request environments not targeted by any policy

[luxas]

Category

Other

Describe the feature you'd like to request

I have a valid, auto-generated 5000 line schema of Kubernetes types, and tried out the cedar-lean-cli analyze compare command.

I tried comparing two policysets that should be equivalent, namely:

simple1.cedar

permit (
  principal == k8s::User::"lucas",
  action == k8s::Action::"create",
  resource is core::configmaps
);

simple2.cedar

permit (
  principal == k8s::User::"lucas",
  action == k8s::Action::"create",
  resource is core::configmaps
) when {
    resource.name != "foo"
};

permit (
  principal == k8s::User::"lucas",
  action == k8s::Action::"create",
  resource is core::configmaps
) when {
    resource.name == "foo"
};

Then I ran

time cedar-lean-cli analyze compare simple1.cedar simple2.cedar api.cedarschema

which took around 4 minutes. I wondered why it's so slow, until I waited for the output, and found out it does the checks for every request environment. That makes sense for sure, but in my case I guess it's known that all request environments not targeted by either policy must be the same, without checking.

There were 1707 request environments, it (only) took on average 146ms to evaluate a fully empty request environment with lots of schema, but no policy attached.

So I guess that could be an optimization to cut a significant amount of time from larger policy comparisons.

Describe alternatives you've considered

Additional context

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

[lianah]

One way to implement this is to use the validator to check the policies against the request environment and if it does not apply skip it. Note that (for subtle technical reasons detailed here) the symbolic compilation has to run on the well-typed policies as outputted by the validator after type checking here, where wellTypedPolicy is computed here. So in your case, because analysis is running on well-typed policies I would assume for almost all the request environments the validator reduces the policies to false, so the SMT solver never gets involved. I wonder if most of the time is being spent in doing the per-request environment validation + the overhead of calling the Lean code + symbolically encoding the request environment & the trivially vacuous policy.

The current validation code does type checking per-request environment so you we could see how long the Rust cedar CLI takes to validate these policies against your full 5000 lines schema. If it takes significantly less time it could mean most of the overhead is in the Lean symbolic encoding of the request environment and trivially empty policies so there is an optimization we could do.

Even if we skip the analysis for request environments that don't apply, we would still want to report those requests environments as warnings in case it is not intentional like in your case.