From ddfee63caa8f88fc702b8402f3c56cb650412c03 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 15 May 2025 11:19:26 -0400 Subject: [PATCH 01/26] inital draft --- text/0000-generalized-templates.md | 229 +++++++++++++++++++++++++++++ 1 file changed, 229 insertions(+) create mode 100644 text/0000-generalized-templates.md diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md new file mode 100644 index 00000000..939ea9b2 --- /dev/null +++ b/text/0000-generalized-templates.md @@ -0,0 +1,229 @@ +# Generalized Templates + +## Related issues and PRs + +- Reference Issues: [#3](https://github.com/cedar-policy/rfcs/pull/3), + [#7](https://github.com/cedar-policy/rfcs/pull/7), + [#81](https://github.com/cedar-policy/cedar/issues/81), + +- Implementation PR(s): (leave this empty) + +## Timeline + +- Started: 2025-05-13 +- Accepted: TBD +- Stabilized: TBD + +## Summary + +Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates to support: + +1. Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well. +2. Allowing for an arbitrary number of user defined slots to appear in the ```when/unless``` clause of the policy contingent on the type being explicitly annotated. This would also include slots that are not entity types. + +Both of these additions, do not seem to require substiantial changes to the existing type checking code. However, that may change upon diving deeper into the implementation. + +Generalized templates should only be used when provided a schema and strict validation mode. + +## Basic example + +### Example 1 + +By allowing ```?principal``` and ```?resource``` in the condition of the policy we are able to express the following Cedar template. This example was taken directly from a user of Cedar in [#7](https://github.com/cedar-policy/rfcs/pull/7). + +#### Schema +``` +namespace FS { + entity Disk = { + storage: Long, + }; + entity Folder in Disk; + entity Document in Folder; + entity Person; +} + +action "Navigate" appliesTo { + principal: FS::Person, + resource: [FS::Disk, FS::Folder, FS::Document], +}; + +action "Write" appliesTo { + principal: FS::Person, + resource: [FS::Disk, FS::Folder, FS::Document], +}; +``` + +#### Cedar Template +``` +@id("Admin") +permit( + principal == ?principal, + action, + resource in ?resource) +when { + // take any action in the scope that you're admin on + resource in ?resource + + // allow access up the tree for navigation + || (action == Action::"Navigate" && ?resource in resource) +}; +``` + +### Example 2 + +In this example suppose that a company only wants to provide access to it's internal services only when the employee starts working and has finished all of their security training. A user of Cedar trying to implement this policy might implement it as follows with our generalized templates. + +#### Schema +``` +namespace Company { + entity Employee = { + startDate: dateTime + }; + entity InternalServices; +} + +action "Access" appliesTo { + principal: Company::Employee, + resource: Company::InternalServices, + context: {"date": datetime } +} +``` + +#### Template +``` +template(?date: datetime) => +permit( + principal == ?principal, + action == Action::"Access", + resource is Company::InternalServices +) when { + context.date > employee.startDate && context.date > ?date +}; +``` + +### Example 3 + +Suppose there are certain professors with dual appointments under two different departments. You want to give students of their group access to both the resources in the first department and the resources in their second department. + +Note: Although we can create two seperate templates and instantiate them individually, by using generalized templates we are able to make sure that these two templates stay in sync. Error states where only one part of the template is applied but not the other would not occur. Generalized templates subsumes the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7). + +#### Schema +``` +namespace University { + entity Person = { + graduationDate: dateTime + }; + entity Department; + entity InternalDoc in Department; +} + +action "View" appliesTo { + principal: University::Person, + resource: University::InternalDoc, + context: {"date": dateTime } +} +``` + +#### Template +``` +template(?department1: University::Department, ?department2: University::Department) => +permit( + principal == ?principal + action == Action::"View", + resource +) when { + (resource in ?department1 || + resource in ?department2) && + context.date < principal.graduationDate +}; +``` + +## Motivation + +This is a follow up on the discussion on [#3](https://github.com/cedar-policy/rfcs/pull/3). + +The main motivation to support generalized templates is to allow users to take advantages of templates: (1) prevention against injection attacks (2) ability to change a group of policies overtime. At the same time however, we still want to balance validation, and analysis on templates. + +In it's previous form, generalized templates were proposed to allow ```?principal``` and ```?resource``` in the condition if it was in the scope and disallowing arbitrary slots. However, this would only be useful when we are using the ```is``` or ```in``` constraint. Since when we have ```==``` we can just directly use the variables ```principal``` for ```?principal``` and ```resource``` for ```?resource``` directly. This did not seem to have any direct use cases so the proposal was eventually rejected. + +In this proposal, by having the Cedar user explicitly supply types we solve 2 main problems: + +1. We can support analysis on templates + +2. Link time validation would be more performant (we can just check that the supplied values are inhabitants of the types of the slots rather than running the type checker on the policy when the slots are filled in) + +## Detailed design + +The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well would not change any of the existing validator code. + +For example, consider this schema and policy. + +``` +namespace FS { + entity Disk = { + storage: Long, + }; + entity Folder in Disk; + entity Document in Folder; + entity Person; +} + +action "Navigate" appliesTo { + principal: FS::Person, + resource: [FS::Disk, FS::Folder, FS::Document], +}; + +permit (principal, action == Action::"Navigate", resource in ?resource) +when { + ?resource has storage && ?resource.storage == 5 +}; +``` +Currently, how Cedar's typechecker works for templates is by enumerating all possible valid request environments for a particular action. Take for example, in this case the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Then under these individual request environments we generate the possible slot types for principal and resource. +| Request Environment | Principal Slot Types | Resource Slot Types +| -------- | ------- | ------- | +| ```(FS::Person, FS::Disk)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk``` | +| ```(FS::Person, FS::Folder)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder``` | +| ```(FS::Person, FS::Document)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder```, ```?resource: FS::Document``` | + +With this, we check to see if, for any combination of valid request environment and their corresponding ```principal``` and ```resource``` slot types, our policy evaluates to a boolean. + +Since ```?resource``` and ```?principal``` can now appear in the condition of the template we now have to also ensure that for all valid request environments, principal slot type, and resource slot type combinations our template will always evaluate to a boolean. This change would just involve performing a substitution of the appropriate type for each case in the condition in addition to the scope. + +The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding a map to store slot variables that are not in the scope with their corresponding types. + +This proposal will have to touch Cedar's AST, typechecker, parser and introduce validation while linking with Cedar templates. + +The proposed syntax looks as follows template(?bound1: type1, ?bound2: type2) =>. + + + +## Drawbacks + +Type annotations for slots can be a user burden. + +## Alternatives + +1. Type inference. We would perform type inference by considering the valid types of the slots that allow for Cedar templates to be well typed (evaluate to a boolean). + +Any slot on the left or the right of a ```==, <, <=, !=``` would have type as the opposite side. Two slots cannot be compared using ```==, <, <=, !=```. + +Any slot that is being compared using ```.lessThan()``` would have ```decimal``` type. + +Any slot that is used with ```&&, ||, !``` has boolean type. + +Any slot that is used with ```if then else ``` must have boolean type if it appears in the guard and can have AnyType + +Slots can only appear on the left hand side of a ```has``` and must be a type of an entity that has this attribute. + +... + +Downsides: +1. It is possible that the inferred possible types is different from what the user expects and annotation isn't a large burden. +2. It is unclear how this would work with analysis of templates. We can enumerate the valid types that can appear but this can be a very large set. +3. There would need to be some restrictions on where slots can appear that can be unintuitive for users. + +## Unresolved questions + +1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it (here)[https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728]. Initial thoughts are to ensure that the user supplies a map + +2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them until link time. This would also involve some changes in the validator code since we would not be able to From 2b3461e2a4b60b43c79a1a5f08229d7791b3c123 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 15 May 2025 15:31:07 -0400 Subject: [PATCH 02/26] fixed example 1 (the example wasn't correct initially), added a new example to show utility of slots in condition, and edited detailed design --- text/0000-generalized-templates.md | 101 +++++++++++++++++++---------- 1 file changed, 67 insertions(+), 34 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index 939ea9b2..89e4636e 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -19,7 +19,7 @@ Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates to support: 1. Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well. -2. Allowing for an arbitrary number of user defined slots to appear in the ```when/unless``` clause of the policy contingent on the type being explicitly annotated. This would also include slots that are not entity types. +2. Allowing for an arbitrary number of user defined slots to appear in the ```when/unless``` clause of the template contingent on the type being explicitly annotated. This would also include slots that are not entity types. Both of these additions, do not seem to require substiantial changes to the existing type checking code. However, that may change upon diving deeper into the implementation. @@ -29,7 +29,49 @@ Generalized templates should only be used when provided a schema and strict vali ### Example 1 -By allowing ```?principal``` and ```?resource``` in the condition of the policy we are able to express the following Cedar template. This example was taken directly from a user of Cedar in [#7](https://github.com/cedar-policy/rfcs/pull/7). +By allowing ```?principal``` and ```?resource``` in the condition of the policy if it also appears in the scope, it allows us to express templates where it is bound to a general variable. In this example since we are able to allow ```?resource``` in the condition of the policy we are able to express the constraint that we can only view resource's who's owner is the same as the owner of the resource that we instantiate for the typed hole. + +#### Schema +``` +namespace FS { + entity Disk = { + storage: Long, + }; + entity Folder in Disk = { + owner: String, + }; + entity Document in Folder = { + owner: String, + }; + entity Person; +} + +action "Navigate" appliesTo { + principal: FS::Person, + resource: [FS::Disk, FS::Folder, FS::Document], +}; + +action "Write" appliesTo { + principal: FS::Person, + resource: [FS::Disk, FS::Folder, FS::Document], +}; +``` + +#### Cedar Template +``` +@id("Admin") +template(?folder: FS::Folder) +permit( + principal == ?principal, + action, + resource in ?resource) +when { + ?resource.created_by == resource.created_by +}; +``` + +### Example 2 +By allowing generalized typed slots we are able to express the following Cedar template. This example was taken directly from a user of Cedar in [#7](https://github.com/cedar-policy/rfcs/pull/7) and was what initially motivated generalized templates. #### Schema ``` @@ -56,36 +98,35 @@ action "Write" appliesTo { #### Cedar Template ``` @id("Admin") +template(?folder: FS::Folder) permit( principal == ?principal, action, resource in ?resource) when { // take any action in the scope that you're admin on - resource in ?resource + resource in ?folder // allow access up the tree for navigation - || (action == Action::"Navigate" && ?resource in resource) + || (action == Action::"Navigate" && ?folder in resource) }; ``` -### Example 2 +### Example 3 -In this example suppose that a company only wants to provide access to it's internal services only when the employee starts working and has finished all of their security training. A user of Cedar trying to implement this policy might implement it as follows with our generalized templates. +In this example suppose that a company only wants to provide access to it's internal services only when the employee starts working. A user of Cedar trying to implement this policy might implement it as follows with our generalized templates. #### Schema ``` namespace Company { - entity Employee = { - startDate: dateTime - }; + entity Employee; entity InternalServices; } action "Access" appliesTo { principal: Company::Employee, resource: Company::InternalServices, - context: {"date": datetime } + context: { "date": datetime } } ``` @@ -97,11 +138,11 @@ permit( action == Action::"Access", resource is Company::InternalServices ) when { - context.date > employee.startDate && context.date > ?date + context.date > ?date }; ``` -### Example 3 +### Example 4 Suppose there are certain professors with dual appointments under two different departments. You want to give students of their group access to both the resources in the first department and the resources in their second department. @@ -144,19 +185,15 @@ This is a follow up on the discussion on [#3](https://github.com/cedar-policy/rf The main motivation to support generalized templates is to allow users to take advantages of templates: (1) prevention against injection attacks (2) ability to change a group of policies overtime. At the same time however, we still want to balance validation, and analysis on templates. -In it's previous form, generalized templates were proposed to allow ```?principal``` and ```?resource``` in the condition if it was in the scope and disallowing arbitrary slots. However, this would only be useful when we are using the ```is``` or ```in``` constraint. Since when we have ```==``` we can just directly use the variables ```principal``` for ```?principal``` and ```resource``` for ```?resource``` directly. This did not seem to have any direct use cases so the proposal was eventually rejected. - -In this proposal, by having the Cedar user explicitly supply types we solve 2 main problems: - -1. We can support analysis on templates +In it's previous form, generalized templates were proposed to allow ```?principal``` and ```?resource``` in the condition if it was in the scope and disallowing arbitrary slots. However, this addition would not be able to capture the use cases of examples #2 and examples #3. -2. Link time validation would be more performant (we can just check that the supplied values are inhabitants of the types of the slots rather than running the type checker on the policy when the slots are filled in) +In this proposal, by having the Cedar user explicitly supply types for slots that are not ```?principal``` and ```?resource``` we are able to express all of the examples listed above while still supporting analysis on templates and allowing for link time validation to be more performant (we can just check that the supplied values are inhabitants of the types of the slots rather than running the type checker on the instantiated template when the slots are filled in). Types are also a form of documentation that can help with reading templates in the future. ## Detailed design -The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well would not change any of the existing validator code. +The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well will likely will not require substantial changes to the typechecker code. -For example, consider this schema and policy. +For example, consider this schema and template: ``` namespace FS { @@ -178,24 +215,22 @@ when { ?resource has storage && ?resource.storage == 5 }; ``` -Currently, how Cedar's typechecker works for templates is by enumerating all possible valid request environments for a particular action. Take for example, in this case the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Then under these individual request environments we generate the possible slot types for principal and resource. +Currently, how Cedar's typechecker works for templates is by enumerating all possible request environments for a particular action. Take for example, in this case the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Then under these individual request environments we generate the possible slot types for principal and resource. | Request Environment | Principal Slot Types | Resource Slot Types | -------- | ------- | ------- | | ```(FS::Person, FS::Disk)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk``` | | ```(FS::Person, FS::Folder)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder``` | | ```(FS::Person, FS::Document)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder```, ```?resource: FS::Document``` | -With this, we check to see if, for any combination of valid request environment and their corresponding ```principal``` and ```resource``` slot types, our policy evaluates to a boolean. +With this, we check to see if for all request environments any combination of their respective ```?principal``` and ```?resource``` slot types evaluates to a boolean. If they do, then our typechecker passes otherwise it fails. -Since ```?resource``` and ```?principal``` can now appear in the condition of the template we now have to also ensure that for all valid request environments, principal slot type, and resource slot type combinations our template will always evaluate to a boolean. This change would just involve performing a substitution of the appropriate type for each case in the condition in addition to the scope. +With this extension, we would now need to check if for all combinations of valid types for ```principal```, ```resource```, ```?principal```, and ```?resource``` our template including the condition evaluates to a boolean. Cedar's validator already handles this case and the only change that would need to made is to check whether or not ```?principal``` or ```?resource``` appears in the scope of the template. -The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding a map to store slot variables that are not in the scope with their corresponding types. +The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding an additional map to store slot variables that are not in the scope with their corresponding types. This will likely not involve any changes to the typechecker and typechecking can proceed as described above. -This proposal will have to touch Cedar's AST, typechecker, parser and introduce validation while linking with Cedar templates. +The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid types and variable names for slots cannot conflict. ```?principal``` and ```?resource``` are reserved slot names and should not be used within ```template()```. -The proposed syntax looks as follows template(?bound1: type1, ?bound2: type2) =>. - - +This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. ## Drawbacks @@ -203,7 +238,7 @@ Type annotations for slots can be a user burden. ## Alternatives -1. Type inference. We would perform type inference by considering the valid types of the slots that allow for Cedar templates to be well typed (evaluate to a boolean). +1. Type inference. We would perform type inference by considering the valid types of the slots that allow for Cedar templates to evaluate to a boolean. Any slot on the left or the right of a ```==, <, <=, !=``` would have type as the opposite side. Two slots cannot be compared using ```==, <, <=, !=```. @@ -215,12 +250,10 @@ Any slot that is used with ```if then else ``` must have boolea Slots can only appear on the left hand side of a ```has``` and must be a type of an entity that has this attribute. -... - Downsides: -1. It is possible that the inferred possible types is different from what the user expects and annotation isn't a large burden. -2. It is unclear how this would work with analysis of templates. We can enumerate the valid types that can appear but this can be a very large set. -3. There would need to be some restrictions on where slots can appear that can be unintuitive for users. +1. Type annotation is not much overhead. +2. It is possible that the inferred possible types is different from what the user expects. +3. There would need to be some restrictions on where slots can appear that can be unintuitive for users. (```?slot1 == ?slot2```, in this case we can only type either slots as AnyType) ## Unresolved questions From 4faa74f2c63939cea04b0a5a375b1002f6aedc1f Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 15 May 2025 15:43:56 -0400 Subject: [PATCH 03/26] reworded --- text/0000-generalized-templates.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index 89e4636e..0a113f31 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -29,7 +29,7 @@ Generalized templates should only be used when provided a schema and strict vali ### Example 1 -By allowing ```?principal``` and ```?resource``` in the condition of the policy if it also appears in the scope, it allows us to express templates where it is bound to a general variable. In this example since we are able to allow ```?resource``` in the condition of the policy we are able to express the constraint that we can only view resource's who's owner is the same as the owner of the resource that we instantiate for the typed hole. +By allowing ```?principal``` and ```?resource``` in the condition of the policy if it also appears in the scope, it allows us to express templates where we want to access attributes of a slot. In this example since we are able to allow ```?resource``` in the condition of the policy we are able to express the constraint that we can only view resource's who's owner is the same as the owner of the resource that we instantiate for the typed hole. #### Schema ``` @@ -76,9 +76,7 @@ By allowing generalized typed slots we are able to express the following Cedar t #### Schema ``` namespace FS { - entity Disk = { - storage: Long, - }; + entity Disk; entity Folder in Disk; entity Document in Folder; entity Person; @@ -146,7 +144,7 @@ permit( Suppose there are certain professors with dual appointments under two different departments. You want to give students of their group access to both the resources in the first department and the resources in their second department. -Note: Although we can create two seperate templates and instantiate them individually, by using generalized templates we are able to make sure that these two templates stay in sync. Error states where only one part of the template is applied but not the other would not occur. Generalized templates subsumes the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7). +Note: Although we can create two seperate templates and instantiate them individually, by using generalized templates we are able to make sure that these two templates stay in sync. Error states where only one part of the template is applied but not the other would not occur. Generalized templates allows us to subsume the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7) and with typed slots we can for the most part express the motivating example for template-groups. #### Schema ``` From 46f6f5bb367b980c6870506a3997989ef0ceeca4 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 15 May 2025 15:46:11 -0400 Subject: [PATCH 04/26] expanded on downside of type inference --- text/0000-generalized-templates.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index 0a113f31..d6edf239 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -251,7 +251,7 @@ Slots can only appear on the left hand side of a ```has``` and must be a type of Downsides: 1. Type annotation is not much overhead. 2. It is possible that the inferred possible types is different from what the user expects. -3. There would need to be some restrictions on where slots can appear that can be unintuitive for users. (```?slot1 == ?slot2```, in this case we can only type either slots as AnyType) +3. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) ## Unresolved questions From 603ac750fc1653b3271aef394d1b28a6dc4d9fd0 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 15 May 2025 16:00:11 -0400 Subject: [PATCH 05/26] updated unresolved questions --- text/0000-generalized-templates.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index d6edf239..b0cc3e5a 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -159,7 +159,7 @@ namespace University { action "View" appliesTo { principal: University::Person, resource: University::InternalDoc, - context: {"date": dateTime } + context: { "date": dateTime } } ``` @@ -255,6 +255,9 @@ Downsides: ## Unresolved questions -1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it (here)[https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728]. Initial thoughts are to ensure that the user supplies a map +1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. + +2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. + +3. Would we want to support generalized templates for policies with no schema? Maybe we can do a type of link time type check rather than at creation time since we are not performing validation with a schema or analysis. -2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them until link time. This would also involve some changes in the validator code since we would not be able to From 26a48a5bd518aedd48c5849ef6b512f896bebe51 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Fri, 16 May 2025 13:44:19 -0400 Subject: [PATCH 06/26] added how generalized templates works with policies that don't use schemas --- text/0000-generalized-templates.md | 50 +++++++++++++++++------------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index b0cc3e5a..53b93683 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -23,7 +23,7 @@ Cedar templates are quite restrictive. There are only two slots provided (```?pr Both of these additions, do not seem to require substiantial changes to the existing type checking code. However, that may change upon diving deeper into the implementation. -Generalized templates should only be used when provided a schema and strict validation mode. +For user's without schemas generalized templates will be supported. Correct type annotations will need to be supplied by a user of Cedar and a link time check will be performed to make sure that instantiations of the template are values of that type. However, note that without a schema it is still possible for a program that passes the link time type check to exhibit runtime errors. ## Basic example @@ -46,12 +46,12 @@ namespace FS { entity Person; } -action "Navigate" appliesTo { +action Navigate appliesTo { principal: FS::Person, resource: [FS::Disk, FS::Folder, FS::Document], }; -action "Write" appliesTo { +action Write appliesTo { principal: FS::Person, resource: [FS::Disk, FS::Folder, FS::Document], }; @@ -59,8 +59,7 @@ action "Write" appliesTo { #### Cedar Template ``` -@id("Admin") -template(?folder: FS::Folder) +template(?folder: FS::Folder) => permit( principal == ?principal, action, @@ -82,12 +81,12 @@ namespace FS { entity Person; } -action "Navigate" appliesTo { +action Navigate appliesTo { principal: FS::Person, resource: [FS::Disk, FS::Folder, FS::Document], }; -action "Write" appliesTo { +action Write appliesTo { principal: FS::Person, resource: [FS::Disk, FS::Folder, FS::Document], }; @@ -95,8 +94,7 @@ action "Write" appliesTo { #### Cedar Template ``` -@id("Admin") -template(?folder: FS::Folder) +template(?folder: FS::Folder) => permit( principal == ?principal, action, @@ -106,7 +104,7 @@ when { resource in ?folder // allow access up the tree for navigation - || (action == Action::"Navigate" && ?folder in resource) + || (action == Action::Navigate && ?folder in resource) }; ``` @@ -121,10 +119,10 @@ namespace Company { entity InternalServices; } -action "Access" appliesTo { +action Access appliesTo { principal: Company::Employee, resource: Company::InternalServices, - context: { "date": datetime } + context: { date: datetime } } ``` @@ -133,7 +131,7 @@ action "Access" appliesTo { template(?date: datetime) => permit( principal == ?principal, - action == Action::"Access", + action == Action::Access, resource is Company::InternalServices ) when { context.date > ?date @@ -156,10 +154,10 @@ namespace University { entity InternalDoc in Department; } -action "View" appliesTo { +action View appliesTo { principal: University::Person, resource: University::InternalDoc, - context: { "date": dateTime } + context: { date: dateTime } } ``` @@ -168,7 +166,7 @@ action "View" appliesTo { template(?department1: University::Department, ?department2: University::Department) => permit( principal == ?principal - action == Action::"View", + action == Action::View, resource ) when { (resource in ?department1 || @@ -203,12 +201,12 @@ namespace FS { entity Person; } -action "Navigate" appliesTo { +action Navigate appliesTo { principal: FS::Person, resource: [FS::Disk, FS::Folder, FS::Document], }; -permit (principal, action == Action::"Navigate", resource in ?resource) +permit (principal, action == Action::Navigate, resource in ?resource) when { ?resource has storage && ?resource.storage == 5 }; @@ -226,6 +224,19 @@ With this extension, we would now need to check if for all combinations of valid The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding an additional map to store slot variables that are not in the scope with their corresponding types. This will likely not involve any changes to the typechecker and typechecking can proceed as described above. +For users that don't provide a schema, generalized templates will support typed slots with link time checking of types. Here, it is up to the user to provide correct types. Note that without schemas there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only check that is provided when you do not use a schema with generalized templates is that the value you substitute in for ```?bound1``` is indeed of the type that you had specified, in this case ```Bool```. + +``` +template(?bound1: Bool) => +permit ( + principal, + action, + resource, +) when { + 1 + ?bound1 +}; +``` + The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid types and variable names for slots cannot conflict. ```?principal``` and ```?resource``` are reserved slot names and should not be used within ```template()```. This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. @@ -258,6 +269,3 @@ Downsides: 1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. 2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. - -3. Would we want to support generalized templates for policies with no schema? Maybe we can do a type of link time type check rather than at creation time since we are not performing validation with a schema or analysis. - From e9da4422b1375c22c15ea07824fd25c92b6e7ecf Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Fri, 16 May 2025 13:51:00 -0400 Subject: [PATCH 07/26] fixed typo --- text/0000-generalized-templates.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index 53b93683..c2bc2d58 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -181,7 +181,7 @@ This is a follow up on the discussion on [#3](https://github.com/cedar-policy/rf The main motivation to support generalized templates is to allow users to take advantages of templates: (1) prevention against injection attacks (2) ability to change a group of policies overtime. At the same time however, we still want to balance validation, and analysis on templates. -In it's previous form, generalized templates were proposed to allow ```?principal``` and ```?resource``` in the condition if it was in the scope and disallowing arbitrary slots. However, this addition would not be able to capture the use cases of examples #2 and examples #3. +In it's previous form, generalized templates were proposed to allow ```?principal``` and ```?resource``` in the condition if it was in the scope and disallowing arbitrary slots. However, this addition would not be able to capture the use cases of examples #2, #3, and #4. In this proposal, by having the Cedar user explicitly supply types for slots that are not ```?principal``` and ```?resource``` we are able to express all of the examples listed above while still supporting analysis on templates and allowing for link time validation to be more performant (we can just check that the supplied values are inhabitants of the types of the slots rather than running the type checker on the instantiated template when the slots are filled in). Types are also a form of documentation that can help with reading templates in the future. @@ -269,3 +269,5 @@ Downsides: 1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. 2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. + +3. Will it be confusing for user's that \ No newline at end of file From 762d5afbf67cc2bda6cd9dd6e9dd961e6f830a0d Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Fri, 16 May 2025 14:15:22 -0400 Subject: [PATCH 08/26] updated unresolved questions --- text/0000-generalized-templates.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index c2bc2d58..5e8d9154 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -187,7 +187,7 @@ In this proposal, by having the Cedar user explicitly supply types for slots tha ## Detailed design -The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well will likely will not require substantial changes to the typechecker code. +The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well will not require changes to the typechecker code. For example, consider this schema and template: @@ -222,7 +222,7 @@ With this, we check to see if for all request environments any combination of th With this extension, we would now need to check if for all combinations of valid types for ```principal```, ```resource```, ```?principal```, and ```?resource``` our template including the condition evaluates to a boolean. Cedar's validator already handles this case and the only change that would need to made is to check whether or not ```?principal``` or ```?resource``` appears in the scope of the template. -The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding an additional map to store slot variables that are not in the scope with their corresponding types. This will likely not involve any changes to the typechecker and typechecking can proceed as described above. +The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding an additional map to store slot variables with their corresponding types. This will likely not involve any changes to the typechecker and typechecking can proceed as described above. For users that don't provide a schema, generalized templates will support typed slots with link time checking of types. Here, it is up to the user to provide correct types. Note that without schemas there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only check that is provided when you do not use a schema with generalized templates is that the value you substitute in for ```?bound1``` is indeed of the type that you had specified, in this case ```Bool```. @@ -270,4 +270,4 @@ Downsides: 2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. -3. Will it be confusing for user's that \ No newline at end of file +3. Will it be confusing for users' of Cedar that even though we perform a type check when we don't use a schema that there can still be runtime errors? \ No newline at end of file From 10252536478728b2022dec05c61468d875b7ef9c Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Fri, 16 May 2025 15:21:48 -0400 Subject: [PATCH 09/26] updated RFC to mention that ?resource and ?principal slots can be optionally annotated --- text/0000-generalized-templates.md | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index 5e8d9154..c8dcb1ca 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -16,14 +16,14 @@ ## Summary -Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates to support: +Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users' of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates to support: 1. Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well. 2. Allowing for an arbitrary number of user defined slots to appear in the ```when/unless``` clause of the template contingent on the type being explicitly annotated. This would also include slots that are not entity types. Both of these additions, do not seem to require substiantial changes to the existing type checking code. However, that may change upon diving deeper into the implementation. -For user's without schemas generalized templates will be supported. Correct type annotations will need to be supplied by a user of Cedar and a link time check will be performed to make sure that instantiations of the template are values of that type. However, note that without a schema it is still possible for a program that passes the link time type check to exhibit runtime errors. +For policies without schemas generalized templates will be supported. Correct type annotations will need to be supplied by a user of Cedar and a link time check will be performed to make sure that instantiations of the template are values of that type. However, note that without a schema it is still possible for a program that passes the link time type check to exhibit runtime errors. ## Basic example @@ -237,7 +237,9 @@ permit ( }; ``` -The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid types and variable names for slots cannot conflict. ```?principal``` and ```?resource``` are reserved slot names and should not be used within ```template()```. +The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid types and variable names for slots cannot conflict. + +```?principal``` and ```?resource``` can optionally have their types annotated in ```template()```. A similiar effect can be done using the ```is``` operator in the condition. However, this would allow templates to be instantiated with slots always evaluate to false. By having an explicit type annotation, we prevent these instantiations from being linked in the first place. This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. From 2db0f1b7935b62163a3f295781e17cc9c7459dbc Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Fri, 16 May 2025 16:11:07 -0400 Subject: [PATCH 10/26] fixed typo, policy templates need quotes around action --- text/0000-generalized-templates.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0000-generalized-templates.md b/text/0000-generalized-templates.md index c8dcb1ca..0d8a0ed3 100644 --- a/text/0000-generalized-templates.md +++ b/text/0000-generalized-templates.md @@ -131,7 +131,7 @@ action Access appliesTo { template(?date: datetime) => permit( principal == ?principal, - action == Action::Access, + action == Action::"Access", resource is Company::InternalServices ) when { context.date > ?date @@ -166,7 +166,7 @@ action View appliesTo { template(?department1: University::Department, ?department2: University::Department) => permit( principal == ?principal - action == Action::View, + action == Action::"View", resource ) when { (resource in ?department1 || From 286e7f70e8faee9abfb09527c421e44249a0df5b Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Mon, 19 May 2025 15:49:13 -0400 Subject: [PATCH 11/26] Renamed file to correspond with issue number --- ...0-generalized-templates.md => 0097-generalized-templates.md} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename text/{0000-generalized-templates.md => 0097-generalized-templates.md} (99%) diff --git a/text/0000-generalized-templates.md b/text/0097-generalized-templates.md similarity index 99% rename from text/0000-generalized-templates.md rename to text/0097-generalized-templates.md index 0d8a0ed3..d15ff3b1 100644 --- a/text/0000-generalized-templates.md +++ b/text/0097-generalized-templates.md @@ -272,4 +272,4 @@ Downsides: 2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. -3. Will it be confusing for users' of Cedar that even though we perform a type check when we don't use a schema that there can still be runtime errors? \ No newline at end of file +3. Will it be confusing for users' of Cedar that even though we perform a type check when we don't use a schema that there can still be runtime errors? From a9935c9e951f8628971e7398233687da38ac33df Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Mon, 19 May 2025 15:53:45 -0400 Subject: [PATCH 12/26] Changed file name to match issue number --- ...097-generalized-templates.md => 0098-generalized-templates.md} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename text/{0097-generalized-templates.md => 0098-generalized-templates.md} (100%) diff --git a/text/0097-generalized-templates.md b/text/0098-generalized-templates.md similarity index 100% rename from text/0097-generalized-templates.md rename to text/0098-generalized-templates.md From b81dd2d89abd081fdb0c56304010fa7592d2800e Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 22 May 2025 09:39:55 -0400 Subject: [PATCH 13/26] fixed typo in example 1 Signed-off-by: Alan Wang --- text/0098-generalized-templates.md | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index d15ff3b1..cb6e77e7 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -35,7 +35,7 @@ By allowing ```?principal``` and ```?resource``` in the condition of the policy ``` namespace FS { entity Disk = { - storage: Long, + owner: String, }; entity Folder in Disk = { owner: String, @@ -59,13 +59,12 @@ action Write appliesTo { #### Cedar Template ``` -template(?folder: FS::Folder) => permit( principal == ?principal, action, resource in ?resource) when { - ?resource.created_by == resource.created_by + ?resource.owner == resource.owner }; ``` From 6aa5519c819929c4f24519086ff0cc2bd325e2fb Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Thu, 22 May 2025 16:30:48 -0400 Subject: [PATCH 14/26] Added more detail about implementation of typed slots --- text/0098-generalized-templates.md | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index cb6e77e7..6bc1584b 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -236,11 +236,21 @@ permit ( }; ``` -The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid types and variable names for slots cannot conflict. - ```?principal``` and ```?resource``` can optionally have their types annotated in ```template()```. A similiar effect can be done using the ```is``` operator in the condition. However, this would allow templates to be instantiated with slots always evaluate to false. By having an explicit type annotation, we prevent these instantiations from being linked in the first place. -This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. +The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid schema types. Schema types are chosen over AST types because they allow us to more precisely specify the type for sets and records. Each new typed slot requires a distinct variable name. However, within the when/unless clause the same typed slot can be used multiple times. The grammar of template annotations is as follows. ```Type``` is taken directly from the Cedar documentation for schema types. + +``` +Template := 'template' '(' ( TypeAnnotation { ',' TypeAnnotation } ) ')' '=>' + +TypeAnnotation := ‘?’ IDENT ‘:’ Type + +Type := Path | SetType | RecType +``` + +Typed slots can only be instantiated with value types. In the implementation this corresponds to the ```RestrictedExpression``` type. + +This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. In addition to maintain backwards compatability with the current API, interacting with generalized templates will have to be treated under a seperate set of API functions. ## Drawbacks From 816b76eb8c4d2ac290c6aaa386e468ebe79f3ec6 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Mon, 2 Jun 2025 09:52:22 -0400 Subject: [PATCH 15/26] Included details about the JSON policy format for typed slots --- text/0098-generalized-templates.md | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 6bc1584b..3701d731 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -252,6 +252,19 @@ Typed slots can only be instantiated with value types. In the implementation thi This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. In addition to maintain backwards compatability with the current API, interacting with generalized templates will have to be treated under a seperate set of API functions. +The changes to the JSON policy format would include another attribute ```typed_slots``` and would look as follows: +``` +"typed_slots": [ + { "type": "University::Department", "id": "?department1" }, + { "type": "University::Department", "id": "?department2" }, + ] +``` + +In the JSON policy format, typed slots can be referred to with the same syntax as what is done for ```?principal``` and ```?resource```, except with the identifier being replaced. It would look as follows: +``` +"slot": "?department1" +``` + ## Drawbacks Type annotations for slots can be a user burden. @@ -271,9 +284,10 @@ Any slot that is used with ```if then else ``` must have boolea Slots can only appear on the left hand side of a ```has``` and must be a type of an entity that has this attribute. Downsides: -1. Type annotation is not much overhead. -2. It is possible that the inferred possible types is different from what the user expects. -3. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) +1. It could result in analysis being overly general, since it would now have to consider all possible combinations of the types of the slots that will allow for link time validation to succeed. +2. Type annotation is not much overhead. +3. It is possible that the inferred possible types is different from what the user expects. +4. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) ## Unresolved questions @@ -281,4 +295,6 @@ Downsides: 2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. -3. Will it be confusing for users' of Cedar that even though we perform a type check when we don't use a schema that there can still be runtime errors? +3. Will it be confusing for users' of Cedar that even though we perform a type check when we don't use a schema that there can still be runtime errors? + +4. Currently, there will be no reserved keywords for typed slots. Should there be any? From e49b0af34bf954196f0bd05b7c0b63708aee9a75 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Mon, 2 Jun 2025 14:56:40 -0400 Subject: [PATCH 16/26] Fix typo --- text/0098-generalized-templates.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 3701d731..abe67221 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -205,7 +205,7 @@ action Navigate appliesTo { resource: [FS::Disk, FS::Folder, FS::Document], }; -permit (principal, action == Action::Navigate, resource in ?resource) +permit (principal == ?principal, action == Action::"Navigate", resource in ?resource) when { ?resource has storage && ?resource.storage == 5 }; From 0a8106d0efe55758ce68152621c5be9e9a4fc4c9 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Tue, 3 Jun 2025 15:30:54 -0400 Subject: [PATCH 17/26] Revised RFC after doc meeting Signed-off-by: Alan Wang --- text/0098-generalized-templates.md | 100 ++++++++++++++++++----------- 1 file changed, 64 insertions(+), 36 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index abe67221..16035ec0 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -16,20 +16,21 @@ ## Summary -Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users' of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates to support: +Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates in two different ways: -1. Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well. -2. Allowing for an arbitrary number of user defined slots to appear in the ```when/unless``` clause of the template contingent on the type being explicitly annotated. This would also include slots that are not entity types. +1. We want to relax the restriction on the two slots (```?principal``` and ```?resource```) that Cedar currently provides to allow them to appear in the condition of the template if they also appear in the scope. -Both of these additions, do not seem to require substiantial changes to the existing type checking code. However, that may change upon diving deeper into the implementation. +2. We want to allow for an arbitrary number of user defined slots to appear in the condition (```when/unless```) clause of the template if the type is explicitly annotated. User defined slots are different from the slots in Cedar currently because they can be instantiated with values that are not entity types and also can not appear in the scope. -For policies without schemas generalized templates will be supported. Correct type annotations will need to be supplied by a user of Cedar and a link time check will be performed to make sure that instantiations of the template are values of that type. However, note that without a schema it is still possible for a program that passes the link time type check to exhibit runtime errors. +These two additions to generalize Cedar templates will not require substiantial changes to the existing type checking code. + +Generalized templates will be supported for users of Cedar that do not use a schema. Without a schema, type annotations for generalized templates are optional. Templates will not be validated, but type checking will be performed during link-time. While this ensures that the provided values match the type of slot they are filling, it does not ensure that the policy won't experience a run-time type error. ## Basic example ### Example 1 -By allowing ```?principal``` and ```?resource``` in the condition of the policy if it also appears in the scope, it allows us to express templates where we want to access attributes of a slot. In this example since we are able to allow ```?resource``` in the condition of the policy we are able to express the constraint that we can only view resource's who's owner is the same as the owner of the resource that we instantiate for the typed hole. +By allowing ```?principal``` and ```?resource``` in the condition of the policy if they also appear in the scope, we can write templates that access attributes of a ```?principal``` or ```?resource slot```. In this example, since we are able to allow ```?resource``` in the condition of the policy, we are able to express the constraint that we can only view resources whose owner is the same as the owner of the entity that we instantiate for the typed hole. #### Schema ``` @@ -109,7 +110,7 @@ when { ### Example 3 -In this example suppose that a company only wants to provide access to it's internal services only when the employee starts working. A user of Cedar trying to implement this policy might implement it as follows with our generalized templates. +In this example, suppose that a company only wants to provide access to it's internal services only when the employee starts working. Using generalized templates, a user of Cedar might implement it as follows: #### Schema ``` @@ -139,9 +140,9 @@ permit( ### Example 4 -Suppose there are certain professors with dual appointments under two different departments. You want to give students of their group access to both the resources in the first department and the resources in their second department. +Suppose there are certain professors with dual appointments under two different departments who want to give students of their group access to both the resources in the first department and the resources in their second department. -Note: Although we can create two seperate templates and instantiate them individually, by using generalized templates we are able to make sure that these two templates stay in sync. Error states where only one part of the template is applied but not the other would not occur. Generalized templates allows us to subsume the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7) and with typed slots we can for the most part express the motivating example for template-groups. +Note: Although we can create two seperate templates and instantiate them individually, we would need to make sure they stay in sync. With generalized templates, since there is only one template we do not need to do so. Error states where only one part of the template is applied but not the other would not be able to occur. Generalized templates allows us to subsume the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7) and with typed slots we can express the motivating example for template-groups. #### Schema ``` @@ -178,17 +179,19 @@ permit( This is a follow up on the discussion on [#3](https://github.com/cedar-policy/rfcs/pull/3). -The main motivation to support generalized templates is to allow users to take advantages of templates: (1) prevention against injection attacks (2) ability to change a group of policies overtime. At the same time however, we still want to balance validation, and analysis on templates. +Templates offer a way to change a group of policies overtime and to prevent against injection attacks that can occur when creating policies at runtime. However, there are policies that users of Cedar want to create at runtime that can't be expressed with templates today. By generalizing Cedar templates, we hope to allow for more users of Cedar to take advantage of these benefits while still balancing Cedar's core features: validation, analysis, and performance. -In it's previous form, generalized templates were proposed to allow ```?principal``` and ```?resource``` in the condition if it was in the scope and disallowing arbitrary slots. However, this addition would not be able to capture the use cases of examples #2, #3, and #4. +In it's previous form, generalized templates were proposed to only allow ```?principal``` and ```?resource``` slots in the condition if they also appear in the scope. However, with only this addition we would not be able to express the use cases of examples #2, #3, and #4. -In this proposal, by having the Cedar user explicitly supply types for slots that are not ```?principal``` and ```?resource``` we are able to express all of the examples listed above while still supporting analysis on templates and allowing for link time validation to be more performant (we can just check that the supplied values are inhabitants of the types of the slots rather than running the type checker on the instantiated template when the slots are filled in). Types are also a form of documentation that can help with reading templates in the future. +In this proposal, we add on to the previous one to also allow an arbitrary number of user defined slots to appear in the condition clause of the template if the type is explicitly annotated. -## Detailed design +By having the Cedar user explicitly supply types for slots that are not ```?principal``` and ```?resource``` we are able to express examples #2, #3, and #4 while still supporting validation and analysis on templates. Link time validation is also more performant because we can just check that the types of the supplied values are the same as the type annotations provided rather than running the type checker on the instantiated template. This is important since link time validation occurs during runtime. Types are also a form of documentation that can help with reviewing your templates in the future. -The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy only if they also appear in the scope as well will not require changes to the typechecker code. +## Detailed design +### Implementation +The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy if they also appear in the scope will not require any changes to the typechecker code. -For example, consider this schema and template: +Consider this schema and template: ``` namespace FS { @@ -210,7 +213,7 @@ when { ?resource has storage && ?resource.storage == 5 }; ``` -Currently, how Cedar's typechecker works for templates is by enumerating all possible request environments for a particular action. Take for example, in this case the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Then under these individual request environments we generate the possible slot types for principal and resource. +Currently, how Cedar's typechecker works is by enumerating all possible request environments for a particular action. In this case the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Then under these individual request environments we generate the possible slot types for principal and resource. | Request Environment | Principal Slot Types | Resource Slot Types | -------- | ------- | ------- | | ```(FS::Person, FS::Disk)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk``` | @@ -219,11 +222,14 @@ Currently, how Cedar's typechecker works for templates is by enumerating all pos With this, we check to see if for all request environments any combination of their respective ```?principal``` and ```?resource``` slot types evaluates to a boolean. If they do, then our typechecker passes otherwise it fails. -With this extension, we would now need to check if for all combinations of valid types for ```principal```, ```resource```, ```?principal```, and ```?resource``` our template including the condition evaluates to a boolean. Cedar's validator already handles this case and the only change that would need to made is to check whether or not ```?principal``` or ```?resource``` appears in the scope of the template. +With this extension, we would now need to check if for all combinations of valid types for ```principal```, ```resource```, ```?principal```, and ```?resource``` our template including the condition evaluates to a boolean. Cedar's validator already handles this case and the only change that would need to be made is to check for whether or not ```?principal``` or ```?resource``` appears in the scope of the template. -The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy contingent on the type being explicitly annotated would involve adding an additional map to store slot variables with their corresponding types. This will likely not involve any changes to the typechecker and typechecking can proceed as described above. +The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy if the type is annotated would involve modifying Cedar's AST to include generalized slots that also store types and modifying the associated type checking code to use the type associated with it. This will not involve any major changes to the typechecker and typechecking can proceed as described above. -For users that don't provide a schema, generalized templates will support typed slots with link time checking of types. Here, it is up to the user to provide correct types. Note that without schemas there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only check that is provided when you do not use a schema with generalized templates is that the value you substitute in for ```?bound1``` is indeed of the type that you had specified, in this case ```Bool```. +Note: Typed slots can only be instantiated with value types. In the implementation this corresponds to the ```RestrictedExpression``` type. + +### Users of Cedar that do not use a Schema +For users that don't provide a schema, generalized templates will support optional typed slots with link time type checking. Here, it is up to the user to provide correct types. Note that without schemas there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only guarantee that is provided when you do not use a schema with generalized templates is that if you annotate the slot with a type, the value you substitute in for ```?bound1``` is indeed of the type that you had specified, in this case ```Bool```. ``` template(?bound1: Bool) => @@ -236,9 +242,8 @@ permit ( }; ``` -```?principal``` and ```?resource``` can optionally have their types annotated in ```template()```. A similiar effect can be done using the ```is``` operator in the condition. However, this would allow templates to be instantiated with slots always evaluate to false. By having an explicit type annotation, we prevent these instantiations from being linked in the first place. - -The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid schema types. Schema types are chosen over AST types because they allow us to more precisely specify the type for sets and records. Each new typed slot requires a distinct variable name. However, within the when/unless clause the same typed slot can be used multiple times. The grammar of template annotations is as follows. ```Type``` is taken directly from the Cedar documentation for schema types. +### Syntax +The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid schema types. Schema types are chosen over AST types because they allow us to more precisely specify the type for sets and records. Each new typed slot requires a distinct variable name. However, within the when/unless clause the same typed slot can be used multiple times. The grammar of template annotations is as follows. ```Type``` is taken directly from the Cedar documentation for schema types. The template syntax (```template(?bound1: type1, ?bound2: type2) =>```) must go after all the annotations. ``` Template := 'template' '(' ( TypeAnnotation { ',' TypeAnnotation } ) ')' '=>' @@ -248,16 +253,13 @@ TypeAnnotation := ‘?’ IDENT ‘:’ Type Type := Path | SetType | RecType ``` -Typed slots can only be instantiated with value types. In the implementation this corresponds to the ```RestrictedExpression``` type. - -This proposal will have to touch Cedar's AST, typechecker, parser and introduce type checking when linking with templates. In addition to maintain backwards compatability with the current API, interacting with generalized templates will have to be treated under a seperate set of API functions. - +### JSON Policy Format The changes to the JSON policy format would include another attribute ```typed_slots``` and would look as follows: ``` "typed_slots": [ { "type": "University::Department", "id": "?department1" }, { "type": "University::Department", "id": "?department2" }, - ] +] ``` In the JSON policy format, typed slots can be referred to with the same syntax as what is done for ```?principal``` and ```?resource```, except with the identifier being replaced. It would look as follows: @@ -265,13 +267,33 @@ In the JSON policy format, typed slots can be referred to with the same syntax a "slot": "?department1" ``` + +### ```?principal``` and ```?resource``` Slots + +```?principal``` and ```?resource``` can optionally have their types annotated in ```template()```. A similiar effect can be achieved using the ```is``` operator in the condition. However, this would allow templates to be instantiated with slots that always evaluate to false. By having an explicit type annotation, we prevent these instantiations from being linked in the first place. + +Aside from the optional type annotation for ```?principal``` and ```?resource``` slots, there are some other differences between them and user defined slots. For one, ```?principal``` and ```?resource``` slots must appear in the scope of the template and can optionally be in the condition of the template, however user defined slots can only appear in the condition clause. Because of this difference ```?principal``` and ```?resource``` slots can only be filled in with entity types and user defined slots can be filled in with any ```SchemaType```. + +Currently, there is no good way forward to unify the behavior between these two kinds of slots. + +### What is allowed and not allowed? +1. Every slot not ```?principal``` and ```?resource``` needs to have a type associated with it +2. Disallow ```?action``` and ```?context``` slots +3. Annotated ```?principal``` and ```?resource``` types must be an entity type +4. All slots within the template annotation (```template()```) must be used in the template +5. ```?principal``` and ```?resource``` slots must appear in the scope +6. User defined slots can not appear in the scope +6. All slot names must beigin with ```?``` + ## Drawbacks -Type annotations for slots can be a user burden. +1. Using ```?principal``` and ```?resource``` in the condition clause can cause confusion because it looks similiar to ```principal``` and ```resource```. +2. Type annotations for slots can be a user burden. ## Alternatives -1. Type inference. We would perform type inference by considering the valid types of the slots that allow for Cedar templates to evaluate to a boolean. +### Type Inference +We would perform type inference by considering the valid types of the slots that allow for Cedar templates to evaluate to a boolean. Any slot on the left or the right of a ```==, <, <=, !=``` would have type as the opposite side. Two slots cannot be compared using ```==, <, <=, !=```. @@ -283,18 +305,24 @@ Any slot that is used with ```if then else ``` must have boolea Slots can only appear on the left hand side of a ```has``` and must be a type of an entity that has this attribute. +... + Downsides: 1. It could result in analysis being overly general, since it would now have to consider all possible combinations of the types of the slots that will allow for link time validation to succeed. -2. Type annotation is not much overhead. -3. It is possible that the inferred possible types is different from what the user expects. -4. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) +2. It is possible that the inferred possible types is different from what the user expects. +3. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) + +### Moving the type annotations to the Schema file rather than having them defined in the template. + +By moving the type annotations to the Schema file we can keep the notion of types all in one place. + +Downsides: +1. By moving types into the Schema file we would not be able to have slots that are localized per template since there is no way to reference a specific template in the Schema. Instead we will have to declare all the slot names and their associated types in the global namespace. +2. It is awkward to have type annotations in the Schema since when writing the Schema we have no foresight about what slots we will need in the policy. +3. It would prevent you from using link time type checking for generalized templates if you do not use a schema. ## Unresolved questions 1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. -2. Would we want to generalize the action clause. This can support even more general templates. However, it becomes less clear what the connection of each template is with each other if we support a ```?action``` slot. This would also likely result in difficulty with analysis of templates since now ```?principal``` and ```?resource``` would have no constraints on them. - -3. Will it be confusing for users' of Cedar that even though we perform a type check when we don't use a schema that there can still be runtime errors? -4. Currently, there will be no reserved keywords for typed slots. Should there be any? From 328cc7a716857c7b437465690efd07e84b614f9b Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Tue, 10 Jun 2025 13:53:02 -0400 Subject: [PATCH 18/26] updates Signed-off-by: Alan Wang --- text/0098-generalized-templates.md | 162 +++++++++++++---------------- 1 file changed, 73 insertions(+), 89 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 16035ec0..ab90e216 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -16,21 +16,17 @@ ## Summary -Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates in two different ways: +Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates by allowing for an arbitrary number of user defined slots. User defined slots have different rules depending on whether or not they appear in the scope. If the user defined slot appears in the scope then it's type annotations are optional. Note that user defined slots that appear in the scope can only appear on the right-hand side of the ```==``` or ```in``` operators. This includes in operators when appearing together with an is operator, but excludes solitary is operators. User defined slots that appear in the scope can also be used in the condition as well. If the user defined slot appears in the condition of the template, then it must have it's type annotated and the type can be of any valid Cedar Schema Type including common types. -1. We want to relax the restriction on the two slots (```?principal``` and ```?resource```) that Cedar currently provides to allow them to appear in the condition of the template if they also appear in the scope. +In order to eliminate confusion, if using ```?principal``` and ```?resource``` slots they must be used exactly the same way as how they are being used currently. -2. We want to allow for an arbitrary number of user defined slots to appear in the condition (```when/unless```) clause of the template if the type is explicitly annotated. User defined slots are different from the slots in Cedar currently because they can be instantiated with values that are not entity types and also can not appear in the scope. - -These two additions to generalize Cedar templates will not require substiantial changes to the existing type checking code. - -Generalized templates will be supported for users of Cedar that do not use a schema. Without a schema, type annotations for generalized templates are optional. Templates will not be validated, but type checking will be performed during link-time. While this ensures that the provided values match the type of slot they are filling, it does not ensure that the policy won't experience a run-time type error. +For users of Cedar who do not use a schmea, type annotations for generalized templates are optional. Templates will not be validated, but type checking will be performed during link-time. While this ensures that the provided values match the type of slot they are filling, it does not ensure that the policy won't experience a run-time type error. ## Basic example ### Example 1 -By allowing ```?principal``` and ```?resource``` in the condition of the policy if they also appear in the scope, we can write templates that access attributes of a ```?principal``` or ```?resource slot```. In this example, since we are able to allow ```?resource``` in the condition of the policy, we are able to express the constraint that we can only view resources whose owner is the same as the owner of the entity that we instantiate for the typed hole. +By allowing user defined slots that appear in the scope to also appear in the condition of the template, we are able to access attributes of that slot. In this example, this allows us to express the constraint that we can only access resources whose owner is the same as the owner of the entity that we instantiate for the ```?fs``` slot. #### Schema ``` @@ -61,16 +57,17 @@ action Write appliesTo { #### Cedar Template ``` permit( - principal == ?principal, + principal == ?person, action, - resource in ?resource) + resource in ?fs) when { - ?resource.owner == resource.owner + ?fs.owner == resource.owner }; ``` ### Example 2 -By allowing generalized typed slots we are able to express the following Cedar template. This example was taken directly from a user of Cedar in [#7](https://github.com/cedar-policy/rfcs/pull/7) and was what initially motivated generalized templates. + +By allowing arbitrary user defined slots, we are able to express the following Cedar template. This example was taken directly from a user of Cedar in [#7](https://github.com/cedar-policy/rfcs/pull/7). #### Schema ``` @@ -104,13 +101,13 @@ when { resource in ?folder // allow access up the tree for navigation - || (action == Action::Navigate && ?folder in resource) + || (action == Action::"Navigate" && ?folder in resource) }; ``` ### Example 3 -In this example, suppose that a company only wants to provide access to it's internal services only when the employee starts working. Using generalized templates, a user of Cedar might implement it as follows: +Suppose that a company only wants to provide access to it's internal services only when the employee starts working. We can now use Generalized Cedar templates to define it as follows: #### Schema ``` @@ -140,9 +137,7 @@ permit( ### Example 4 -Suppose there are certain professors with dual appointments under two different departments who want to give students of their group access to both the resources in the first department and the resources in their second department. - -Note: Although we can create two seperate templates and instantiate them individually, we would need to make sure they stay in sync. With generalized templates, since there is only one template we do not need to do so. Error states where only one part of the template is applied but not the other would not be able to occur. Generalized templates allows us to subsume the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7) and with typed slots we can express the motivating example for template-groups. +Suppose there are professors with dual appointments under two different departments who want to give students of their group access to both the resources in the first department and the resources in the second department. We can implement this template currently in Cedar by creating two seperate templates and instantiating them individually. The downside of this is that it would be up to the user of Cedar to ensure that they have made sure to instantiate both templates. Previously, [template groups](https://github.com/cedar-policy/rfcs/pull/7) was proposed as a solution to the problem mentioned above. However, with Generalized Cedar templates, we can solve this problem as follows: #### Schema ``` @@ -179,17 +174,28 @@ permit( This is a follow up on the discussion on [#3](https://github.com/cedar-policy/rfcs/pull/3). -Templates offer a way to change a group of policies overtime and to prevent against injection attacks that can occur when creating policies at runtime. However, there are policies that users of Cedar want to create at runtime that can't be expressed with templates today. By generalizing Cedar templates, we hope to allow for more users of Cedar to take advantage of these benefits while still balancing Cedar's core features: validation, analysis, and performance. +Cedar templates offer a way to change a group of policies overtime and to prevent against injection attacks that can occur when creating policies at runtime. However, there are policies that users of Cedar want to create at runtime that can't be expressed using templates today. By generalizing Cedar templates, we hope to allow for more users to be able to use templates while still balancing Cedar's core features: validation, analysis, and performance. -In it's previous form, generalized templates were proposed to only allow ```?principal``` and ```?resource``` slots in the condition if they also appear in the scope. However, with only this addition we would not be able to express the use cases of examples #2, #3, and #4. +While annotating the types of user defined slots inccurs some user burden, it allows us to express examples #2, #3, and #4 while still supporting validation and analysis. It also allows us to keep Cedar performant. With types, link time validation only requires checking that the supplied values have the same type as what is annotated, the alternative being running the type checker everytime you instantiate your template. Types also serve as a form of documentation that can help you remember what your templates are able to be linked against. -In this proposal, we add on to the previous one to also allow an arbitrary number of user defined slots to appear in the condition clause of the template if the type is explicitly annotated. +## Detailed design -By having the Cedar user explicitly supply types for slots that are not ```?principal``` and ```?resource``` we are able to express examples #2, #3, and #4 while still supporting validation and analysis on templates. Link time validation is also more performant because we can just check that the types of the supplied values are the same as the type annotations provided rather than running the type checker on the instantiated template. This is important since link time validation occurs during runtime. Types are also a form of documentation that can help with reviewing your templates in the future. +### Details +We restrict the usage of ```?principal``` and ```?resource``` to the current implementation of templates in Cedar. Although, it would have been possible to allow for ```?principal``` and ```?resource``` to appear in the condition of the template, it can be confusing to distinguish between slots and variables. Therefore, only user defined slots that appear in the scope are allowed to be in the condition of the template. Note that just like in a typical programming language, nothing prevents you from coming up with confusing slot names, but ultimately this is up to the user's discretion. A template such as the following can be expressed: + +``` +permit(principal == ?resources, action == Action::"Navigate", resource == ?principals) +``` + +User defined slots that appear in the scope of the template will only be allowed to link with entity types. User defined slots that appear only in the condition of the template will only be allowed to be linked with values, this corresponds with the ```RestrictedExpression``` type in ```cedar-policy-core```. + +For users that do not use a schema, there is no notion of common types as common types only appear when using a schema. -## Detailed design ### Implementation -The implementation of (1) Allowing ```?principal``` and ```?resource``` in the condition of the policy if they also appear in the scope will not require any changes to the typechecker code. + +To allow for the arbitrary user defined slots, we will need to modify the parser, type checker, AST. The modfications needed for the typechecker will not be signficant. + +Below I provide a brief explanation of how Cedar's typechecker will work for user defined slots that appear in the scope: Consider this schema and template: @@ -208,28 +214,27 @@ action Navigate appliesTo { resource: [FS::Disk, FS::Folder, FS::Document], }; -permit (principal == ?principal, action == Action::"Navigate", resource in ?resource) +permit (principal == ?person, action == Action::"Navigate", resource in ?fs) when { - ?resource has storage && ?resource.storage == 5 + ?fs has storage && ?fs.storage == 5 }; ``` -Currently, how Cedar's typechecker works is by enumerating all possible request environments for a particular action. In this case the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Then under these individual request environments we generate the possible slot types for principal and resource. + +Cedar's typechecker works by enumerating all possible request environments for a particular action. For the action ```Navigate```, the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Under these individual request environments, we then generate the possible slot types for ```?person``` and ```?fs```. So far, this proceeds exactly as it would with Cedar templates currently, the only difference being a change in the slot names. + | Request Environment | Principal Slot Types | Resource Slot Types | -------- | ------- | ------- | | ```(FS::Person, FS::Disk)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk``` | | ```(FS::Person, FS::Folder)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder``` | | ```(FS::Person, FS::Document)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder```, ```?resource: FS::Document``` | -With this, we check to see if for all request environments any combination of their respective ```?principal``` and ```?resource``` slot types evaluates to a boolean. If they do, then our typechecker passes otherwise it fails. - -With this extension, we would now need to check if for all combinations of valid types for ```principal```, ```resource```, ```?principal```, and ```?resource``` our template including the condition evaluates to a boolean. Cedar's validator already handles this case and the only change that would need to be made is to check for whether or not ```?principal``` or ```?resource``` appears in the scope of the template. +Under each individual enumeration, we now check to see if these respective assignment of types to variables and user defined slots evaluates to a boolean. If every enumeration does, then our template passes the typechecker, otherwise it fails. With this extension, we would just need to ensure that for all enumerations, the condition of the policy also evaluates to a boolean. -The implementation of (2) Allowing for an arbitrary number of user defined slots to appear in the condition of the policy if the type is annotated would involve modifying Cedar's AST to include generalized slots that also store types and modifying the associated type checking code to use the type associated with it. This will not involve any major changes to the typechecker and typechecking can proceed as described above. - -Note: Typed slots can only be instantiated with value types. In the implementation this corresponds to the ```RestrictedExpression``` type. +Since user defined slots that only appear in the condition of the template are required to have their types annotated, we do not need to perform this enumeration. Instead, now we use the type supplied by the user for the user defined slots and see if the template evaluates to a boolean type. ### Users of Cedar that do not use a Schema -For users that don't provide a schema, generalized templates will support optional typed slots with link time type checking. Here, it is up to the user to provide correct types. Note that without schemas there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only guarantee that is provided when you do not use a schema with generalized templates is that if you annotate the slot with a type, the value you substitute in for ```?bound1``` is indeed of the type that you had specified, in this case ```Bool```. + +For users that do not use a schema, the user defined slots can be optionally annotated with types. If the types are annotated, generalized templates link time type checking will be performed. Here, it is up to the user to provide the correct types as without a schema. Note that even if types are supplied, there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only guarantee provided when you do not use a schema is if you annotate a user defined slot with a type, the value you instatiate the slot with is of the type that you had supplied. ``` template(?bound1: Bool) => @@ -243,7 +248,9 @@ permit ( ``` ### Syntax -The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid schema types. Schema types are chosen over AST types because they allow us to more precisely specify the type for sets and records. Each new typed slot requires a distinct variable name. However, within the when/unless clause the same typed slot can be used multiple times. The grammar of template annotations is as follows. ```Type``` is taken directly from the Cedar documentation for schema types. The template syntax (```template(?bound1: type1, ?bound2: type2) =>```) must go after all the annotations. + +The proposed syntax for generalized templates looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and must come after all annotations. +Each new user defined requires a distinct variable name. User defined slots in the scope must be unique. However, within the condition clause the same user defined slot can be used multiple times. The grammar of template annotations is as follows: ``` Template := 'template' '(' ( TypeAnnotation { ',' TypeAnnotation } ) ')' '=>' @@ -253,76 +260,53 @@ TypeAnnotation := ‘?’ IDENT ‘:’ Type Type := Path | SetType | RecType ``` -### JSON Policy Format -The changes to the JSON policy format would include another attribute ```typed_slots``` and would look as follows: -``` -"typed_slots": [ - { "type": "University::Department", "id": "?department1" }, - { "type": "University::Department", "id": "?department2" }, -] -``` - -In the JSON policy format, typed slots can be referred to with the same syntax as what is done for ```?principal``` and ```?resource```, except with the identifier being replaced. It would look as follows: -``` -"slot": "?department1" -``` - - -### ```?principal``` and ```?resource``` Slots - -```?principal``` and ```?resource``` can optionally have their types annotated in ```template()```. A similiar effect can be achieved using the ```is``` operator in the condition. However, this would allow templates to be instantiated with slots that always evaluate to false. By having an explicit type annotation, we prevent these instantiations from being linked in the first place. - -Aside from the optional type annotation for ```?principal``` and ```?resource``` slots, there are some other differences between them and user defined slots. For one, ```?principal``` and ```?resource``` slots must appear in the scope of the template and can optionally be in the condition of the template, however user defined slots can only appear in the condition clause. Because of this difference ```?principal``` and ```?resource``` slots can only be filled in with entity types and user defined slots can be filled in with any ```SchemaType```. - -Currently, there is no good way forward to unify the behavior between these two kinds of slots. - ### What is allowed and not allowed? -1. Every slot not ```?principal``` and ```?resource``` needs to have a type associated with it -2. Disallow ```?action``` and ```?context``` slots -3. Annotated ```?principal``` and ```?resource``` types must be an entity type -4. All slots within the template annotation (```template()```) must be used in the template + +1. Every slot in the condition of the template must have a type annotation +2. ```?action``` and ```?context``` are reserved names +3. Slots that appear in the scope can only be of Entity type +4. ```?principal``` and ```?resource``` can only be used as how they are currently +5. All slot names must begin with ```?``` +6. All slots within the template annotation (```template()```) must be used in the template 5. ```?principal``` and ```?resource``` slots must appear in the scope -6. User defined slots can not appear in the scope -6. All slot names must beigin with ```?``` ## Drawbacks -1. Using ```?principal``` and ```?resource``` in the condition clause can cause confusion because it looks similiar to ```principal``` and ```resource```. -2. Type annotations for slots can be a user burden. +1. Type annotations for user defined slots can be a user burden. ## Alternatives -### Type Inference -We would perform type inference by considering the valid types of the slots that allow for Cedar templates to evaluate to a boolean. - -Any slot on the left or the right of a ```==, <, <=, !=``` would have type as the opposite side. Two slots cannot be compared using ```==, <, <=, !=```. - -Any slot that is being compared using ```.lessThan()``` would have ```decimal``` type. +### Performing type inference +Type inference would work by coming up with the valid types of user defined slots that result in the templates to evaluating to a boolean. -Any slot that is used with ```&&, ||, !``` has boolean type. +#### Pros: +Eliminates the user burden of providing type annotations -Any slot that is used with ```if then else ``` must have boolean type if it appears in the guard and can have AnyType +#### Downsides: +1. It could result in analysis being overly general, since it would now have to consider all possible enumerations of the types of the slots that will allow for link time validation to succeed. +2. There would need to be some restrictions on how these slots can be used which can be unintuitive for users. (```?slot1 == ?slot2```) +3. It is possible that the inferred possible types is different from what the user expects. +4. The performance of the algorthim will be worse. -Slots can only appear on the left hand side of a ```has``` and must be a type of an entity that has this attribute. +### Moving type annotations to the Schema file -... +#### Pros: +By moving the type annotations to the Schema file, the notion of types can all be kept in one place. -Downsides: -1. It could result in analysis being overly general, since it would now have to consider all possible combinations of the types of the slots that will allow for link time validation to succeed. -2. It is possible that the inferred possible types is different from what the user expects. -3. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) - -### Moving the type annotations to the Schema file rather than having them defined in the template. - -By moving the type annotations to the Schema file we can keep the notion of types all in one place. - -Downsides: -1. By moving types into the Schema file we would not be able to have slots that are localized per template since there is no way to reference a specific template in the Schema. Instead we will have to declare all the slot names and their associated types in the global namespace. -2. It is awkward to have type annotations in the Schema since when writing the Schema we have no foresight about what slots we will need in the policy. -3. It would prevent you from using link time type checking for generalized templates if you do not use a schema. +#### Downsides: +1. We would not be able to have user defined slots per template since we do not have a way of referencing particular templates from the schema. Therefore, we would have to declare user defined slots globally for all templates. +2. It may be confusing for users to need to define slots in the Schema file, as you would need to have foresight about what templates you want to design. +3. Link time type checking would not be able to be done for users that do not use schemas. ## Unresolved questions 1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. - +# Changelog since 6/2 +## Letting users define slots in the scope if they are used in the same way as how ```?principal``` and ```?resource``` are used today. +Pros: +1. Allows for users to define more suggestive names rather than using ```?principal``` and ```?resource```. +2. Gives a solution to the problem of confusing ```?principal``` and ```?resource``` when used in the condition of the template. +3. Makes clearer the distinction between ```?principal``` and ```?resource``` vs. user defined slots. +Cons: +1. It might be confusing why ```?principal``` and ```?resource``` aren't treated the same as user defined slots. \ No newline at end of file From af74f31407ea346abbf5cca6a2bb67f8efdc7cd5 Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Tue, 10 Jun 2025 15:55:59 -0400 Subject: [PATCH 19/26] updates to changelog Signed-off-by: Alan Wang --- text/0098-generalized-templates.md | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index ab90e216..c32f063a 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -16,7 +16,7 @@ ## Summary -Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates by allowing for an arbitrary number of user defined slots. User defined slots have different rules depending on whether or not they appear in the scope. If the user defined slot appears in the scope then it's type annotations are optional. Note that user defined slots that appear in the scope can only appear on the right-hand side of the ```==``` or ```in``` operators. This includes in operators when appearing together with an is operator, but excludes solitary is operators. User defined slots that appear in the scope can also be used in the condition as well. If the user defined slot appears in the condition of the template, then it must have it's type annotated and the type can be of any valid Cedar Schema Type including common types. +Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates by allowing for an arbitrary number of user defined slots. User defined slots have different rules depending on whether or not they appear in the scope. If the user defined slot appears in the scope then it's type annotations are optional. Note that user defined slots that appear in the scope can only appear on the right-hand side of the ```==``` or ```in``` operators. This includes in operators when appearing together with an is operator, but excludes solitary is operators. User defined slots that appear in the scope can be used in the condition as well. If the user defined slot appears in the condition of the template, then it must have it's type annotated and the type can be of any valid Cedar Schema Type including common types. In order to eliminate confusion, if using ```?principal``` and ```?resource``` slots they must be used exactly the same way as how they are being used currently. @@ -187,7 +187,7 @@ We restrict the usage of ```?principal``` and ```?resource``` to the current imp permit(principal == ?resources, action == Action::"Navigate", resource == ?principals) ``` -User defined slots that appear in the scope of the template will only be allowed to link with entity types. User defined slots that appear only in the condition of the template will only be allowed to be linked with values, this corresponds with the ```RestrictedExpression``` type in ```cedar-policy-core```. +User defined slots that appear in the scope of the template will only be allowed to link with Entity types. User defined slots that appear only in the condition of the template will only be allowed to be linked with values, this corresponds with the ```RestrictedExpression``` type in ```cedar-policy-core```. For users that do not use a schema, there is no notion of common types as common types only appear when using a schema. @@ -303,10 +303,15 @@ By moving the type annotations to the Schema file, the notion of types can all b 1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. # Changelog since 6/2 -## Letting users define slots in the scope if they are used in the same way as how ```?principal``` and ```?resource``` are used today. -Pros: -1. Allows for users to define more suggestive names rather than using ```?principal``` and ```?resource```. -2. Gives a solution to the problem of confusing ```?principal``` and ```?resource``` when used in the condition of the template. + +1. User defined slots are allowed to appear in the scope if they are used in the same way as how ```?principal``` and ```?resource``` is currently being used. User defined slots have different rules depending on whether or not they appear in the scope. If the user defined slot appears in the scope then it's type annotations are optional. However if provided, it must be of an Entity type. User defined slots that appear in the scope can be used in the condition as well. If the user defined slot appears in the condition of the template, then it must have it's type annotated and the type can be of any valid Cedar Schema Type including common types. + +2. ```?principal``` and ```?resource``` will be treated the same as how it is currently being used. This means that you will not be able to use it in the condition of the template nor supply type annotations. + +## Pros: +1. Allows for users to define more suggestive names in the scope rather than using ```?principal``` and ```?resource```. +2. Users aren't allowed to use ```?principal``` and ```?resource``` in the condition, so they can't be confused with the variables of the same name. This use case can still be done if the user provides their own names. 3. Makes clearer the distinction between ```?principal``` and ```?resource``` vs. user defined slots. -Cons: -1. It might be confusing why ```?principal``` and ```?resource``` aren't treated the same as user defined slots. \ No newline at end of file + +## Cons: +1. It might be confusing why ```?principal``` and ```?resource``` aren't treated the same as user defined slots. However, by doing so its gets rid of the user needing to remember corner cases. \ No newline at end of file From 1b36ab60c9855851455d222a96de2586e59e1669 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:13:45 -0400 Subject: [PATCH 20/26] Fixed missing comma --- text/0098-generalized-templates.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index c32f063a..aec64d00 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -160,7 +160,7 @@ action View appliesTo { ``` template(?department1: University::Department, ?department2: University::Department) => permit( - principal == ?principal + principal == ?principal, action == Action::"View", resource ) when { @@ -314,4 +314,4 @@ By moving the type annotations to the Schema file, the notion of types can all b 3. Makes clearer the distinction between ```?principal``` and ```?resource``` vs. user defined slots. ## Cons: -1. It might be confusing why ```?principal``` and ```?resource``` aren't treated the same as user defined slots. However, by doing so its gets rid of the user needing to remember corner cases. \ No newline at end of file +1. It might be confusing why ```?principal``` and ```?resource``` aren't treated the same as user defined slots. However, by doing so its gets rid of the user needing to remember corner cases. From 0eb54258989b15b885ad98367b523402c4e88db9 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Mon, 16 Jun 2025 16:51:10 -0400 Subject: [PATCH 21/26] Update 0098-generalized-templates.md Fixed capitalization of datetime --- text/0098-generalized-templates.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index aec64d00..83f48156 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -143,7 +143,7 @@ Suppose there are professors with dual appointments under two different departme ``` namespace University { entity Person = { - graduationDate: dateTime + graduationDate: datetime }; entity Department; entity InternalDoc in Department; @@ -152,7 +152,7 @@ namespace University { action View appliesTo { principal: University::Person, resource: University::InternalDoc, - context: { date: dateTime } + context: { date: datetime } } ``` From c421d5f410818352dd82bf7906da540277bb1a05 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Wed, 25 Jun 2025 10:39:58 -0400 Subject: [PATCH 22/26] Formatting changes --- text/0098-generalized-templates.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 83f48156..150a8cd0 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -199,6 +199,7 @@ Below I provide a brief explanation of how Cedar's typechecker will work for use Consider this schema and template: +#### Schema ``` namespace FS { entity Disk = { @@ -213,7 +214,10 @@ action Navigate appliesTo { principal: FS::Person, resource: [FS::Disk, FS::Folder, FS::Document], }; +``` +#### Template +``` permit (principal == ?person, action == Action::"Navigate", resource in ?fs) when { ?fs has storage && ?fs.storage == 5 From f0b491eb30918a908cb899a09db27c6e2c69d34f Mon Sep 17 00:00:00 2001 From: Alan Wang Date: Mon, 4 Aug 2025 16:59:32 -0400 Subject: [PATCH 23/26] updates to generalized templates proposal Signed-off-by: Alan Wang --- text/0098-generalized-templates.md | 264 ++++++++++++----------------- 1 file changed, 110 insertions(+), 154 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 150a8cd0..4be9f56a 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -16,134 +16,93 @@ ## Summary -Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the policy. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates by allowing for an arbitrary number of user defined slots. User defined slots have different rules depending on whether or not they appear in the scope. If the user defined slot appears in the scope then it's type annotations are optional. Note that user defined slots that appear in the scope can only appear on the right-hand side of the ```==``` or ```in``` operators. This includes in operators when appearing together with an is operator, but excludes solitary is operators. User defined slots that appear in the scope can be used in the condition as well. If the user defined slot appears in the condition of the template, then it must have it's type annotated and the type can be of any valid Cedar Schema Type including common types. +Cedar templates are quite restrictive. There are only two slots provided (```?principal``` and ```?resource```) and they are limited to appearing in the scope of the template. This results in users of Cedar needing to come up with their own [solution](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1632645305) to handling templates that can not be expressed in Cedar currently. In this RFC, we propose to generalize Cedar templates in two different ways: -In order to eliminate confusion, if using ```?principal``` and ```?resource``` slots they must be used exactly the same way as how they are being used currently. +1. We want to relax the restriction on the two slots (```?principal``` and ```?resource```) that Cedar currently provides to allow them to appear in the condition of the template if they also appear in the scope. -For users of Cedar who do not use a schmea, type annotations for generalized templates are optional. Templates will not be validated, but type checking will be performed during link-time. While this ensures that the provided values match the type of slot they are filling, it does not ensure that the policy won't experience a run-time type error. +2. We want to allow for an arbitrary number of user defined slots to appear in the condition (```when/unless```) clause of the template if the type is explicitly annotated. Annotated types can be of any valid Cedar Schema Type including common types. User defined slots are different from ```?principal``` and ```?resource``` slots because they can be instantiated with values that are not entity types and also can not appear in the scope. + +For users of Cedar who do not use a schema, type declarations for generalized templates are optional. Templates will not be validated, but type checking will be performed during link-time. While this ensures that the provided values match the type of slot they are filling, it does not ensure that the policy won't experience a run-time type error. ## Basic example ### Example 1 -By allowing user defined slots that appear in the scope to also appear in the condition of the template, we are able to access attributes of that slot. In this example, this allows us to express the constraint that we can only access resources whose owner is the same as the owner of the entity that we instantiate for the ```?fs``` slot. +Suppose you are building a document signing application. For security purposes, you want to make sure that whenever someone shares a document the receiver can only access it for x amount of days. We can use generalized templates to define this as shown below. + +Everytime this template is instantiated the slots ```?principal``` and ```?resource``` will be replaced with the entity type that represents the person that you want to share the document with and the entity type representing the document that you want to share. Additionally ```?startTime``` and ```?endTime``` will be replaced with the datetime bounds. + +By using generalized templates compared to an attribute of an entity to express this policy, we do not have to store information that is only relevant to our authorization decisions within an external data store. This allows us to have a cleaner seperation of concerns. #### Schema ``` -namespace FS { - entity Disk = { - owner: String, - }; - entity Folder in Disk = { - owner: String, - }; - entity Document in Folder = { - owner: String, - }; - entity Person; -} - -action Navigate appliesTo { - principal: FS::Person, - resource: [FS::Disk, FS::Folder, FS::Document], +entity Document = { + owner: Person }; +entity Person; -action Write appliesTo { +action Access appliesTo { principal: FS::Person, - resource: [FS::Disk, FS::Folder, FS::Document], + resource: [FS::Document], + context: { date: datetime } }; ``` -#### Cedar Template +#### Template ``` -permit( - principal == ?person, - action, - resource in ?fs) -when { - ?fs.owner == resource.owner -}; +template(?startTime: datetime, ?endTime: datetime) => +permit(principal == ?principal, +action, +resource == ?resource) when +{ ?startTime <= context.now && +context.now <= ?endTime }; ``` -### Example 2 +### Example 2 +In this example, suppose we have a file sharing application where we can create folders and documents. Every document created must be in a folder. We want to express the policy that if you are an owner of the folder then you can access any document within it. We can use generalized templates to define this as shown below. -By allowing arbitrary user defined slots, we are able to express the following Cedar template. This example was taken directly from a user of Cedar in [#7](https://github.com/cedar-policy/rfcs/pull/7). +Now everytime we create a folder, we link ```?resource``` with that folder to express this relationship. -#### Schema +An alternative way to do this is to store an additional owner attribute for every document, however this has a couple of drawbacks compared to using Generalized Templates. + +(1) We lose the intent behind why we are authoring this policy. + +(2) When transferring ownership of a folder to someone else you would have to manually update the owner attribute for all document's that belong to that folder + +#### Schema ``` namespace FS { - entity Disk; - entity Folder in Disk; + entity Folder; entity Document in Folder; - entity Person; + entity Person = { + owned_documents: Set + }; } -action Navigate appliesTo { +action AccessDocument appliesTo { principal: FS::Person, - resource: [FS::Disk, FS::Folder, FS::Document], -}; - -action Write appliesTo { - principal: FS::Person, - resource: [FS::Disk, FS::Folder, FS::Document], -}; -``` - -#### Cedar Template -``` -template(?folder: FS::Folder) => -permit( - principal == ?principal, - action, - resource in ?resource) -when { - // take any action in the scope that you're admin on - resource in ?folder - - // allow access up the tree for navigation - || (action == Action::"Navigate" && ?folder in resource) + resource: FS::Document, }; ``` -### Example 3 - -Suppose that a company only wants to provide access to it's internal services only when the employee starts working. We can now use Generalized Cedar templates to define it as follows: - -#### Schema +#### Template ``` -namespace Company { - entity Employee; - entity InternalServices; -} - -action Access appliesTo { - principal: Company::Employee, - resource: Company::InternalServices, - context: { date: datetime } +permit(principal, action == Action::"AccessDocument", resource in ?resource) { + ?resource in principal.owned_documents } ``` -#### Template -``` -template(?date: datetime) => -permit( - principal == ?principal, - action == Action::"Access", - resource is Company::InternalServices -) when { - context.date > ?date -}; -``` +### Example 3 -### Example 4 +Suppose there are certain professors with dual appointments under two different departments who want to give students of their group access to both the resources in the first department and the resources in their second department. -Suppose there are professors with dual appointments under two different departments who want to give students of their group access to both the resources in the first department and the resources in the second department. We can implement this template currently in Cedar by creating two seperate templates and instantiating them individually. The downside of this is that it would be up to the user of Cedar to ensure that they have made sure to instantiate both templates. Previously, [template groups](https://github.com/cedar-policy/rfcs/pull/7) was proposed as a solution to the problem mentioned above. However, with Generalized Cedar templates, we can solve this problem as follows: +Note: Although we can create two seperate templates and instantiate them individually, we would need to make sure they stay in sync. With generalized templates, since there is only one template we do not need to do so. Error states where only one part of the template is applied but not the other would not be able to occur. Generalized templates allows us to subsume the functionality described in [#7](https://github.com/cedar-policy/rfcs/pull/7) and with typed slots we can express the motivating example for template-groups. #### Schema ``` namespace University { entity Person = { - graduationDate: datetime + graduationDate: dateTime }; entity Department; entity InternalDoc in Department; @@ -152,7 +111,7 @@ namespace University { action View appliesTo { principal: University::Person, resource: University::InternalDoc, - context: { date: datetime } + context: { date: dateTime } } ``` @@ -160,7 +119,7 @@ action View appliesTo { ``` template(?department1: University::Department, ?department2: University::Department) => permit( - principal == ?principal, + principal == ?principal action == Action::"View", resource ) when { @@ -174,28 +133,13 @@ permit( This is a follow up on the discussion on [#3](https://github.com/cedar-policy/rfcs/pull/3). -Cedar templates offer a way to change a group of policies overtime and to prevent against injection attacks that can occur when creating policies at runtime. However, there are policies that users of Cedar want to create at runtime that can't be expressed using templates today. By generalizing Cedar templates, we hope to allow for more users to be able to use templates while still balancing Cedar's core features: validation, analysis, and performance. +Cedar templates offer a way to change a group of policies overtime and to prevent against injection attacks that can occur when creating policies at runtime. However, there are policies that users of Cedar want to create at runtime that can't be expressed using templates today. By generalizing Cedar templates, we hope to allow for more users to be able to use templates while still balancing Cedar's core features: validation, analysis, performance, and ergonomics. -While annotating the types of user defined slots inccurs some user burden, it allows us to express examples #2, #3, and #4 while still supporting validation and analysis. It also allows us to keep Cedar performant. With types, link time validation only requires checking that the supplied values have the same type as what is annotated, the alternative being running the type checker everytime you instantiate your template. Types also serve as a form of documentation that can help you remember what your templates are able to be linked against. +While annotating the types of user defined slots inccurs some user burden, it allows us additional expressivity while still supporting validation and analysis. It also allows us to keep Cedar performant. With types, link time validation only requires checking that the supplied values have the same type as what is annotated, the alternative being running the type checker everytime you instantiate your template. Types also serve as a form of documentation that can help you remember what your templates are able to be linked against. ## Detailed design - -### Details -We restrict the usage of ```?principal``` and ```?resource``` to the current implementation of templates in Cedar. Although, it would have been possible to allow for ```?principal``` and ```?resource``` to appear in the condition of the template, it can be confusing to distinguish between slots and variables. Therefore, only user defined slots that appear in the scope are allowed to be in the condition of the template. Note that just like in a typical programming language, nothing prevents you from coming up with confusing slot names, but ultimately this is up to the user's discretion. A template such as the following can be expressed: - -``` -permit(principal == ?resources, action == Action::"Navigate", resource == ?principals) -``` - -User defined slots that appear in the scope of the template will only be allowed to link with Entity types. User defined slots that appear only in the condition of the template will only be allowed to be linked with values, this corresponds with the ```RestrictedExpression``` type in ```cedar-policy-core```. - -For users that do not use a schema, there is no notion of common types as common types only appear when using a schema. - ### Implementation - -To allow for the arbitrary user defined slots, we will need to modify the parser, type checker, AST. The modfications needed for the typechecker will not be signficant. - -Below I provide a brief explanation of how Cedar's typechecker will work for user defined slots that appear in the scope: +Below I provide a brief explanation of how Cedar's typechecker will work for ```?principal``` and ```?resource``` slots in the condition of the template and for user defined slots. Consider this schema and template: @@ -215,16 +159,14 @@ action Navigate appliesTo { resource: [FS::Disk, FS::Folder, FS::Document], }; ``` - #### Template ``` -permit (principal == ?person, action == Action::"Navigate", resource in ?fs) +permit (principal == ?principal, action == Action::"Navigate", resource in ?resource) when { - ?fs has storage && ?fs.storage == 5 + ?resource has storage && ?resource.storage == 5 }; ``` - -Cedar's typechecker works by enumerating all possible request environments for a particular action. For the action ```Navigate```, the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Under these individual request environments, we then generate the possible slot types for ```?person``` and ```?fs```. So far, this proceeds exactly as it would with Cedar templates currently, the only difference being a change in the slot names. +Currently, how Cedar's typechecker works is by enumerating all possible request environments for a particular action. Based off this schema, the possible ```principal``` and ```resource``` pairs would be ```(FS::Person, FS::Disk)```, ```(FS::Person, FS::Folder)```, ```(FS::Person, FS::Document)```. Under these individual request environments, we can generate the possible slot types for principal and resource. | Request Environment | Principal Slot Types | Resource Slot Types | -------- | ------- | ------- | @@ -232,13 +174,14 @@ Cedar's typechecker works by enumerating all possible request environments for a | ```(FS::Person, FS::Folder)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder``` | | ```(FS::Person, FS::Document)``` | ```?principal: FS::Person``` | ```?resource: FS::Disk```, ```?resource: FS::Folder```, ```?resource: FS::Document``` | -Under each individual enumeration, we now check to see if these respective assignment of types to variables and user defined slots evaluates to a boolean. If every enumeration does, then our template passes the typechecker, otherwise it fails. With this extension, we would just need to ensure that for all enumerations, the condition of the policy also evaluates to a boolean. +Under each individual enumeration, we now check to see if these respective assignment of types to variables and user defined slots evaluates to a boolean. If every enumeration does, then our template passes the typechecker, otherwise it fails. With ```?principal``` and ```?resource``` now appearing in the condition of the template, we would just need to use the type supplied by the request environment to type check it. -Since user defined slots that only appear in the condition of the template are required to have their types annotated, we do not need to perform this enumeration. Instead, now we use the type supplied by the user for the user defined slots and see if the template evaluates to a boolean type. +Since user defined slots are required to have their types annotated, we do not need to perform this enumeration. Instead, now we use the type supplied by the user and see if the template evaluates to a boolean type. -### Users of Cedar that do not use a Schema +Note: Typed slots can only be instantiated with value types. In the implementation this corresponds to the ```RestrictedExpression``` type. -For users that do not use a schema, the user defined slots can be optionally annotated with types. If the types are annotated, generalized templates link time type checking will be performed. Here, it is up to the user to provide the correct types as without a schema. Note that even if types are supplied, there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only guarantee provided when you do not use a schema is if you annotate a user defined slot with a type, the value you instatiate the slot with is of the type that you had supplied. +### Users of Cedar that do not use a Schema +For users that don't provide a schema, generalized templates will support optional typed slots with link time type checking. Here, it is up to the user to provide correct types. Note that without schemas there are no guarantees made about the runtime behavior of your program. Policies such as the following, where ```?bound1``` is provided a substitution of ```true``` will still be able to be expressed and an error will be thrown at runtime. The only guarantee that is provided when you do not use a schema with generalized templates is that if you annotate the slot with a type, the value you substitute in for ```?bound1``` is indeed of the type that you had specified, in this case ```Bool```. ``` template(?bound1: Bool) => @@ -251,10 +194,10 @@ permit ( }; ``` -### Syntax +In addition, there is some subtlety involved when handling type declarations involving primitive types. The main issue stems from entity types being allowed to shadow primitive type. Without a schema to distinguish whether or not this is the case, we opt to be more permissive. We interpret primitive types as both entity types and Cedar primitive types and typechecking passes if one of the cases typechecks. -The proposed syntax for generalized templates looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and must come after all annotations. -Each new user defined requires a distinct variable name. User defined slots in the scope must be unique. However, within the condition clause the same user defined slot can be used multiple times. The grammar of template annotations is as follows: +### Syntax +The proposed syntax looks as follows ```template(?bound1: type1, ?bound2: type2) =>``` and types specified must be valid schema types. Schema types are chosen over AST types because they allow us to more precisely specify the type for sets and records. Each new typed slot requires a distinct variable name. However, within the ```when/unless``` clause the same typed slot can be used multiple times. The grammar of template declarations is as follows. ```Type``` is taken directly from the Cedar documentation for schema types. The template syntax (```template(?bound1: type1, ?bound2: type2) =>```) must go after all the declarations. ``` Template := 'template' '(' ( TypeAnnotation { ',' TypeAnnotation } ) ')' '=>' @@ -264,58 +207,71 @@ TypeAnnotation := ‘?’ IDENT ‘:’ Type Type := Path | SetType | RecType ``` -### What is allowed and not allowed? +### JSON Policy Format +The changes to the JSON policy format would include another attribute ```typed_slots``` and would look as follows: +``` +"typed_slots": [ + { "type": "University::Department", "id": "?department1" }, + { "type": "University::Department", "id": "?department2" }, +] +``` -1. Every slot in the condition of the template must have a type annotation -2. ```?action``` and ```?context``` are reserved names -3. Slots that appear in the scope can only be of Entity type -4. ```?principal``` and ```?resource``` can only be used as how they are currently -5. All slot names must begin with ```?``` -6. All slots within the template annotation (```template()```) must be used in the template +In the JSON policy format, typed slots can be referred to with the same syntax as what is done for ```?principal``` and ```?resource```, except with the identifier being replaced. It would look as follows: +``` +"slot": "?department1" +``` + + +### ```?principal``` and ```?resource``` Slots + +```?principal``` and ```?resource``` can optionally have their types annotated in ```template()```. A similiar effect can be achieved using the ```is``` operator in the condition. However, this would allow templates to be instantiated with slots that always evaluate to false. By having an explicit type annotation we prevent these instantiations from being linked in the first place. + +Aside from the optional type annotation for ```?principal``` and ```?resource``` slots, there are some other differences between them and user defined slots. For one, ```?principal``` and ```?resource``` slots must appear in the scope of the template and can optionally be in the condition of the template, however user defined slots can only appear in the condition clause. Because of this difference ```?principal``` and ```?resource``` slots can only be filled in with entity types and user defined slots can be filled in with any ```SchemaType```. + +### What is allowed and not allowed? +1. Every user defined slot needs to have a type associated with it +2. Disallow ```?action``` and ```?context``` slots +3. Annotated ```?principal``` and ```?resource``` types must be an entity type +4. All slots within the template declaration (```template()```) must be used in the template 5. ```?principal``` and ```?resource``` slots must appear in the scope +6. User defined slots can not appear in the scope +6. All slot names must begin with ```?``` ## Drawbacks -1. Type annotations for user defined slots can be a user burden. +1. Using ```?principal``` and ```?resource``` in the condition clause can cause confusion because it looks similiar to ```principal``` and ```resource```. +2. Type declarations for slots can be a user burden. ## Alternatives -### Performing type inference -Type inference would work by coming up with the valid types of user defined slots that result in the templates to evaluating to a boolean. +### Type Inference +We would perform type inference by considering the valid types of the slots that allow for Cedar templates to evaluate to a boolean. -#### Pros: -Eliminates the user burden of providing type annotations +Any slot on the left or the right of a ```==, <, <=, !=``` would have the same type as the opposite side. Two slots cannot be compared using ```==, <, <=, !=```. -#### Downsides: -1. It could result in analysis being overly general, since it would now have to consider all possible enumerations of the types of the slots that will allow for link time validation to succeed. -2. There would need to be some restrictions on how these slots can be used which can be unintuitive for users. (```?slot1 == ?slot2```) -3. It is possible that the inferred possible types is different from what the user expects. -4. The performance of the algorthim will be worse. +Any slot that is being compared using ```.lessThan()``` would have ```decimal``` type. -### Moving type annotations to the Schema file +Any slot that is used with ```&&, ||, !``` has boolean type. -#### Pros: -By moving the type annotations to the Schema file, the notion of types can all be kept in one place. +Any slot that is used with ```if then else ``` must have boolean type if it appears in the guard and can have AnyType -#### Downsides: -1. We would not be able to have user defined slots per template since we do not have a way of referencing particular templates from the schema. Therefore, we would have to declare user defined slots globally for all templates. -2. It may be confusing for users to need to define slots in the Schema file, as you would need to have foresight about what templates you want to design. -3. Link time type checking would not be able to be done for users that do not use schemas. +Slots can only appear on the left hand side of a ```has``` and must be a type of an entity that has this attribute. -## Unresolved questions +... -1. What should the syntax be for supplying aribtrary bound variables be. There was some discussion of it [here](https://github.com/cedar-policy/rfcs/pull/3#issuecomment-1611845728). Initial thoughts are to ensure that the user supplies a map so there is no confusion with regards to ordering. +Downsides: +1. It could result in analysis being overly general, since it would now have to consider all possible combinations of the types of the slots that will allow for link time validation to succeed. +2. It is possible that the inferred possible types is different from what the user expects. +3. There would need to be some restrictions on where slots can appear which can be unintuitive for users. (```?slot1 == ?slot2```, would result in us only being able to infer the type of the slot as AnyType) -# Changelog since 6/2 +### Moving the type declarations to the Schema file rather than having them defined in the template. -1. User defined slots are allowed to appear in the scope if they are used in the same way as how ```?principal``` and ```?resource``` is currently being used. User defined slots have different rules depending on whether or not they appear in the scope. If the user defined slot appears in the scope then it's type annotations are optional. However if provided, it must be of an Entity type. User defined slots that appear in the scope can be used in the condition as well. If the user defined slot appears in the condition of the template, then it must have it's type annotated and the type can be of any valid Cedar Schema Type including common types. +By moving the type declarations to the Schema file we can keep the notion of types all in one place and also not have to deal with the duplication of code to parse types. -2. ```?principal``` and ```?resource``` will be treated the same as how it is currently being used. This means that you will not be able to use it in the condition of the template nor supply type annotations. +Downsides: +1. By moving types into the Schema file we would not be able to have slots that are localized per template since there is no way to reference a specific template in the Schema. Instead we will have to declare all the slot names and their associated types in the global namespace. +2. It is awkward to have type declarations in the Schema since when writing the Schema we have no foresight about what slots we will need in the template. +3. It would prevent you from using link time type checking for generalized templates if you do not use a schema. -## Pros: -1. Allows for users to define more suggestive names in the scope rather than using ```?principal``` and ```?resource```. -2. Users aren't allowed to use ```?principal``` and ```?resource``` in the condition, so they can't be confused with the variables of the same name. This use case can still be done if the user provides their own names. -3. Makes clearer the distinction between ```?principal``` and ```?resource``` vs. user defined slots. +## Unresolved questions -## Cons: -1. It might be confusing why ```?principal``` and ```?resource``` aren't treated the same as user defined slots. However, by doing so its gets rid of the user needing to remember corner cases. From 3e6f896f368c1cd7065dbf7a339984b31ddb2025 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Tue, 5 Aug 2025 11:22:41 -0400 Subject: [PATCH 24/26] Fixed typo --- text/0098-generalized-templates.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 4be9f56a..569ce810 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -75,7 +75,7 @@ namespace FS { entity Folder; entity Document in Folder; entity Person = { - owned_documents: Set + owned_folders: Set }; } @@ -88,7 +88,7 @@ action AccessDocument appliesTo { #### Template ``` permit(principal, action == Action::"AccessDocument", resource in ?resource) { - ?resource in principal.owned_documents + ?resource in principal.owned_folders } ``` From feb8a9d0b81fa1588a97af70f9ab0543a61ed570 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Tue, 12 Aug 2025 14:51:21 -0400 Subject: [PATCH 25/26] Fixed typo --- text/0098-generalized-templates.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 569ce810..73350f7b 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -87,9 +87,9 @@ action AccessDocument appliesTo { #### Template ``` -permit(principal, action == Action::"AccessDocument", resource in ?resource) { +permit(principal, action == Action::"AccessDocument", resource in ?resource) when { ?resource in principal.owned_folders -} +}; ``` ### Example 3 From a58f491fdb5a6681860c1c8f0cfc2501cce0bd50 Mon Sep 17 00:00:00 2001 From: Alan Wang <33503035+alanwang67@users.noreply.github.com> Date: Tue, 12 Aug 2025 16:47:10 -0400 Subject: [PATCH 26/26] removed extra space --- text/0098-generalized-templates.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/text/0098-generalized-templates.md b/text/0098-generalized-templates.md index 73350f7b..8a64eb21 100644 --- a/text/0098-generalized-templates.md +++ b/text/0098-generalized-templates.md @@ -176,7 +176,7 @@ Currently, how Cedar's typechecker works is by enumerating all possible request Under each individual enumeration, we now check to see if these respective assignment of types to variables and user defined slots evaluates to a boolean. If every enumeration does, then our template passes the typechecker, otherwise it fails. With ```?principal``` and ```?resource``` now appearing in the condition of the template, we would just need to use the type supplied by the request environment to type check it. -Since user defined slots are required to have their types annotated, we do not need to perform this enumeration. Instead, now we use the type supplied by the user and see if the template evaluates to a boolean type. +Since user defined slots are required to have their types annotated, we do not need to perform this enumeration. Instead, now we use the type supplied by the user and see if the template evaluates to a boolean type. Note: Typed slots can only be instantiated with value types. In the implementation this corresponds to the ```RestrictedExpression``` type.