Set intersection, difference, length, and union operators

[luxas]

Category

Cedar language or syntax features/changes

Describe the feature you'd like to request

This issue tracks the interest in common operations on sets: intersection, difference, length, and union.
I asked @emina about these before, and she mentioned that they are analyzable, but avoided so far for performance reasons. She told that sets in SMT are unbounded, and can thus have infinite length, so to expose a length field in Cedar, one would need to perform expensive conversions back and forth. In addition, execution of a Cedar policy cannot yield a value that is bigger or smaller than what is given as input, but the intersection, difference and union operators could change that.

I guess that some optimizations could be done to e.g. evaluate set operations lazily instead of eagerly (eventually all usage of sets turn into a boolean through contains* or similar), but it's a fair point.

For the Kubernetes use-case, authorization of updates get both the old (already in storage) and new (request) objects, and in such cases, you naturally care about differences, e.g. (object.finalizers - oldobject.finalizers).isEmpty() || (object.finalizers - oldobject.finalizers) == ["allowed-value"] instead of something like (copied from upbound/kubernetes-cedar-authorizer#13)

  // if (new finalizers >= old finalizers), verify either equality or one added finalizer
  (if resource.request.metadata.finalizers.unorderedSet.containsAll(resource.stored.metadata.finalizers.unorderedSet) then
    (resource.stored.metadata.finalizers.unorderedSet.containsAll(resource.request.metadata.finalizers.unorderedSet)
    || (resource.request.metadata.finalizers.unorderedSet.contains("my-controller-finalizer") && 
        resource.request.metadata.finalizers.length == resource.stored.metadata.finalizers.length + 1))
  // There was at least one old finalizer not in the new set, verify new finalizers < old, and that the difference is "my-controller-finalizer"
  else
    (resource.stored.metadata.finalizers.unorderedSet.containsAll(resource.request.metadata.finalizers.unorderedSet &&
     resource.stored.metadata.finalizers.unorderedSet.contains("my-controller-finalizer") &&
     resource.request.metadata.finalizers.length == resource.stored.metadata.finalizers.length - 1)
  )

that'd you'd need to do today.

I'm not asking for this to be implemented right away, but I just wanted to open this issue to gauge interest in this feature.

Describe alternatives you've considered

Users can expose the set and the length separately, but that can produce symcc false positives.
Some of the operations could maybe technically be emulated using existing operations, but it's quite a lot of work for users and error-prone.

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

[cdisselkoen]

Intersection is already kind of available (if you only care about whether the intersection is empty or not) as .containsAny(). s1.containsAny(s2) is true exactly when the intersection is non-empty. Do you have a use for intersection that does some other operation on the set-intersection other than checking whether it is empty?

For your example about checking whether the set-difference is empty, I believe this is also already available as .containsAll(), or am I missing something? (object.finalizers - oldobject.finalizers).isEmpty() should be the same as oldobject.finalizers.containsAll(object.finalizers).

Do we want new syntax sugars or synonyms that are implemented with existing operations? would that improve the user experience described in this issue?

[luxas]

The point of the example was that the difference between the old and the new set can differ in at most one value (added or removed): the authorized finalizer name ("allowed-value"). If one does not care about the false positives in symcc that could arise from splitting the length and set into separate "unrelated" values, then I think the policy that I have there does manage to check for this off-by-one-allowed-value case. It's just not very easy for the policy author (which could also be fine, as with one could possibly use an extension function #2126 as a easy-to-use "macro" during validation time that before policy evaluation is substituted for the above concrete "pure Cedar" implementation).

I guess that whenever the RHS of contains* is a literal set, it is possible to check for union and intersection as well "manually", such as:

# "&" == intersection, "|" == union, "-" == difference
(set1 & set2).contains("foo") ==> set1.contains("foo") && set2.contains("foo")
(set1 | set2).contains("foo") ==> set1.contains("foo") || set2.contains("foo")
(set1 - set2).contains("foo") ==> set1.contains("foo") && !set2.contains("foo")

(set1 & set2).containsAll(["foo", "bar"]) ==> set1.containsAll(["foo", "bar"]) && set2.containsAll(["foo", "bar"])
(set1 & set2).containsAll(["foo", "bar"]) ==> set1.containsAll(["foo", "bar"]) || (set1.contains("foo") && set2.contains("bar")) || (set2.contains("foo") && set1.contains("bar")) || set2.containsAll(["foo", "bar"])
(set1 - set2).containsAll(["foo", "bar"]) ==> set1.containsAll(["foo", "bar"]) && !set2.containsAny(["foo", "bar"])

(set1 & set2).containsAny(["foo", "bar"]) ==> (set1.contains("foo") && set2.contains("foo")) || (set1.contains("bar") && set2.contains("bar"))
(set1 | set2).containsAny(["foo", "bar"]) ==> (set1.contains("foo") || set2.contains("foo")) || (set1.contains("bar") || set2.contains("bar"))
(set1 - set2).containsAny(["foo", "bar"]) ==> (set1.contains("foo") && !set2.contains("foo")) || (set1.contains("bar") && !set2.contains("bar"))

Another way to solve the "you are only allowed to add or remove one specific value" authorization, would be to model it as

(oldObject.finalizers | ["allowed-value"]) == (newObject.finalizers | ["allowed-value"])

as if none or both of the sets have it, this becomes oldObject.finalizers == newObject.finalizers, but the check passes also when e.g. oldObject didn't have the allowed value before, but now it'd be added, or vice versa.

Mostly I opened this issue to gauge interest and how worthwhile others think this is, and as @john-h-kastner-aws asked me to mention all the things that came up when I was looking into integrating with Kubernetes. For comparison, CEL is heavily used in Kubernetes today, and that has full-blown map, exists, forall etc. loop implementations which makes this kind of checking quite easy.