diff --git a/cedar-lean/Cedar/Spec/Value.lean b/cedar-lean/Cedar/Spec/Value.lean index 87bc5d3be..f08470763 100644 --- a/cedar-lean/Cedar/Spec/Value.lean +++ b/cedar-lean/Cedar/Spec/Value.lean @@ -323,4 +323,4 @@ instance : Ord Value where deriving instance Inhabited for Value -end Cedar.Spec \ No newline at end of file +end Cedar.Spec diff --git a/cedar-lean/Cedar/Thm.lean b/cedar-lean/Cedar/Thm.lean index e5cfe4bda..2bec3bb93 100644 --- a/cedar-lean/Cedar/Thm.lean +++ b/cedar-lean/Cedar/Thm.lean @@ -16,3 +16,4 @@ import Cedar.Thm.Basic import Cedar.Thm.Slicing +import Cedar.Thm.Soundness diff --git a/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean b/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean new file mode 100644 index 000000000..451755238 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Lemmas/Typechecker.lean @@ -0,0 +1,175 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec +import Cedar.Validation + +/-! +This file contains useful definitions and lemmas about the `Typechecker` functions. + +todo: fill in `sorry`s. Some invariants may need to be adjusted. The current +definitions are an informed guess based on the corresponding Dafny proof. +-/ + +namespace Cedar.Thm + +open Cedar.Data +open Cedar.Spec +open Cedar.Validation + +def InstanceOfBoolType : Bool → BoolType → Prop + | true, .tt => True + | false, .ff => True + | _, .anyBool => True + | _, _ => False + +def InstanceOfEntityType (e : EntityUID) (ety: EntityType) : Prop := + ety = e.ty + +def InstanceOfExtType : Ext → ExtType → Prop + | .decimal _, .decimal => True + | .ipaddr _, .ipAddr => True + | _, _ => False + +inductive InstanceOfType : Value → CedarType → Prop := + | instance_of_bool (b : Bool) (bty : BoolType) + (h₁ : InstanceOfBoolType b bty) : + InstanceOfType (.prim (.bool b)) (.bool bty) + | instance_of_int : + InstanceOfType (.prim (.int _)) .int + | instance_of_string : + InstanceOfType (.prim (.string _)) .string + | instance_of_entity (e : EntityUID) (ety: EntityType) + (h₁ : InstanceOfEntityType e ety) : + InstanceOfType (.prim (.entityUID e)) (.entity ety) + | instance_of_set (s : Set Value) (ty : CedarType) + (h₁ : forall v, v ∈ s → InstanceOfType v ty) : + InstanceOfType (.set s) (.set ty) + | instance_of_record (r : Map Attr Value) (rty : RecordType) + -- if an attribute is present, then it has the expected type + (h₁ : ∀ (k : Attr) (v : Value) (qty : QualifiedType), + rty.find? k = some qty → r.find? k = some v → InstanceOfType v qty.getType) + -- required attributes are present + (h₂ : ∀ (k : Attr) (qty : QualifiedType), rty.find? k = some qty → qty.isRequired → r.contains k) : + InstanceOfType (.record r) (.record rty) + | instance_of_ext (x : Ext) (xty : ExtType) + (h₁ : InstanceOfExtType x xty) : + InstanceOfType (.ext x) (.ext xty) + +def InstanceOfRequestType (request : Request) (reqty : RequestType) : Prop := + InstanceOfEntityType request.principal reqty.principal ∧ + request.action = reqty.action ∧ + InstanceOfEntityType request.resource reqty.resource ∧ + InstanceOfType request.context (.record reqty.context) + +/-- +For every entity in the store, +1. The entity's type is defined in the type store. +2. The entity's attributes match the attribute types indicated in the type store. +3. The entity's ancestors' types are consistent with the ancestor information + in the type store. +-/ +def InstanceOfEntityTypeStore (entities : Entities) (ets: EntityTypeStore) : Prop := + ∀ uid data, entities.find? uid = some data → + ∃ attrTys ancestorTys, ets.find? uid.ty = some (attrTys, ancestorTys) ∧ + InstanceOfType data.attrs (.record attrTys) ∧ + ∀ ancestor, ancestor ∈ data.ancestors → ancestor.ty ∈ ancestorTys + +/-- +For every action in the entity store, the action's ancestors are consistent +with the ancestor information in the action store. +-/ +def InstanceOfActionStore (entities : Entities) (as: ActionStore) : Prop := + ∀ uid data, entities.find? uid = some data → as.contains uid → + ∃ ancestors, as.find? uid = some ancestors → + ∀ ancestor, ancestor ∈ data.ancestors → ancestor ∈ ancestors + +def RequestAndEntitiesMatchEnvironment (env : Environment) (request : Request) (entities : Entities) : Prop := + InstanceOfRequestType request env.reqty ∧ + InstanceOfEntityTypeStore entities env.ets ∧ + InstanceOfActionStore entities env.acts + +/-- +The type soundness property says that if the typechecker assigns a type to an +expression, then it must be the case that the expression `EvaluatesTo` a value +of that type. The `EvaluatesTo` predicate covers the (obvious) case where evaluation +has no errors, but it also allows for errors of type `entityDoesNotExist` and +`extensionError`. + +The typechecker cannot protect against these errors because they depend on runtime +information (i.e., the entities passed into the authorization request, and +extension function applications on authorization-time data). All other errors +(`attrDoesNotExist` and `typeError`) can be prevented statically. + +_Note_: Currently, `extensionError`s can also be ruled out at validation time +because the only extension functions that can error are constructors, and all +constructors are required to be applied to string literals, meaning that they +can be fully evaluated during validation. This is not guaranteed to be the case +in the future. +-/ +def EvaluatesTo (e: Expr) (request : Request) (entities : Entities) (v : Value) : Prop := + evaluate e request entities = .error .entityDoesNotExist ∨ + evaluate e request entities = .error .extensionError ∨ + evaluate e request entities = .ok v + +/-- +On input to the typechecking function, for any (e,k) in the Capabilities, +e is a record- or entity-typed expression that has key k. +-/ +def CapabilitiesInvariant (c : Capabilities) (request : Request) (entities : Entities) : Prop := + ∀ (e : Expr) (k : Attr), (e, k) ∈ c → EvaluatesTo (.hasAttr e k) request entities true + +/-- +The Capabilities output by the typechecking function will satisfy +`CapabilitiesInvariant` provided that the input expression evaluates to true. +-/ +def GuardedCapabilitiesInvariant (e: Expr) (c: Capabilities) (request : Request) (entities : Entities) : Prop := + evaluate e request entities = .ok true → + CapabilitiesInvariant c request entities + +-- Easy property: the empty capability set satisifies the invariant +theorem empty_capabilities_invariant (request : Request) (entities : Entities) : + CapabilitiesInvariant ∅ request entities +:= by + intro e k h + contradiction + +theorem instance_of_type_bool_is_bool (v : Value) (ty : CedarType) : + InstanceOfType v ty → + ty ⊑ .bool .anyBool → + ∃ b, v = .prim (.bool b) +:= by + intro h₀ h₁ + cases v <;> cases ty <;> try cases h₀ <;> + try simp [subty, lub?] at h₁ + case instance_of_bool b bty => + exists b + +/-- +If an expression is well-typed according to the typechecker, and the input +environment and capabilities satisfy some invariants, then either (1) evaluation +produces a value of the returned type or (2) it returns an error of type +`entityDoesNotExist` or `extensionError`. Both options are encoded in the +`EvaluatesTo` predicate. +-/ +theorem type_of_is_sound (e : Expr) (c₁ c₂ : Capabilities) (env : Environment) (t : CedarType) (request : Request) (entities : Entities) : + CapabilitiesInvariant c₁ request entities → + RequestAndEntitiesMatchEnvironment env request entities → + typeOf e c₁ env = .ok (t, c₂) → + GuardedCapabilitiesInvariant e c₂ request entities ∧ + ∃ (v : Value), EvaluatesTo e request entities v ∧ InstanceOfType v t +:= by + sorry diff --git a/cedar-lean/Cedar/Thm/Soundness.lean b/cedar-lean/Cedar/Thm/Soundness.lean new file mode 100644 index 000000000..f9eb51cd7 --- /dev/null +++ b/cedar-lean/Cedar/Thm/Soundness.lean @@ -0,0 +1,103 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Spec +import Cedar.Thm.Lemmas.Typechecker +import Mathlib.Data.List.Basic + +/-! +This file defines the top-level soundness property for the valdator. + +todo: fill in `sorry`s. Some invariants may need to be adjusted. The current +definitions are an informed guess based on the corresponding Dafny proof. +--/ + +namespace Cedar.Thm + +open Cedar.Spec +open Cedar.Validation + +def EvaluatesToBool (policy : Policy) (request : Request) (entities : Entities) : Prop := + ∃ (b : Bool), EvaluatesTo policy.toExpr request entities b + +/-- +If a policy successfully validates, then evaluating that policy with any request +will either (1) return a Boolean value or (2) return an error of type `entityDoesNotExist` +or `extensionError`. Both options are encoded in the `EvaluatesToBool` predicate. +The validator cannot protect against `entityDoesNotExist` and `extensionError` +errors because it has no knowledge of the entities/context that will be provided +at authorization time. +-/ +theorem typecheck_policy_is_sound (policy : Policy) (env : Environment) (t : CedarType) (request : Request) (entities : Entities) : + RequestAndEntitiesMatchEnvironment env request entities → + typecheckPolicy policy env = .ok t → + EvaluatesToBool policy request entities +:= by + intro h₀ h₁ + unfold typecheckPolicy at h₁ + cases h₂ : (typeOf (Policy.toExpr policy) ∅ env) <;> + rw [h₂] at h₁ <;> + simp at h₁ + case ok res => + cases h₃ : (res.fst ⊑ CedarType.bool BoolType.anyBool) <;> + rw [h₃] at h₁ <;> + simp at h₁ + clear h₁ t + have h₁ : GuardedCapabilitiesInvariant policy.toExpr res.2 request entities ∧ ∃ (v : Value), EvaluatesTo policy.toExpr request entities v ∧ InstanceOfType v res.1 := by + apply type_of_is_sound (env:=env) (c₁:=∅) + apply empty_capabilities_invariant + apply h₀ + apply h₂ + cases h₁ with + | intro _ h₁ => + cases h₁ with + | intro v h₁ => + cases h₁ with + | intro h₁ h₄ => + have h₅ : ∃ b, v = .prim (.bool b) := by + apply instance_of_type_bool_is_bool + apply h₄ + apply h₃ + cases h₅ with + | intro b h₅ => + unfold EvaluatesToBool + exists b + rewrite [← h₅] + apply h₁ + +def RequestMatchesSchema (schema : Schema) (request : Request) : Prop := + match schema.acts.find? request.action with + | some entry => + request.principal.ty ∈ entry.appliesToPricipal ∧ + request.resource.ty ∈ entry.appliesToResource ∧ + InstanceOfType request.context (.record entry.context) + | _ => False + +def RequestAndEntitiesMatchSchema (schema : Schema) (request : Request) (entities : Entities) : Prop := + RequestMatchesSchema schema request ∧ + InstanceOfEntityTypeStore entities schema.ets ∧ + InstanceOfActionStore entities (schema.acts.mapOnValues (fun entry => entry.descendants)) + +/-- +Top-level soundness theorem: If validation succeeds, then for any request +consistent with the schema, every policy in the store will satisfy `EvaluatesToBool`. +-/ +theorem validate_is_sound (policies : Policies) (schema : Schema) (request : Request) (entities : Entities) : + RequestAndEntitiesMatchSchema schema request entities → + validate policies schema = .ok () → + ∀ policy, policy ∈ policies → EvaluatesToBool policy request entities +:= by + sorry diff --git a/cedar-lean/Cedar/Validation.lean b/cedar-lean/Cedar/Validation.lean index 2f8780fb5..82e60b672 100644 --- a/cedar-lean/Cedar/Validation.lean +++ b/cedar-lean/Cedar/Validation.lean @@ -16,4 +16,5 @@ import Cedar.Validation.Types import Cedar.Validation.Subtyping -import Cedar.Validation.Typechecker \ No newline at end of file +import Cedar.Validation.Typechecker +import Cedar.Validation.Validator diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean index b83d68ae0..bd7d6784a 100644 --- a/cedar-lean/Cedar/Validation/Typechecker.lean +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -284,4 +284,4 @@ def typeOf (x : Expr) (c : Capabilities) (env : Environment) : ResultType := let tys ← xs.mapM₁ (λ ⟨x₁, _⟩ => justType (typeOf x₁ c env)) typeOfCall xfn tys xs -end Cedar.Validation \ No newline at end of file +end Cedar.Validation diff --git a/cedar-lean/Cedar/Validation/Types.lean b/cedar-lean/Cedar/Validation/Types.lean index 3172923a1..01e4c98e5 100644 --- a/cedar-lean/Cedar/Validation/Types.lean +++ b/cedar-lean/Cedar/Validation/Types.lean @@ -40,6 +40,14 @@ inductive Qualified (α : Type u) where | optional (a : α) | required (a : α) +def Qualified.getType {α} : Qualified α → α + | optional a => a + | required a => a + +def Qualified.isRequired {α} : Qualified α → Bool + | optional _ => false + | required _ => true + inductive CedarType where | bool (bty : BoolType) | int @@ -174,4 +182,4 @@ deriving instance DecidableEq for TypeError deriving instance Inhabited for CedarType -end Cedar.Validation \ No newline at end of file +end Cedar.Validation diff --git a/cedar-lean/Cedar/Validation/Validator.lean b/cedar-lean/Cedar/Validation/Validator.lean new file mode 100644 index 000000000..b274b7915 --- /dev/null +++ b/cedar-lean/Cedar/Validation/Validator.lean @@ -0,0 +1,97 @@ +/- + Copyright 2022-2023 Amazon.com, Inc. or its affiliates. All Rights Reserved. + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar.Validation.Typechecker + +/-! This file defines the Cedar validator. -/ + +namespace Cedar.Validation + +open Cedar.Spec +open Cedar.Data + +----- Definitions ----- + +structure SchemaActionEntry where + appliesToPricipal : Set EntityType + appliesToResource : Set EntityType + descendants : Set EntityUID + context : RecordType + +abbrev SchemaActionStore := Map EntityUID SchemaActionEntry + +structure Schema where + ets : EntityTypeStore + acts : SchemaActionStore + +/-- +For a given action, compute the cross-product of the applicable principal and +resource types. +-/ +def SchemaActionEntry.toRequestTypes (action : EntityUID) (entry : SchemaActionEntry) : List RequestType := + entry.appliesToPricipal.toList.foldl (fun acc principal => + let reqtys : List RequestType := + entry.appliesToResource.toList.map (fun resource => + { + principal := principal, + action := action, + resource := resource, + context := entry.context + }) + reqtys ++ acc) ∅ + +/-- Return every schema-defined environment. -/ +def Schema.toEnvironments (schema : Schema) : List Environment := + let requestTypes : List RequestType := + schema.acts.toList.foldl (fun acc (action,entry) => entry.toRequestTypes action ++ acc) ∅ + requestTypes.map ({ + ets := schema.ets, + acts := schema.acts.mapOnValues (fun entry => entry.descendants), + reqty := · + }) + +inductive ValidationError where + | typeError (pid : PolicyID) (error : TypeError) + | impossiblePolicy (pid : PolicyID) + +abbrev ValidationResult := Except ValidationError Unit + +/-- Check that a policy is Boolean-typed. -/ +def typecheckPolicy (policy : Policy) (env : Environment) : Except ValidationError CedarType := + match typeOf policy.toExpr ∅ env with + | .ok (ty, _) => + if ty ⊑ .bool .anyBool + then .ok ty + else .error (.typeError policy.id (.unexpectedType ty)) + | .error e => .error (.typeError policy.id e) + +def allFalse (tys : List CedarType) : Bool := + tys.all (· == .bool .ff) + +/-- Check a policy under multiple environments. -/ +def typecheckPolicyWithEnvironments (policy : Policy) (envs : List Environment) : ValidationResult := do + let policyTypes ← envs.mapM (typecheckPolicy policy) + if allFalse policyTypes then .error (.impossiblePolicy policy.id) else .ok () + +/-- +Analyze a set of policies to checks that all are boolean-typed, and that +none are guaranteed to be false under all possible environments. +-/ +def validate (policies : Policies) (schema : Schema) : ValidationResult := + let envs := schema.toEnvironments + policies.forM (typecheckPolicyWithEnvironments · envs) + +end Cedar.Validation