Strongly well-formed ancestor relations #

The Cedar specification requires the entity hierarchy to be a DAG. This means that a legal ancestor relation on entities is the transitive closure of a DAG: it is (1) acyclic and (b) transitive.

This file formalizes the hierarchy requirements on the ancestor relation as extra constraints on well-formed Entities. A set of Entities is strongly well-formed if it satisfies the WellFormed predicate, as well as the Acyclic and Transitive predicate on its ancestor relation.

We apply the same notion of strong well-formedness to symbolic environments. Specifically, if an Entity type is enumerated (such as Cedar's action), then the concrete the ancestor relation over that type must be concrete, acyclic, and transitive. Moreover, an enumerated type can only have other enumerated types as ancestors, and a non-enumerated type can only have other non-enumerated types as ancestors. These constraints are enforced for actions, and we will continue to enforce them for other enums in the future.

If needed, we could allow enumerated types to have arbirary entities as parents, but at the cost of generating more assumptions and complicating the proofs. Specifically, to lift this restriction, we need to the following:

Change the definition of footprints to include all members of every enumerated type, which will cause transitivity and acyclicity constraints to be generated for these members along with the entities referenced in the analyzed policies.
Change the definition of SameEntities es εs so that es includes all enumerated values from εs. This is necessary to show soundness of assumption generation (see mem_footprint_reduce_exists_swf; similar lemma must hold for enumerated entities that would be included in the footprint). This will require adjusting the proof that the result of concretize? matches the input symbolic environment according to the new stricter definition of SameEntities. (It does, but this needs to be proven.)
Drop the hierarchy assumptions defined in this file. They become unnecessary since they are checked / enforced by the assumption generator.
Adjust the proofs of assumption generation soundness and completeness. These proofs should become more uniform in that they can treat UDFs and UUFs symmetrically.

We use strong well-formedness to prove the correctness of Cedar's assumption generation (Cedar.SymCC.Enforcer.enforce). Specifically, the assumptions are weak enough to be satisfied by all well-formed ancestor relations. And they are strong enough to be satisfied only by (finite) well-formed ancestor relations.

Finally, strongly well-formed environments also restrict the shape of the symbolic request. Specifically, the terms to which the request variables must be either variables or literals. They cannot be arbitrary terms because we need to be able to show that every "get attribute" term in the encoding corresponds to a "get attribute" expression in an input policy. This means that request terms cannot include spurious "get attribute" subterms. Note that we can relax this strong well-formedness constraint on the context term to allow combination of variables and literals, similar to the partial evaluator. This would complicate proofs so we won't do it until we find a use case for this functionality.

See Cedar/Thm/Verification.lean for an example of how these definitions are used to prove soundness and completeness of the Cedar.SymCC.Verifier.verifyEquivalent query, which checks that two Cedar policies are equivalent on all strongly well-formed environments env represented by a given symbolic environment εnv.