Propose a path extension type

[apg]

Rendered

Checklist

• Added RFC to text/SUMMARY.md in numerical order

[patjakdev]

I wonder about the feasibility of generalizing the proposed path type to an ordered list type, where path becomes just a list[string].

The biggest wart that I think can think of is that list[string] would be the only type to allow for the special wildcard syntax when doing matching. A new any keyword could potentially be added to allow for wildcards in lists of other types.

[patjakdev]

I might propose prefixLike instead of prefixMatches for symmetry with the like operator.

You might also consider a prefixEquals for situations where * should be treated as a literal asterisk rather than a wildcard without the need to escape it.

[apg]

I'm not sure about the Like vs Matches. I think Matches might work better given its relationship to structual pattern matching, though, you're right about the name symmetry--prefixLike might be more ergonomic. Open to other feedback here!

[patjakdev]

Presumably, this method errors if a non-string is passed as an argument.

[apg]

Yeah. That would make sense! I'll have to update this.

[patjakdev]

Interesting. This might be the first extension type constructor that doesn't require a string literal for strict validation since it's not possible to pass an invalid value.

[patjakdev]

Include the Cedar format as well?

[patjakdev]

Isn't this the same thing as Alternative F? I suppose alternatives A and B are also the same thing as Alternative F.

[patjakdev]

I don't quite understand what this is getting at.

[apg]

Basically, matches("*") is strict on the number of components. In the example above path("foo", "bar").matches("*", "bar") is fine because it has two components. The variant prefixMatches supports the variable number of components.

[patjakdev]

Seems fine to me.

If we were to generalize path into list, though, it would be a problem because the type would be unknown.

[apg]

I wonder about the feasibility of generalizing the proposed path type to an ordered list type, where path becomes just a list[string].

The biggest wart that I think can think of is that list[string] would be the only type to allow for the special wildcard syntax when doing matching. A new any keyword could potentially be added to allow for wildcards in lists of other types.

I think this is something @emina would have to look at. I simply based this off of this comment #103 (comment). It seems as though general lists would be analyzable if they worked like the proposal (only integer literals for accessing elements, no length).

[chaluli]

Rather than adding a new path type. I think we can enriching the regular language matching mechanism we currently using in string matching (the like operator) to support the glob matching this PR is trying to support.

I concretely propose the following syntax:

string.matches(glob("glob literal", "delimiter"))      # globs support both * and ** patterns (1 or 0+ components)
string.matches(re("regular language literal"))         # optional but is the most general matching mechanism
string.componentAt(n_index, "delimiter") == (expr)     # resource.domain.componentAt(1, '.') == principal.team
string.countComponents("delimiter") OP (Integer)       # resource.domain.countCompoents('.') <= 4

These all remain analyzable because like the like operator, they can be directly compiled into string operations that are supported in SMTLib (mostly str.in_re(s, R) where R is a regular language literal, which is exactly what the like operator already compiles to when analyzed). Note, we mean that the regular language literal is equivalent to an NFA not a regular expression (which may be non-regular due to forward/backward lookups, groups, etc.)

my_string.matches(re("R")) becomes str.in_re(my_string, R) (here we assume that R is a regular language as described by SMTLib standard).

my_string.matches(glob("*.github.com", ".")) becomes str.in_re(my_string, "[^\.]*\.github\.com") Behaves just like the like operator but makes use of delimiter.

