Cedar - Emina Torlak

Stream: Lean Together 2024

[David Thrane Christiansen]

Cedar in Lean

[David Renshaw]

Can Cedar express something like this?
"Alice is allowed to share her documents with anyone on the engineering team."
That is, Alice is allowed to edit her Cedar policies in a constrained way.

[Henrik Böving]

For the FFI memory leaks: Are you aware of the difference between borrowed and non borrowed arguments in Lean, they influence how reference counting is done. I recall that I used to have issues with properly freeing memory in my FFI code because I didn't account for borrowed vs non borrowed arguments.

[Kesha Hietala]

We haven't looked too much into the memory leaks yet, but know they're there :sweat_smile:

We're using the lean-sys crate for FFI. We'd love help improving our code if anyone is interested! Cedar's formalization is available open-source in https://github.com/cedar-policy/cedar-spec . The Lean code is in cedar-spec/cedar-lean/ and the relevant FFI is in cedar-spec/cedar-drt/src/lean_impl.rs. Feel free to file issues or open pull requests :smiley:

[Kesha Hietala]

David Renshaw said:

Can Cedar express something like this?
"Alice is allowed to share her documents with anyone on the engineering team."
That is, Alice is allowed to edit her Cedar policies in a constrained way.

Cedar policies use a <principal, action, resource, context> request format. In this case, the principal would be Alice and action would be Share. The resource could be either the document or the sharee depending on your model -- let's say it's the sharee and that we put the relevant document into the context. The policy might look like:

permit(
  principal == User::"Alice",
  action == Action::"Share",
  resource in Team::"Engineering"
);

We have a variety of resources for learning about Cedar (see references linked here). My favorite is the interactive Cedar tutorial.