From f0a5ad934b1039679a45603ef530889fe59d4363 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Tue, 11 Jul 2023 16:28:25 -0400 Subject: [PATCH 01/10] Proposal for amending strict mode validation --- text/0019-stricter-validation.md | 77 ++++++++++++++++++++++++++++++++ text/policy.cedar | 8 ++++ text/schema.cedarschema.json | 43 ++++++++++++++++++ 3 files changed, 128 insertions(+) create mode 100644 text/0019-stricter-validation.md create mode 100644 text/policy.cedar create mode 100644 text/schema.cedarschema.json diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md new file mode 100644 index 00000000..ae8a05be --- /dev/null +++ b/text/0019-stricter-validation.md @@ -0,0 +1,77 @@ +# RFC Template (Fill in your title here) + +## Related issues and PRs + +- Reference Issues: +- Implementation PR(s): + +## Timeline + +- Start Date: 11-07-2023 +- Date Entered FCP: +- Date Accepted: +- Date Landed: + +## Summary + +Internally, strict validation of a policy is implemented as 1/ checking and transforming the policy using a _permissive_ validation mode; 2/ annotating the transformed policy with types, and 3/ checking the types against more restrictive rules. We would like to be able to at least _explain_ strict mode independently of permissive mode, but there is no easy way to do that. This RFC proposes to separate strict mode from permissive mode, making the implementation simpler and more understandable/explainable, though somewhat more strict. + +## Motivation + +Consider this policy, given in file [`policy.cedar`](policy.cedar), where `principal` is always of type `User`: +``` +permit( + principal, + action == Action::"read", + resource) +when { + (if context.sudo then Admin::"root" else principal) == resource.owner || + resource.isPublic +} +``` +If we validate this policy against the schema [`schema.cedarschema.json`](schema.cedarschema.json), then `resource.owner` is always of type `User`. As a result, the policy is rejected by strict-mode validation, with two errors: +1. the `if`/`then`/`else` is trying to return entity type `Admin` in the true branch, and entity type `User` on the false branch, and these two are not equal. +1. since `resource.owner` has type `User`, it will have a type different than that returned by the `if`/`then`/`else`, which can sometimes return `Admin`. + +But if we change `"User"` in [`schema.cedarschema.json`](schema.cedarschema.json) on line 13 to `"Org"`, then `resource.owner` is always of type `Org`. As a result, the policy is accepted! The two error conditions given above seem not to have changed -- the conditional returns different types, and those types may not equal the type of `resource.owner` -- so it's puzzling what changed to make the policy acceptable. + +The reason is that strict-mode validation is dependent on permissive-mode validation. In particular, strict-mode validation is implemented in three steps: 1/ validate and transform the policy using permissive mode; 2/ annotate the transformed policy AST with types; and 3/ check the types against more restrictive rules. + +In the first case, when `resource.owner` is always of type `User`, the expression `(if ...) == resource.owner` has type `Boolean` in permissive mode and as a result no transformation takes place in step 1. As a result, it is rejected in step 3 due to the errors given above. + +In the second case (after we change the schema), `resource.owner` is always of type `Org`. Under permissive mode, the `(if ...) == resource.owner` expression has singleton type `False`. That’s because the `(if ...)` expression has type `User|Admin` ("`User` or `Admin`") and `User|Admin` entities can never be equal to `Org` entities. Both the _singleton type_ `False` (which only validates an expression that _always_ evaluates to `false`) and _union types_ like `User|Admin` are features of permissive mode and are not present in strict mode. Because of these features, step 1 will replace the `False`-typed `(if ...) == resource.owner` with value `false`, transforming the policy to be `permit(principal,action,resource) when { false || resource.isPublic }`. Since this policy does not require union types and otherwise meets strict mode restrictions, it is accepted in step 3. + +In sum: To see why the second case is acceptable, we have to understand the interaction between permissive mode and strict mode. This is subtle and difficult to explain. Instead, we want to implement strict mode as a standalone feature, which does not depend on features only present in permissive mode. + +## Detailed design + +We propose to change strict-mode validation so that it has the following features taken from permissive mode: +* singleton boolean `True`/`False` types (which have 1/ special consideration of them with `&&`, `||`, and conditionals, and 2/ subtyping between them and `Boolean`, as is done now for permissive mode). +* depth subtyping, but not width subtyping, to support examples like `{ foo: True } <: { foo: bool }`. +* a requirement that arguments to `==` have the same type _unless_ we know that comparison will always be false, in which case we can give the `==` type `False`. The same goes for `contains`, `containsAll`, and other constructs that use `==` under the covers. +* a requirement that branches of a conditional have the same type _unless_ we can simplify the conditional due to the guard having a `True`/`False` type. +* (no union types) + +The current way we implement strict mode will change to accommodate these additions. We propose the following: + +1. Change the Rust code to implement strict mode by reusing the logic of permissive mode​ and using a flag to perform more restrictive checks. For example, when given `User` and `Admin` entity types, the code performing the least-upper-bound computation will return union type `User|Admin` in permissive mode, and will fail in strict mode. And, the code for conditionals would force branches' types to match in strict mode, but not in permissive mode. Etc. +2. When checking in strict mode, we construct a new AST that performs the needed transformations, as in step 2 today. +3. Either way, we can add type annotations. For strict mode, they could be added during the transformation; for permissive mode, no transformation is needed. No checking is done after annotations are added, since the checking is always done, regardless of mode, prior to the transformation. + +Permissive mode validation considers different `Action`s to have distinct types, e.g., `Action::"view"` and `Action::"update"` don't have the same type. This is in anticipation supporting distinct actions having distinct attribute sets. Today, the least upper bound of any two actions is the type _AnyEntity_, which is a general supertype of all entities, used internally. Such a type supports expressions that are found in the policy scope such as `action in [Action::"view", Action::"edit"]`. This expression typechecks because the least upper bound of `Action::"view"` and `Action::"edit"` is _AnyEntity_ so the expression is type `Set<`_AnyEntity_`>`. Therefore in our amended strict mode we either need to: +1. Support _AnyEntity_ as part of depth subtyping. +2. Stop giving different `Action` entities different types, and if/when they support `Action` attributes we force them to share the same overall type (using optional attributes where different actions differ). + +## Drawbacks + +The main drawback of this approach is that strict-mode validation will be more restrictive. This is by design: Policies like the one in the motivating example will be rejected where before they were accepted. Accepting this RFC means we are prioritizing understandability over precision under the assumption that the lost precision will not be missed (e.g., since users wouldn't have expected to get it anyway). + +A secondary drawback is that this will result in a non-trivial, and backwards-incompatible code change. + +## Alternatives + +The proposal is, we believe, the minimal change to make strict mode self-contained, but not too different from what was there before. It also should not result in pervasive changes to the existing code. Alternative designs we considered (e.g., allowing more permissive mode features in strict mode) would be more invasive. + +## Unresolved questions + +See the discussion above about sets of `Action` entities. \ No newline at end of file diff --git a/text/policy.cedar b/text/policy.cedar new file mode 100644 index 00000000..05e20d5a --- /dev/null +++ b/text/policy.cedar @@ -0,0 +1,8 @@ +permit( + principal, + action == Action::"read", + resource) +when { + (if context.sudo then Admin::"root" else principal) == resource.owner || + resource.isPublic +}; diff --git a/text/schema.cedarschema.json b/text/schema.cedarschema.json new file mode 100644 index 00000000..1e5153e6 --- /dev/null +++ b/text/schema.cedarschema.json @@ -0,0 +1,43 @@ +{ + "": { + "entityTypes": { + "User": {}, + "Org": {}, + "Admin": {}, + "Object": { + "shape": { + "type": "Record", + "attributes": { + "owner": { + "type": "Entity", + "name": "Org" + }, + "isPublic": { + "type": "Boolean" + } + } + } + } + }, + "actions": { + "read": { + "appliesTo": { + "principalTypes": [ + "User" + ], + "resourceTypes": [ + "Object" + ], + "context": { + "type": "Record", + "attributes": { + "sudo": { + "type": "Boolean" + } + } + } + } + } + } + } +} \ No newline at end of file From 1f2b69470a6fb4e0461796301a7c99fc45e0a18b Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Tue, 11 Jul 2023 16:53:07 -0400 Subject: [PATCH 02/10] Title --- text/0019-stricter-validation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index ae8a05be..2826b541 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -1,4 +1,4 @@ -# RFC Template (Fill in your title here) +# Standalone strict validation ## Related issues and PRs From 3d3693f91a40681b302d5070298be52cd523a388 Mon Sep 17 00:00:00 2001 From: John Kastner Date: Mon, 31 Jul 2023 18:26:56 +0000 Subject: [PATCH 03/10] Update RFC --- text/.0019-stricter-validation.md.swp | Bin 0 -> 20480 bytes text/0019-stricter-validation.md | 107 +++++++++++++++++++----- text/{ => 0019}/policy.cedar | 0 text/{ => 0019}/schema.cedarschema.json | 0 4 files changed, 86 insertions(+), 21 deletions(-) create mode 100644 text/.0019-stricter-validation.md.swp rename text/{ => 0019}/policy.cedar (100%) rename text/{ => 0019}/schema.cedarschema.json (100%) diff --git a/text/.0019-stricter-validation.md.swp b/text/.0019-stricter-validation.md.swp new file mode 100644 index 0000000000000000000000000000000000000000..86e8c37ab522ee8d9005761d8220aec0bc9e2224 GIT binary patch literal 20480 zcmeI3-;X3!6~_w}6&3t}@c|$7G8mX4-90lqiMj)e85UO8xU$)ul_-*_n(o`v#a34} zRn^lwxCn1XdGkTzKY>c(k7p9WnCPn-AQ7H@@l6vS{G4-d{g@x%8ci^!CVMl})m8VN z`#tA;&yQQXyY}@97tNW$TENf8g5Yz%eP#6cEx!ux{$vn5eJv`=)aLTlyZwypet%S4 z>sR;p*Q5T%#@dbI*2nbqI6_ zbO>|^bO>|^bO>|^bO>|^{9hnY&Q1l-vy)r>ZdU#8TaNs`&3~?bYZ1Y<>b_I{`z8PT z==c6|_p3voL!d*TL!d*TL!d*TL!d*TL!d*TL!d*TL*P9?AmV`iv#k3!S)23!s{ViL zqe1Xz#;c59Gk(hW5#xu9?=!x~m@%GYe1);eIKvn)`i#5o41$j{PBCs}ym&_te3$V& zW5&45ILCO1@z)Or!JCZN8Gm5>A&WSM-g7{xlm|)4Wt*7I6{;_ugwBwPh41c4S7ji1*SUxR9D+ zKHW6inJKI_i^+j0Czij5SvoSqsIVq3Of($YSsCpnwr3XBOrm{j%FN8ukM?X4jSrYg03``7|zym-BfogA21ZVQ<+J|_M^0XquNax`Y+0?cp{rF%dl2o5K98m;t9$ZXj> zAKF2-;LVay@k|!c0jrHoc`&mkd_3O^2j;54c@(jp&K54mV>1{GR?OM6=IDe##HB)D zpRo5LPWKX9^2tqpK1vG9^xKoDeEWqT7wBdf%~7m~Sx+1a((P&7!&eKN-`E;W<1{qO zOQC!WO_rO`U0YgFjp_C3HlT~k7>tKeYErw;o_4LV&&;Dl6snsw)lCEQNLEf%l%2zZ z@0id@ZkC_m#|jhP=EsgazM|d{N%WR z<@FN^DS9Tx;VPy91DsF6+Gu=k978tBN#e=~d^4`47VDg-WiGYZpM>r$<=n&2WCs?$vsrJuNe zd7kBk*@Hw=6YXaE7EHGJBIh+Tj2YO}{2iLdxSy{b(+Q_>dt=f^Zxxa?vnVfxeWP5= zRo+iKdYdd*Gp`f6oa96gQCP8Q)>o_0p-SxAq z<85y1$~F!pq#;iHpekZx74EgeYwj7jZlXQH2KF+|Fw5H1h(q~2u>}Y|GRNY^E!qy3 z#8{S8+fRm$zz6!?p8xx4&<>wk9_Y(^tM72bieQ|?#GUmGrJp6(eJNBEyg8F~(cqAo zh#C0px18i2I31W4L`g9bBQYE5#hu#5B7uFXgoQn6=yqXhWcq!@t9}fE&Ml#m=OqT) zTr5UW?kURUB$KeA@J^!xozwHW$ia09X(3=A3V1A2Wcc^}IK%weXTfF<|AntBIgo3L zue8mh$vDsyPJ^{TJ;$bQT-EzIETZJ9`;44St-TPRS%szDJ~66Ym+*w~I9v^ZIpvp? zfLWyr62*#aYRhh8p_sY}Q#Z`qAgTq-R^20n5Ckt4lroww|{a_+YH^p2JmR zN%~rf>3QG9F2dHvOyPs9*ThrU?KI z`8!Xk$iIH%X87McLA8_3laWgTU8W=zj&L>vLEI;J?2t1^`LW~e&?PQ0iMo^yxG3cU z_%wUc8+vA!*n&-?5gd-pfXNOFIloM<<`G4J2%xcTEQe5Uy=;vG&qVcb()MSgRepjxbgVpDI6XiH%WqrV{4);q<#Zq0f>WtoPSG-#@)}dPC>lhE*k4 z%H$WSYR+xq(&go1MW4THH5L&7E)>Pwl49tymu-SLBu#ozH+$)F!B>U_tK!eY=qV6; z4y68<^Z(DtK|b|=b$UjE5NoHTplO&;LYi{zt}_ zsLjtaKE=43@fJ1uON=*oY2bCn?-{>ite*;kHO6nK-Ctw;lJN^hfebn0n~ZNTM5a$O z-ou|OByvK>qqrE(T~(<$r(~X3bs<^2M0rPZl#RaJbGC9d75+{3QOh%EN|O3 zCzJ!XwKitH z<-0VvrWxhYVmBiHg>E#z(SYL1%xa4fTTc6=^!qV2p!$nEvxxFh(I@U@(;1#86ewHu zx?tsPP?&;xvkLmx1)>>Rjp(UV%Q}S}D;QLeYENM9%0B8C5?CJPACcanxoIv*?JE5P ztt0MHsudGKPEaVKDJlaaJiw*8 z%P#n53JqS~o=1aZBd1HFs``Tsl3-u)a_nrS2ZR<>up>P_DO81th{Y6x(my zYpyOYMnffH5J)1{p^(Z3EGZFZ?}zb1$&sg0B$n)|9p%e^9y zX{oKMsc^aoQ>Gn?H6WMG^-h#2Hd95Ep1~WWCsJjnVhWIrFYEk%idGxYlb=}PSVi-! z;Y*8Rm?2N0a}*|Y!iteRxmD%t3VP4fpDhLT(o@I%tj;171Li8MY3nQrkR@I1#JrI6;LOO@d zjM8ST!>r_Xz50Fp6rThU*Io1tektUt{)Bp?>shcpRfmY~m#FMR?Y^(9(08mL>BO8qo=}fZ zM5MLU>JT69yo1`2-MJJ+pB-~*<#4TaMHo*>18afAA|YPa03*-ynG~0aQm$EIi~Akf z3P#hYl*HwT{;RC=xHLFdIrQ1kaGq;#Oe#78$;moY!JCAZ^dp;MqEbO2G|dL=+;!_P zN=Z7j2-FRYGoL&XlpZk4_*JW~zQQGGAZx>255Lqpt1T)Ww~_G2b(oPxX5|8oLBwlz zGgiD>x)90}Th^WEVvaM<*Qa0}hdnt4 z6r%}!QBlzHtN-3g57cuVKDkH&dy-Cy>iA4^4!Si3 zaf|$4cO<(iK9bL z_M%k5`-qp5(9^me32n%`SRVD85bDcPlrHk&QcEd73m4e>or45mtmUMnPTq_e}6# xS|^uN-MS&B2f@6}N4IxITZ-=SyS&$)NWWSIWPfZ$T4PA-UJIvhbYyFT;GZ2*g1!I% literal 0 HcmV?d00001 diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index 2826b541..971ef977 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -2,15 +2,15 @@ ## Related issues and PRs -- Reference Issues: -- Implementation PR(s): +- Reference Issues: +- Implementation PR(s): ## Timeline - Start Date: 11-07-2023 -- Date Entered FCP: +- Date Entered FCP: - Date Accepted: -- Date Landed: +- Date Landed: ## Summary @@ -18,22 +18,22 @@ Internally, strict validation of a policy is implemented as 1/ checking and tran ## Motivation -Consider this policy, given in file [`policy.cedar`](policy.cedar), where `principal` is always of type `User`: +Consider this policy, given in file [`policy.cedar`](./0019/policy.cedar), where `principal` is always of type `User`: ``` permit( principal, action == Action::"read", - resource) + resource) when { (if context.sudo then Admin::"root" else principal) == resource.owner || resource.isPublic } ``` -If we validate this policy against the schema [`schema.cedarschema.json`](schema.cedarschema.json), then `resource.owner` is always of type `User`. As a result, the policy is rejected by strict-mode validation, with two errors: +If we validate this policy against the schema [`schema.cedarschema.json`](./0019/schema.cedarschema.json), then `resource.owner` is always of type `User`. As a result, the policy is rejected by strict-mode validation, with two errors: 1. the `if`/`then`/`else` is trying to return entity type `Admin` in the true branch, and entity type `User` on the false branch, and these two are not equal. 1. since `resource.owner` has type `User`, it will have a type different than that returned by the `if`/`then`/`else`, which can sometimes return `Admin`. -But if we change `"User"` in [`schema.cedarschema.json`](schema.cedarschema.json) on line 13 to `"Org"`, then `resource.owner` is always of type `Org`. As a result, the policy is accepted! The two error conditions given above seem not to have changed -- the conditional returns different types, and those types may not equal the type of `resource.owner` -- so it's puzzling what changed to make the policy acceptable. +But if we change `"User"` in [`schema.cedarschema.json`](./0019/schema.cedarschema.json) on line 13 to `"Org"`, then `resource.owner` is always of type `Org`. As a result, the policy is accepted! The two error conditions given above seem not to have changed -- the conditional returns different types, and those types may not equal the type of `resource.owner` -- so it's puzzling what changed to make the policy acceptable. The reason is that strict-mode validation is dependent on permissive-mode validation. In particular, strict-mode validation is implemented in three steps: 1/ validate and transform the policy using permissive mode; 2/ annotate the transformed policy AST with types; and 3/ check the types against more restrictive rules. @@ -46,21 +46,90 @@ In sum: To see why the second case is acceptable, we have to understand the inte ## Detailed design We propose to change strict-mode validation so that it has the following features taken from permissive mode: -* singleton boolean `True`/`False` types (which have 1/ special consideration of them with `&&`, `||`, and conditionals, and 2/ subtyping between them and `Boolean`, as is done now for permissive mode). -* depth subtyping, but not width subtyping, to support examples like `{ foo: True } <: { foo: bool }`. -* a requirement that arguments to `==` have the same type _unless_ we know that comparison will always be false, in which case we can give the `==` type `False`. The same goes for `contains`, `containsAll`, and other constructs that use `==` under the covers. -* a requirement that branches of a conditional have the same type _unless_ we can simplify the conditional due to the guard having a `True`/`False` type. -* (no union types) +* Singleton boolean `True`/`False` types (which have 1/ special consideration of them with `&&`, `||`, and conditionals, and 2/ subtyping between them and `Boolean`, as is done now for permissive mode). +* Depth subtyping, but not width subtyping, to support examples like `{ foo: True } <: { foo: bool }`. + +Strict-mode validation will continue to apply the restriction it currently applies: +* Arguments to `==` must have the compatibles types (i.e., an upper bound exists according to the strict - depth only - definitions of subtyping) _unless_ we know that comparison will always be false, in which case we can give the `==` type `False`. The same goes for `contains`, `containsAll`, and `containsAny`. +* Arguments to an `in` expression must be compatible with the entity type hierarchy, or we must know that the comparison is always false. +* Branches of a conditional must have compatible types _unless_ we can simplify the conditional due to the guard having a `True`/`False` type. +* The elements of a set must have compatible types. +* As a consequence of the two prior restrictions, union types cannot be constructed. +* Empty set literals may not exist in a policy because we do not currently infer the type of the elements of an empty set. +* Extension type constructors may only be applied to literals. The current way we implement strict mode will change to accommodate these additions. We propose the following: 1. Change the Rust code to implement strict mode by reusing the logic of permissive mode​ and using a flag to perform more restrictive checks. For example, when given `User` and `Admin` entity types, the code performing the least-upper-bound computation will return union type `User|Admin` in permissive mode, and will fail in strict mode. And, the code for conditionals would force branches' types to match in strict mode, but not in permissive mode. Etc. -2. When checking in strict mode, we construct a new AST that performs the needed transformations, as in step 2 today. +2. When checking in strict mode, we construct a new AST that performs the needed transformations, as in step 2 today. 3. Either way, we can add type annotations. For strict mode, they could be added during the transformation; for permissive mode, no transformation is needed. No checking is done after annotations are added, since the checking is always done, regardless of mode, prior to the transformation. -Permissive mode validation considers different `Action`s to have distinct types, e.g., `Action::"view"` and `Action::"update"` don't have the same type. This is in anticipation supporting distinct actions having distinct attribute sets. Today, the least upper bound of any two actions is the type _AnyEntity_, which is a general supertype of all entities, used internally. Such a type supports expressions that are found in the policy scope such as `action in [Action::"view", Action::"edit"]`. This expression typechecks because the least upper bound of `Action::"view"` and `Action::"edit"` is _AnyEntity_ so the expression is type `Set<`_AnyEntity_`>`. Therefore in our amended strict mode we either need to: -1. Support _AnyEntity_ as part of depth subtyping. -2. Stop giving different `Action` entities different types, and if/when they support `Action` attributes we force them to share the same overall type (using optional attributes where different actions differ). +### Actions + +Permissive mode validation considers different `Action`s to have distinct types, e.g., `Action::"view"` and `Action::"update"` don't have the same type. This is in anticipation of supporting distinct actions having distinct attribute sets. Today, the least upper bound of any two actions is the type _AnyEntity_, which is a general supertype of all entities, used internally. Such a type supports expressions that are found in the policy scope such as `action in [Action::"view", Action::"edit"]`. This expression typechecks because the least upper bound of `Action::"view"` and `Action::"edit"` is _AnyEntity_ so the expression is type `Set<`_AnyEntity_`>`. +However, these are different types which may have different attributes, so we need width subtyping to define an upper bound, but width subtyping is not supported by strict validation. + +We will resolve this issue by making all `Action` entities of a particular action entity type have the same type in both strict and permissive validation. +Actions having the same type would need to have the same attributes record type. +If the actions have the same type, then strict mode validation can let different actions occur in the same set. +Since actions do not _currently_ have attributes, this does not effect permissive policy typechecking today. +The restriction is that it would not be possible to declare one action with an attribute `{"foo": 1}` while another action has an attribute `{"foo": false}` + +### Template slots + +There are no restrictions on what entity type can be used to instantiate a slot in a template, so the permissive typechecker also uses `AnyEntity` here. +The only restriction on the type of a slot is that it must be instantiated with an entity type that exists in the schema. +Based on this, we will modify both permissive and strict validation to precisely typecheck a template by extending the query type environment to include a type environment for template slots. +In the same way that we typecheck a policy once for each possible binding for the types of `principal`, `action`, and `resource`, we will also typecheck a template once for every possible binding for the type of any slots in that template. + +Typechecking for every entity type may seem excessive, +but we know that a template slot can only occur in an `==` or `in` expression in the policy scope where the `principal` or `resource` is compared to the slot. +We will infer the type `False` for these expression if the slot is an entity type that cannot be `==` or `in` the principal or resource entity type, short-circuiting the rest of typechecking for that type environment. +Typechecking could be optimized by recognizing and ignoring type environments that will be `False` based only on the policy scope. + +For example, using the schema from the motivating example, the following template will typecheck. + +``` +permit(principal == ?principal, action == Action::"read", resource); +``` + +Using the usual request type environment construction, there is one environment `(User, Action::"read", Object)`. +Because this is a template containing `?principal`, we extend the environment with each possible type for the slot: `User`, `Org`, `Admin` and `Object`. +When typechecking, the validator sees `principal == ?principal && ...` first in every environment which is always an equality between two entity types. +The `principal` is always a `User` while `?principal` is one of the possible slot types depending on the type environment. +In every environment where `?principal` is not `User`, the equality has type `False`, causing the `&&` to short-circuit to type `False`, +The rest of the policy is typechecked as usual when `?principal` is `User`. + +This change to template typechecking does not introduce any new type errors and in fact will enable more precise typechecking if we expand where in a policy template slots may be used. + +### Unspecified principal/resource entity types + +The validator has a concept of an unspecified principal or resource entity type in an action `appliesTo` specification. +When `principalTypes` or `resourceTypes` is omitted, we interpret the schema as declaring that the action does not apply to any particular principal/resource entity type. +It instead applies to the "unspecified" principal or resource, which allows a users to make authorization requests using that action without providing the principal or resource, +or when providing an entity with any of the defined entity types as the principal or resource. +This is implemented by assigning the `AnyEntity` type to a variable when it is unspecified, +but this depends on width subtyping between entity types which we want to eliminate from strict validation. + +It is not possible to extend the set of type environments to handle this case in a way that does not use `AnyEntity`. +Constructing one type environment for each declared entity type does not soundly handle the case where an entity is _not_ provided in the query. +If some attribute exists for every declared entity type, then an access to that attribute would be permitted, but that attribute cannot be safely accessed if an entity is not used in the query. +We would need to further extend set of type environments to include an entity representing this case, +but, other than `AnyEntity`, we do not have a type that can represent the type of an unspecified entity. + +Instead, we observe that the existence of `AnyEntity` on it's own is not a problem for strict validation. +It is only a problem when it allows for construction of a union type representing multiple entity types. +We want to typecheck the policy with a distinct type environment for every entity type and for an unspecified entity. +For each query environment, we can over-approximate by instead using `AnyEntity` as the type of the query variable. +In each query environment, `AnyEntity` represents exactly one entity type, +and will always represent exactly one entity type as long as the least upper bound of `AnyEntity` with every type is not defined. + +If we approximate every type environment with `AnyEntity`, the different type environments are now identical, so we only need to typecheck once with this approximate type environment. +Using the `AnyEntity` types will cause the strict-mode validator to reject some expressions which might otherwise be well typed. +For example, `principal == User::"alice"` is well typed when `principal` is `User`, and for any other entity type for `principal`, including the unspecified entity type, the expression could have type `False`, but we will not accept it. +This is an acceptable for unspecified entities because we do not believe policies should in general be doing comparison with unspecified entities. +Of course, these comparisons are still supported by the permissive mode validator. +This same tradeoff is not acceptable for template slots: `principal == ?principal` must be accepted by the strict mode validator. ## Drawbacks @@ -71,7 +140,3 @@ A secondary drawback is that this will result in a non-trivial, and backwards-in ## Alternatives The proposal is, we believe, the minimal change to make strict mode self-contained, but not too different from what was there before. It also should not result in pervasive changes to the existing code. Alternative designs we considered (e.g., allowing more permissive mode features in strict mode) would be more invasive. - -## Unresolved questions - -See the discussion above about sets of `Action` entities. \ No newline at end of file diff --git a/text/policy.cedar b/text/0019/policy.cedar similarity index 100% rename from text/policy.cedar rename to text/0019/policy.cedar diff --git a/text/schema.cedarschema.json b/text/0019/schema.cedarschema.json similarity index 100% rename from text/schema.cedarschema.json rename to text/0019/schema.cedarschema.json From 830bc75928a4c5c45bbe3127fc8d52badd51aae7 Mon Sep 17 00:00:00 2001 From: John Kastner Date: Mon, 31 Jul 2023 19:01:22 +0000 Subject: [PATCH 04/10] text --- text/0019-stricter-validation.md | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index 971ef977..fd907501 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -117,8 +117,9 @@ If some attribute exists for every declared entity type, then an access to that We would need to further extend set of type environments to include an entity representing this case, but, other than `AnyEntity`, we do not have a type that can represent the type of an unspecified entity. -Instead, we observe that the existence of `AnyEntity` on it's own is not a problem for strict validation. -It is only a problem when it allows for construction of a union type representing multiple entity types. +Instead, we observe that the existence of `AnyEntity` on it's own is not a problem for strict validation, +so we _can_ in fact use it as the type of an unspecified entity in strict mode validation. +The `AnyEntity` type is only a problem when it allows for construction of a union type representing multiple entity types. We want to typecheck the policy with a distinct type environment for every entity type and for an unspecified entity. For each query environment, we can over-approximate by instead using `AnyEntity` as the type of the query variable. In each query environment, `AnyEntity` represents exactly one entity type, From 6b399ab784105efc2285f269e28161776466522f Mon Sep 17 00:00:00 2001 From: John Kastner Date: Mon, 31 Jul 2023 19:01:55 +0000 Subject: [PATCH 05/10] rm swp --- text/.0019-stricter-validation.md.swp | Bin 20480 -> 0 bytes 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 text/.0019-stricter-validation.md.swp diff --git a/text/.0019-stricter-validation.md.swp b/text/.0019-stricter-validation.md.swp deleted file mode 100644 index 86e8c37ab522ee8d9005761d8220aec0bc9e2224..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 20480 zcmeI3-;X3!6~_w}6&3t}@c|$7G8mX4-90lqiMj)e85UO8xU$)ul_-*_n(o`v#a34} zRn^lwxCn1XdGkTzKY>c(k7p9WnCPn-AQ7H@@l6vS{G4-d{g@x%8ci^!CVMl})m8VN z`#tA;&yQQXyY}@97tNW$TENf8g5Yz%eP#6cEx!ux{$vn5eJv`=)aLTlyZwypet%S4 z>sR;p*Q5T%#@dbI*2nbqI6_ zbO>|^bO>|^bO>|^bO>|^{9hnY&Q1l-vy)r>ZdU#8TaNs`&3~?bYZ1Y<>b_I{`z8PT z==c6|_p3voL!d*TL!d*TL!d*TL!d*TL!d*TL!d*TL*P9?AmV`iv#k3!S)23!s{ViL zqe1Xz#;c59Gk(hW5#xu9?=!x~m@%GYe1);eIKvn)`i#5o41$j{PBCs}ym&_te3$V& zW5&45ILCO1@z)Or!JCZN8Gm5>A&WSM-g7{xlm|)4Wt*7I6{;_ugwBwPh41c4S7ji1*SUxR9D+ zKHW6inJKI_i^+j0Czij5SvoSqsIVq3Of($YSsCpnwr3XBOrm{j%FN8ukM?X4jSrYg03``7|zym-BfogA21ZVQ<+J|_M^0XquNax`Y+0?cp{rF%dl2o5K98m;t9$ZXj> zAKF2-;LVay@k|!c0jrHoc`&mkd_3O^2j;54c@(jp&K54mV>1{GR?OM6=IDe##HB)D zpRo5LPWKX9^2tqpK1vG9^xKoDeEWqT7wBdf%~7m~Sx+1a((P&7!&eKN-`E;W<1{qO zOQC!WO_rO`U0YgFjp_C3HlT~k7>tKeYErw;o_4LV&&;Dl6snsw)lCEQNLEf%l%2zZ z@0id@ZkC_m#|jhP=EsgazM|d{N%WR z<@FN^DS9Tx;VPy91DsF6+Gu=k978tBN#e=~d^4`47VDg-WiGYZpM>r$<=n&2WCs?$vsrJuNe zd7kBk*@Hw=6YXaE7EHGJBIh+Tj2YO}{2iLdxSy{b(+Q_>dt=f^Zxxa?vnVfxeWP5= zRo+iKdYdd*Gp`f6oa96gQCP8Q)>o_0p-SxAq z<85y1$~F!pq#;iHpekZx74EgeYwj7jZlXQH2KF+|Fw5H1h(q~2u>}Y|GRNY^E!qy3 z#8{S8+fRm$zz6!?p8xx4&<>wk9_Y(^tM72bieQ|?#GUmGrJp6(eJNBEyg8F~(cqAo zh#C0px18i2I31W4L`g9bBQYE5#hu#5B7uFXgoQn6=yqXhWcq!@t9}fE&Ml#m=OqT) zTr5UW?kURUB$KeA@J^!xozwHW$ia09X(3=A3V1A2Wcc^}IK%weXTfF<|AntBIgo3L zue8mh$vDsyPJ^{TJ;$bQT-EzIETZJ9`;44St-TPRS%szDJ~66Ym+*w~I9v^ZIpvp? zfLWyr62*#aYRhh8p_sY}Q#Z`qAgTq-R^20n5Ckt4lroww|{a_+YH^p2JmR zN%~rf>3QG9F2dHvOyPs9*ThrU?KI z`8!Xk$iIH%X87McLA8_3laWgTU8W=zj&L>vLEI;J?2t1^`LW~e&?PQ0iMo^yxG3cU z_%wUc8+vA!*n&-?5gd-pfXNOFIloM<<`G4J2%xcTEQe5Uy=;vG&qVcb()MSgRepjxbgVpDI6XiH%WqrV{4);q<#Zq0f>WtoPSG-#@)}dPC>lhE*k4 z%H$WSYR+xq(&go1MW4THH5L&7E)>Pwl49tymu-SLBu#ozH+$)F!B>U_tK!eY=qV6; z4y68<^Z(DtK|b|=b$UjE5NoHTplO&;LYi{zt}_ zsLjtaKE=43@fJ1uON=*oY2bCn?-{>ite*;kHO6nK-Ctw;lJN^hfebn0n~ZNTM5a$O z-ou|OByvK>qqrE(T~(<$r(~X3bs<^2M0rPZl#RaJbGC9d75+{3QOh%EN|O3 zCzJ!XwKitH z<-0VvrWxhYVmBiHg>E#z(SYL1%xa4fTTc6=^!qV2p!$nEvxxFh(I@U@(;1#86ewHu zx?tsPP?&;xvkLmx1)>>Rjp(UV%Q}S}D;QLeYENM9%0B8C5?CJPACcanxoIv*?JE5P ztt0MHsudGKPEaVKDJlaaJiw*8 z%P#n53JqS~o=1aZBd1HFs``Tsl3-u)a_nrS2ZR<>up>P_DO81th{Y6x(my zYpyOYMnffH5J)1{p^(Z3EGZFZ?}zb1$&sg0B$n)|9p%e^9y zX{oKMsc^aoQ>Gn?H6WMG^-h#2Hd95Ep1~WWCsJjnVhWIrFYEk%idGxYlb=}PSVi-! z;Y*8Rm?2N0a}*|Y!iteRxmD%t3VP4fpDhLT(o@I%tj;171Li8MY3nQrkR@I1#JrI6;LOO@d zjM8ST!>r_Xz50Fp6rThU*Io1tektUt{)Bp?>shcpRfmY~m#FMR?Y^(9(08mL>BO8qo=}fZ zM5MLU>JT69yo1`2-MJJ+pB-~*<#4TaMHo*>18afAA|YPa03*-ynG~0aQm$EIi~Akf z3P#hYl*HwT{;RC=xHLFdIrQ1kaGq;#Oe#78$;moY!JCAZ^dp;MqEbO2G|dL=+;!_P zN=Z7j2-FRYGoL&XlpZk4_*JW~zQQGGAZx>255Lqpt1T)Ww~_G2b(oPxX5|8oLBwlz zGgiD>x)90}Th^WEVvaM<*Qa0}hdnt4 z6r%}!QBlzHtN-3g57cuVKDkH&dy-Cy>iA4^4!Si3 zaf|$4cO<(iK9bL z_M%k5`-qp5(9^me32n%`SRVD85bDcPlrHk&QcEd73m4e>or45mtmUMnPTq_e}6# xS|^uN-MS&B2f@6}N4IxITZ-=SyS&$)NWWSIWPfZ$T4PA-UJIvhbYyFT;GZ2*g1!I% From b9461ebd6c7539a69b6c8da81d02c8dc89d6bdfc Mon Sep 17 00:00:00 2001 From: John Kastner Date: Fri, 4 Aug 2023 21:09:16 +0000 Subject: [PATCH 06/10] Unspecifed --- text/0019-stricter-validation.md | 25 ++----------------------- 1 file changed, 2 insertions(+), 23 deletions(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index fd907501..5c430979 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -106,31 +106,10 @@ This change to template typechecking does not introduce any new type errors and The validator has a concept of an unspecified principal or resource entity type in an action `appliesTo` specification. When `principalTypes` or `resourceTypes` is omitted, we interpret the schema as declaring that the action does not apply to any particular principal/resource entity type. -It instead applies to the "unspecified" principal or resource, which allows a users to make authorization requests using that action without providing the principal or resource, -or when providing an entity with any of the defined entity types as the principal or resource. +It instead applies to the "unspecified" principal or resource, which allows a users to make authorization requests using that action without providing the principal or resource. This is implemented by assigning the `AnyEntity` type to a variable when it is unspecified, but this depends on width subtyping between entity types which we want to eliminate from strict validation. - -It is not possible to extend the set of type environments to handle this case in a way that does not use `AnyEntity`. -Constructing one type environment for each declared entity type does not soundly handle the case where an entity is _not_ provided in the query. -If some attribute exists for every declared entity type, then an access to that attribute would be permitted, but that attribute cannot be safely accessed if an entity is not used in the query. -We would need to further extend set of type environments to include an entity representing this case, -but, other than `AnyEntity`, we do not have a type that can represent the type of an unspecified entity. - -Instead, we observe that the existence of `AnyEntity` on it's own is not a problem for strict validation, -so we _can_ in fact use it as the type of an unspecified entity in strict mode validation. -The `AnyEntity` type is only a problem when it allows for construction of a union type representing multiple entity types. -We want to typecheck the policy with a distinct type environment for every entity type and for an unspecified entity. -For each query environment, we can over-approximate by instead using `AnyEntity` as the type of the query variable. -In each query environment, `AnyEntity` represents exactly one entity type, -and will always represent exactly one entity type as long as the least upper bound of `AnyEntity` with every type is not defined. - -If we approximate every type environment with `AnyEntity`, the different type environments are now identical, so we only need to typecheck once with this approximate type environment. -Using the `AnyEntity` types will cause the strict-mode validator to reject some expressions which might otherwise be well typed. -For example, `principal == User::"alice"` is well typed when `principal` is `User`, and for any other entity type for `principal`, including the unspecified entity type, the expression could have type `False`, but we will not accept it. -This is an acceptable for unspecified entities because we do not believe policies should in general be doing comparison with unspecified entities. -Of course, these comparisons are still supported by the permissive mode validator. -This same tradeoff is not acceptable for template slots: `principal == ?principal` must be accepted by the strict mode validator. +Instead of treating it as `AnyEntity`, we will instead treat it more precisely as some specific entity type that is not equal to any other entity type. ## Drawbacks From 8d9acd06eebdfed8e82a16d35459ddd962aa057a Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Wed, 9 Aug 2023 11:38:46 -0400 Subject: [PATCH 07/10] Wording updates for clarity --- text/0019-stricter-validation.md | 33 ++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index 5c430979..8f5c4cb8 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -69,18 +69,23 @@ The current way we implement strict mode will change to accommodate these additi Permissive mode validation considers different `Action`s to have distinct types, e.g., `Action::"view"` and `Action::"update"` don't have the same type. This is in anticipation of supporting distinct actions having distinct attribute sets. Today, the least upper bound of any two actions is the type _AnyEntity_, which is a general supertype of all entities, used internally. Such a type supports expressions that are found in the policy scope such as `action in [Action::"view", Action::"edit"]`. This expression typechecks because the least upper bound of `Action::"view"` and `Action::"edit"` is _AnyEntity_ so the expression is type `Set<`_AnyEntity_`>`. However, these are different types which may have different attributes, so we need width subtyping to define an upper bound, but width subtyping is not supported by strict validation. -We will resolve this issue by making all `Action` entities of a particular action entity type have the same type in both strict and permissive validation. -Actions having the same type would need to have the same attributes record type. -If the actions have the same type, then strict mode validation can let different actions occur in the same set. -Since actions do not _currently_ have attributes, this does not effect permissive policy typechecking today. -The restriction is that it would not be possible to declare one action with an attribute `{"foo": 1}` while another action has an attribute `{"foo": false}` +We will resolve this issue by making all `Action` entities have one type -- `Action` -- in both strict and permissive validation. +Doing so means that expressions like `[Action::"view", Action::"edit"]` have type `Set` and thus do not need width subtyping to be well-typed. +Moreover, expressions like `if principal.isAdmin then Action::"edit" else Action::"editLimited"` will now typecheck in strict mode, since both branches have the same type (`Action`). + +A drawback of this change is that if we allow action entities to have attributes in the future, all of them must be typeable with the same record type. +For action entities that have an attribute that others do not, the attribute can be made optional. +However, two entities would not be able to have the same attribute at _different_ types, e.g., `{ foo: String }` vs. `{ foo: Long }`. +Arguably, this restriction is clearer and more intuitive than what would have been allowed before. ### Template slots -There are no restrictions on what entity type can be used to instantiate a slot in a template, so the permissive typechecker also uses `AnyEntity` here. +There are no restrictions on what entity type can be used to instantiate a slot in a template, so the permissive typechecker also uses _AnyEntity_ here. The only restriction on the type of a slot is that it must be instantiated with an entity type that exists in the schema. -Based on this, we will modify both permissive and strict validation to precisely typecheck a template by extending the query type environment to include a type environment for template slots. -In the same way that we typecheck a policy once for each possible binding for the types of `principal`, `action`, and `resource`, we will also typecheck a template once for every possible binding for the type of any slots in that template. + +Because _AnyEntity_ cannot be used in strict validation, we will modify both permissive and strict validation to precisely typecheck a template by extending the query type environment to include a type environment for template slots. + +In the same way that we typecheck a policy once for each possible binding for the types of `principal` and `resource` for a given action, we will also typecheck a template once for every possible binding for the type of any slots in that template. Typechecking for every entity type may seem excessive, but we know that a template slot can only occur in an `==` or `in` expression in the policy scope where the `principal` or `resource` is compared to the slot. @@ -97,7 +102,7 @@ Using the usual request type environment construction, there is one environment Because this is a template containing `?principal`, we extend the environment with each possible type for the slot: `User`, `Org`, `Admin` and `Object`. When typechecking, the validator sees `principal == ?principal && ...` first in every environment which is always an equality between two entity types. The `principal` is always a `User` while `?principal` is one of the possible slot types depending on the type environment. -In every environment where `?principal` is not `User`, the equality has type `False`, causing the `&&` to short-circuit to type `False`, +In every environment where `?principal` is not `User`, the equality has type `False`, causing the `&&` to short-circuit to type `False`. The rest of the policy is typechecked as usual when `?principal` is `User`. This change to template typechecking does not introduce any new type errors and in fact will enable more precise typechecking if we expand where in a policy template slots may be used. @@ -105,11 +110,11 @@ This change to template typechecking does not introduce any new type errors and ### Unspecified principal/resource entity types The validator has a concept of an unspecified principal or resource entity type in an action `appliesTo` specification. -When `principalTypes` or `resourceTypes` is omitted, we interpret the schema as declaring that the action does not apply to any particular principal/resource entity type. -It instead applies to the "unspecified" principal or resource, which allows a users to make authorization requests using that action without providing the principal or resource. -This is implemented by assigning the `AnyEntity` type to a variable when it is unspecified, -but this depends on width subtyping between entity types which we want to eliminate from strict validation. -Instead of treating it as `AnyEntity`, we will instead treat it more precisely as some specific entity type that is not equal to any other entity type. +When `principalTypes` or `resourceTypes` is omitted from the schema for a given action, we interpret the schema as declaring that the action does not apply to any particular principal/resource entity type. +It instead applies to the _unspecified_ principal or resource, which allows users to make authorization requests for that action without providing a specific principal or resource entity. This is implemented now by assigning the _AnyEntity_ type to a variable when it is unspecified, but doing so is not possible in strict validation due to its lack of width subtyping. + +To resolve this issue, both permissive and strict validation will no longer type an unspecified principal/resource as _AnyEntity_, and instead treat it more precisely as some _specific but not named_ entity type that is _not equal to any other entity type_. +This change essentially matches what was the intended semantics of the unspecified entity all along: It shouldn't matter which entity you pass in, policy evaluation will always behave the same. ## Drawbacks From 57f97d82529b7399014689b65222ae1c66bbef04 Mon Sep 17 00:00:00 2001 From: Mike Hicks Date: Wed, 9 Aug 2023 13:11:28 -0400 Subject: [PATCH 08/10] rewording to clarify the impact of the more complex changes --- text/0019-stricter-validation.md | 67 ++++++++++++++++++++++---------- 1 file changed, 46 insertions(+), 21 deletions(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index 8f5c4cb8..69a80d03 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -47,7 +47,7 @@ In sum: To see why the second case is acceptable, we have to understand the inte We propose to change strict-mode validation so that it has the following features taken from permissive mode: * Singleton boolean `True`/`False` types (which have 1/ special consideration of them with `&&`, `||`, and conditionals, and 2/ subtyping between them and `Boolean`, as is done now for permissive mode). -* Depth subtyping, but not width subtyping, to support examples like `{ foo: True } <: { foo: bool }`. +* Depth subtyping, but not width subtyping, to support examples like `{ foo: True } <: { foo: Boolean }`. Strict-mode validation will continue to apply the restriction it currently applies: * Arguments to `==` must have the compatibles types (i.e., an upper bound exists according to the strict - depth only - definitions of subtyping) _unless_ we know that comparison will always be false, in which case we can give the `==` type `False`. The same goes for `contains`, `containsAll`, and `containsAny`. @@ -58,23 +58,28 @@ Strict-mode validation will continue to apply the restriction it currently appli * Empty set literals may not exist in a policy because we do not currently infer the type of the elements of an empty set. * Extension type constructors may only be applied to literals. -The current way we implement strict mode will change to accommodate these additions. We propose the following: - -1. Change the Rust code to implement strict mode by reusing the logic of permissive mode​ and using a flag to perform more restrictive checks. For example, when given `User` and `Admin` entity types, the code performing the least-upper-bound computation will return union type `User|Admin` in permissive mode, and will fail in strict mode. And, the code for conditionals would force branches' types to match in strict mode, but not in permissive mode. Etc. -2. When checking in strict mode, we construct a new AST that performs the needed transformations, as in step 2 today. -3. Either way, we can add type annotations. For strict mode, they could be added during the transformation; for permissive mode, no transformation is needed. No checking is done after annotations are added, since the checking is always done, regardless of mode, prior to the transformation. +Validating `Action` entities, template slots `?principal` and `?resource`, and unspecified `principal` and `resource` types must be done differently so as not to rely on the "top" entity type _AnyEntity_, which is essentially an infinite-width union type, used internally. +Next, we describe how we propose to handle these situations, in both permissive and strict validation. +Importantly, these changes all retain or even _improve_ precision compared to the status quo -- they will _not_ be the reason that policies that typechecked under the old strict mode no longer do. ### Actions -Permissive mode validation considers different `Action`s to have distinct types, e.g., `Action::"view"` and `Action::"update"` don't have the same type. This is in anticipation of supporting distinct actions having distinct attribute sets. Today, the least upper bound of any two actions is the type _AnyEntity_, which is a general supertype of all entities, used internally. Such a type supports expressions that are found in the policy scope such as `action in [Action::"view", Action::"edit"]`. This expression typechecks because the least upper bound of `Action::"view"` and `Action::"edit"` is _AnyEntity_ so the expression is type `Set<`_AnyEntity_`>`. -However, these are different types which may have different attributes, so we need width subtyping to define an upper bound, but width subtyping is not supported by strict validation. - -We will resolve this issue by making all `Action` entities have one type -- `Action` -- in both strict and permissive validation. -Doing so means that expressions like `[Action::"view", Action::"edit"]` have type `Set` and thus do not need width subtyping to be well-typed. -Moreover, expressions like `if principal.isAdmin then Action::"edit" else Action::"editLimited"` will now typecheck in strict mode, since both branches have the same type (`Action`). - -A drawback of this change is that if we allow action entities to have attributes in the future, all of them must be typeable with the same record type. -For action entities that have an attribute that others do not, the attribute can be made optional. +Permissive mode validation considers different `Action`s to have distinct types, e.g., `Action::"view"` and `Action::"update"` don't have the same type. +This is in anticipation of supporting distinct actions having distinct attribute sets. +The least upper bound of any two actions is the type _AnyEntity_. +Such a type supports expressions that are found in the policy scope such as `action in [Action::"view", Action::"edit"]`. +This expression typechecks because the least upper bound of `Action::"view"` and `Action::"edit"` is _AnyEntity_ so the expression is type `Set<`_AnyEntity_`>`. +Since _AnyEntity_ cannot be used in strict validation, the current code special-cases the above expression, treating it as equivalent to `action in Action::"view" || action in Action::"edit"`. +However, this approach is unsatisfying as it only supports literal sets of `Action` entities. + +It turns out we can resolve this issue by making all `Action` entities have one type -- `Action` -- in both strict and permissive validation. +This change strictly _adds_ precision to validation, compared to the status quo. +Expressions like `[Action::"view", Action::"edit"]` have type `Set` and thus do not need _AnyEntity_ to be well-typed. +Expressions like `if principal.isAdmin then Action::"edit" else Action::"editLimited"` will typecheck in strict validation, since both branches have the same type (`Action`). + +A possible drawback of this change is that it will not allow distinct actions to have distinct attribute sets (if indeed we add attributes to actions in the future). +Rather, all actions must be typeable with the same record type. +As a mitigation, for action entities that have an attribute that others do not, the attribute can be made optional. However, two entities would not be able to have the same attribute at _different_ types, e.g., `{ foo: String }` vs. `{ foo: Long }`. Arguably, this restriction is clearer and more intuitive than what would have been allowed before. @@ -82,9 +87,12 @@ Arguably, this restriction is clearer and more intuitive than what would have be There are no restrictions on what entity type can be used to instantiate a slot in a template, so the permissive typechecker also uses _AnyEntity_ here. The only restriction on the type of a slot is that it must be instantiated with an entity type that exists in the schema. +The strict validator today does not properly support validating templates, which is something we want to allow. Because _AnyEntity_ cannot be used in strict validation, we will modify both permissive and strict validation to precisely typecheck a template by extending the query type environment to include a type environment for template slots. +Doing so will strictly _improve_ precision for permissive validation; all templates that validated before will still do so after this change. +Here is how the change will work. In the same way that we typecheck a policy once for each possible binding for the types of `principal` and `resource` for a given action, we will also typecheck a template once for every possible binding for the type of any slots in that template. Typechecking for every entity type may seem excessive, @@ -105,22 +113,39 @@ The `principal` is always a `User` while `?principal` is one of the possible slo In every environment where `?principal` is not `User`, the equality has type `False`, causing the `&&` to short-circuit to type `False`. The rest of the policy is typechecked as usual when `?principal` is `User`. -This change to template typechecking does not introduce any new type errors and in fact will enable more precise typechecking if we expand where in a policy template slots may be used. +This change will match the precision of the validator today, and will enable more precise typechecking if we expand where in a policy template slots may be used. +In particular, if we allowed expressions like `?principal.foo == 2` in the condition of a policy, the above approach would allow us to know precisely that `?principal` will always have a `foo` attribute, whereas the current approach using _AnyEntity_ would not be able to. ### Unspecified principal/resource entity types The validator has a concept of an unspecified principal or resource entity type in an action `appliesTo` specification. When `principalTypes` or `resourceTypes` is omitted from the schema for a given action, we interpret the schema as declaring that the action does not apply to any particular principal/resource entity type. -It instead applies to the _unspecified_ principal or resource, which allows users to make authorization requests for that action without providing a specific principal or resource entity. This is implemented now by assigning the _AnyEntity_ type to a variable when it is unspecified, but doing so is not possible in strict validation due to its lack of width subtyping. +It instead applies to the _unspecified_ principal or resource, which allows users to make authorization requests for that action without providing a specific principal or resource entity. This is implemented now for permissive validation by assigning the _AnyEntity_ type to a variable when it is unspecified. +The strict validator currently handles the unspecified principal/resource types in an ad hoc manner. + +To resolve this issue, both permissive and strict validation will no longer type an unspecified principal/resource as _AnyEntity_, and instead treat it more precisely as some specific entity type that is _not equal to any other entity type_. +This change closely matches these semantics of authorization request processing using the unspecified entity type. +It also is more precise than using _AnyEntity_. +In particular, for an expression like `principal == User::"Alice"` in a policy, using _AnyEntity_ for the type of `principal` would give this expression the type `Boolean`. +But we know better: This expression will always evaluate to `false` when `principal` is unspecified in the request. +Giving `principal` an entity type not equal to any other type would allow us to type the expression as `False`, and therefore uncover that the policy containing this expression might never properly apply. -To resolve this issue, both permissive and strict validation will no longer type an unspecified principal/resource as _AnyEntity_, and instead treat it more precisely as some _specific but not named_ entity type that is _not equal to any other entity type_. -This change essentially matches what was the intended semantics of the unspecified entity all along: It shouldn't matter which entity you pass in, policy evaluation will always behave the same. +### Implementation details + +The current way we implement strict mode will change to accommodate these additions. We propose the following: + +1. Change the Rust code to implement strict mode by reusing the logic of permissive mode​ and using a flag to perform more restrictive checks. For example, when given `User` and `Admin` entity types, the code performing the least-upper-bound computation will return union type `User|Admin` in permissive mode, and will fail in strict mode. And, the code for conditionals would force branches' types to match in strict mode, but not in permissive mode. Etc. +2. When checking in strict mode, we construct a new AST that performs the needed transformations, as in step 2 today. +3. Either way, we can add type annotations. For strict mode, they could be added during the transformation; for permissive mode, no transformation is needed. No checking is done after annotations are added, since the checking is always done, regardless of mode, prior to the transformation. ## Drawbacks -The main drawback of this approach is that strict-mode validation will be more restrictive. This is by design: Policies like the one in the motivating example will be rejected where before they were accepted. Accepting this RFC means we are prioritizing understandability over precision under the assumption that the lost precision will not be missed (e.g., since users wouldn't have expected to get it anyway). +The main drawback of this approach is that strict-mode validation will be more restrictive. This is by design: Policies like the one in the motivating example will be rejected where before they were accepted. Accepting this RFC means we are prioritizing understandability over precision under the assumption that the lost precision will not be missed. + +Policies that validated before but will not validate now are quite odd -- they would rely on the use of width subtyping, unions, etc. to determine that an expression will always evaluate to `true` (or `false`) and thus can be transformed away. But policies like these will be like those in the motivating example at the start of this RFC, and are probably not what the user intended in the first place. Ultimately, flagging them as erroneous is safer. -A secondary drawback is that this will result in a non-trivial, and backwards-incompatible code change. +A secondary drawback is that this change will result in a non-trivial, and backwards-incompatible code change. +Mitigating this issue is that the backward incompatibility will be minimal in practice (per the above), and we will use verification-guided development to prove that the change is sound (i.e., will not introduce design or implementation mistakes). ## Alternatives From 7d0cb522c41af3fe7019c96c2dad844c9685c0d1 Mon Sep 17 00:00:00 2001 From: John Kastner Date: Fri, 18 Aug 2023 20:07:40 +0000 Subject: [PATCH 09/10] Enter FCP --- text/0019-stricter-validation.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index 69a80d03..c67f23cc 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -3,12 +3,12 @@ ## Related issues and PRs - Reference Issues: -- Implementation PR(s): +- Implementation PR(s): https://github.com/cedar-policy/cedar/pull/282 and https://github.com/cedar-policy/cedar-spec/pull/111 ## Timeline - Start Date: 11-07-2023 -- Date Entered FCP: +- Date Entered FCP: 18-08-2023 - Date Accepted: - Date Landed: From 836f30b3b9d3ec22ac85c3d5ec7805f03971de51 Mon Sep 17 00:00:00 2001 From: John Kastner Date: Thu, 31 Aug 2023 13:06:13 +0000 Subject: [PATCH 10/10] FCP ended --- text/0019-stricter-validation.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0019-stricter-validation.md b/text/0019-stricter-validation.md index c67f23cc..bc6d1f3b 100644 --- a/text/0019-stricter-validation.md +++ b/text/0019-stricter-validation.md @@ -9,7 +9,7 @@ - Start Date: 11-07-2023 - Date Entered FCP: 18-08-2023 -- Date Accepted: +- Date Accepted: 18-08-2023 - Date Landed: ## Summary