diff --git a/cedar-dafny/def/core.dfy b/cedar-dafny/def/core.dfy index 9cca52348..56ba0fc6b 100644 --- a/cedar-dafny/def/core.dfy +++ b/cedar-dafny/def/core.dfy @@ -155,7 +155,8 @@ module def.core { datatype UnaryOp = Not | Neg | MulBy(i: int) | - Like(p: Pattern) + Like(p: Pattern) | + Is(ety: EntityType) datatype BinaryOp = Eq | In | @@ -228,13 +229,22 @@ module def.core { } } - datatype Scope = Any | Eq(entity: EntityUID) | In(entity: EntityUID) + datatype Scope = + Any | + Eq(entity: EntityUID) | + In(entity: EntityUID) | + Is(ety: EntityType) | + IsIn(ety:EntityType, entity: EntityUID) { function toExpr(v: Var): Expr { match this { case Any => PrimitiveLit(Primitive.Bool(true)) case Eq(e) => BinaryApp(BinaryOp.Eq, Var(v), PrimitiveLit(Primitive.EntityUID(e))) case In(e) => BinaryApp(BinaryOp.In, Var(v), PrimitiveLit(Primitive.EntityUID(e))) + case Is(ety) => UnaryApp(UnaryOp.Is(ety), Var(v)) + case IsIn(ety, e) => + And(UnaryApp(UnaryOp.Is(ety), Var(v)), + BinaryApp(BinaryOp.In, Var(v), PrimitiveLit(Primitive.EntityUID(e)))) } } } diff --git a/cedar-dafny/def/engine.dfy b/cedar-dafny/def/engine.dfy index 5688ab158..4479eab88 100644 --- a/cedar-dafny/def/engine.dfy +++ b/cedar-dafny/def/engine.dfy @@ -206,6 +206,9 @@ module def.engine { case Like(p) => var s :- Value.asString(x); Ok(Value.Bool(wildcardMatch(s, p))) + case Is(ety) => + var e :- Value.asEntity(x); + Ok(Value.Bool(e.ty == ety)) } } diff --git a/cedar-dafny/def/templates.dfy b/cedar-dafny/def/templates.dfy index 97c6ec068..9a47d8cc0 100644 --- a/cedar-dafny/def/templates.dfy +++ b/cedar-dafny/def/templates.dfy @@ -126,11 +126,16 @@ module def.templates { } } - datatype ScopeTemplate = Any | Eq(entityOrSlot: EntityUIDOrSlot) | In(entityOrSlot: EntityUIDOrSlot) + datatype ScopeTemplate = + Any | + Eq(entityOrSlot: EntityUIDOrSlot) | + In(entityOrSlot: EntityUIDOrSlot) | + Is(ety: EntityType) | + IsIn(ety: EntityType, entityOrSlot: EntityUIDOrSlot) { function slotReqs(): SlotReqs { match this { - case Any => emptySlotReqs + case Any | Is(_) => emptySlotReqs case _ => entityOrSlot.slotReqs() } } @@ -191,6 +196,8 @@ module def.templates { case Any => Scope.Any case In(e) => Scope.In(linkEntityUIDOrSlot(e)) case Eq(e) => Scope.Eq(linkEntityUIDOrSlot(e)) + case Is(ety) => Scope.Is(ety) + case IsIn(ety,e) => Scope.IsIn(ety,linkEntityUIDOrSlot(e)) } } diff --git a/cedar-dafny/difftest/main.dfy b/cedar-dafny/difftest/main.dfy index 0ef5470fa..699b26ec6 100644 --- a/cedar-dafny/difftest/main.dfy +++ b/cedar-dafny/difftest/main.dfy @@ -193,6 +193,10 @@ module difftest.main { var expr :- deserializeField(body, "expr", exprFromProdJsonRec); var pat :- deserializeField(body, "pattern", patternFromProdJson); Ok(UnaryApp(Like(pat), expr)) + case "Is" => + var expr :- deserializeField(body, "expr", exprFromProdJsonRec); + var ety :- deserializeField(body, "entity_type", nameFromProdJson); + Ok(UnaryApp(UnaryOp.Is(EntityType(ety)), expr)) case "Set" => var exprs :- deserializeSeq(body, exprFromProdJsonRec); Ok(Expr.Set(exprs)) @@ -245,7 +249,13 @@ module difftest.main { map[ "Any" := _ => Ok(ScopeTemplate.Any), "In" := bodyDeserializer(entityUIDOrSlotFromProdJson, e => Ok(ScopeTemplate.In(e))), - "Eq" := bodyDeserializer(entityUIDOrSlotFromProdJson, e => Ok(ScopeTemplate.Eq(e))) + "Eq" := bodyDeserializer(entityUIDOrSlotFromProdJson, e => Ok(ScopeTemplate.Eq(e))), + "Is" := bodyDeserializer(nameFromProdJson, ety => Ok(ScopeTemplate.Is(EntityType(ety)))), + "IsIn" := tupleDeserializer2Elts( + nameFromProdJson, + entityUIDOrSlotFromProdJson, + (ety, e) => Ok(ScopeTemplate.IsIn(EntityType(ety),e)) + ) ]) } diff --git a/cedar-dafny/thm/pslicing.dfy b/cedar-dafny/thm/pslicing.dfy index 74de78397..7a6d71733 100644 --- a/cedar-dafny/thm/pslicing.dfy +++ b/cedar-dafny/thm/pslicing.dfy @@ -134,8 +134,8 @@ module pslicing { function headBasedTarget(p: Policy): Target { Target( - if p.principalScope.scope.Any? then None else Some(p.principalScope.scope.entity), - if p.resourceScope.scope.Any? then None else Some(p.resourceScope.scope.entity)) + if p.principalScope.scope.Any? || p.principalScope.scope.Is? then None else Some(p.principalScope.scope.entity), + if p.resourceScope.scope.Any? || p.resourceScope.scope.Is? then None else Some(p.resourceScope.scope.entity)) } function headBasedPolicySlice(request: Request, store: Store): PolicyStore { diff --git a/cedar-dafny/validation/thm/model.dfy b/cedar-dafny/validation/thm/model.dfy index bb4ff64a9..e06ab7d28 100644 --- a/cedar-dafny/validation/thm/model.dfy +++ b/cedar-dafny/validation/thm/model.dfy @@ -715,6 +715,35 @@ module validation.thm.model { ensures IsSafe(r,s,UnaryApp(Like(p),e),Type.Bool(AnyBool)) { reveal IsSafe(); + } + + lemma IsOpSafe(r: Request, s: EntityStore, e: Expr, ety: EntityType) + requires IsSafe(r,s,e,Type.Entity(AnyEntity)) + ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(AnyBool)) + { + reveal IsSafe(); + } + + lemma IsOpSafeTrue(r: Request, s: EntityStore, e: Expr, ety: EntityType, lub: EntityLUB) + requires IsSafe(r,s,e,Type.Entity(lub)) + requires lub.EntityLUB? + requires ety in lub.tys && |lub.tys| == 1 + ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(True)) + { + assert lub.tys == {ety} by { + def.util.EntityTypeLeqIsTotalOrder(); + var _ := def.util.SetToSortedSeq(lub.tys,def.util.EntityTypeLeq); + } + reveal IsSafe(); + } + + lemma IsOpSafeFalse(r: Request, s: EntityStore, e: Expr, ety: EntityType, lub: EntityLUB) + requires IsSafe(r,s,e,Type.Entity(lub)) + requires lub.EntityLUB? + requires ety !in lub.tys + ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(False)) + { + reveal IsSafe(); } lemma SetConstrSafe(r: Request, s: EntityStore, es: seq, t: Type) diff --git a/cedar-dafny/validation/thm/soundness.dfy b/cedar-dafny/validation/thm/soundness.dfy index 75f671e23..970943032 100644 --- a/cedar-dafny/validation/thm/soundness.dfy +++ b/cedar-dafny/validation/thm/soundness.dfy @@ -663,6 +663,57 @@ module validation.thm.soundness { } } + lemma SoundIs(e: Expr, ety: EntityType, t: Type, effs: Effects) + decreases UnaryApp(UnaryOp.Is(ety),e) , 0 + requires WellFormedRequestAndStore() + requires EffectsInvariant(effs) + requires Typesafe(UnaryApp(UnaryOp.Is(ety),e),effs,t) + ensures IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t) + ensures getEffects(UnaryApp(UnaryOp.Is(ety),e),effs) == Effects.empty() + { + var t' :| getType(UnaryApp(UnaryOp.Is(ety),e),effs) == t' && subty(t',t,ValidationMode.Permissive); + assert TC.inferIs(ety,e,effs) == types.Ok(t'); + + assert TC.ensureEntityType(e,effs).Ok?; + var t1 := getType(e,effs); + assert t1.Entity?; + + assert IsSafe(r,s,e,t1) by { Sound(e,t1,effs); } + match t1 { + case Entity(AnyEntity) => + assert t' == Type.Bool(AnyBool); + assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(AnyBool)) by { + IsOpSafe(r,s,e,ety); + } + case Entity(EntityLUB(tys)) => + if ety !in tys { + assert t' == Type.Bool(False); + assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t') by { + IsOpSafeFalse(r,s,e,ety,EntityLUB(tys)); + } + assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t) by { + SubtyCompat(t',t); + SemSubtyTransport(r,s,UnaryApp(UnaryOp.Is(ety),e),t',t); + } + } else if ety in tys && |tys| == 1 { + assert t' == Type.Bool(True); + assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t') by { + IsOpSafeTrue(r,s,e,ety,EntityLUB(tys)); + } + assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),t) by { + SubtyCompat(t',t); + SemSubtyTransport(r,s,UnaryApp(UnaryOp.Is(ety),e),t',t); + } + } else { + assert IsSafe(r,s,UnaryApp(UnaryOp.Is(ety),e),Type.Bool(AnyBool)) by { + assert subty(t1,Type.Entity(AnyEntity),ValidationMode.Permissive); + assert IsSafe(r,s,e,Type.Entity(AnyEntity)) by { Sound(e,Type.Entity(AnyEntity),effs); } + IsOpSafe(r,s,e,ety); + } + } + } + } + const unspecifiedEntityType := Type.Entity(EntityLUB({EntityType.UNSPECIFIED})) // Take advantage of the fact that in the current implementation, an @@ -1439,6 +1490,7 @@ module validation.thm.soundness { case UnaryApp(Neg,e') => SoundNeg(e',t,effs); case UnaryApp(MulBy(i),e') => SoundMulBy(i,e',t,effs); case UnaryApp(Like(p),e') => SoundLike(e',p,t,effs); + case UnaryApp(Is(ety),e') => SoundIs(e',ety,t,effs); case BinaryApp(Eq,e1,e2) => SoundEq(e1,e2,t,effs); case BinaryApp(Less,e1,e2) => SoundIneq(Less,e1,e2,t,effs); case BinaryApp(LessEq,e1,e2) => SoundIneq(BinaryOp.LessEq,e1,e2,t,effs); diff --git a/cedar-dafny/validation/thm/strict_inf_strict.dfy b/cedar-dafny/validation/thm/strict_inf_strict.dfy index c2722a7e1..3fa654dd9 100644 --- a/cedar-dafny/validation/thm/strict_inf_strict.dfy +++ b/cedar-dafny/validation/thm/strict_inf_strict.dfy @@ -152,6 +152,7 @@ module validation.thm.strict_inf_strict { case UnaryApp(Neg,e') => case UnaryApp(MulBy(i),e') => case UnaryApp(Like(p),e') => + case UnaryApp(Is(ety),e') => case BinaryApp(Eq,e1,e2) => case BinaryApp(Less,e1,e2) => case BinaryApp(LessEq,e1,e2) => diff --git a/cedar-dafny/validation/thm/strict_soundness.dfy b/cedar-dafny/validation/thm/strict_soundness.dfy index 6e45d3de7..43547e9b9 100644 --- a/cedar-dafny/validation/thm/strict_soundness.dfy +++ b/cedar-dafny/validation/thm/strict_soundness.dfy @@ -121,6 +121,17 @@ module validation.thm.strict_soundness { } } + lemma StrictIs(ety: EntityType, e: Expr, effs: Effects) + decreases UnaryApp(UnaryOp.Is(ety), e), 0 + requires S_TC.infer(UnaryApp(UnaryOp.Is(ety), e), effs).Ok? + ensures P_TC.infer(UnaryApp(UnaryOp.Is(ety), e), effs) == S_TC.infer(UnaryApp(UnaryOp.Is(ety), e), effs) + { + assert S_TC.ensureEntityType(e, effs).Ok?; + assert P_TC.ensureEntityType(e, effs) == S_TC.ensureEntityType(e, effs) by { + StrictTypecheckingIsStrict(e, effs); + } + } + lemma StrictArith2Ineq(o: BinaryOp, e1: Expr, e2: Expr, effs: Effects) decreases BinaryApp(o, e1, e2), 0 requires o.Add? || o.Sub? || o.Less? || o.LessEq? @@ -361,6 +372,7 @@ module validation.thm.strict_soundness { case UnaryApp(Neg,e') => StrictArith1(Neg, e', effs); case UnaryApp(MulBy(i),e') => StrictArith1(MulBy(i), e', effs); case UnaryApp(Like(p),e') => StrictLike(p, e', effs); + case UnaryApp(Is(ety),e') => StrictIs(ety, e', effs); case BinaryApp(Eq,e1,e2) => StrictEq(e1, e2, effs); case BinaryApp(Less,e1,e2) => StrictArith2Ineq(Less, e1, e2, effs); case BinaryApp(LessEq,e1,e2) => StrictArith2Ineq(LessEq, e1, e2, effs); diff --git a/cedar-dafny/validation/typechecker.dfy b/cedar-dafny/validation/typechecker.dfy index 827b6331d..d10ccc75b 100644 --- a/cedar-dafny/validation/typechecker.dfy +++ b/cedar-dafny/validation/typechecker.dfy @@ -557,6 +557,21 @@ module validation.typechecker { Ok(Type.Bool(AnyBool)) } + function inferIs(ety: EntityType, e: Expr, effs: Effects): Result + decreases UnaryApp(UnaryOp.Is(ety),e) , 0 + { + var elub :- ensureEntityType(e,effs); + match elub { + case AnyEntity => Ok(Type.Bool(AnyBool)) + case EntityLUB(tys) => + if ety !in tys + then Ok(Type.Bool(False)) + else if ety in tys && |tys| == 1 + then Ok(Type.Bool(True)) + else Ok(Type.Bool(AnyBool)) + } + } + function inferArith1(ghost op: UnaryOp, e: Expr, effs: Effects): Result requires op.Neg? || op.MulBy? decreases UnaryApp(op,e) , 0 @@ -667,6 +682,7 @@ module validation.typechecker { case UnaryApp(Neg,e1) => wrap(inferArith1(Neg,e1,effs)) case UnaryApp(MulBy(i),e1) => wrap(inferArith1(MulBy(i),e1,effs)) case UnaryApp(Like(p),e1) => wrap(inferLike(p,e1,effs)) + case UnaryApp(Is(ety),e1) => wrap(inferIs(ety,e1,effs)) case BinaryApp(Eq,e1,e2) => wrap(inferEq(e1,e2,effs)) case BinaryApp(Less,e1,e2) => wrap(inferIneq(Less,e1,e2,effs)) case BinaryApp(LessEq,e1,e2) => wrap(inferIneq(LessEq,e1,e2,effs)) diff --git a/cedar-policy-generators/src/policy.rs b/cedar-policy-generators/src/policy.rs index 0c7babc1d..c8c3c3a6a 100644 --- a/cedar-policy-generators/src/policy.rs +++ b/cedar-policy-generators/src/policy.rs @@ -292,7 +292,7 @@ impl PrincipalOrResourceConstraint { 1 => Ok(Self::IsTypeInSlot(hierarchy.arbitrary_entity_type(u)?)) ) } else { - // 32% Eq, 32% In (16% with and without Is), 32% Is (16% with and without In) + // 32% Eq, 16% In, 16% Is, 16% IsIn let uid = hierarchy.arbitrary_uid(u)?; gen!(u, 2 => Ok(Self::Eq(uid)), diff --git a/cedar-policy-generators/src/schema.rs b/cedar-policy-generators/src/schema.rs index cd2e6adc7..ea2317489 100644 --- a/cedar-policy-generators/src/schema.rs +++ b/cedar-policy-generators/src/schema.rs @@ -1037,15 +1037,22 @@ impl Schema { hierarchy: &Hierarchy, u: &mut Unstructured<'_>, ) -> Result { - // 20% of the time, NoConstraint; 40%, Eq; 40%, In - gen!(u, - 2 => Ok(PrincipalOrResourceConstraint::NoConstraint), - 4 => Ok(PrincipalOrResourceConstraint::Eq( - self.exprgenerator(Some(hierarchy)).arbitrary_principal_uid(u)?, - )), - 4 => Ok(PrincipalOrResourceConstraint::In( - self.exprgenerator(Some(hierarchy)).arbitrary_principal_uid(u)?, - ))) + // 20% of the time, NoConstraint + if u.ratio(1, 5)? { + Ok(PrincipalOrResourceConstraint::NoConstraint) + } else { + // 32% Eq, 16% In, 16% Is, 16% IsIn + let uid = self + .exprgenerator(Some(hierarchy)) + .arbitrary_principal_uid(u)?; + let ety = u.choose(self.entity_types())?.clone(); + gen!(u, + 2 => Ok(PrincipalOrResourceConstraint::Eq(uid)), + 1 => Ok(PrincipalOrResourceConstraint::In(uid)), + 1 => Ok(PrincipalOrResourceConstraint::IsType(ety)), + 1 => Ok(PrincipalOrResourceConstraint::IsTypeIn(ety, uid)) + ) + } } fn arbitrary_principal_constraint_size_hint(depth: usize) -> (usize, Option) { arbitrary::size_hint::and( @@ -1063,15 +1070,22 @@ impl Schema { hierarchy: &Hierarchy, u: &mut Unstructured<'_>, ) -> Result { - // 20% of the time, NoConstraint; 40%, Eq; 40%, In - gen!(u, - 2 => Ok(PrincipalOrResourceConstraint::NoConstraint), - 4 => Ok(PrincipalOrResourceConstraint::Eq( - self.exprgenerator(Some(hierarchy)).arbitrary_resource_uid(u)?, - )), - 4 => Ok(PrincipalOrResourceConstraint::In( - self.exprgenerator(Some(hierarchy)).arbitrary_resource_uid(u)?, - ))) + // 20% of the time, NoConstraint + if u.ratio(1, 5)? { + Ok(PrincipalOrResourceConstraint::NoConstraint) + } else { + // 32% Eq, 16% In, 16% Is, 16% IsIn + let uid = self + .exprgenerator(Some(hierarchy)) + .arbitrary_resource_uid(u)?; + let ety = u.choose(self.entity_types())?.clone(); + gen!(u, + 2 => Ok(PrincipalOrResourceConstraint::Eq(uid)), + 1 => Ok(PrincipalOrResourceConstraint::In(uid)), + 1 => Ok(PrincipalOrResourceConstraint::IsType(ety)), + 1 => Ok(PrincipalOrResourceConstraint::IsTypeIn(ety, uid)) + ) + } } fn arbitrary_resource_constraint_size_hint(depth: usize) -> (usize, Option) { arbitrary::size_hint::and(