From df3074aebca89ab462992a16f1b301bd4e305d13 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 26 Dec 2023 17:24:03 +0000 Subject: [PATCH 1/6] wip --- cedar-drt/fuzz/src/lib.rs | 78 ++++++++++--------- .../Thm/Validation/Typechecker/HasAttr.lean | 13 +++- cedar-lean/Cedar/Validation/Typechecker.lean | 5 +- cedar-lean/DiffTest/Parser.lean | 11 ++- 4 files changed, 64 insertions(+), 43 deletions(-) diff --git a/cedar-drt/fuzz/src/lib.rs b/cedar-drt/fuzz/src/lib.rs index 9b16a9570..e0e960950 100644 --- a/cedar-drt/fuzz/src/lib.rs +++ b/cedar-drt/fuzz/src/lib.rs @@ -157,47 +157,49 @@ pub fn run_val_test( let definitional_res = custom_impl.validate(&schema, policies, mode); - match definitional_res { - Err(err) => { - // TODO(#175): For now, ignore cases where the Lean code returned an error due to - // an unknown extension function. - if !err.contains("jsonToExtFun: unknown extension function") { - panic!( - "Unexpected parse error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}", - &policies, schema - ); - } - } - Ok(definitional_res) => { - // TODO:(#126) Temporary fix to ignore a known mismatch between the spec and `cedar-policy`. - // The issue is that the `cedar-policy` will always return an error for an - // unrecognized entity or action, even if that part of the expression - // should be excluded from typechecking (e.g., `true || Undefined::"foo"` - // should be well typed due to short-circuiting). - if rust_res.validation_errors().any(|e| { - matches!( - e.error_kind(), - ValidationErrorKind::UnrecognizedEntityType(_) - | ValidationErrorKind::UnrecognizedActionId(_) - ) - }) { - return; + // If `cedar-policy` does not return an error, then the spec should not return an error. + // This implies type soundness of the `cedar-policy` validator since type soundness of the + // spec is formally proven. + // + // In particular, we have proven that if the spec validator does not return an error (B), + // then there are no authorization-time errors modulo some restrictions (C). So (B) ==> (C). + // DRT checks that if the `cedar-policy` validator does not return an error (A), then neither + // does the spec validator (B). So (A) ==> (B). By transitivity then, (A) ==> (C). + + if rust_res.validation_passed() { + match definitional_res { + Err(err) => { + // TODO(#175): For now, ignore cases where the Lean code returned an error due to + // an unknown extension function. + if !err.contains("jsonToExtFun: unknown extension function") { + panic!( + "Unexpected parse error\nPolicies:\n{}\nSchema:\n{:?}\nError: {err}", + &policies, schema + ); + } } + Ok(definitional_res) => { + // The definitional validator may return "impossiblePolicy" due to greater precision. + // If the definitional validator returns "impossiblePolicy" then the input expression is + // well-typed, although it is guaranteed to always evaluate to false. + if definitional_res.validation_errors.contains(&"impossiblePolicy".to_string()) { + return; + } - // The `validation_passed` decisions should match. - assert_eq!( - rust_res.validation_passed(), - definitional_res.validation_passed(), - "Mismatch for Policies:\n{}\nSchema:\n{:?}\ncedar-policy response: {:?}\nTest engine response: {:?}\n", - &policies, - schema, - rust_res, - definitional_res, - ); + // But the definitional validator should not return any other error. + assert!( + definitional_res.validation_passed(), + "Mismatch for Policies:\n{}\nSchema:\n{:?}\ncedar-policy response: {:?}\nTest engine response: {:?}\n", + &policies, + schema, + rust_res, + definitional_res, + ); - // TODO(#69): We currently don't check for a relationship between validation errors. - // E.g., the error reported by the definitional validator should be in the list - // of errors reported by the production validator, but we don't check this. + // TODO(#69): We currently don't check for a relationship between validation errors. + // E.g., the error reported by the definitional validator should be in the list + // of errors reported by the production validator, but we don't check this. + } } } } diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean index 3dab6235e..fb6b15585 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean @@ -46,10 +46,9 @@ theorem type_of_hasAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabili simp [h₁] } case mk.h_2 _ _ => - split at h₁ - split at h₁ <;> try split at h₁ + split at h₁ <;> split at h₁ <;> try split at h₁ all_goals { - simp [ok] at h₁ + try simp [ok] at h₁ try simp [h₁] } @@ -147,6 +146,14 @@ theorem type_of_hasAttr_is_sound_for_entities {x₁ : Expr} {a : Attr} {c₁ c case intro.h₁.true.h_2 => rcases (Map.not_contains_of_empty a) with _ contradiction + case intro.intro.h_2 => + simp [ok] at h₃ + split at h₃ <;> try simp [err, hasAttrInRecord] at h₃ + rcases h₃ with ⟨h₃, _⟩ + simp [←h₃] + apply InstanceOfType.instance_of_bool + simp [InstanceOfBoolType] + theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean index 0b7228558..7edec7fb7 100644 --- a/cedar-lean/Cedar/Validation/Typechecker.lean +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -192,7 +192,10 @@ def typeOfHasAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env | .entity ety => match env.ets.attrs? ety with | .some rty => hasAttrInRecord rty x a c false - | .none => err (.unknownEntity ety) + | .none => + match actionUID? x env.acts with + | .some _ => ok (.bool .anyBool) + | .none => err (.unknownEntity ety) | _ => err (.unexpectedType ty) def getAttrInRecord (ty : CedarType) (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) : ResultType := diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean index ddbf9abea..7c78bc6ff 100644 --- a/cedar-lean/DiffTest/Parser.lean +++ b/cedar-lean/DiffTest/Parser.lean @@ -450,6 +450,15 @@ def invertJsonSchemaActionStore (acts : JsonSchemaActionStore) : SchemaActionSto context := v.context })) acts) +-- Add special "unspecified" entity type with no attributes or ancestors +def addUnspecifiedEntityType (ets : EntityTypeStore) : EntityTypeStore := + let unspecifiedEntry : EntityTypeStoreEntry := + { + ancestors := Set.empty + attrs := Map.empty + } + Map.make (ets.toList ++ [({id := "", path := []}, unspecifiedEntry)]) + mutual partial def jsonToQualifiedCedarType (json : Lean.Json) : ParseResult (Qualified CedarType) := do @@ -525,7 +534,7 @@ partial def jsonToSchema (json : Lean.Json) : ParseResult Schema := do let actionsKVs ← getJsonField json "actionIds" >>= jsonArrayToKVList let actions ← mapMKeysAndValues actionsKVs jsonToEuid jsonToSchemaActionEntry .ok { - ets := invertJsonEntityTypeStore (Map.make entityTypes), + ets := addUnspecifiedEntityType (invertJsonEntityTypeStore (Map.make entityTypes)), acts := invertJsonSchemaActionStore (Map.make actions) } From c33ee192b0fa45491721b75cb1f74d76521479a8 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 6 Feb 2024 15:24:04 +0000 Subject: [PATCH 2/6] fix more merge issues --- cedar-lean/DiffTest/Parser.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean index aba14c16f..9d954b4b4 100644 --- a/cedar-lean/DiffTest/Parser.lean +++ b/cedar-lean/DiffTest/Parser.lean @@ -451,8 +451,8 @@ def invertJsonActionSchema (acts : JsonActionSchema) : ActionSchema := })) acts) -- Add special "unspecified" entity type with no attributes or ancestors -def addUnspecifiedEntityType (ets : EntityTypeStore) : EntityTypeStore := - let unspecifiedEntry : EntityTypeStoreEntry := +def addUnspecifiedEntityType (ets : EntitySchema) : EntitySchema := + let unspecifiedEntry : EntitySchemaEntry := { ancestors := Set.empty attrs := Map.empty From a6645931975dc47535bcb9a12ef9eb397d646740 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 6 Feb 2024 17:37:18 +0000 Subject: [PATCH 3/6] more fixes --- cedar-drt/fuzz/src/lib.rs | 7 ++++--- cedar-lean/Cedar/Validation/Typechecker.lean | 9 ++++++--- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/cedar-drt/fuzz/src/lib.rs b/cedar-drt/fuzz/src/lib.rs index f7ae2d851..0e66c735a 100644 --- a/cedar-drt/fuzz/src/lib.rs +++ b/cedar-drt/fuzz/src/lib.rs @@ -199,9 +199,10 @@ pub fn run_val_test( } } Ok(definitional_res) => { - // The definitional validator may return "impossiblePolicy" due to greater precision. - // If the definitional validator returns "impossiblePolicy" then the input expression is - // well-typed, although it is guaranteed to always evaluate to false. + // Even if the Rust validator succeeds, the definitional validator may + // return "impossiblePolicy" due to greater precision. In this case, the + // input policy is well-typed, although it is guaranteed to always evaluate + // to false. if definitional_res.validation_errors.contains(&"impossiblePolicy".to_string()) { return; } diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean index d3f0c5a78..0f8c1d3ca 100644 --- a/cedar-lean/Cedar/Validation/Typechecker.lean +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -185,6 +185,9 @@ def hasAttrInRecord (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) else ok (.bool .anyBool) (Capabilities.singleton x a) | .none => ok (.bool .ff) +def actionType? (ety : EntityType) (acts: ActionSchema) : Bool := + acts.keys.any (EntityUID.ty · == ety) + def typeOfHasAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env : Environment) : ResultType := match ty with | .record rty => hasAttrInRecord rty x a c true @@ -192,9 +195,9 @@ def typeOfHasAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env match env.ets.attrs? ety with | .some rty => hasAttrInRecord rty x a c false | .none => - match actionUID? x env.acts with - | .some _ => ok (.bool .anyBool) - | .none => err (.unknownEntity ety) + if actionType? ety env.acts + then ok (.bool .anyBool) + else err (.unknownEntity ety) | _ => err (.unexpectedType ty) def getAttrInRecord (ty : CedarType) (rty : RecordType) (x : Expr) (a : Attr) (c : Capabilities) : ResultType := From 32e886a5a7598a0c4824e97ce7864e40da6483e3 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 6 Feb 2024 20:52:17 +0000 Subject: [PATCH 4/6] another fix --- .../Cedar/Thm/Validation/Typechecker/HasAttr.lean | 12 ++++++++++-- cedar-lean/Cedar/Validation/Typechecker.lean | 2 +- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean index f8c16e165..d6f38c07f 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean @@ -149,10 +149,18 @@ theorem type_of_hasAttr_is_sound_for_entities {x₁ : Expr} {a : Attr} {c₁ c case h_2 => simp [ok] at h₃ split at h₃ <;> try simp [err, hasAttrInRecord] at h₃ - rcases h₃ with ⟨h₃, _⟩ + replace ⟨h₃, _⟩ := h₃ simp [←h₃] apply InstanceOfType.instance_of_bool - simp [InstanceOfBoolType] + unfold Entities.attrsOrEmpty + rename_i _ h₇ _ _ + simp [EntitySchema.attrs?] at h₇ + replace ⟨_, h₂, _⟩ := h₂ + cases h₈ : Map.find? entities uid <;> simp + simp [Map.not_contains_of_empty, InstanceOfBoolType] + replace ⟨_, h₈, _⟩ := h₂ uid _ h₈ + rw [h₇] at h₈ + contradiction theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : CedarType} {request : Request} {entities : Entities} diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean index 0f8c1d3ca..000daaee7 100644 --- a/cedar-lean/Cedar/Validation/Typechecker.lean +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -196,7 +196,7 @@ def typeOfHasAttr (ty : CedarType) (x : Expr) (a : Attr) (c : Capabilities) (env | .some rty => hasAttrInRecord rty x a c false | .none => if actionType? ety env.acts - then ok (.bool .anyBool) + then ok (.bool .ff) -- action attributes not allowed else err (.unknownEntity ety) | _ => err (.unexpectedType ty) From 8dc76199ef7e94ed6bb274f31c83e2526a0fd75d Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 6 Feb 2024 21:42:11 +0000 Subject: [PATCH 5/6] cargo fmt --- cedar-drt/fuzz/src/lib.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/cedar-drt/fuzz/src/lib.rs b/cedar-drt/fuzz/src/lib.rs index 0e66c735a..cc20ed93a 100644 --- a/cedar-drt/fuzz/src/lib.rs +++ b/cedar-drt/fuzz/src/lib.rs @@ -203,7 +203,10 @@ pub fn run_val_test( // return "impossiblePolicy" due to greater precision. In this case, the // input policy is well-typed, although it is guaranteed to always evaluate // to false. - if definitional_res.validation_errors.contains(&"impossiblePolicy".to_string()) { + if definitional_res + .validation_errors + .contains(&"impossiblePolicy".to_string()) + { return; } From 03fddd77ebdbb3a25c852810950891b0c32c1964 Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Wed, 7 Feb 2024 16:05:20 +0000 Subject: [PATCH 6/6] adress review comment --- cedar-drt/fuzz/src/lib.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/cedar-drt/fuzz/src/lib.rs b/cedar-drt/fuzz/src/lib.rs index cc20ed93a..044cde3e7 100644 --- a/cedar-drt/fuzz/src/lib.rs +++ b/cedar-drt/fuzz/src/lib.rs @@ -203,10 +203,7 @@ pub fn run_val_test( // return "impossiblePolicy" due to greater precision. In this case, the // input policy is well-typed, although it is guaranteed to always evaluate // to false. - if definitional_res - .validation_errors - .contains(&"impossiblePolicy".to_string()) - { + if definitional_res.validation_errors == vec!["impossiblePolicy".to_string()] { return; }