The string.componentAt(n_index, "delimiter") and string.countComponents("delimiter") unfortunately requires the delimiter be a single character (or at least not e.g., .. or // where there are repeating segments). The first makes use of str.substr/indexof (formula grows linearly in the value of n_index, fine for n_index = 0, 1, 2, 3, 4, etc. but very bad for n_index = 10000).

[emina]

The string.componentAt(n_index, "delimiter") and string.countComponents("delimiter") unfortunately requires the delimiter be a single character (or at least not e.g., .. or // where there are repeating segments). The first makes use of str.substr/indexof (formula grows linearly in the value of n_index, fine for n_index = 0, 1, 2, 3, 4, etc. but very bad for n_index = 10000).

I don’t think we should use st.substr/indexof or anything that brings the theory of integers into the translation. We’ve carefully avoided this so far, because Cedar itself doesn’t have integers: it uses 64-bit vectors. So, unless n_index is a literal, the translation has to go back and forth between the two representations, which leads to poor performance in practice. Or if it is, then the formula grows linearly with n_index (as the path representation’s formula would).

Taking a step back, maybe we should re-consider an MVP solution that handles most use cases: like matching with a delimiter. This would introduce a variation of the like operator, along the lines of <expr> like(<delim>) <pattern>, or whatever syntax we find most palatable. This translates directly into a str.in_re check, where the <delim> character is treated as a literal in the pattern. While not as expressive as either paths or globing, it avoids the theory of integers and/or linear scaling of the formula with index size. It should perform comparably to like without delimiters. And it should be easier to implement / formalize / maintain than the alternatives.

[chaluli]

Taking a step back, maybe we should re-consider an MVP solution that handles most use cases: like matching with a delimiter. This would introduce a variation of the like operator, along the lines of <expr> like(<delim>) <pattern>, or whatever syntax we find most palatable. This translates directly into a str.in_re check, where the <delim> character is treated as a literal in the pattern. While not as expressive as either paths or globing, it avoids the theory of integers and/or linear scaling of the formula with index size. It should perform comparably to like without delimiters. And it should be easier to implement / formalize / maintain than the alternatives.

I agree with this. The like matching with a delimiter I think is the biggest improvement to effort ratio without introducing any new operators into the SMT encoding for analyzability. The last two could be done but put us into a situation where we need to increase the kinds of SMT operators in our encoding and/or increase the size of the produced formula proportional to the value of a literal (not good).

[apg]

I've been thinking about this today, and I think I can get behind it. I'm wondering about syntax though:

1. like('/') -- this introduces a new type, character, that we'd have to deal with.
2. like("/") -- this doesn't introduce a new type, maybe is only valid if it's length 1?
3. like("::") -- Is this valid? How would like("::") match the string a:::b given the potential ambiguity?

2 makes the most sense to me, but it feels rather unergonomic to use it and restrict it to a single character, when it generally isn't restricted in size.

[emina]

I've been thinking about this today, and I think I can get behind it. I'm wondering about syntax though:

1. like('/') -- this introduces a new type, character, that we'd have to deal with.
2. like("/") -- this doesn't introduce a new type, maybe is only valid if it's length 1?
3. like("::") -- Is this valid? How would like("::") match the string a:::b given the potential ambiguity?

2 makes the most sense to me, but it feels rather unergonomic to use it and restrict it to a single character, when it generally isn't restricted in size.

I’d stick with just single character separators to start with, not arbitrary strings. If we find that we absolutely need string separators later, we can allow them while remaining backward compatible.

Since the separator string is a literal, CST -> AST or the validator can simply reject any literal with more than character. So we wouldn’t need a new type.

We can explore other syntactic forms too (e.g., <expr> like (<pattern>, <delim>)) or make this a function. My instinct was to reuse like because the two operators are very similar. But we don’t have to if we feel that would cause too much confusion or parsing issues.

[apg]

I like the idea of <expr> like (<pattern>, <delim>), but that probably complicates the grammar. It's probably easier to introduce a builtin function well_liked(<expr>, <pattern>, <delim>)

[chaluli]

I think this is substantially similar to the like operator. Perhaps we could do something like:

<expr> like(<delimiter>) <pattern>

"github.com" like(".") "*.github.com"                # false
"cedar.github.com" like(".") "*.github.com"          # true
"policies.cedar.github.com" like(".") "*.github.com" # false

We also need to nail down the multi-delimited pattern format.

I see you propose "**.github.com" to match "github.com", "cedar.github.com", "policies.cedar.github.com", etc.

Do we want "**" to mean any number of delimited sections?
Pro: simple pattern, fairly intuitive.
Con: I believe in the current like operator "*" and "**" match the same sets of strings. In the proposed update the * character is playing double duty: the first * is match any character (except the delimiter) any number of times and the second occurrence of * is repeat the preceding pattern (the first wild card) 0 or more times. I think this is due to inter-mixing the glob meaning of * and the regular language meaning of * which are very similar but slightly different.

Perhaps not necessary for a V1. But we might want to also consider if we want to allow matching each delimited section against a pattern rather than just wild-card.

For example

"<pattern>.<pattern>.<pattern>" like(".") "(<pattern>)<repeat-delimited-section-sentinel-character>"

However, that is getting closer to full support for regular language patterns than the simple glob matching Cedar currently supports.

[mwhicks1]

Do we want "**" to mean any number of delimited sections?

I would like to confirm: Is the semantics of like with a delimiter that * components maximally match everything except the delimiter? In other words, "github.com" like('.') "*.com" is true but "foo.github.com" like('.') "*.com" is false? That seems to be a pretty small change to the normal like handling today; is that sufficient for the use-cases the owner of this RFC has in mind?

Assuming yes, I like this idea of using **. It is naturally backward compatible with normal like because that form does not have a delimiter -- for normal like you interpret ** the same as *. One caveat is that if users are not careful and they take an expression principal.host like "*.github.com" and change it to principal.host like('.') "*.github.com" it will start to return false for things that used to be true -- they will have to explicitly change the * to ** to be as before. Probably that's a good thing; if you are explicitly updating your policy to add the delimiter, you are looking for more precise behavior and will thus change the pattern too.

[apg]

I would like to confirm: Is the semantics of like with a delimiter that * components maximally match everything except the delimiter? In other words, "github.com" like('.') ".com" is true but "foo.github.com" like('.') ".com" is false? That seems to be a pretty small change to the normal like handling today; is that sufficient for the use-cases the owner of this RFC has in mind?

Yeah, let's break this down so we're on the same page:

1. "github.com" like('.') "*.com" is true but "foo.github.com" like('.') "*.com" is false? -- YES. * with "." as the delimiter defines a segment that each * can match.
2. "foo.bar.github.com like "**.github.com" is true, because, as you say "**" is exactly like like "*.github.com" today.

** having the semantics of "It matches any number of delimited segments" makes a lot of sense to me, and I believe matches the semantics I proposed in this RFC. To put it in the Perl Compatible Regular Expressions perspective:

1. * is equivalent to .*
2. ** is equivalent to .*
3. * with a delim, D, is equivalent to [^D]+D (e.g. *.github.com only matches if there's a, e.g., xxxx. in front)
4. ** with a delim, D, is equivalent to ([^D]+D)+ (e.g. **.github.com matches if there's one or more, e.g., xxxx. in front)

[mwhicks1]

** having the semantics of "It matches any number of delimited segments" makes a lot of sense to me, and I believe matches the semantics I proposed in this RFC.

Excellent! If you are aligned with this, would you be able to rework the RFC to make this the proposal and move the current proposal to "Alternatives" for posterity?

I think this is a nice extension. It seems to be useful and it fits the language design well.

[chaluli]

3. * with a delim, D, is equivalent to [^D]+D (e.g. *.github.com only matches if there's a, e.g., xxxx. in front)

I belive it's simply [^D]+, right? Otherwise, "domain.github.com" like(".") "*.github.com" would be false; and "domain..github.com" like(".") "*.github.com" would be true (note the double .).

4. ** with a delim, D, is equivalent to ([^D]+D)+ (e.g. **.github.com matches if there's one or more, e.g., xxxx. in front)

I believe the intended semantics is ([^D]+D)*[D^]+ for a similar reason to the above.

Otherwise, that looks like a good change.

[paxan]

like      "*.github.com" # matches any subdomain 
          under "github.com", but not "github.com"
like(".") "*.github.com" # matches "foo.github.com",
          but not "yo.foo.github.com", not "github.com"

so ** is not even needed right?

[chaluli]

like      "*.github.com" # matches any subdomain 
          under "github.com", but not "github.com"
like(".") "*.github.com" # matches "foo.github.com",
          but not "yo.foo.github.com", not "github.com"

so ** is not even needed right?

In @apg 's suggested semantics. The delimited glob operators match non-empty sequences. Where in the non-delimited glob operators match possibly empty sequences. So,

".github.com" like(".") "*.github.com"      # False
".github.com" like(".") "**.github.com"     # False
"abc..github.com" like(".") "**.github.com" # False

".google.com" like "*.google.com"           # True
"abc..github.com" like "*.github.com"       # True

[sspencer-slack]

FWIW, Slack's Secops use case also prefers the "like" mechanism over the original path proposal. We believe that it is easier for users to reason about and implementation is probably simpler as well.

We like the double star ** semantic for "one or more non-empty sections divided by the delimiter". so in other words:

"test..github.com" like "*.github.com"  # True
"test..github.com" like "**.github.com" # True (but pointless, extra star)
"test..github.com" like(".") "**.github.com" # False (empty group)
"test.b.github.com" like(".") "**.github.com" # True
"test.b.github.com" like(".") "*.github.com" # False (only matches one group)
"test.github.com" like(".") "*.github.com" # True
"testgithub.com" like(".") "*github.com" # True ? (I think this should be True because I think the delimiter means "Match to the first delimiter, next marker, or start/end of string").
"testgithub.com" like(".") "**github.com" # True (same as previous in this case).

[apg]

I belive it's simply [^D]+, right?

Hmm. You're right. It definitely seems like you'd like to write it *.github.com, but I wonder if that means we should be doing something like X like "(*.)github.com" or X like "(**.)github.com"?

That could also provide an avenue for (/*)/apg to prefix well formed (Unix style) file system paths.

Thinking this through, I think the main benefit of the Path type is that the delimiter is eliminated entirely so these quirks don't exist.

[chaluli]

If you propose the (*.)github.com syntax, that makes me think perhaps we could support e.g., (**.)github.com/(**/) with more than 1 kind of delimiter in a single string (i.e., for matching URL-like strings). Though one could perhaps split the domain from the path and check them independently rather than mixing delimiters within a single pattern.

Note that the (*.)github.com pattern syntax is not backwards compatible. Because ( and ) are are allowable literals within a pattern. We can't give them the special meaning to group a delimiter sequence.

[apg]

Note that the (*.)github.com pattern syntax is not backwards compatible. Because ( and ) are are allowable literals within a pattern. We can't give them the special meaning to group a delimiter sequence.

Right. Now that I see it, I don't think we can ignore the position of the delimiter. It's too restrictive to always assume it's after especially if a segment can't be empty.