Extend level based slicing soundness proof to rule out entity-does-exist errors

[john-h-kastner-aws]

Category

Lean formalization

Describe the feature you'd like to request

The current proof shows that entity slicing cannot change the result of evaluating an expression, but the current statement of the property suggests that a policy that errors due to dereferencing a non-existent before slicing would get the same error after slicing.

The entity slicing function will return None if the traversal of attributes tries to access an entity that doesn't exist. This should ensure that, if entity slicing succeeds, then policy evaluation cannot ever try to dereference an entity that doesn't exist. It should be easy to prove a slightly weaker property: if entity slicing succeeds, then policy evaluation will never error because of dereferencing an entity that doesn't exist. Notably this won't rule out a has or in expression accessing a non-existent entity because they will just evaluate to false. Proving that these never dereference an non-existent entity would be more annoying, likely requiring a new model of the evaluator that tracks this sort of non-fatal error condition.

Describe alternatives you've considered

.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change

[john-h-kastner-aws]

Merging #745 will mean that the property stated here doesn't hold anymore. If we want to prove something like it, we should define a separate predicate over entities to check that all entity references can be resolved up to depth level.