cedar-lean

Cedar Lean

This folder contains the Lean formalization of, and proofs about, Cedar.

Auto-generated documentation is available at https://cedar-policy.github.io/cedar-spec/docs/.

Setup

Follow these instructions to set up Lean and install the VS Code plugin.

Usage

To use VS Code, open the cedar-lean folder as the root directory.

Warning

The VS Code Lean plugin will not work properly if this project is opened with cedar-spec as the root.

To build code and proofs from the command line:

cd cedar-lean
lake update
lake build Cedar

To run the unit tests:

lake exe CedarUnitTests

We provide a CLI for CedarLean in cedar-lean-cli. You can find its usage here.

Updating the Lean toolchain

To change the version of Lean used, you will need to update three files:

• lean-toolchain controls the Lean version. You can find all available versions here.
• lakefile.lean lists the project dependencies. Make sure that batteries and doc-gen4 are pinned to commits that match the Lean version.
• lake-manifest.json, which will be automatically updated by running lake update after updating the previous two files.

Contributing

To contribute Lean code or proofs, follow these style guidelines.

Key definitions

Definitional engine (Cedar/Spec/)

• evaluate returns the result of evaluating an expression.
• satisfied checks if a policy is satisfied for a given request and entities.
• isAuthorized checks if a request is allowed or denied for a given policy store and entities.

Definitional validator (Cedar/Validation/)

• typeOf returns the result of type checking an expression against a schema.
• checkLevel checks that an expression does not exceed the specified maximum entity entity deference level

Definitional symbolic compiler (Cedar/SymCC/)

• SymCC.Compiler.compile returns the result of compiling an expression to an SMT term.
• SymCC.Authorizer.isAuthorized returns the result of compiling the authorization semantics of a set of policies to an SMT term.
• See Cedar/SymCC.lean for other key definitions and how they are used to formulate SMT queries.

Verified properties

Basic authorization theorems (Cedar/Thm/Authorization.lean)

• If some forbid policy is satisfied, then the request is denied.
• A request is allowed only if it is explicitly permitted (i.e., there is at least one permit policy that is satisfied).
• If not explicitly permitted, a request is denied.
• Authorization produces the same result regardless of policy evaluation order or duplicates.

Sound policy slicing (Cedar/Thm/Slicing.lean)

• Given a sound policy slice, the result of authorization is the same with the slice as it is with the full policy store.

Sound type checking (Cedar/Thm/Typechecking.lean)

• If an expression is well-typed according to the typechecker, then either evaluation returns a value of that type, or it returns an error of type entityDoesNotExist, extensionError, or arithBoundsError. All other errors are impossible.

Sound level-based entity slicing (Cedar/Thm/Validation/Levels.lean)

• If an expression is well-typed and does not exceed a maximum entity dereference level n, then, for any set of entities, the result of evaluating the expression with entities sliced at level n is the same as evaluating the expression with the original set of entities.

Sound and complete symbolic compilation (Cedar/Thm/SymbolicCompilation.lean)

• Compiling an expression results in an SMT term that both overapproximates (soundness) and underapproximates (completeness) the semantics of that expression.
• Symbolic compilation always succeeds on a well-typed Cedar expression and produces a well-formed and well-typed term.

Sound and complete verification (Cedar/Thm/Verification.lean)

• Verification checks (such as equivalence, implication, etc.) based on the symbolic compiler are sound (no false negatives) and complete (no false positives).