Frontend formalization: CST to AST

[victornicolet]

Adding parser to CST and verified CST to AST translation.

The original PR description from @ychtao :

The verification-guided development approach only covered the Cedar core -- after the AST has been generated, and has no Lean formalization or proofs about the front-end. This project aims to extend the verification coverage to the CST-to-AST translation phase.

CST Syntax

The CST syntax in Lean is defined the same way as it is in Rust. Since the Cedar grammar encodes precedence levels with different generators, the CST syntax definition is stratified, with one type definition corresponding to each of the precedence levels. Note that some error/annotation constructs (e.g. OverBang in NegOp, annotations) are not implemented in the Lean code. An enum definition with more than 2 constructs in Rust (e.g. Primary) corresponds to an inductive definition in Lean. A struct definition or an enum definition with 1 construct in Rust corresponds to a structure definition in Lean. Since the definition of the lowest level type Primary uses the definition of Expr, all the type definitions are mutually recursive, thus put into a mutual block. The syntax definition is in the file Cedar/Frontend/Cst/Syntax.lean.

All the definitions below the Expr level (Primary, Member, Unary, MultExpr, AddExpr, Relation, AndExpr, OrExpr, ExprData, ExprImpl and Expr) will be referred to as "CST expression types". Everything above that Policies, Policy and PolicyImpl) will be referred to as "CST policy types".

CST Semantics

The evaluation of CST expression types uses the same output type as the AST evaluator -- Result Value, which output a Value if successful, or an Error otherwise. The Error has to be extended to CstError, the errors that occur only during CST evaluation. An evaluate function is implemented for each of the CST expression types, all in a mutual block. One obstacle to this implementation is the termination proof. Not all evaluators have a decreasing input expression size that can serve as a terminating factor. A counterexample would be MultExpr, whose evaluator is basically a recursion on the extended field. The solution is to single out the recursive part of the function as MultExpr.foldOps, designate the length of extended as the termination factor, and has the MultExpr.evaluate function terminate by the size of the input expression.

The evaluation of CST policy types mirrors that of the AST -- first converted to a CST expression and then call the expression evaluation. The conversion is straight-forward, converting each of the scopes to an expression and conjunct them with the conditions. The CST authorizer of also similar to the AST's. It finds the "satisfied policies" w.r.t to the request, and judge based on the presence of forbid/permit satisfied policies. Erroring policies is also tracked.

The semantics is defined in Cedar/Frontend/Cst/Semantics.lean and Cedar/Frontend/Cst/Authorizer.lean.

CST Translation to AST

The translation is implemented in a way that's as close as possible to the Rust implementation. The translation of the CST expression types is divided into two steps -- first translating to an intermediate type ExprOrSpecial, then to an AST Expr. Since the role of certain construct like name, strLit are not clear only given the lower-level expression types, the information is kept in ExprOrSpecial and deferred to later stages of translation. Similar to the evaluator, there is a toExprOrSpecial? function for each layer of the CST expression types in a mutual block. The termination proof is also handled in a similar manner.

The translation of the CST policy types involves translation of the three variable scopes and the conditions. Principal and Resource scopes are handled similarly, while Action scopes need special treatment. Then the translator checks if the scopes are in order Principal, Action, Resource), translates the scopes and conditions, and assembles them into an AST policy. Note that the policy set translation is all-or-nothing -- one failed policy translation would cause the translation of the whole set to be aborted.

The translation is defined in Cedar/Frontend/Cst/ToAst.lean.

CST Translation Soundness

The soundness theorem says that if the translation of a CST policy set produces an AST policy set, then the semantics is preserved -- the authorization result is the same on any request. Since the evaluation and translation both involves two levels, the policy level and expression level, the soundness proof also consists of two steps:

1. Expression level translation soundness: the evaluation result of a CST expression is equal to the result of a translated AST expression. The expression translation proofs can be found in `Cedar/Thm/Translation/ExprTranslation.lean`.

2. Policy conversion: given a CST policy, if we translate it to an AST policy and then convert it to an AST expression, the result is equivalent to first converting it to a CST expression and then translating to an AST expression. The proofs can be found in `Cedar/Thm/Translation/PolicyToExpr.lean`.

Combining the two steps above gives us the soundness theorem translation_is_sound in Cedar/Thm/Frontend.lean.

CST Translation Completeness

The soundness theorem gives a guarantee that the translation preserves the semantics, but it does not specify which of the CSTs can be translated. Therefore we need a completeness. To state the completeness theorem, an "error collecting semantics" of Cedar CST. The error collector produces the same output value as the vanilla semantics, but also visits all branches of the program and collects errors potentially missed by short-circuit evaluation. The error collector is defined based on the semantics, in Cedar/Frontend/Cst/ErrorCollectingSemantics.lean.

The completeness theorem says that, if the error collector does not find any CstError, those specific to CST evaluation, then the CST can be translated successfully. It's done in a similar two-step approach. The intermediate theorems and proofs can be found in /Cedar/Thm/Frontend/Translation/Completeness.lean, and the final theorem is translation_is_strongly_complete in Cedar/Thm/Frontend.lean.

Properties Transfer: Authorization Safety

Three authorization properties have been proved regarding authorization safety -- forbid_trumps_permit, default_deny, and explicit_allow. These properties are originally proved for the AST in Cedar/Thm/Authorization.lean. In this project, these proofs are transferred to the CST, and can be found in Cedar/Thm/Frontend/Authorizer.lean.

Properties Transfer: Sound Slicing

Slicing is an optimization technique that selects the relevant policies (called a slice) to a request and only evaluate those policies. The "sound slicing" properties says that when authorizing against the slice yields the same decision as authorizing against the full policy set. To state this policy, a native scope analysis of the CST is defined in Cedar/Frontend/Cst/Slice.lean by extracting the scopes of the policy. The main theorem Cst.isAuthorized_eq_for_scope_based_policy_slice is stated and proved in Cedar/Thm/Frontend/PolicySlice.lean.

Properties Transfer: Validation Soundness

The CST validation soundness theorem says that for a CST policy, if the translated AST policy passes the validator, then the evaluation of the CST policy will not result in a type error. It is proved using the translation soundness and the existing validation soundness proofs of the AST. The theorem cst_validation_is_sound can be found in Cedar/Thm/Frontend/Validation.lean.