gravitational / rbac-linter Goto Github PK

In Z3, it isn't enough to define what elements are in a set - you also have to define what elements are not in a set, otherwise the solver uses the trivial model of a set containing every element of the given sort. The result of this requirement is some fairly hideous quantification constraints in the role_analyzer.labels_as_z3_map and role_analyzer.traits_as_z3_map functions. This doesn't seem to cause any problems by itself yet, although the models it generates are basically unintelligible; it may cause tractability issues for some inputs to role_query.py, although that seems unlikely. For simplicity an alternative representation of sets should be explored which avoids this problem. However, this direction of using specified functions instead of uninterpreted functions could lead to unforeseen issues with functionality used by role_equivalence_check.py.

In Teleport's RBAC for allow rule to apply, all labels should match for Allow rule to apply, and Any label could match for Deny rule to apply:

So this above should be tweaked for allow and deny rules

I think this would be a fairly simple fix. In regexp.replace the start/end tokens would be quite difficult to implement, but for ordinary regex constraints of the form:

'key' : '^staging|prod$'

the tokens are actually irrelevant, because the regex implicitly matches the entirety of the text - its start must be the text's start, and its end must be the text's end. It's possible someone could define a constraint like:

'key' : 'foo^bar'

but this would just be invalid and match nothing. So the fix to add support would be as follows:

• if the ^ and $ characters are at the start/end of the regex, ignore them
• if the ^ and $ are not at the start/end of the regex, either raise a ValueError exception or match nothing with Empty(ReSort(StringSort))

To make it more robust, this analysis should be done on the output of sre_parse.parse rather than the raw regex string. There are various alternative positional markers like [\A], [\b], [\B], and [\Z] that the parser will help identify with the sre_constants.AT category.