Authorization with Cedar
The goal for this week is to understand what Cedar does and why Amazon built it. The security aspect is important: OWASP Top 10 Proactive Controls "C1: Implement Access Control" recommends many of these principles. We also care about how they built Cedar because Verification-Guided Development is a realistic approach to high-assurance software development, including assurances for security objectives. If you survive this week, you should be able to
- explain what Cedar actually is and why Amazon built it in this complicated manner,
- define simple policy rules in Cedar and call them from a python project, and
- advocate with fanatical passion for the wider adoption of Verification-Guided Development at work and beyond.
Background on Access Control
As we are considering Cedar mainly a case study in verification-guided development, we will not dive too deeply into the theory of access control. But we want to understand the concepts and problems that Cedar is trying to solve, especially since authorization is such a difficult area of cyber security. For this, you may consult the following:
- An overview of access control is given by Dieter Gollmann at the CyBOK Authentication, Authorization and Accountability knowledge area webinar (slides).
- For an overview of Cedar and why Amazon built it...
- you may watch the industry-oriented hype (it is actually reasonably interesting),
- but hopefully you prefer the more academically oriented talk by Emina Torlak.
- Most importantly, the Cedar documentation has an important section on Terminology and Cedar Design Patterns, which explains how traditional access control models are expressed in Cedar.
Cedar Tutorial (with PyCedar and VSCode)
You can simply do the Cedar tutorial online, but it is nice to see how it works in VSCode. There is a series of videos on the cedar-craft channel that takes this approach. With `cedarpy` we have a more realistic integration (and tool support) than the online interfaces; in particular, both policies and entities are validated against the schema and mistakes are shown in the IDE.
Installation
You should have a sufficiently recent version of python installed; this was tested with Python 3.13.2.
- you should install VSCode and make sure you can open it from the command line with
code .which might not work out-of-the-box on MacOS, see instructions. - Next, and this is very important, you need to install the VSCode plugin.
- Finally, you should use git to download the support code:
git clone https://github.com/sws-lab/softsec25 cd softsec2025 python3 -m venv .venv source .venv/bin/activate cd cedar/tutorial pip install -r requirements.txt code .
For these exercises, there are also machine-generated instructions for these exercises. I did have to edit some of it, but mostly these readme files are generated based on the test cases by Claude 3.5 Sonnet, so let's see if you find it more helpful than what I write here. Certainly, it has good instructions for how to run the tests!
As you may note by the titles, I really like the Cedar design pattern discussion of access control in terms of the external data each policy depends upon.
Exercise 1: Discretionary Access Control
In this light, discretionary rules in Cedar do not depend on anything other than what we write in the policy. To emphasize this fact, we can just give the Cedar engine an empty list of entities. In general, making manual choices about which entities are relevant is dangerous, which is why the official tutorial is not as reckless, but with only two hard-coded rules, it is evident that the result will be the same.
For the first exercise, you'll only need to edit disc.cedar; however, you should look at the elegant schema defined in disc.cedarschema.
entity Photo;
entity User;
action "update", "view", "delete" appliesTo {
principal: User,
resource: Photo,
};
This will make sure that VSCode will not allow you to write nonsense actions, such as "edit" instead of "update", and will complain if a policy tries to allow a Photo to edit a Human; remember, we should not anthropomorphize Photos! Anyway, now you can do the things suggested in the tutorial:
- Policy Structure. Based on the existing rule in disc.cedar that allows Alice to update her photo, add a new allow rule for Bob to view Portrait.jpg.
- Forbid Policies. Try to add the forbid policy, just to check that the tests now fail. You will not get any points for this, but you should try things out because Cedar is mysterious and important.
- Sets: Modify the Alice's rule so that she can view and delete VacationPhoto94.jpg (or delete and view, we are not bound by the order of things).
Exercise 2: Membership Permissions
Now we consider the tutorial's example on Role-Based Access Control. Here, we do need to edit mem.cedarentities.json for user and group definitions, and add one rule for the new group to mem.cedar.
- First, edit mem.cedarentities.json to add Eve as a new user and create the PhotographyJudge group, then add Eve as a member of this group. This should be completely analogous to what is already there. Also, add a new allow rule in mem.cedar for PhotographyJudge to view genericPhoto.jpg, again completely identical to the others.
- Next, modify `mem.cedarentities.json` to add PhotographyJudge as a parent of vacationPhotoJudges and juniorPhotographerJudges, which also syntactically identical to what is there before.
Exercise 3: Relational Permissions
For the final exercise, we skip basic attribute usage and jump to Attribute-based access control (part 2), where permissions are determined by relationships between principals and resources. The schema and entity files (rel.cedarschema and rel.cedarentities.json) are already set up with the necessary relationships from the original tutorial, so you'll focus on the policy rules in rel.cedar.
Start by examining the existing ownership rules in rel.cedar, and add a department-based rule very similar to the existing one. This is actually easier than the previous exercise, but I think you know enough to jump to next project.
Submit your solution to moodle.
Grand Challenge: Rewrite Permissions with Cedar
This challenge is not really that grand, but I needed to distinguish it from the previous exercises. The task here is simply to refactor a beautiful python web app that I generated with Claude 3.5 because this could be the Uber of Instagrams if I could only get access rights correctly implemented. After some high-level prompt-engineering I managed to refactor the access control to be consolidated, and I believe it is correct, but it's expressed in these complicated attribute-based formulas (app.py#L46-L59). The goal would be refactor this into a Cedar-based app: photoapp-cedar. Most of it works, but I need help with the Cedar policies!
Basically, you should edit the file policies.cedar, and it should be enough to only edit that file. Here are the policies you should express:
- Any user can see public images.
- Any user can view and delete their own images.
- The admin can delete public images of any user.
- Users under the age of 18 (or guests) should not see images marked explicit.
Try to make it so that there is a one-to-one relationship between these requirements and your policies; otherwise, I could just have used the boolean formulas. I need your policies to be expressed in a way that my auditor can understand, please!
Testing ...
You should be able to test the thing if you set it up and run like above:
cd 02-cedar/photoapp-cedar python3 -m venv .venv source .venv/bin/activate pip install -r requirements.txt pytest -v
Submit your solution to moodle.
Is it safe?
This was a Claude-generated thing, and the first version just put all images in a static folder, so all authorization checks could be bypassed (Insecure Direct Object Reference). I prompted Claude to fix this, but if you want bonus points, feel free to find vulnerabilities in the code.