Path extension type

[benkehoe]

I'm looking to gather use cases for an extension type for paths. I see value in it, and @emina suggested seeing about whether other people have a need for it as well before writing up an RFC. So, I guess I'm asking folks to comment on this about their use cases for path matching in policies.

Many filesystem and filesystem-like use cases (AWS S3, URLs, etc.) have identifiers that encode a tree hierarchy, i.e. paths. Policies for these use cases often include matching against certain components of the path but not others.

A path of a fixed length can be modeled directly as a record (as with the colon-separated parts of an AWS ARN) but not for a path of variable length (as with the last component of many ARNs).

A path of variable length can, of course, be modeled with hierarchy, but this can be significant overhead especially when parents are implicit and may not actually exist as entities themselves (e.g., in URLs).

It can also be modeled with tags, splitting the path into tags, for example a path "foo/bar/baz" modeled as tags "path1": "foo", "path2": "bar", "path3": "baz". Then matching a path like foo/*/baz is:

resource.hasTag("path1") && resource.getTag("path1") == "foo"
&&
resource.hasTag("path2") && resource.getTag("path2") like "*" // can be omitted
&&
resource.hasTag("path3") && resource.getTag("path3") == "baz"
&&
! resource.hasTag("path4")

This certainly works, but is pretty awkward, and might not be obvious to Cedar users (I know it took me some time to work out). Packaging it up as a Path type seems useful. You'd have a .getComponent(i) function. It seems like .getLength() might not be workable, but boolean comparator functions for length like .lengthEquals(n) might work? .hasComponent(i) is equivalent to .lengthGreaterThanOrEqualTo(i+1) at least, and ! .hasComponent(i) to .lengthLessThan(i+1). Maybe they could only take constants?

So you'd have something like:

resource.path.lengthEquals(3)
&&
resource.path.getComponent(0) == "foo"
&&
resource.path.getComponent(1) like "*" // can be omitted
&&
resource.path.getComponent(2) == "baz"

[D-McAdams]

Agree that first-class support for "paths" would be helpful in scenarios. Here is a prior RFC with a similar request:
cedar-policy/cedar-docs#78

Sample use cases I've observed:

• URL paths including firewall-style rules, SPIFFE SVIDs, and any other resource that models themselves as a URL.
• MQTT paths
• Semver parsing (delimited with dots)

We even had someone ask for it for OAuth scopes: #44
That was interesting because OAuth scopes should have been modeled as a Set. But, the implementation had already shipped with a string, so they were looking for help on how to make-do with that reality.

If I remember correctly, the conversation surfaced the following questions:

• Analyzability. This introduces ordered lists which are more challenging to analyze, and is a reason why Cedar uses Sets instead of Arrays.
• Flexibility on delimiters. Do we let users specify any delimiter?
• How to handle domain-specific parsing rules. For example, is "/path//to///resource/" considered 3 elements or 7 elements (with 4 of them being empty strings)?
• Are paths always a sequence of strings, or can they be a sequence of other types such as numbers (as in the semver example)
• Are paths sufficient to solve the user requirements, or will we find that with URL paths, customers immediately return with more requests to normalize the URL in more ways (such as by lowercasing) such that a first-class type for URL is the more robust answer (which may itself need a "path" type").

[benkehoe]

Thanks for the links, I had looked at the split issue but missed the comment about paths, and hadn't seen the issue on the docs repo.

My first request was "delimiter-aware matching" like matches(string, expression, delimiter) so that you could do matches(somePath, "foo/*/bar", "/"), but I think Cedar's general approach of "do the parsing/preprocessing yourself outside of Cedar" makes sense, which makes what Cedar needs to know just the sequence of components.

Thoughts on the questions you listed:

• Analyzability. This introduces ordered lists which are more challenging to analyze, and is a reason why Cedar uses Sets instead of Arrays. For sure. I suspect (with my layperson's understanding) one challenge is the validator, which today keeps boolean capabilities but might need to keep some sort of integer capability to track length checks.
• Flexibility on delimiters. Do we let users specify any delimiter? [and] How to handle domain-specific parsing rules. For example, is "/path//to///resource/" considered 3 elements or 7 elements (with 4 of them being empty strings)? I think the syntax maybe has two routes. One is that the already-split components are specified as a sequence e.g. Path("foo", "baz", "bar"), in which case delimiter doesn't enter in to it, but we currently don't have syntax for ordered lists or variadic functions. The other is something like Path("foo/baz/bar", "/"), and like datetimes the input itself is discarded after conversion to the internal sequence representation, and this brings in all the problems you outline, so I tend to think the first is probably better.
• Are paths always a sequence of strings, or can they be a sequence of other types such as numbers (as in the semver example) My gut feeling is strings only. I think semver is well-served by records, given that it has a fixed number of elements. A semver extension type might be interesting, but I think it's probably a separate use case from paths.
• Are paths sufficient to solve the user requirements, or will we find that with URL paths, customers immediately return with more requests to normalize the URL in more ways (such as by lowercasing) such that a first-class type for URL is the more robust answer (which may itself need a "path" type"). I think path is a building block on which these sorts of things can be built. A URL overall can be a record, but without paths in Cedar, the expressiveness is limited. The normalization part, I tend to buy in to the position that normalization should happen outside of Cedar, though I get why people hate it.

[emina]

Here is one proposal for a path abstraction that would be analyzable. The question is whether it would be useful.

This is a rough sketch, and the syntax / method names are chosen just for illustration purposes.

First, we would introduce a Path extension type. Conceptually, a path is a sequence of strings.

Paths are constructed with an n-ary method that takes zero or more strings, e.g., path("foo", context.thing, "bar"). Note that arguments to path don't have to be string literals.

While Paths are internally represented as lists, we won't expose this representation at the Cedar level. For example, we won't have methods to get the length of the path or to access a path element directly using indexes. The reason is that these operations are not analyzable for finite lists. There are some restricted variants that are analyzable---e.g., we force all indexes to be integer literals and not something like context.position---but with the added restrictions, the path abstraction wouldn't be much more ergonomic than the tag-based solution.

What we can do instead is define two operations that allow you to compare a path to a sequence of patterns. (These could be compressed into one method or maybe get some dedicated like syntax, but they are easiest to explain as two methods.)

The first operation is the n-ary method Path.matches. The receiver of this method is a Path, and the arguments are a sequence of zero or more literal strings that represent patterns to match. For example, context.path.matches("foo", "*", "bar") returns true if context.path has exactly 3 elements, each of which matches the corresponding pattern. In other words, it's a short-hand for context.path == 3 && context.path[0] like "foo" && context.path[1] like "*" && context.path[2] like "bar".

The second operation is the n-ary method Path.prefixMatches. The receiver and arguments are the same as for Path.matches. The only difference is that prefixMatches checks only that a prefix of the path matches the pattern and not necessarily the whole path. For example, context.path.prefixMatches("foo", "*", "bar") returns true if context.path has at least 3 elements, and the first 3 elements match the corresponding pattern. So, the call is a short-hand for context.path <= 3 && context.path[0] like "foo" && context.path[1] like "*" && context.path[2] like "bar".

If you are curious as to why this is analyzable, the reason is that the pattern sequence (arguments to matches and prefixMatches) is known statically. We know exactly how long it is and what its contents are (from the restrictions I've placed above on the syntax of matches and prefixMatches calls). So, the analyzer will basically unroll the loop the that does the element-by-element matching of the path against the pattern. This is analyzable, but obviously, its scalability is very closely tied to the length of these patterns. Unrolling the matching loop for a pattern with 100 elements won't be great for performance :))

[benkehoe]

I think it would be useful with just .matches() and .prefixMatches(), though I think component access with integer literal indexes is useful too. It's a shame if .suffixMatches() wouldn't be possible.

My main reasoning for why a Path type would be useful to include is exactly that it's difficult to reason about how to accomplish, and thus instead of putting some guidance in the docs, packaging it up into a proper abstraction is a good thing.

You've got context.path == 3; does that mean a length test would be directly possible on the path?

I started thinking about whether it should be Path or a more general Sequence<>, but I the challenge of what .matches() would look like for, say, integers means that's probably not a good direction.

[emina]

It's a shame if .suffixMatches() wouldn't be possible. My main reasoning for why it would be useful to include is exactly that it's difficult to reason about how to accomplish, and thus instead of putting some guidance in the docs, packaging it up into a proper abstraction is a good thing.

Unfortunately, .suffixMatches() isn't easily analyzable. To see why, note that implementing .suffixMatches(...) involves unbounded loops. We have to effectively reverse both lists (the input and the pattern) and perform .prefixMatches. The problem is that the reversal operation on the input list requires a loop with no fixed a priori bound, so we can't unroll this and encode the operation that way.

There is an alternative way to encode .suffixMatches() that targets a specific solver, but this alternative would require a lot of engineering effort (compared to just matches and prefixMatches), and it would introduce significant complexity into the resulting logical formula (more "theories" in SMT lingo). This usually means taking a performance hit on the analysis. And in this case, it's not clear to me without further research whether the alternative encoding remains decidable (i.e., the solver is always able to decide if the formula has a solution or not).

So, unless there is a lot demand / use cases for .suffixMatches(), it would be tough to justify supporting it.

[benkehoe]

I think a substantial portion of .suffixMatches() use cases would be just the final element, e.g. match against the filename. But that use case can be accomplished by having the final element in a separate attribute (either with the path still including it or not), so I think that removes most of the argument in favor of .suffixMatches().

Also, I realized my earlier comment was confusing. This sentence

My main reasoning for why it would be useful to include is exactly that it's difficult to reason about how to accomplish, and thus instead of putting some guidance in the docs, packaging it up into a proper abstraction is a good thing.

was in reference to the Path type in general, not .suffixMatches()