Cedar security

This section provides information about security as it relates to the Cedar policy language.

Topics on this page

Shared responsibility
Security of Cedar
Security of applications using Cedar
- Understanding Cedar semantics
- Validating your Cedar policies against your schema
Input Validation
Security best practices for applications using Cedar

Shared responsibility

Security is a shared responsibility between Cedar and its users. It is the responsibility of Cedar to correctly evaluate policies to arrive at an authorization decision. It is the responsibility of users of Cedar to correctly define policies that implement their authorization model. Although Cedar provides tools such as the policy validator to validate your policies against the schema, it is ultimately the user’s responsibility to write policies correctly.

Security of Cedar

It is the responsibility of Cedar to implement the Cedar policy language correctly as described in this guide.

We, members of the Cedar development team, ensure Cedar’s correctness and security by developing several artifacts:

A formal model implemented in Dafny. Dafny is an open-source, verification-aware programming language. The Dafny model consists of executable definitions of Cedar’s components which represent the semantics of Cedar, and properties of those components. Dafny verifies that the properties hold. It gives us confidence that our definition of the ground truth is correct.
A production authorization engine written in Rust. We use only the safe subset of Rust, giving us memory safety, type safety, and data-race safety.
A differential testing engine that can test automatically that #1 and #2 have the same semantics.

[How Cedar is verified as correct and secure.]

In particular, Cedar provides two properties about authorization queries:

default-deny – Authorization queries result in a Deny unless an explicit permit policy evaluates to true.
forbid-trumps-permit – A single forbid policy evaluating to true results in a Deny.

Security of applications using Cedar

It is the responsibility of applications using Cedar to implement their authorization logic correctly using Cedar policies. To do this, application developers must understand the semantics of Cedar policies. Developers should understand the risks associated with an incorrectly implemented authorization model and take appropriate steps to mitigate those risks. We will provide customers with tools to help them author correct and secure policies, such as policy validation, semantic analysis, and policy templates.

Understanding Cedar semantics

To create correct authorization policies, developers must understand the semantics of Cedar. This guide contains a detailed description of every feature of the language and how it is evaluated. It also includes several examples.

Developers must understand how the results of evaluating individual policies are combined to reach an authorization decision. In particular, note the following:

default-deny – Authorization queries will result in a Deny unless an explicit permit policy evaluates to true.
forbid-overrides-permit – A single forbid policy evaluating to true results in a Deny.
An error in a policy results in that policy being ignored for the purpose of an evaluation decision. (skip-on-error semantics)

Validating your Cedar policies against your schema

Cedar users can check that policies are consistent with a schema. The schema defines the expected structure and type of Cedar entities represented in requests. In particular, the schema defines the set of entity types and how they are used (as actions, principals, or resources), how entities can be grouped into a hierarchy, and what attributes the entities have. Users can validate a policy before adding it to the store. By providing a schema, policies that pass validation don’t result in runtime errors when they are run against schema-compliant entities and requests.

The Cedar validator can detect the many types of bugs, including the following:

Detect unrecognized entity types and actions – For example, misspelling “Album” as “Albom” or “viewPhoto” as “viewPhoot”.
Detect actions being applied to unsupported principals and resources – For example, saying that a Photo can View a User.
Detect improper use of in or == – For example, writing principal in Album::"trip" when principal cannot be a Photo.
Detect unrecognized attributes – For example, referencing principal.jobbLevel when the attribute should be jobLevel.
Type mismatches in attributes – For example, principal.hireDate + 3 (Illegal to add integers and dates)
Detect optional attributes referenced without an existence check. – For example, principal.optionalValue < 100 instead of principal has optionalValue && principal.optionalValue < 100
Detect invalid parameters to the constructors of extension types. – For example, IP("3.45.1111.43") isn’t a valid IP address.

Writing a schema and using the policy validator can give you increased confidence that you’ve written your authorization policies correctly. It is your responsibility to write a schema that correctly models your data. It is the responsibility of Cedar to ensure that the validator is correct. We achieve a high confidence in the correctness of the validator by formally modeling it using Dafny. We have proved the correctness of the validation algorithm, and we use differential testing to ensure the production validator matches the behavior of the formal model. For more information, see Cedar policy validation against schema.

