From 8e2a2aec8d7f28ab4d406e0816eb90a3eebba1a4 Mon Sep 17 00:00:00 2001 From: Bhakti <38060792+bhaktishh@users.noreply.github.com> Date: Mon, 12 Aug 2024 14:30:44 -0400 Subject: [PATCH] Entity and Request Validation (#399) Co-authored-by: Shah Co-authored-by: bhakti shah Co-authored-by: Bhakti Shah Co-authored-by: Bhakti Shah Co-authored-by: Kesha Hietala --- cedar-drt/README.md | 3 +- cedar-drt/fuzz/Cargo.toml | 12 ++ .../fuzz/fuzz_targets/entity-validation.rs | 83 ++++++++ .../fuzz/fuzz_targets/request-validation.rs | 123 ++++++++++++ cedar-drt/fuzz/fuzz_targets/validation-drt.rs | 5 +- cedar-drt/fuzz/src/lib.rs | 83 ++++++++ cedar-drt/set_env_vars.sh | 2 +- cedar-drt/src/definitional_request_types.rs | 12 ++ cedar-drt/src/lean_impl.rs | 54 ++++++ cedar-lean/Cedar/Validation.lean | 1 + .../Validation/RequestEntityValidator.lean | 179 ++++++++++++++++++ cedar-lean/Cli/Main.lean | 8 +- cedar-lean/DiffTest/Main.lean | 22 +++ 13 files changed, 583 insertions(+), 4 deletions(-) create mode 100644 cedar-drt/fuzz/fuzz_targets/entity-validation.rs create mode 100644 cedar-drt/fuzz/fuzz_targets/request-validation.rs mode change 100644 => 100755 cedar-drt/set_env_vars.sh create mode 100644 cedar-lean/Cedar/Validation/RequestEntityValidator.lean diff --git a/cedar-drt/README.md b/cedar-drt/README.md index b692f9a60..48e9a3339 100644 --- a/cedar-drt/README.md +++ b/cedar-drt/README.md @@ -16,6 +16,8 @@ The table below lists all available fuzz targets, including which component of t | [`rbac`](fuzz/fuzz_targets/rbac.rs) | Authorizer | DRT | Diff test authorizer on sets of RBAC policies, including template instantiations | | [`validation-drt-type-directed`](fuzz/fuzz_targets/validation-drt-type-directed.rs) | Validator | DRT | Diff test validation using (mostly) well-typed inputs | | [`validation-drt`](fuzz/fuzz_targets/validation-drt.rs) | Validator | DRT | Diff test validation | +| [`entity-validation`](fuzz/fuzz_targets/entity-validation.rs) | Entity Validator | DRT | Diff test entity validation | +| [`request-validation`](fuzz/fuzz_targets/request-validation.rs) | Request Validator | DRT | Diff test request validation | | | | | | | [`formatter`](fuzz/fuzz_targets/formatter.rs) | Policy formatter, Pretty printer, Parser | PBT | Test round trip property: parse ∘ format ∘ pretty-print == id for ASTs | | [`formatter-bytes`](fuzz/fuzz_targets/formatter-bytes.rs) | Policy formatter, Parser | PBT | The same as `formatter`, but we start with an arbitrary string instead of pretty-printing a policy AST | @@ -32,7 +34,6 @@ The table below lists all available fuzz targets, including which component of t | [`validation-pbt`](fuzz/fuzz_targets/validation-pbt.rs) | Validator | PBT | Test that validated policies do not result in type errors | | [`validation-pbt-type-directed`](fuzz/fuzz_targets/validation-pbt-type-directed.rs) | Validator | PBT | Test that validated policies do not result in type errors using (mostly) well-typed inputs | | [`wildcard-matching`](fuzz/fuzz_targets/wildcard-matching.rs) | String matching algorithm used for the `like` operator | PBT | Test algorithm against a regex-based implementation | - ## Logging If the fuzz targets are compiled with the `log` features, then they will log their entire corpus to the file pointed at in the `LOGFILE` environment variable. diff --git a/cedar-drt/fuzz/Cargo.toml b/cedar-drt/fuzz/Cargo.toml index 3ae1a1636..120ead007 100644 --- a/cedar-drt/fuzz/Cargo.toml +++ b/cedar-drt/fuzz/Cargo.toml @@ -180,3 +180,15 @@ name = "convert-policy-json-to-cedar" path = "fuzz_targets/convert-policy-json-to-cedar.rs" test = false doc = false + +[[bin]] +name = "entity-validation" +path = "fuzz_targets/entity-validation.rs" +test = false +doc = false + +[[bin]] +name = "request-validation" +path = "fuzz_targets/request-validation.rs" +test = false +doc = false diff --git a/cedar-drt/fuzz/fuzz_targets/entity-validation.rs b/cedar-drt/fuzz/fuzz_targets/entity-validation.rs new file mode 100644 index 000000000..95e9ec792 --- /dev/null +++ b/cedar-drt/fuzz/fuzz_targets/entity-validation.rs @@ -0,0 +1,83 @@ +/* + * Copyright Cedar Contributors + * + * 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. + */ + +#![no_main] +use cedar_drt::*; +use cedar_drt_inner::*; +use cedar_policy_core::extensions::Extensions; +use cedar_policy_generators::{ + hierarchy::Hierarchy, hierarchy::HierarchyGenerator, schema::Schema, settings::ABACSettings, +}; +use libfuzzer_sys::arbitrary::{self, Arbitrary, Unstructured}; +use log::{debug, info}; +use serde::Serialize; + +/// Input expected by this fuzz target +#[derive(Debug, Clone, Serialize)] +pub struct FuzzTargetInput { + /// generated schema + #[serde(skip)] + pub schema: Schema, + /// generated hierarchy + #[serde(skip)] + pub hierarchy: Hierarchy, +} + +/// settings for this fuzz target +const SETTINGS: ABACSettings = ABACSettings { + match_types: false, + enable_extensions: true, + max_depth: 7, + max_width: 7, + enable_additional_attributes: true, + enable_like: true, + enable_action_groups_and_attrs: true, + enable_arbitrary_func_call: true, + enable_unknowns: false, + enable_action_in_constraints: true, + enable_unspecified_apply_spec: true, +}; + +impl<'a> Arbitrary<'a> for FuzzTargetInput { + fn arbitrary(u: &mut Unstructured<'a>) -> arbitrary::Result { + let schema: Schema = Schema::arbitrary(SETTINGS.clone(), u)?; + let hierarchy = schema.arbitrary_hierarchy(u)?; + Ok(Self { schema, hierarchy }) + } + + fn size_hint(depth: usize) -> (usize, Option) { + arbitrary::size_hint::and_all(&[ + Schema::arbitrary_size_hint(depth), + HierarchyGenerator::size_hint(depth), + ]) + } +} + +fuzz_target!(|input: FuzzTargetInput| { + initialize_log(); + let def_impl = LeanDefinitionalEngine::new(); + + // generate a schema + if let Ok(schema) = ValidatorSchema::try_from(input.schema) { + debug!("Schema: {:?}", schema); + if let Ok(entities) = Entities::try_from(input.hierarchy) { + let (_, total_dur) = time_function(|| { + run_ent_val_test(&def_impl, schema, entities, Extensions::all_available()) + }); + info!("{}{}", TOTAL_MSG, total_dur.as_nanos()); + } + } +}); diff --git a/cedar-drt/fuzz/fuzz_targets/request-validation.rs b/cedar-drt/fuzz/fuzz_targets/request-validation.rs new file mode 100644 index 000000000..c5023d077 --- /dev/null +++ b/cedar-drt/fuzz/fuzz_targets/request-validation.rs @@ -0,0 +1,123 @@ +/* + * Copyright Cedar Contributors + * + * 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. + */ + +#![no_main] +use cedar_drt::*; +use cedar_drt_inner::*; +use cedar_policy_core::extensions::Extensions; +use cedar_policy_generators::{ + abac::ABACRequest, hierarchy::Hierarchy, hierarchy::HierarchyGenerator, schema::Schema, + settings::ABACSettings, +}; +use libfuzzer_sys::arbitrary::{self, Arbitrary, Unstructured}; +use log::{debug, info}; +use serde::Serialize; + +/// Input expected by this fuzz target +#[derive(Debug, Clone, Serialize)] +pub struct FuzzTargetInput { + /// generated schema + #[serde(skip)] + pub schema: Schema, + /// generated hierarchy + #[serde(skip)] + pub hierarchy: Hierarchy, + + /// the requests to try for this schema and hierarchy. We try 8 requests per + /// schema/hierarchy + #[serde(skip)] + pub requests: [ABACRequest; 8], +} + +/// settings for this fuzz target +const SETTINGS: ABACSettings = ABACSettings { + match_types: false, + enable_extensions: true, + max_depth: 7, + max_width: 7, + enable_additional_attributes: true, + enable_like: true, + enable_action_groups_and_attrs: true, + enable_arbitrary_func_call: true, + enable_unknowns: false, + enable_action_in_constraints: true, + enable_unspecified_apply_spec: true, +}; + +impl<'a> Arbitrary<'a> for FuzzTargetInput { + fn arbitrary(u: &mut Unstructured<'a>) -> arbitrary::Result { + let schema: Schema = Schema::arbitrary(SETTINGS.clone(), u)?; + let hierarchy = schema.arbitrary_hierarchy(u)?; + let requests = [ + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + schema.arbitrary_request(&hierarchy, u)?, + ]; + Ok(Self { + schema, + hierarchy, + requests, + }) + } + + fn size_hint(depth: usize) -> (usize, Option) { + arbitrary::size_hint::and_all(&[ + Schema::arbitrary_size_hint(depth), + HierarchyGenerator::size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + Schema::arbitrary_request_size_hint(depth), + ]) + } +} + +// Non-type-directed fuzzing of (strict) validation. +fuzz_target!(|input: FuzzTargetInput| { + initialize_log(); + let def_impl = LeanDefinitionalEngine::new(); + + // generate a schema + if let Ok(schema) = ValidatorSchema::try_from(input.schema) { + debug!("Schema: {:?}", schema); + let requests = input + .requests + .into_iter() + .map(Into::into) + .collect::>(); + for request in requests.iter().cloned() { + debug!("Request: {request}"); + let (_, total_dur) = time_function(|| { + run_req_val_test( + &def_impl, + schema.clone(), + request, + Extensions::all_available(), + ) + }); + info!("{}{}", TOTAL_MSG, total_dur.as_nanos()); + } + } +}); diff --git a/cedar-drt/fuzz/fuzz_targets/validation-drt.rs b/cedar-drt/fuzz/fuzz_targets/validation-drt.rs index 89f1f5a61..c24c90880 100644 --- a/cedar-drt/fuzz/fuzz_targets/validation-drt.rs +++ b/cedar-drt/fuzz/fuzz_targets/validation-drt.rs @@ -18,7 +18,9 @@ use cedar_drt::*; use cedar_drt_inner::*; use cedar_policy_core::ast; -use cedar_policy_generators::{abac::ABACPolicy, schema::Schema, settings::ABACSettings}; +use cedar_policy_generators::{ + abac::ABACPolicy, hierarchy::HierarchyGenerator, schema::Schema, settings::ABACSettings, +}; use libfuzzer_sys::arbitrary::{self, Arbitrary, Unstructured}; use log::{debug, info}; use serde::Serialize; @@ -59,6 +61,7 @@ impl<'a> Arbitrary<'a> for FuzzTargetInput { fn size_hint(depth: usize) -> (usize, Option) { arbitrary::size_hint::and_all(&[ Schema::arbitrary_size_hint(depth), + HierarchyGenerator::size_hint(depth), Schema::arbitrary_policy_size_hint(&SETTINGS, depth), ]) } diff --git a/cedar-drt/fuzz/src/lib.rs b/cedar-drt/fuzz/src/lib.rs index 4d28e477d..5179f1395 100644 --- a/cedar-drt/fuzz/src/lib.rs +++ b/cedar-drt/fuzz/src/lib.rs @@ -43,6 +43,8 @@ use std::collections::HashSet; /// Times for cedar-policy authorization and validation. pub const RUST_AUTH_MSG: &str = "rust_auth (ns) : "; pub const RUST_VALIDATION_MSG: &str = "rust_validation (ns) : "; +pub const RUST_ENT_VALIDATION_MSG: &str = "rust_entity_validation (ns) : "; +pub const RUST_REQ_VALIDATION_MSG: &str = "rust_request_validation (ns) : "; /// Compare the behavior of the partial evaluator in `cedar-policy` against a custom Cedar /// implementation. Panics if the two do not agree. `expr` is the expression to @@ -294,6 +296,87 @@ pub fn run_val_test( } } +pub fn run_req_val_test( + custom_impl: &impl CedarTestImplementation, + schema: ValidatorSchema, + request: ast::Request, + extensions: &Extensions<'_>, +) { + let (rust_res, rust_auth_dur) = time_function(|| { + ast::Request::new_with_unknowns( + request.principal().clone(), + request.action().clone(), + request.resource().clone(), + request.context().cloned(), + Some(&schema), + extensions, + ) + }); + info!("{}{}", RUST_REQ_VALIDATION_MSG, rust_auth_dur.as_nanos()); + + let definitional_res = custom_impl.validate_request(&schema, &request); + match definitional_res { + TestResult::Failure(_) => { + panic!("request validation test: failed to parse"); + } + TestResult::Success(definitional_res) => { + if rust_res.is_ok() { + assert!( + definitional_res.validation_passed(), + "Definitional Errors: {:?}\n, Rust output: {:?}", + definitional_res.errors, + rust_res.unwrap() + ); + } else { + assert!( + !definitional_res.validation_passed(), + "Errors: {:?}", + definitional_res.errors + ); + } + } + } +} + +pub fn run_ent_val_test( + custom_impl: &impl CedarTestImplementation, + schema: ValidatorSchema, + entities: Entities, + extensions: &Extensions<'_>, +) { + let (rust_res, rust_auth_dur) = time_function(|| { + Entities::from_entities( + entities.iter().cloned(), + Some(&cedar_policy_validator::CoreSchema::new(&schema)), + TCComputation::AssumeAlreadyComputed, + extensions, + ) + }); + info!("{}{}", RUST_ENT_VALIDATION_MSG, rust_auth_dur.as_nanos()); + let definitional_res = custom_impl.validate_entities(&schema, &entities); + match definitional_res { + TestResult::Failure(_) => { + panic!("entity validation test: failed to parse"); + } + TestResult::Success(definitional_res) => { + if rust_res.is_ok() { + assert!( + definitional_res.validation_passed(), + "Definitional Errors: {:?}\n, Rust output: {:?}", + definitional_res.errors, + rust_res.unwrap() + ); + } else { + assert!( + !definitional_res.validation_passed(), + "Errors: {:?}", + definitional_res.errors + ); + } + } + } +} + #[test] fn test_run_auth_test() { use cedar_drt::LeanDefinitionalEngine; diff --git a/cedar-drt/set_env_vars.sh b/cedar-drt/set_env_vars.sh old mode 100644 new mode 100755 index ad0452ff7..c4a5bd67a --- a/cedar-drt/set_env_vars.sh +++ b/cedar-drt/set_env_vars.sh @@ -26,4 +26,4 @@ else if awk "BEGIN {exit !($GLIBC_VERSION < 2.27)}"; then export LD_PRELOAD=${LD_PRELOAD+$LD_PRELOAD:}$(lean --print-prefix)/lib/glibc/libm.so fi -fi +fi \ No newline at end of file diff --git a/cedar-drt/src/definitional_request_types.rs b/cedar-drt/src/definitional_request_types.rs index 0bc2cd67f..f86f5a9da 100644 --- a/cedar-drt/src/definitional_request_types.rs +++ b/cedar-drt/src/definitional_request_types.rs @@ -56,3 +56,15 @@ pub struct ValidationRequest<'a> { pub policies: &'a ast::PolicySet, pub mode: ValidationMode, } + +#[derive(Debug, Serialize)] +pub struct RequestValidationRequest<'a> { + pub schema: &'a ValidatorSchema, + pub request: &'a ast::Request, +} + +#[derive(Debug, Serialize)] +pub struct EntityValidationRequest<'a> { + pub schema: &'a ValidatorSchema, + pub entities: &'a Entities, +} diff --git a/cedar-drt/src/lean_impl.rs b/cedar-drt/src/lean_impl.rs index 7d31a9e5c..d22931404 100644 --- a/cedar-drt/src/lean_impl.rs +++ b/cedar-drt/src/lean_impl.rs @@ -54,6 +54,8 @@ extern "C" { fn evaluateDRT(req: *mut lean_object) -> *mut lean_object; fn partialEvaluateDRT(req: *mut lean_object) -> *mut lean_object; fn partialAuthorizeDRT(req: *mut lean_object) -> *mut lean_object; + fn validateRequestDRT(req: *mut lean_object) -> *mut lean_object; + fn validateEntitiesDRT(req: *mut lean_object) -> *mut lean_object; fn initialize_DiffTest_Main(builtin: u8, ob: *mut lean_object) -> *mut lean_object; } @@ -373,6 +375,34 @@ impl LeanDefinitionalEngine { let response_string = lean_obj_p_to_rust_string(response); Self::deserialize_validation_response(response_string) } + + pub fn validate_request( + &self, + schema: &ValidatorSchema, + request: &ast::Request, + ) -> TestResult { + let request: String = serde_json::to_string(&RequestValidationRequest { schema, request }) + .expect("failed to serialize request"); + let cstring = CString::new(request).expect("CString::new failed"); + let req = unsafe { lean_mk_string(cstring.as_ptr() as *const u8) }; + let response = unsafe { validateRequestDRT(req) }; + let response_string = lean_obj_p_to_rust_string(response); + Self::deserialize_validation_response(response_string) + } + + pub fn validate_entities( + &self, + schema: &ValidatorSchema, + entities: &Entities, + ) -> TestResult { + let request: String = serde_json::to_string(&EntityValidationRequest { schema, entities }) + .expect("failed to serialize request"); + let cstring = CString::new(request).expect("CString::new failed"); + let req = unsafe { lean_mk_string(cstring.as_ptr() as *const u8) }; + let response = unsafe { validateEntitiesDRT(req) }; + let response_string = lean_obj_p_to_rust_string(response); + Self::deserialize_validation_response(response_string) + } } impl Drop for LeanDefinitionalEngine { @@ -455,6 +485,30 @@ impl CedarTestImplementation for LeanDefinitionalEngine { }) } + fn validate_entities( + &self, + schema: &ValidatorSchema, + entities: &Entities, + ) -> TestResult { + let result = self.validate_entities(schema, entities); + result.map(|res| { + let errors = res.errors.into_iter().collect(); + TestValidationResult { errors, ..res } + }) + } + + fn validate_request( + &self, + schema: &ValidatorSchema, + request: &ast::Request, + ) -> TestResult { + let result = self.validate_request(schema, request); + result.map(|res| { + let errors = res.errors.into_iter().collect(); + TestValidationResult { errors, ..res } + }) + } + fn error_comparison_mode(&self) -> ErrorComparisonMode { ErrorComparisonMode::PolicyIds } diff --git a/cedar-lean/Cedar/Validation.lean b/cedar-lean/Cedar/Validation.lean index 0e215c2b4..a869684ba 100644 --- a/cedar-lean/Cedar/Validation.lean +++ b/cedar-lean/Cedar/Validation.lean @@ -18,3 +18,4 @@ import Cedar.Validation.Types import Cedar.Validation.Subtyping import Cedar.Validation.Typechecker import Cedar.Validation.Validator +import Cedar.Validation.RequestEntityValidator diff --git a/cedar-lean/Cedar/Validation/RequestEntityValidator.lean b/cedar-lean/Cedar/Validation/RequestEntityValidator.lean new file mode 100644 index 000000000..76fd25320 --- /dev/null +++ b/cedar-lean/Cedar/Validation/RequestEntityValidator.lean @@ -0,0 +1,179 @@ +/- + Copyright Cedar Contributors + + 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. +-/ + +/- This file includes boolean definitions for the propositions declared in `Cedar/Thm/Validation/Typechecker/Types.lean`.-/ +import Cedar.Validation.Validator +import Cedar.Validation.Typechecker +namespace Cedar.Validation + +open Cedar.Spec +open Cedar.Data + +inductive RequestValidationError where +| typeError (msg : String) + +abbrev RequestValidationResult := Except RequestValidationError Unit + +inductive EntityValidationError where +| typeError (msg : String) + +abbrev EntityValidationResult := Except EntityValidationError Unit + +def instanceOfBoolType (b : Bool) (bty : BoolType) : Bool := + match b, bty with + | true, .tt => true + | false, .ff => true + | _, .anyBool => true + | _, _ => false + +def instanceOfEntityType (e : EntityUID) (ety : EntityType ) : Bool := ety == e.ty + +def instanceOfExtType (ext : Ext) (extty: ExtType) : Bool := +match ext, extty with + | .decimal _, .decimal => true + | .ipaddr _, .ipAddr => true + | _, _ => false + +def requiredAttributePresent (r : Map Attr Value) (rty : Map Attr (Qualified CedarType)) (k : Attr) := +match rty.find? k with + | .some qty => if qty.isRequired then r.contains k else true + | _ => true + +def instanceOfType (v : Value) (ty : CedarType) : Bool := + match v, ty with + | .prim (.bool b), .bool bty => instanceOfBoolType b bty + | .prim (.int _), .int => true + | .prim (.string _), .string => true + | .prim (.entityUID e), .entity ety => instanceOfEntityType e ety + | .set s, .set ty => s.elts.attach.all (λ ⟨v, _⟩ => instanceOfType v ty) + | .record r, .record rty => + r.keys.all rty.keys.contains && + (r.kvs.attach₂.all (λ ⟨(k, v), _⟩ => (match rty.find? k with + | .some qty => instanceOfType v qty.getType + | _ => true))) && + rty.keys.all (requiredAttributePresent r rty) + | .ext x, .ext xty => instanceOfExtType x xty + | _, _ => false + termination_by v + decreasing_by + all_goals simp_wf + case _ h₁ => + have := Set.sizeOf_lt_of_mem h₁ + omega + case _ h₁ => + cases r + simp only [Map.kvs] at h₁ + simp only [Map.mk.sizeOf_spec] + omega + +def instanceOfRequestType (request : Request) (reqty : RequestType) : Bool := + 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 instanceOfEntitySchema (entities : Entities) (ets : EntitySchema) : EntityValidationResult := + entities.toList.forM λ (uid, data) => instanceOfEntityData uid data +where + instanceOfEntityData uid data := + match ets.find? uid.ty with + | .some entry => if instanceOfType data.attrs (.record entry.attrs) then + if data.ancestors.all (λ ancestor => entry.ancestors.contains ancestor.ty) then .ok () + else .error (.typeError s!"entity ancestors inconsistent with type store information") + else .error (.typeError "entity attributes do not match type store") + | _ => .error (.typeError "entity type not defined in type store") + +/-- +For every action in the entity store, the action's ancestors are consistent +with the ancestor information in the action store. +-/ +def instanceOfActionSchema (entities : Entities) (as : ActionSchema) : EntityValidationResult := + as.toList.forM λ (uid, data) => instanceOfActionSchemaData uid data +where + instanceOfActionSchemaData uid data := + match entities.find? uid with + | .some entry => if data.ancestors == entry.ancestors + then .ok () + else .error (.typeError "action ancestors inconsistent with type store information") + | _ => .error (.typeError s!"action type {uid.eid} not defined in type store") + +def requestMatchesEnvironment (env : Environment) (request : Request) : Bool := instanceOfRequestType request env.reqty + +def validateRequest (schema : Schema) (request : Request) : RequestValidationResult := + if ((schema.toEnvironments.any (requestMatchesEnvironment · request))) + then .ok () + else .error (.typeError "request could not be validated in any environment") + +def entitiesMatchEnvironment (env : Environment) (entities : Entities) : EntityValidationResult := + instanceOfEntitySchema entities env.ets >>= λ _ => instanceOfActionSchema entities env.acts + +def actionSchemaEntryToEntityData (ase : ActionSchemaEntry) : EntityData := { + ancestors := ase.ancestors, + attrs := Map.empty +} + +/-- +Update the entity schema with the entities created for action schema entries. +This involves the construction of the ancestor information for the associated types +by inspecting the concrete hierarchy. +-/ +def updateSchema (schema : Schema) (actionSchemaEntities : Entities) : Schema := + let uniqueTys := Set.make (actionSchemaEntities.keys.map (·.ty)).elts + let newEntitySchemaEntries := uniqueTys.elts.map makeEntitySchemaEntries + { + ets := Map.make (schema.ets.kvs ++ newEntitySchemaEntries), + acts := schema.acts + } + where + makeEntitySchemaEntries ty := + let entriesWithType := actionSchemaEntities.filter (λ k _ => k.ty == ty) + let allAncestorsForType := List.join (entriesWithType.values.map (λ edt => + edt.ancestors.elts.map (·.ty) )) + let ese : EntitySchemaEntry := { + ancestors := Set.make allAncestorsForType, + attrs := Map.empty + } + (ty, ese) + +def validateEntities (schema : Schema) (entities : Entities) : EntityValidationResult := + let actionEntities := (schema.acts.mapOnValues actionSchemaEntryToEntityData) + let entities := Map.make (entities.kvs ++ actionEntities.kvs) + let schema := updateSchema schema actionEntities + schema.toEnvironments.forM (entitiesMatchEnvironment · entities) + +-- json + +def entityValidationErrorToJson : EntityValidationError → Lean.Json + | .typeError x => x + +instance : Lean.ToJson EntityValidationError where + toJson := entityValidationErrorToJson + +def requestValidationErrorToJson : RequestValidationError → Lean.Json + | .typeError x => x + +instance : Lean.ToJson RequestValidationError where + toJson := requestValidationErrorToJson + + +end Cedar.Validation diff --git a/cedar-lean/Cli/Main.lean b/cedar-lean/Cli/Main.lean index a6fce8adc..9b4384658 100644 --- a/cedar-lean/Cli/Main.lean +++ b/cedar-lean/Cli/Main.lean @@ -46,5 +46,11 @@ unsafe def main (args : List String) : IO Unit := | "evaluate" => let response := evaluate request IO.println s!"{repr response}" - | _ => printUsage s!"Invalid command `{command}` (expected `authorize`, `validate` or `evaluate`)" + | "validateRequest" => + let response := validateRequestDRT request + IO.println response + | "validateEntities" => + let response := validateEntitiesDRT request + IO.println response + | _ => printUsage s!"Invalid command `{command}` (expected `authorize`, `validate`, `validateRequest`, `validateEntities`, or `evaluate`)" | n => printUsage s!"Incorrect number of arguments (expected 2, but got {n})" diff --git a/cedar-lean/DiffTest/Main.lean b/cedar-lean/DiffTest/Main.lean index 893db805c..bd7ba6cce 100644 --- a/cedar-lean/DiffTest/Main.lean +++ b/cedar-lean/DiffTest/Main.lean @@ -115,6 +115,28 @@ def runAndTime (f : Unit -> α) : BaseIO (Timed α) := do .ok { data := test_passed , duration } toString (Lean.toJson result) +@[export validateEntitiesDRT] unsafe def validateEntitiesDRT (req : String) : String := + let result : ParseResult (Timed EntityValidationResult) := + match Lean.Json.parse req with + | .error e => .error s!"validateEntitiesDRT: failed to parse input: {e}" + | .ok json => do + let schema ← getJsonField json "schema" >>= jsonToSchema + let entities ← getJsonField json "entities" >>= jsonToEntities + let result := runAndTime (λ () => Cedar.Validation.validateEntities schema entities ) + .ok (unsafeBaseIO result) + toString (Lean.toJson result) + +@[export validateRequestDRT] unsafe def validateRequestDRT (req : String) : String := + let result : ParseResult (Timed RequestValidationResult) := + match Lean.Json.parse req with + | .error e => .error s!"validateRequestDRT: failed to parse input: {e}" + | .ok json => do + let schema ← getJsonField json "schema" >>= jsonToSchema + let request ← getJsonField json "request" >>= jsonToRequest + let result := runAndTime (λ () => Cedar.Validation.validateRequest schema request ) + .ok (unsafeBaseIO result) + toString (Lean.toJson result) + -- variant of `evaluateDRT` that returns the result of evaluation; used in the Cli def evaluate (req : String) : ParseResult (Result Value) := match Lean.Json.parse req with