Input Validation

The Cedar spec places no restrictions on the size of Cedar policies, schemas, or requests. It is important for services accepting arbitrary Cedar inputs to place a bound on input sizes to protect against memory exhaustion. The parsers provided by Cedar are safe to execute on bounded, arbitrary inputs, and are the suggested way to validate inputs. Cedar policies of a bounded size are guaranteed to terminate, and are effect free.

Security best practices for applications using Cedar

Some security best practices for applications that use Cedar are as follows:

Policies should follow the principle of least privilege. Grant only the permissions required to perform the task at hand.
Be careful about who you allow to modify your policies. We’ve endeavored to make Cedar a safe environment in which to evaluate policies, there are always risks when it comes to running arbitrary code submitted by users. Here are a few things to keep in mind if you plan on evaluating arbitrary cedar policies submitted by end users.
- Cedar has no facilities for I/O, so Cedar policies are unable to perform activities like reading files or talking to the network.
- The evaluation of one Cedar policy can’t effect the evaluation of another policy.
- While all Cedar policies are guaranteed to terminate, a malicious user could attempt to submit very lengthy policies, incurring either storage or performance costs. If you are evaluating arbitrary Cedar policies, we recommend that you put a length limit in place.
- Cedar provides on authorization – determining what an authenticated user can do. However, Cedar does not perform authentication – verifying the identity of the users who attempt to access your application. You application must provide authentication services separately and then proceed with authorization of only successfully authenticated users.
Write a schema and have Cedar validate it to ensure your authorization policies don’t encounter runtime errors.
Put all authorization logic in your Cedar policies. Don’t spread authorization logic around different locations in your application.
Use policy templates where applicable to avoid duplicating authorization logic. This approach also provides a single location for future changes. (Don’t-Repeat-Yourself)
If you create policies dynamically, avoid using string concatenation. Instead, use policy templates. Creating policies with string concatenation is error-prone and insecure. If an attacker gained control of the inputs to concatenation, they could achieve code injection.

Here, “code injection” refers to injection of Cedar code, not arbitrary code execution. It is the responsibility of the Cedar library to prevent arbitrary code injection.

For example, consider a policy dynamically created as shown here:
```
 let src = "permit (" + input + ", action == Action::\"view\", resource) when { principal.level > 3 }";
 let policy = parse(src);
 addToPolicySet(policy);
```
You could provide a good value for input, such as principal == User::"alice". That value works fine and produces the following policy in variable src.
```
 permit (principal == User::"alice", action == Action::"view", resource) when { principal.level > 3 };
```
But, if an attacker could somehow control the value for input, they could achieve Cedar code injection. For example, if the attacker set input to the following.
```
 "principal,action,resource); //"
```
The completed policy in src would look like the following example.
```
 permit (principal,action,resource); //, action == ,Action::"view", resource) when { principal.level > 3 };
```
That policy permits all actions on all resources by anyone, regardless of level.
Use unique, immutable, and non-recyclable IDs for entity identifiers. An example of a mutable identifier is a username or group name in a workforce directory, where the value of the name can change. For example, consider the following policy.
```
 permit (principal == User::"alice",action in ...,resource in ...);
```
Imagine that Alice leaves the organization, and another user named Alice joins the organization. If the new Alice reuses the “alice” username, then she would attain the permissions of any lingering policies that hadn’t been removed.

For these reasons, policies must refer to only unique, normalized, immutable, and non-recyclable identifiers. We recommend that you use UUIDs or similar formats that meet the same criteria, such as sequence numbers or URNs.
```
 permit (
     principal == User::"2dad2883-cba1-4a1e-b212-a6c0a5290dad", // "Alice"
     action in ...,
     resource in ...
 );
```
Ensure that data used for authorization decisions, such as policies, entities, or context information, can’t be accessed or modified by potential attackers.
Normalize input data prior to invoking the authorization APIs.