diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index c3e33b3ae..6b5dd95af 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -44,7 +44,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" nameonly keySource: BeaconKeySource , nameonly standardBeacons: StandardBeaconList , nameonly compoundBeacons: Option , - nameonly virtualFields: Option + nameonly virtualFields: Option , + nameonly encryptedParts: Option , + nameonly signedParts: Option ) type BeaconVersionList = x: seq | IsValid_BeaconVersionList(x) witness * predicate method IsValid_BeaconVersionList(x: seq) { diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index 43a48f726..562bf0a2b 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -722,6 +722,11 @@ structure BeaconVersion { compoundBeacons : CompoundBeaconList, @javadoc("The Virtual Fields to be calculated, supporting other searchable enryption configurations.") virtualFields : VirtualFieldList, + + @javadoc("The list of Encrypted Parts that may be included in any compound beacon.") + encryptedParts : EncryptedPartsList, + @javadoc("The list of Signed Parts that may be included in any compound beacon.") + signedParts : SignedPartsList, } //= specification/searchable-encryption/search-config.md#initialization diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy index 5613bfd90..44cd0f975 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy @@ -194,7 +194,6 @@ module BaseBeacon { } function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes) : (ret : Result) - requires asSet ensures ret.Success? ==> ret.value.SS? ensures !value.SS? && !value.NS? && !value.BS? ==> ret.Failure? ensures ret.Success? ==> HasNoDuplicates(ret.value.SS) @@ -241,11 +240,20 @@ module BaseBeacon { //= type=implication //# * The resulting set MUST NOT contain duplicates. && (ret.value.Some? ==> HasNoDuplicates(ret.value.value.SS)) + //= specification/searchable-encryption/beacons.md#asset-initialization + //= type=implication + //# * Writing an item MUST fail if the item contains this beacon's attribute, + //# and that attribute is not of type Set. + && var value := TermLoc.TermToAttr(loc, item, None); + && (value.Some? && !(value.value.SS? || value.value.NS? || value.value.BS?) ==> ret.Failure?) { var value := TermLoc.TermToAttr(loc, item, None); if value.None? then Success(None) else + //= specification/searchable-encryption/beacons.md#asset-initialization + //# * The Standard Beacon MUST be stored in the item as a Set, + //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set. var setValue :- ValueToSet(value.value, key); Success(Some(setValue)) } @@ -346,18 +354,13 @@ module BaseBeacon { BeaconizeBinarySet(value[1..], key, converted + [h]) } - function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes) + function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes, forContains : bool) : (ret : Result) - //= specification/searchable-encryption/beacons.md#asset-initialization - //= type=implication - //# * Writing an item MUST fail if the item contains this beacon's attribute, - //# and that attribute is not of type Set. - ensures asSet && !value.SS? && !value.NS? && !value.BS? ==> ret.Failure? { - //= specification/searchable-encryption/beacons.md#asset-initialization - //# * The Standard Beacon MUST be stored in the item as a Set, - //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set. - if asSet then + // in query, allow beaconization of terminals + if asSet && !value.S? && !value.N? && !value.B? then + ValueToSet(value, key) + else if forContains && (value.SS? || value.NS? || value.BS?) then ValueToSet(value, key) else var bytes :- DynamoToStruct.TopLevelAttributeToBytes(value).MapFailure(e => E(e)); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 4e475b014..35d1a324c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -128,13 +128,13 @@ module SearchConfigToInfo { //# For a [Multi Key Store](#multi-key-store-initialization) the [Entry Capacity](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md#entry-capacity) //# MUST be key store's max cache size. var cacheType : MPT.CacheType := - if config.multi? then - if config.multi.cache.Some? then - config.multi.cache.value + if config.multi? then + if config.multi.cache.Some? then + config.multi.cache.value + else + MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000)) else - MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1000)) - else - MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1)); + MPT.Default(Default := MPT.DefaultCache(entryCapacity := 1)); //= specification/searchable-encryption/search-config.md#key-store-cache //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md) @@ -198,7 +198,24 @@ module SearchConfigToInfo { && output.value.keySource == source { var virtualFields :- ConvertVirtualFields(outer, config.virtualFields); - var beacons :- ConvertBeacons(outer, source.client, virtualFields, config.standardBeacons, config.compoundBeacons); + var std :- AddStandardBeacons(config.standardBeacons, outer, source.client, virtualFields); + + var signed := if config.signedParts.Some? then config.signedParts.value else []; + + var globalSignedParts :- GetSignedParts(signed, outer, "Global Parts List"); + + var globalEncryptedParts : PartSet := PartSet([], {}, {}); + if config.encryptedParts.Some? { + globalEncryptedParts :- GetEncryptedParts(config.encryptedParts.value, std, "Global Parts List"); + } + + var beacons : I.BeaconMap; + if config.compoundBeacons.Some? { + beacons :- AddCompoundBeacons(config.compoundBeacons.value, outer, source.client, virtualFields, std, globalSignedParts, globalEncryptedParts); + } else { + beacons := std; + } + var _ :- CheckBeacons(beacons); //= specification/searchable-encryption/search-config.md#beacon-version-initialization //# Initialization MUST fail if the [beacon key source](#beacon-key-source) is a [multi key store](#multi-key-store-initialization) @@ -389,17 +406,24 @@ module SearchConfigToInfo { function method IsValidTwin(converted : I.BeaconMap, name : string, length : B.BeaconLength, twin : string) : (ret : Result) ensures ret.Success? ==> - && twin in converted - && converted[twin].Standard? - && converted[twin].std.length == length + && twin in converted + && converted[twin].Standard? + && converted[twin].std.length == length { if twin in converted then - if converted[twin].Standard? then - if converted[twin].std.length == length then + var tb := converted[twin]; + if tb.Standard? then + if tb.std.twin.Some? then + if name == twin then + Failure(E("Beacon " + name + " is twinned to itself.")) + else + Failure(E("Beacon " + name + " is twinned to " + twin + " which is in turn twinned to " + tb.std.twin.value + + ". Twin chains are not allowed.")) + else if tb.std.length == length then Success(true) else Failure(E("Beacon " + name + " is twinned to " + twin + " but " + name + " has length " + Base10Int2String(length as int) - + " and " + twin + " has length " + Base10Int2String(converted[twin].std.length as int) + ".")) + + " and " + twin + " has length " + Base10Int2String(tb.std.length as int) + ".")) else Failure(E("Beacon " + name + " is twinned to " + twin + " but " + twin + " is a compound beacon.")) else @@ -471,7 +495,7 @@ module SearchConfigToInfo { } var newBeacon :- B.MakeStandardBeacon(client, beacons[0].name, beacons[0].length as B.BeaconLength, locString, - isPartOnly, isAsSet, twin); + isPartOnly, isAsSet, twin); //= specification/searchable-encryption/search-config.md#beacon-version-initialization //# Initialization MUST fail if the [terminal location](virtual.md#terminal-location) @@ -511,18 +535,63 @@ module SearchConfigToInfo { loc.value } + datatype PartSet = PartSet ( + parts : seq, + names : set, + prefixes : set + ) { + function method add(part : CB.BeaconPart, name : string) : Result + { + if part.getName() in names then + Failure(E("Duplicate part name " + part.getName() + " in " + name + ".")) + else if part.getPrefix() in prefixes then + Failure(E("Duplicate prefix " + part.getPrefix() + " in " + name + ".")) + else + Success(PartSet( + parts := parts + [part], + names := names + {part.getName()}, + prefixes := prefixes + {part.getPrefix()} + )) + } + + function method GetSetAsString(strings : set) : string + requires |strings| != 0 + { + var names := SortedSets.ComputeSetToOrderedSequence2(strings, CharLess); + Join(names, ", ") + } + + function method combine(other : PartSet, name : string, otherName : string) : Result + { + if |names * other.names| != 0 then + var tags := GetSetAsString(names * other.names); + Failure(E("Duplicate part name(s) " + tags + " between " + name + " and " + otherName + ".")) + else if |prefixes * other.prefixes| != 0 then + var tags := GetSetAsString(prefixes * other.prefixes); + Failure(E("Duplicate prefix(es) " + tags + " between " + name + " and " + otherName + ".")) + else + Success(PartSet( + parts := parts + other.parts, + names := names + other.names, + prefixes := prefixes + other.prefixes + )) + + } + } + // convert configured SignedPart to internal BeaconPart - function method {:tailrecursion} AddSignedParts( + function method {:tailrecursion} GetSignedParts( parts : seq, outer : DynamoDbTableEncryptionConfig, - origSize : nat := |parts|, - converted : seq := [] + name : string, + ghost origSize : nat := |parts|, + converted : PartSet := PartSet([], {}, {}) ) - : (ret : Result, Error>) - requires origSize == |parts| + |converted| - requires forall p <- converted :: p.Signed? - ensures ret.Success? ==> |ret.value| == origSize - ensures ret.Success? ==> forall p <- ret.value :: p.Signed? + : (ret : Result) + requires origSize == |parts| + |converted.parts| + requires forall p <- converted.parts :: p.Signed? + ensures ret.Success? ==> |ret.value.parts| == origSize + ensures ret.Success? ==> forall p <- ret.value.parts :: p.Signed? //= specification/searchable-encryption/search-config.md#beacon-version-initialization //= type=implication @@ -556,28 +625,28 @@ module SearchConfigToInfo { var newPart := CB.Signed(parts[0].prefix, parts[0].name, loc); :- Need(IsSignOnly(outer, newPart.loc), E("Signed Part " + newPart.name + " is built from " + GetLocStr(parts[0].name, parts[0].loc) + " which is not SIGN_ONLY.")); - AddSignedParts(parts[1..], outer,origSize, converted + [newPart]) + var newParts :- converted.add(newPart, name); + GetSignedParts(parts[1..], outer, name, origSize, newParts) } // convert configured EncryptedPart to internal BeaconPart - function method AddEncryptedParts( + function method GetEncryptedParts( parts : seq, - ghost origSize : nat, - ghost numSigned : nat, - converted : seq, std : I.BeaconMap, - name : string + name : string, + ghost origSize : nat := |parts|, + converted : PartSet := PartSet([], {}, {}) ) - : (ret : Result, Error>) - requires origSize == |parts| + |converted| - requires numSigned <= |converted| - requires CB.OrderedParts(converted, numSigned) - ensures ret.Success? ==> |ret.value| == origSize + : (ret : Result) + requires origSize == |parts| + |converted.parts| + requires forall x <- converted.parts :: x.Encrypted? + + ensures ret.Success? ==> |ret.value.parts| == origSize //= specification/searchable-encryption/beacons.md#compound-beacon //= type=implication //# The name MUST be the name of a configured standard beacon. ensures ret.Success? && 0 < |parts| ==> parts[0].name in std && std[parts[0].name].Standard? - ensures ret.Success? ==> CB.OrderedParts(ret.value, numSigned) + ensures ret.Success? ==> forall x <- ret.value.parts :: x.Encrypted? //= specification/searchable-encryption/beacons.md#asset-initialization //= type=implication @@ -588,12 +657,13 @@ module SearchConfigToInfo { Success(converted) else if parts[0].name in std && std[parts[0].name].Standard? && std[parts[0].name].std.asSet then - Failure(E("Compound beacon " + name + " uses " + parts[0].name + " which is an AsSet beacon, and therefore cannot be used in a Compound Beacon.")) + Failure(E(name + " uses " + parts[0].name + " which is an AsSet beacon, and therefore cannot be used in a Compound Beacon.")) else if parts[0].name in std && std[parts[0].name].Standard? then var newPart := CB.Encrypted(parts[0].prefix, std[parts[0].name].std); - AddEncryptedParts(parts[1..], origSize, numSigned, converted + [newPart], std, name) + var newParts :- converted.add(newPart, name); + GetEncryptedParts(parts[1..], std, name, origSize, newParts) else - Failure(E("Compound beacon " + name + " refers to standard beacon " + parts[0].name + " which is not configured.")) + Failure(E(name + " refers to standard beacon " + parts[0].name + " which is not configured.")) } // create the default constructor, if not constructor is specified @@ -753,43 +823,171 @@ module SearchConfigToInfo { AddConstructors2(constructors.value, name, parts, |constructors.value|) } + function method {:tailrecursion} GetGlobalPartsFrom(cons : seq, globalParts : PartSet, signed : bool, parts : PartSet) + : (ret : Result) + requires forall x <- parts.parts :: IsSignedPart(x, signed) + ensures ret.Success? ==> forall x <- ret.value.parts :: IsSignedPart(x, signed) + { + if |cons| == 0 then + Success(parts) + else + var newPart := FindGlobalPart(globalParts.parts, cons[0], signed); + if newPart.Some? then + var newParts :- parts.add(newPart.value, "Global Parts List"); + GetGlobalPartsFrom(cons[1..], globalParts, signed, newParts) + else + GetGlobalPartsFrom(cons[1..], globalParts, signed, parts) + } + + function method {:tailrecursion} GetGlobalParts(cons : seq, globalParts : PartSet, signed : bool, parts : PartSet := PartSet([], {}, {})) + : (ret : Result) + requires forall x <- parts.parts :: IsSignedPart(x, signed) + ensures ret.Success? ==> forall x <- ret.value.parts :: IsSignedPart(x, signed) + { + if |cons| == 0 then + Success(parts) + else + var newParts :- GetGlobalPartsFrom(cons[0].parts, globalParts, signed, parts); + GetGlobalParts(cons[1..], globalParts, signed, newParts) + } + + function method {:opaque} GetAllEncryptedParts( + parts : seq, + cons : seq, + globalEncryptedParts : PartSet, + name : string, + std : I.BeaconMap + ) + : (ret : Result, Error>) + ensures ret.Success? ==> forall x <- ret.value :: x.Encrypted? + { + var p1 :- GetEncryptedParts(parts, std, "Compound beacon " + name); + var p2 :- GetGlobalParts(cons, globalEncryptedParts, false); + var both :- p1.combine(p2, name, "Global Parts List"); + Success(both.parts) + } + + predicate method IsSignedPart(part : CB.BeaconPart, signed : bool) + { + if signed then + part.Signed? + else + part.Encrypted? + } + + function method {:tailrecursion} FindGlobalPart(globalParts : seq, cons : ConstructorPart, signed : bool) + : (ret : Option) + ensures ret.Some? && signed ==> ret.value.Signed? + ensures ret.Some? && !signed ==> ret.value.Encrypted? + { + if |globalParts| == 0 then + None + else if IsSignedPart(globalParts[0], signed) && globalParts[0].getName() == cons.name then + Some(globalParts[0]) + else + FindGlobalPart(globalParts[1..], cons, signed) + } + + function method {:opaque} GetAllSignedParts( + parts : seq, + cons : seq, + globalSignedParts : PartSet, + name : string, + outer : DynamoDbTableEncryptionConfig + ) + : (ret : Result, Error>) + ensures ret.Success? ==> forall x <- ret.value :: x.Signed? + { + var p1 :- GetSignedParts(parts, outer, name); + var p2 :- GetGlobalParts(cons, globalSignedParts, true); + var both :- p1.combine(p2, name, "Global Parts List"); + Success(both.parts) + } + + function method {:opaque} {:tailrecursion} CheckSignedParts(parts : seq, globals : PartSet, name : string) : Result + { + if |parts| == 0 then + Success(true) + else if parts[0].name in globals.names then + Failure(E("Compound beacon " + name + " defines signed part " + parts[0].name + " which is already defined as a global part.")) + else if parts[0].prefix in globals.prefixes then + Failure(E("Compound beacon " + name + " defines signed part " + parts[0].name + " with prefix " + parts[0].prefix + " which is already defined as the prefix of a global part.")) + else + CheckSignedParts(parts[1..], globals, name) + } + + function method {:opaque} {:tailrecursion} CheckEncryptedParts(parts : seq, globals : PartSet, name : string) : Result + { + if |parts| == 0 then + Success(true) + else if parts[0].name in globals.names then + Failure(E("Compound beacon " + name + " defines encrypted part " + parts[0].name + " which is already defined as a global part.")) + else if parts[0].prefix in globals.prefixes then + Failure(E("Compound beacon " + name + " defines encrypted part " + parts[0].name + " with prefix " + parts[0].prefix + " which is already defined as the prefix of a global part.")) + else + CheckEncryptedParts(parts[1..], globals, name) + } + // Construct a CompoundBeacon from its configuration - function method CreateCompoundBeacon( + function method {:opaque} CreateCompoundBeacon( beacon : CompoundBeacon, outer : DynamoDbTableEncryptionConfig, client: Primitives.AtomicPrimitivesClient, virtualFields : V.VirtualFieldMap, - converted : I.BeaconMap + converted : I.BeaconMap, + globalSignedParts : PartSet, + globalEncryptedParts : PartSet ) - : (ret : Result) + : (ret : Result) + + ensures beacon.name in converted ==> ret.Failure? + ensures beacon.name in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[beacon.name] != SE.ENCRYPT_AND_SIGN ==> ret.Failure? //= specification/searchable-encryption/beacons.md#signed-beacons //= type=implication //# The beacon value MUST be stored as `NAME`, rather than the usual `aws_dbe_b_NAME`. ensures ret.Success? ==> - && ret.value.base.name == beacon.name - && var encrypted := if beacon.encrypted.Some? then beacon.encrypted.value else []; - && (|encrypted| == 0 ==> ret.value.base.beaconName == beacon.name) - && (|encrypted| != 0 ==> ret.value.base.beaconName == BeaconPrefix + beacon.name) + && var encryptedParts := if beacon.encrypted.Some? then beacon.encrypted.value else []; + && var constructors := if beacon.constructors.Some? then beacon.constructors.value else []; + && var encrypted := GetAllEncryptedParts(encryptedParts, constructors, globalEncryptedParts, beacon.name, converted); + && encrypted.Success? + && ret.value.base.name == beacon.name + && (|encrypted.value| == 0 ==> ret.value.base.beaconName == beacon.name) + && (|encrypted.value| != 0 ==> ret.value.base.beaconName == BeaconPrefix + beacon.name) + //= specification/searchable-encryption/beacons.md#default-construction + //= type=implication + //# * Initialization MUST fail if no constructors are configured, and no local parts are configured. + ensures + && var encryptedParts := if beacon.encrypted.Some? then beacon.encrypted.value else []; + && var signedParts := if beacon.signed.Some? then beacon.signed.value else []; + && (!(beacon.constructors.Some? || |signedParts| != 0 || |encryptedParts| != 0) ==> ret.Failure?) { // because UnwrapOr doesn't verify when used on a list with a minimum size - var signed := if beacon.signed.Some? then beacon.signed.value else []; - var encrypted := if beacon.encrypted.Some? then beacon.encrypted.value else []; - var isSignedBeacon := |encrypted| == 0; + var signedParts := if beacon.signed.Some? then beacon.signed.value else []; + var encryptedParts := if beacon.encrypted.Some? then beacon.encrypted.value else []; + var constructors := if beacon.constructors.Some? then beacon.constructors.value else []; + var globalParts :- globalSignedParts.combine(globalEncryptedParts, "Global Signed Parts List", "Global Encrypted Parts List"); + var _ :- CheckSignedParts(signedParts, globalParts, beacon.name); + var _ :- CheckEncryptedParts(encryptedParts, globalParts, beacon.name); + var signed :- GetAllSignedParts( signedParts, constructors, globalSignedParts, beacon.name, outer); + var encrypted :- GetAllEncryptedParts(encryptedParts, constructors, globalEncryptedParts, beacon.name, converted); :- Need(beacon.name !in converted, E("Duplicate CompoundBeacon name : " + beacon.name)); - var _ :- BeaconNameAllowed(outer, virtualFields, beacon.name, "CompoundBeacon", isSignedBeacon); + :- Need(beacon.constructors.None? || 0 < |beacon.constructors.value|, E("For beacon " + beacon.name + " an empty constructor list was supplied.")); + :- Need(beacon.constructors.Some? || |signedParts| != 0 || |encryptedParts| != 0, + E("Compound beacon " + beacon.name + " defines no constructors, and also no local parts. Cannot make a default constructor from global parts.")); - var parts :- AddSignedParts(signed, outer); - var numNon := |parts|; - assert CB.OrderedParts(parts, numNon); + var numNon := |signed|; + assert CB.OrderedParts(signed, numNon); + var allParts := signed + encrypted; + assert CB.OrderedParts(allParts, numNon); - var parts :- AddEncryptedParts(encrypted, |parts| + |encrypted|, numNon, parts, converted, beacon.name); - assert CB.OrderedParts(parts, numNon); - :- Need(0 < |parts|, E("For beacon " + beacon.name + " no parts were supplied.")); - :- Need(beacon.constructors.None? || 0 < |beacon.constructors.value|, E("For beacon " + beacon.name + " an empty constructor list was supplied.")); - var constructors :- AddConstructors(beacon.constructors, beacon.name, parts, numNon); + var isSignedBeacon := |encrypted| == 0; + var _ :- BeaconNameAllowed(outer, virtualFields, beacon.name, "CompoundBeacon", isSignedBeacon); + + :- Need(0 < |allParts|, E("For beacon " + beacon.name + " no parts were supplied.")); + var constructors :- AddConstructors(beacon.constructors, beacon.name, allParts, numNon); var beaconName := if isSignedBeacon then beacon.name else BeaconPrefix + beacon.name; :- Need(DDB.IsValid_AttributeName(beaconName), E(beaconName + " is not a valid attribute name.")); @@ -801,7 +999,7 @@ module SearchConfigToInfo { beaconName := beaconName ), beacon.split[0], - parts, + allParts, numNon, constructors ) @@ -812,7 +1010,10 @@ module SearchConfigToInfo { outer : DynamoDbTableEncryptionConfig, client: Primitives.AtomicPrimitivesClient, virtualFields : V.VirtualFieldMap, - converted : I.BeaconMap := map[]) + converted : I.BeaconMap, + globalSignedParts : PartSet, + globalEncryptedParts : PartSet + ) returns (output : Result) modifies client.Modifies requires client.ValidState() @@ -840,8 +1041,8 @@ module SearchConfigToInfo { if |beacons| == 0 { return Success(converted); } - var newBeacon :- CreateCompoundBeacon(beacons[0], outer, client, virtualFields, converted); - output := AddCompoundBeacons(beacons[1..], outer, client, virtualFields, converted[beacons[0].name := I.Compound(newBeacon)]); + var newBeacon :- CreateCompoundBeacon(beacons[0], outer, client, virtualFields, converted, globalSignedParts, globalEncryptedParts); + output := AddCompoundBeacons(beacons[1..], outer, client, virtualFields, converted[beacons[0].name := I.Compound(newBeacon)], globalSignedParts, globalEncryptedParts); } // Is `name` referred to by some compound beacon in `data` @@ -870,17 +1071,17 @@ module SearchConfigToInfo { ensures |names| != 0 && I.IsPartOnly(data[names[0]]) && !ExistsInCompound(allNames, names[0], data) ==> ret.Failure? ensures ret.Success? && 0 < |names| && data[names[0]].Standard? && data[names[0]].std.twin.Some? ==> - && var twin := data[names[0]].std.twin.value; - && IsValidTwin(data, names[0], data[names[0]].std.length, twin).Success? - //= specification/searchable-encryption/beacons.md#twinned-initialization - //= type=implication - //# This name MUST be the name of a previously defined Standard Beacon. - && twin in data - && data[twin].Standard? - //= specification/searchable-encryption/beacons.md#twinned-initialization - //= type=implication - //# This beacon's [length](#beacon-length) MUST be equal to the `other` beacon's [length](#beacon-length). - && data[twin].std.length == data[names[0]].std.length + && var twin := data[names[0]].std.twin.value; + && IsValidTwin(data, names[0], data[names[0]].std.length, twin).Success? + //= specification/searchable-encryption/beacons.md#twinned-initialization + //= type=implication + //# This name MUST be the name of a previously defined Standard Beacon. + && twin in data + && data[twin].Standard? + //= specification/searchable-encryption/beacons.md#twinned-initialization + //= type=implication + //# This beacon's [length](#beacon-length) MUST be equal to the `other` beacon's [length](#beacon-length). + && data[twin].std.length == data[names[0]].std.length { if |names| == 0 then Success(true) @@ -900,27 +1101,4 @@ module SearchConfigToInfo { var beaconNames := SortedSets.ComputeSetToOrderedSequence2(data.Keys, CharLess); CheckAllBeacons(beaconNames, beaconNames, data) } - - // convert configured Beacons to internal BeaconMap - method ConvertBeacons( - outer : DynamoDbTableEncryptionConfig, - client: Primitives.AtomicPrimitivesClient, - virtualFields : V.VirtualFieldMap, - standard : StandardBeaconList, - compound : Option) - returns (output : Result) - modifies client.Modifies - requires client.ValidState() - ensures client.ValidState() - { - var std :- AddStandardBeacons(standard, outer, client, virtualFields); - if compound.Some? { - output := AddCompoundBeacons(compound.value, outer, client, virtualFields, std); - } else { - output := Success(std); - } - if output.Success? { - var _ :- CheckBeacons(output.value); - } - } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index a26051f3c..a84a119fa 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -202,7 +202,8 @@ module DynamoDBFilterExpr { datatype EqualityBeacon = EqualityBeacon ( beacon : Option, - forEquality : bool + forEquality : bool, + forContains : bool ) // returns Beacon, if any, and a flag indicating that the operation is exact match @@ -220,7 +221,7 @@ module DynamoDBFilterExpr { { var b :- GetBeacon2(bv, t, names); var _ :- CanBeacon(b, op, value.s, values); - Success(EqualityBeacon(Some(b), IsEquality(op))) + Success(EqualityBeacon(Some(b), IsEquality(op), op == Contains)) } function method GetBetweenBeacon( @@ -247,14 +248,14 @@ module DynamoDBFilterExpr { { var b :- GetBeacon2(bv, t, names); var _ :- CanBetween(b, op, leftValue.s, rightValue.s, values); - Success(EqualityBeacon(Some(b), false)) + Success(EqualityBeacon(Some(b), false, false)) } function method CanStandardBeacon(op : Token) : (ret : Result) ensures ret.Success? ==> ret.value { match op { - case Ne | Lt | Gt | Le | Ge | Between | BeginsWith | Contains => + case Ne | Lt | Gt | Le | Ge | Between | BeginsWith => Failure(E("The operation '" + TokenToString(op) + "' cannot be used with a standard beacon.")) case _ => Success(true) } @@ -398,6 +399,10 @@ module DynamoDBFilterExpr { else if 4 <= pos && (expr[pos-4].Contains? || expr[pos-4].BeginsWith?) && expr[pos-3].Open? && HasBeacon(b, expr[pos-2], names) && expr[pos-1].Comma? then GetBeacon(b, expr[pos-2], expr[pos-4], expr[pos], names, values) + // contains(value, ATTR .or. begins_with(value, ATTR + else if 2 <= pos < |expr|-2 && (expr[pos-2].Contains? || expr[pos-2].BeginsWith?) && expr[pos-1].Open? + && HasBeacon(b, expr[pos+2], names) && expr[pos+1].Comma? then + GetBeacon(b, expr[pos+2], expr[pos-2], expr[pos], names, values) // ATTR BETWEEN value AND * else if 2 <= pos < |expr|-2 && expr[pos-1].Between? && HasBeacon(b, expr[pos-2], names) && expr[pos+2].Value? then GetBetweenBeacon(b, expr[pos-2], expr[pos-1], expr[pos], expr[pos+2], names, values) @@ -408,13 +413,13 @@ module DynamoDBFilterExpr { else if expr[pos].Value? then var in_pos := GetInPos(expr, pos); if in_pos.None? then - Success(EqualityBeacon(None, true)) + Success(EqualityBeacon(None, true, false)) else if HasBeacon(b, expr[in_pos.value-1], names) then GetBeacon(b, expr[in_pos.value-1], expr[in_pos.value], expr[pos], names, values) else - Success(EqualityBeacon(None, true)) + Success(EqualityBeacon(None, true, false)) else - Success(EqualityBeacon(None, true)) + Success(EqualityBeacon(None, true, false)) } // expr[pos] is a value; return the Attr to which that value refers @@ -471,7 +476,7 @@ module DynamoDBFilterExpr { } // expr[pos] is an argument to a function, which is an Attr which is a beacon - // return an error if that function can operate neither on encrypted values nor on beacons + // return false if that function can operate neither on encrypted values nor on beacons predicate method IsAllowedOnBeaconPred(expr : seq, pos : nat) requires pos < |expr| requires expr[pos].Attr? @@ -553,7 +558,7 @@ module DynamoDBFilterExpr { :- Need(name in oldValues, E(name + " not found in ExpressionAttributeValueMap")); var oldValue := oldValues[name]; var eb :- BeaconForValue(b, expr, pos, names, oldValues); - var newValue :- if eb.beacon.None? then Success(oldValue) else eb.beacon.value.GetBeaconValue(oldValue, keys, eb.forEquality); + var newValue :- if eb.beacon.None? then Success(oldValue) else eb.beacon.value.GetBeaconValue(oldValue, keys, eb.forEquality, eb.forContains); //= specification/dynamodb-encryption-client/ddb-support.md#queryinputforbeacons //# If a single value in ExpressionAttributeValues is used in more than one context, //# for example an expression of `this = :foo OR that = :foo` where `this` and `that` @@ -1647,13 +1652,18 @@ module DynamoDBFilterExpr { ensures b.ValidState() modifies b.Modifies() { - if (context.keyExpr.None? && context.filterExpr.None?) || context.values.None? { + if (context.keyExpr.None? && context.filterExpr.None?) { return Success(context); } else { var keys := DontUseKeys; if !naked { keys :- b.getKeyMap(keyId); } + var values := + if context.values.Some? then + context.values.value + else + map[]; var newValues : DDB.ExpressionAttributeValueMap := map[]; var newKeyExpr := context.keyExpr; var newFilterExpr := context.filterExpr; @@ -1661,19 +1671,19 @@ module DynamoDBFilterExpr { if context.keyExpr.Some? { var parsed := ParseExpr(context.keyExpr.value); - var newContext :- BeaconizeParsedExpr(b, parsed, 0, context.values.value, newNames, keys, newValues); + var newContext :- BeaconizeParsedExpr(b, parsed, 0, values, newNames, keys, newValues); newKeyExpr := Some(ParsedExprToString(newContext.expr)); newValues := newContext.values; newNames := newContext.names; } if context.filterExpr.Some? { var parsed := ParseExpr(context.filterExpr.value); - var newContext :- BeaconizeParsedExpr(b, parsed, 0, context.values.value, newNames, keys, newValues); + var newContext :- BeaconizeParsedExpr(b, parsed, 0, values, newNames, keys, newValues); newFilterExpr := Some(ParsedExprToString(newContext.expr)); newValues := newContext.values; newNames := newContext.names; } - return Success(ExprContext(newKeyExpr, newFilterExpr, Some(newValues), newNames)); + return Success(ExprContext(newKeyExpr, newFilterExpr, if |newValues| == 0 then None else Some(newValues), newNames)); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index c3ad7d649..986846fc1 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy @@ -446,7 +446,7 @@ module SearchableEncryptionInfo { cmp.GetFields(virtualFields) } - function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool) + function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool, forContains : bool) : Result { if keys.DontUseKeys? then @@ -455,7 +455,7 @@ module SearchableEncryptionInfo { :- Need(!keys.ShouldHaveKeys?, E("Need KeyId because of beacon " + std.keyName() + " but no KeyId found in query")); var keys := keys.value; if std.keyName() in keys then - std.GetBeaconValue(value, keys[std.keyName()]) + std.GetBeaconValue(value, keys[std.keyName()], forContains) else Failure(E("Internal error. Beacon " + std.keyName() + " has no key.")) else diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index 4a3745329..dbaff8cf5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -43,7 +43,9 @@ module TestBaseBeacon { keySource := T.single(T.SingleKeyStore(keyId := "foo", cacheTTL := 42)), standardBeacons := [NameB, TitleB, TooBadB], compoundBeacons := Some([BadPrefix]), - virtualFields := None + virtualFields := None, + encryptedParts := None, + signedParts := None ); var src := GetLiteralSource([1,2,3,4,5], version); var res := C.ConvertVersionWithSource(FullTableConfig, version, src); @@ -262,12 +264,12 @@ module TestBaseBeacon { var Unknown := T.EncryptedPart(name := "Unknown", prefix := "U_"); var NameUnknown := T.CompoundBeacon ( - name := "NameUnknown", - split := ".", - encrypted := Some([Name,Unknown]), - signed := None, - constructors := None - ); + name := "NameUnknown", + split := ".", + encrypted := Some([Name,Unknown]), + signed := None, + constructors := None + ); var version := GetLotsaBeacons(); expect version.compoundBeacons.Some?; version := version.(compoundBeacons := Some(version.compoundBeacons.value + [NameUnknown])); @@ -318,6 +320,43 @@ module TestBaseBeacon { expect bv.error == E("Beacon twinBeacon is twinned to NameTitle but NameTitle is a compound beacon."); } + method {:test} ChainedTwin() + { + var version := GetLotsaBeacons(); + var twinBeacon := T.StandardBeacon(name := "twinBeacon", length := 24, loc := None, + style := Some( + T.twinned(T.Twinned(other := "std2")) + )); + var other := T.StandardBeacon(name := "std4", length := 24, loc := None, + style := Some( + T.twinned(T.Twinned(other := "twinBeacon")) + )); + + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); + version := version.(compoundBeacons := None, standardBeacons := [std2, twinBeacon, other]); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Beacon std4 is twinned to twinBeacon which is in turn twinned to std2. Twin chains are not allowed."); + } + + method {:test} SelfTwin() + { + var version := GetLotsaBeacons(); + var twinBeacon := T.StandardBeacon(name := "twinBeacon", length := 24, loc := None, + style := Some( + T.twinned(T.Twinned(other := "twinBeacon")) + )); + + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); + version := version.(compoundBeacons := None, standardBeacons := [std2, twinBeacon]); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(newConfig, version, src); + expect bv.Failure?; + print "\n", bv.error, "\n"; + expect bv.error == E("Beacon twinBeacon is twinned to itself."); + } + method {:test} TwinnedBadReferenceNonExistent() { var version := GetLotsaBeacons(); @@ -375,8 +414,8 @@ module TestBaseBeacon { expect version.compoundBeacons.Some?; var partBeacon := T.StandardBeacon(name := "partOnly", length := 23, loc := None, style := None); var newVersion := version.( - standardBeacons := version.standardBeacons + [partBeacon], - compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) + standardBeacons := version.standardBeacons + [partBeacon], + compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) ); var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); @@ -385,21 +424,21 @@ module TestBaseBeacon { var goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); expect goodAttrs == map[ - "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), - "aws_dbe_b_partOnly" := DDB.AttributeValue.S("405a51"), - "aws_dbe_b_compoundPart" := DDB.AttributeValue.S("S_405a51") - ]; + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.S("405a51"), + "aws_dbe_b_compoundPart" := DDB.AttributeValue.S("S_405a51") + ]; var goodQuery := Beaconize(bv, context, DontUseKeyId); expect goodQuery.Success?; partBeacon := T.StandardBeacon(name := "partOnly", length := 23, loc := None, - style := Some( - T.partOnly(T.PartOnly()) - )); + style := Some( + T.partOnly(T.PartOnly()) + )); newVersion := version.( - standardBeacons := version.standardBeacons + [partBeacon], - compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) + standardBeacons := version.standardBeacons + [partBeacon], + compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) ); bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); @@ -408,9 +447,9 @@ module TestBaseBeacon { //= type=test //# The Standard Beacon MUST NOT be stored in the item for a PartOnly beacon. expect goodAttrs == map[ - "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), - "aws_dbe_b_compoundPart" := DDB.AttributeValue.S("S_405a51") - ]; + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_compoundPart" := DDB.AttributeValue.S("S_405a51") + ]; //= specification/searchable-encryption/beacons.md#partonly-initialization //= type=test @@ -431,7 +470,7 @@ module TestBaseBeacon { expect version.compoundBeacons.Some?; var partBeacon := T.StandardBeacon(name := "partOnly", length := 24, loc := None, style := None); var newVersion := version.( - standardBeacons := version.standardBeacons + [partBeacon] + standardBeacons := version.standardBeacons + [partBeacon] ); var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); @@ -440,17 +479,17 @@ module TestBaseBeacon { var goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); expect goodAttrs == map[ - "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), - "aws_dbe_b_partOnly" := DDB.AttributeValue.S("928d9b") - ]; + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.S("928d9b") + ]; partBeacon := T.StandardBeacon(name := "partOnly", length := 24, loc := None, - style := Some( - T.twinned(T.Twinned(other := "std2")) - )); + style := Some( + T.twinned(T.Twinned(other := "std2")) + )); newVersion := version.( - standardBeacons := version.standardBeacons + [partBeacon] + standardBeacons := version.standardBeacons + [partBeacon] ); bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); @@ -459,9 +498,9 @@ module TestBaseBeacon { //= type=test //# This beacon MUST calculate its [value](#beacon-value) as if it were the `other` beacon. expect goodAttrs == map[ - "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), - "aws_dbe_b_partOnly" := DDB.AttributeValue.S("51e1da") - ]; + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.S("51e1da") + ]; // also check matching beacon value in query var context := ExprContext ( @@ -483,13 +522,13 @@ module TestBaseBeacon { None ); var setBeacon := T.StandardBeacon(name := "setAttr", length := 24, loc := None, - style := Some( - T.asSet(T.AsSet()) - )); + style := Some( + T.asSet(T.AsSet()) + )); var version := GetLotsaBeacons(); var newVersion := version.( - standardBeacons := version.standardBeacons + [setBeacon] + standardBeacons := version.standardBeacons + [setBeacon] ); var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["setAttr" := SE.ENCRYPT_AND_SIGN]); @@ -506,9 +545,17 @@ module TestBaseBeacon { Some(map[":setVal" := DDB.AttributeValue.S("abc")]), None ); + goodQuery :- expect Beaconize(bv, context, DontUseKeyId); + + context := ExprContext ( + None, + Some("setAttr = :setVal"), + Some(map[":setVal" := DDB.AttributeValue.L([])]), + None + ); var badQuery := Beaconize(bv, context, DontUseKeyId); expect badQuery.Failure?; - expect badQuery.error == E("Beacon setAttr has style AsSet, but attribute has type S."); + expect badQuery.error == E("Beacon setAttr has style AsSet, but attribute has type L."); } method {:test} TestSetNotSet() @@ -525,7 +572,7 @@ module TestBaseBeacon { T.asSet(T.AsSet()) )); var newVersion := version.( - standardBeacons := version.standardBeacons + [partBeacon] + standardBeacons := version.standardBeacons + [partBeacon] ); var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); @@ -543,9 +590,9 @@ module TestBaseBeacon { //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set. expect goodAttrs.Success?; expect goodAttrs.value == map[ - "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), - "aws_dbe_b_partOnly" := DDB.AttributeValue.SS(["928d9b", "405a51", "9c6c2e"]) - ]; + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.SS(["928d9b", "405a51", "9c6c2e"]) + ]; //= specification/searchable-encryption/beacons.md#asset-initialization //= type=test @@ -571,7 +618,7 @@ module TestBaseBeacon { T.twinnedSet(T.TwinnedSet(other := "std2")) )); var newVersion := version.( - standardBeacons := version.standardBeacons + [partBeacon] + standardBeacons := version.standardBeacons + [partBeacon] ); var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["partOnly" := SE.ENCRYPT_AND_SIGN]); @@ -589,9 +636,108 @@ module TestBaseBeacon { //# A TwinnedSet Beacon MUST behave both as [Twinned](#twinned-initialization) and [AsSet](#asset-initialization). expect goodAttrs.Success?; expect goodAttrs.value == map[ - "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), - "aws_dbe_b_partOnly" := DDB.AttributeValue.SS(["51e1da", "39ef85", "3ff06a"]) - ]; + "aws_dbe_b_std2" := DDB.AttributeValue.S("51e1da"), + "aws_dbe_b_partOnly" := DDB.AttributeValue.SS(["51e1da", "39ef85", "3ff06a"]) + ]; + } + + method {:test} GlobalPartNotExist() + { + var version := GetLotsaBeacons(); + var NotExist := T.EncryptedPart(name := "NotExist", prefix := "Q_"); + + version := version.(encryptedParts := Some([NotExist])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Global Parts List refers to standard beacon NotExist which is not configured."); + } + + method {:test} DuplicateGlobalSigned() + { + var version := GetLotsaBeacons(); + version := version.(compoundBeacons := None, signedParts := Some([Year, Month, Year])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Duplicate part name Year in Global Parts List."); + } + + method {:test} DuplicateGlobalEncrypted() + { + var version := GetLotsaBeacons(); + version := version.(compoundBeacons := None, encryptedParts := Some([Name, Title, Name])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Duplicate part name Name in Global Parts List."); + } + + method {:test} DuplicateGlobalPrefix() + { + var version := GetLotsaBeacons(); + var Std6 := T.EncryptedPart(name := "std6", prefix := "N_"); + version := version.(compoundBeacons := None, encryptedParts := Some([Name, Title, Std6])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Duplicate prefix N_ in Global Parts List."); + } + + method {:test} DuplicateGlobalVsLocalEncrypted() + { + var version := GetLotsaBeacons(); + version := version.(encryptedParts := Some([Name])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Compound beacon NameTitle defines encrypted part Name which is already defined as a global part."); } + method {:test} DuplicateGlobalVsLocalSigned() + { + var version := GetLotsaBeacons(); + version := version.(signedParts := Some([Month])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Compound beacon Mixed defines signed part Month which is already defined as a global part."); + } + + method {:test} CompoundNoConstructor() + { + var compoundDefault := T.CompoundBeacon ( + name := "compoundDefault", + split := ".", + encrypted := None, + signed := None, + constructors := None + ); + + var version := GetLotsaBeacons(); + version := version.(compoundBeacons := Some([compoundDefault]), signedParts := Some([Month]), encryptedParts := Some([Name, Title])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv := C.ConvertVersionWithSource(FullTableConfig, version, src); + expect bv.Failure?; + expect bv.error == E("Compound beacon compoundDefault defines no constructors, and also no local parts. Cannot make a default constructor from global parts."); + } + + method {:test} CompoundMixed() + { + var Mixed := T.CompoundBeacon ( + name := "Mixed", + split := ".", + encrypted := Some([Title]), + signed := Some([Month]), + constructors := Some([ + T.Constructor(parts := [T.ConstructorPart(name := "Name", required := true), T.ConstructorPart(name := "Year", required := true)]), + T.Constructor(parts := [T.ConstructorPart(name := "Title", required := true), T.ConstructorPart(name := "Month", required := false)]) + ]) + ); + + var version := GetLotsaBeacons(); + version := version.(compoundBeacons := Some([Mixed]), signedParts := Some([Year]), encryptedParts := Some([Name])); + var src := GetLiteralSource([1,2,3,4,5], version); + var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); + } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index d4dbad813..fb9bff6fe 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -153,7 +153,9 @@ module BeaconTestFixtures { keySource := single(SingleKeyStore(keyId := "foo", cacheTTL := 42)), standardBeacons := [std2], compoundBeacons := None, - virtualFields := None + virtualFields := None, + encryptedParts := None, + signedParts := None ); } @@ -169,7 +171,9 @@ module BeaconTestFixtures { keySource := single(SingleKeyStore(keyId := "foo", cacheTTL := 42)), standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), - virtualFields := Some([NameTitleField]) + virtualFields := Some([NameTitleField]), + encryptedParts := None, + signedParts := None ); } diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java index 3d12ad645..dffe86165 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToDafny.java @@ -117,7 +117,15 @@ public static BeaconVersion BeaconVersion( virtualFields = (Objects.nonNull(nativeValue.virtualFields()) && nativeValue.virtualFields().size() > 0) ? Option.create_Some(ToDafny.VirtualFieldList(nativeValue.virtualFields())) : Option.create_None(); - return new BeaconVersion(version, keyStore, keySource, standardBeacons, compoundBeacons, virtualFields); + Option> encryptedParts; + encryptedParts = (Objects.nonNull(nativeValue.encryptedParts()) && nativeValue.encryptedParts().size() > 0) ? + Option.create_Some(ToDafny.EncryptedPartsList(nativeValue.encryptedParts())) + : Option.create_None(); + Option> signedParts; + signedParts = (Objects.nonNull(nativeValue.signedParts()) && nativeValue.signedParts().size() > 0) ? + Option.create_Some(ToDafny.SignedPartsList(nativeValue.signedParts())) + : Option.create_None(); + return new BeaconVersion(version, keyStore, keySource, standardBeacons, compoundBeacons, virtualFields, encryptedParts, signedParts); } public static CompoundBeacon CompoundBeacon( diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java index 53710c30e..d0b29eb71 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/ToNative.java @@ -127,6 +127,12 @@ public static BeaconVersion BeaconVersion( if (dafnyValue.dtor_virtualFields().is_Some()) { nativeBuilder.virtualFields(ToNative.VirtualFieldList(dafnyValue.dtor_virtualFields().dtor_value())); } + if (dafnyValue.dtor_encryptedParts().is_Some()) { + nativeBuilder.encryptedParts(ToNative.EncryptedPartsList(dafnyValue.dtor_encryptedParts().dtor_value())); + } + if (dafnyValue.dtor_signedParts().is_Some()) { + nativeBuilder.signedParts(ToNative.SignedPartsList(dafnyValue.dtor_signedParts().dtor_value())); + } return nativeBuilder.build(); } diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java index 2140ed8b8..3bc307d61 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/BeaconVersion.java @@ -41,6 +41,16 @@ public class BeaconVersion { */ private final List virtualFields; + /** + * The list of Encrypted Parts that may be included in any compound beacon. + */ + private final List encryptedParts; + + /** + * The list of Signed Parts that may be included in any compound beacon. + */ + private final List signedParts; + protected BeaconVersion(BuilderImpl builder) { this.version = builder.version(); this.keyStore = builder.keyStore(); @@ -48,6 +58,8 @@ protected BeaconVersion(BuilderImpl builder) { this.standardBeacons = builder.standardBeacons(); this.compoundBeacons = builder.compoundBeacons(); this.virtualFields = builder.virtualFields(); + this.encryptedParts = builder.encryptedParts(); + this.signedParts = builder.signedParts(); } /** @@ -92,6 +104,20 @@ public List virtualFields() { return this.virtualFields; } + /** + * @return The list of Encrypted Parts that may be included in any compound beacon. + */ + public List encryptedParts() { + return this.encryptedParts; + } + + /** + * @return The list of Signed Parts that may be included in any compound beacon. + */ + public List signedParts() { + return this.signedParts; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -161,6 +187,26 @@ public interface Builder { */ List virtualFields(); + /** + * @param encryptedParts The list of Encrypted Parts that may be included in any compound beacon. + */ + Builder encryptedParts(List encryptedParts); + + /** + * @return The list of Encrypted Parts that may be included in any compound beacon. + */ + List encryptedParts(); + + /** + * @param signedParts The list of Signed Parts that may be included in any compound beacon. + */ + Builder signedParts(List signedParts); + + /** + * @return The list of Signed Parts that may be included in any compound beacon. + */ + List signedParts(); + BeaconVersion build(); } @@ -179,6 +225,10 @@ static class BuilderImpl implements Builder { protected List virtualFields; + protected List encryptedParts; + + protected List signedParts; + protected BuilderImpl() { } @@ -190,6 +240,8 @@ protected BuilderImpl(BeaconVersion model) { this.standardBeacons = model.standardBeacons(); this.compoundBeacons = model.compoundBeacons(); this.virtualFields = model.virtualFields(); + this.encryptedParts = model.encryptedParts(); + this.signedParts = model.signedParts(); } public Builder version(int version) { @@ -247,6 +299,24 @@ public List virtualFields() { return this.virtualFields; } + public Builder encryptedParts(List encryptedParts) { + this.encryptedParts = encryptedParts; + return this; + } + + public List encryptedParts() { + return this.encryptedParts; + } + + public Builder signedParts(List signedParts) { + this.signedParts = signedParts; + return this; + } + + public List signedParts() { + return this.signedParts; + } + public BeaconVersion build() { if (!this._versionSet) { throw new IllegalArgumentException("Missing value for required field `version`"); @@ -272,6 +342,12 @@ public BeaconVersion build() { if (Objects.nonNull(this.virtualFields()) && this.virtualFields().size() < 1) { throw new IllegalArgumentException("The size of `virtualFields` must be greater than or equal to 1"); } + if (Objects.nonNull(this.encryptedParts()) && this.encryptedParts().size() < 1) { + throw new IllegalArgumentException("The size of `encryptedParts` must be greater than or equal to 1"); + } + if (Objects.nonNull(this.signedParts()) && this.signedParts().size() < 1) { + throw new IllegalArgumentException("The size of `signedParts` must be greater than or equal to 1"); + } return new BeaconVersion(this); } } diff --git a/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java new file mode 100644 index 000000000..58a138d84 --- /dev/null +++ b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java @@ -0,0 +1,332 @@ +package software.amazon.cryptography.examples.searchableencryption; + +import java.util.ArrayList; +import java.util.List; +import java.util.HashMap; +import java.util.Map; + +import javax.swing.text.html.Option; + +import software.amazon.awssdk.core.client.config.ClientOverrideConfiguration; +import software.amazon.awssdk.services.dynamodb.DynamoDbClient; +import software.amazon.awssdk.services.dynamodb.model.AttributeValue; +import software.amazon.awssdk.services.dynamodb.model.PutItemRequest; +import software.amazon.awssdk.services.dynamodb.model.PutItemResponse; +import software.amazon.awssdk.services.dynamodb.model.ScanRequest; +import software.amazon.awssdk.services.dynamodb.model.ScanResponse; + +import software.amazon.awssdk.services.kms.KmsClient; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconKeySource; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconVersion; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.CompoundBeacon; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.BeaconStyle; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.TwinnedSet; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.Twinned; + +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.Constructor; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.ConstructorPart; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbTableEncryptionConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.DynamoDbTablesEncryptionConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.SearchConfig; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.EncryptedPart; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.SingleKeyStore; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.model.StandardBeacon; +import software.amazon.cryptography.keystore.KeyStore; +import software.amazon.cryptography.keystore.model.CreateKeyOutput; +import software.amazon.cryptography.keystore.model.KMSConfiguration; +import software.amazon.cryptography.keystore.model.KeyStoreConfig; +import software.amazon.cryptography.materialproviders.IKeyring; +import software.amazon.cryptography.materialproviders.MaterialProviders; +import software.amazon.cryptography.materialproviders.model.CreateAwsKmsHierarchicalKeyringInput; +import software.amazon.cryptography.materialproviders.model.MaterialProvidersConfig; +import software.amazon.cryptography.dbencryptionsdk.structuredencryption.model.CryptoAction; +import software.amazon.cryptography.dbencryptionsdk.dynamodb.DynamoDbEncryptionInterceptor; + +/* + This example demonstrates how to use Beacons Styles on Standard Beacons on encrypted attributes, + put an item with the beacon, and query against that beacon. + This example follows a use case of a database that stores food information. + This is an extension of the "BasicSearchableEncryptionExample" in this directory + and uses the same table schema. + + Running this example requires access to a DDB table with the + following key configuration: + - Partition key is named "work_id" with type (S) + - Sort key is named "inspection_time" with type (S) + + In this example for storing food information, this schema is utilized for the data: + - "work_id" stores a unique identifier for a unit inspection work order (v4 UUID) + - "inspection_date" stores an ISO 8601 date for the inspection (YYYY-MM-DD) + - "fruit" stores one type of fruit + - "basket" stores a set of types of fruit + - "dessert" stores one type of dessert + + The example requires the following ordered input command line parameters: + 1. DDB table name for table to put/query data from + 2. Branch key ID for a branch key that was previously created in your key store. See the + CreateKeyStoreKeyExample. + 3. Branch key wrapping KMS key ARN for the KMS key used to create the branch key with ID + provided in arg 2 + 4. Branch key DDB table ARN for the DDB table representing the branch key store + */ + +public class BeaconStylesSearchableEncryptionExample { + + public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String branchKeyId, String branchKeyWrappingKmsKeyArn, String branchKeyDdbTableName) { + + // 1. Create Beacons. + List standardBeaconList = new ArrayList<>(); + + // The fruit beacon allows searching on the encrypted fruit attribute + // We have selected 30 as an example beacon length, but you should go to + // https://docs.aws.amazon.com/database-encryption-sdk/latest/devguide/choosing-beacon-length.html + // when creating your beacons. + StandardBeacon fruitBeacon = StandardBeacon.builder() + .name("fruit") + .length(30) + .build(); + standardBeaconList.add(fruitBeacon); + + // The basket beacon allows searching on the encrypted basket attribute + // basket is used as a Set, and therefore needs a beacon style to reflect that. + // Further, we need to be able to compare the items in basket to the fruit attribute + // so we `twin` this beacon to `fruit`. + // Since we need both of these things, we use the TwinnedSet style. + StandardBeacon basketBeacon = StandardBeacon.builder() + .name("basket") + .length(30) + .style( + BeaconStyle.builder() + .twinnedSet(TwinnedSet.builder().other("fruit").build()) + .build() + ) + .build(); + standardBeaconList.add(basketBeacon); + + // The dessert beacon allows searching on the encrypted dessert attribute + // We need to be able to compare the dessert attribute to the fruit attribute + // so we `twin` this beacon to `fruit`. + StandardBeacon dessertBeacon = StandardBeacon.builder() + .name("dessert") + .length(30) + .style( + BeaconStyle.builder() + .twinned(Twinned.builder().other("fruit").build()) + .build() + ) + .build(); + standardBeaconList.add(dessertBeacon); + + // 2. Configure the Keystore + // These are the same constructions as in the Basic example, which describes these in more detail. + KeyStore keyStore = KeyStore.builder() + .KeyStoreConfig(KeyStoreConfig.builder() + .kmsClient(KmsClient.create()) + .ddbClient(DynamoDbClient.create()) + .ddbTableName(branchKeyDdbTableName) + .logicalKeyStoreName(branchKeyDdbTableName) + .kmsConfiguration(KMSConfiguration.builder().kmsKeyArn(branchKeyWrappingKmsKeyArn).build()) + .build()) + .build(); + + // 3. Create BeaconVersion. + // This is similar to the Basic example + List beaconVersions = new ArrayList<>(); + beaconVersions.add( + BeaconVersion.builder() + .standardBeacons(standardBeaconList) + .version(1) // MUST be 1 + .keyStore(keyStore) + .keySource(BeaconKeySource.builder() + .single(SingleKeyStore.builder() + .keyId(branchKeyId) + .cacheTTL(6000) + .build()) + .build()) + .build() + ); + + // 4. Create a Hierarchical Keyring + // This is the same configuration as in the Basic example. + final MaterialProviders matProv = MaterialProviders.builder() + .MaterialProvidersConfig(MaterialProvidersConfig.builder().build()) + .build(); + CreateAwsKmsHierarchicalKeyringInput keyringInput = CreateAwsKmsHierarchicalKeyringInput.builder() + .branchKeyId(branchKeyId) + .keyStore(keyStore) + .ttlSeconds(6000l) + .build(); + final IKeyring kmsKeyring = matProv.CreateAwsKmsHierarchicalKeyring(keyringInput); + + // 5. Configure which attributes are encrypted and/or signed when writing new items. + final Map attributeActionsOnEncrypt = new HashMap<>(); + attributeActionsOnEncrypt.put("work_id", CryptoAction.SIGN_ONLY); // Our partition attribute must be SIGN_ONLY + attributeActionsOnEncrypt.put("inspection_date", CryptoAction.SIGN_ONLY); // Our sort attribute must be SIGN_ONLY + attributeActionsOnEncrypt.put("dessert", CryptoAction.ENCRYPT_AND_SIGN); // Beaconized attributes must be encrypted + attributeActionsOnEncrypt.put("fruit", CryptoAction.ENCRYPT_AND_SIGN); // Beaconized attributes must be encrypted + attributeActionsOnEncrypt.put("basket", CryptoAction.ENCRYPT_AND_SIGN); // Beaconized attributes must be encrypted + + // 6. Create the DynamoDb Encryption configuration for the table we will be writing to. + // The beaconVersions are added to the search configuration. + final Map tableConfigs = new HashMap<>(); + final DynamoDbTableEncryptionConfig config = DynamoDbTableEncryptionConfig.builder() + .logicalTableName(ddbTableName) + .partitionKeyName("work_id") + .sortKeyName("inspection_date") + .attributeActionsOnEncrypt(attributeActionsOnEncrypt) + .keyring(kmsKeyring) + .search(SearchConfig.builder() + .writeVersion(1) // MUST be 1 + .versions(beaconVersions) + .build()) + .build(); + tableConfigs.put(ddbTableName, config); + + // 7. Create config + final DynamoDbTablesEncryptionConfig encryptionConfig = + DynamoDbTablesEncryptionConfig.builder() + .tableEncryptionConfigs(tableConfigs) + .build(); + + // 8. Create item one, specifically with "dessert != fruit", and "fruit in basket". + final HashMap item1 = new HashMap<>(); + item1.put("work_id", AttributeValue.builder().s("1").build()); + item1.put("inspection_date", AttributeValue.builder().s("2023-06-13").build()); + item1.put("dessert", AttributeValue.builder().s("cake").build()); + item1.put("fruit", AttributeValue.builder().s("banana").build()); + ArrayList basket = new ArrayList(); + basket.add("banana"); + basket.add("apple"); + basket.add("pear"); + item1.put("basket", AttributeValue.builder().ss(basket).build()); + + // 9. Create item two, specifically with "dessert == fruit", and "fruit not in basket". + final HashMap item2 = new HashMap<>(); + item2.put("work_id", AttributeValue.builder().s("2").build()); + item2.put("inspection_date", AttributeValue.builder().s("2023-06-13").build()); + item2.put("fruit", AttributeValue.builder().s("orange").build()); + item2.put("dessert", AttributeValue.builder().s("orange").build()); + basket = new ArrayList(); + basket.add("strawberry"); + basket.add("blueberry"); + basket.add("blackberry"); + item2.put("basket", AttributeValue.builder().ss(basket).build()); + + // 10. Create the DynamoDb Encryption Interceptor + DynamoDbEncryptionInterceptor encryptionInterceptor = DynamoDbEncryptionInterceptor.builder() + .config(encryptionConfig) + .build(); + + // 11. Create a new AWS SDK DynamoDb client using the DynamoDb Encryption Interceptor above + final DynamoDbClient ddb = DynamoDbClient.builder() + .overrideConfiguration( + ClientOverrideConfiguration.builder() + .addExecutionInterceptor(encryptionInterceptor) + .build()) + .build(); + + // 12. Add the two items + PutItemRequest putRequest = PutItemRequest.builder() + .tableName(ddbTableName) + .item(item1) + .build(); + + PutItemResponse putResponse = ddb.putItem(putRequest); + // Validate object put successfully + assert 200 == putResponse.sdkHttpResponse().statusCode(); + + putRequest = PutItemRequest.builder() + .tableName(ddbTableName) + .item(item2) + .build(); + + putResponse = ddb.putItem(putRequest); + // Validate object put successfully + assert 200 == putResponse.sdkHttpResponse().statusCode(); + + + // 13. Test the first type of Set operation : + // Select records where the basket attribute holds a particular value + Map expressionAttributeValues = new HashMap<>(); + expressionAttributeValues.put(":value", AttributeValue.builder().s("banana").build()); + + ScanRequest scanRequest = ScanRequest.builder() + .tableName(ddbTableName) + .filterExpression("contains(basket, :value)") + .expressionAttributeValues(expressionAttributeValues) + .build(); + + ScanResponse scanResponse = ddb.scan(scanRequest); + // Validate query was returned successfully + assert 200 == scanResponse.sdkHttpResponse().statusCode(); + + // Validate only 1 item was returned: item1 + assert scanResponse.items().size() == 1; + assert scanResponse.items().get(0).equals(item1); + + // 14. Test the second type of Set operation : + // Select records where the basket attribute holds the fruit attribute + scanRequest = ScanRequest.builder() + .tableName(ddbTableName) + .filterExpression("contains(basket, fruit)") + .build(); + + scanResponse = ddb.scan(scanRequest); + // Validate query was returned successfully + assert 200 == scanResponse.sdkHttpResponse().statusCode(); + + // Validate only 1 item was returned: item1 + assert scanResponse.items().size() == 1; + assert scanResponse.items().get(0).equals(item1); + + // 15. Test the third type of Set operation : + // Select records where the fruit attribute exists in a particular set + ArrayList basket3 = new ArrayList(); + basket3.add("boysenberry"); + basket3.add("orange"); + basket3.add("grape"); + expressionAttributeValues.put(":value", AttributeValue.builder().ss(basket3).build()); + + scanRequest = ScanRequest.builder() + .tableName(ddbTableName) + .filterExpression("contains(:value, fruit)") + .expressionAttributeValues(expressionAttributeValues) + .build(); + + scanResponse = ddb.scan(scanRequest); + + // Validate query was returned successfully + assert 200 == scanResponse.sdkHttpResponse().statusCode(); + + // Validate only 1 item was returned: item2 + assert scanResponse.items().size() == 1; + assert scanResponse.items().get(0).equals(item2); + + // Test a Twinned search. Select records where the dessert attribute matches the fruit attribute + scanRequest = ScanRequest.builder() + .tableName(ddbTableName) + .filterExpression("dessert = fruit") + .build(); + + scanResponse = ddb.scan(scanRequest); + + // Validate query was returned successfully + assert 200 == scanResponse.sdkHttpResponse().statusCode(); + + // Validate only 1 item was returned: item2 + assert scanResponse.items().size() == 1; + assert scanResponse.items().get(0).equals(item2); +} + + public static void main(final String[] args) { + if (args.length <= 1) { + throw new IllegalArgumentException("To run this example, include ddbTableName as args[0], branchKeyId as args[1], " + + "branchKeyWrappingKmsKeyId as args[2], and branchKeyDdbTableName as args[3]"); + } + final String ddbTableName = args[0]; + final String branchKeyId = args[1]; + final String branchKeyWrappingKmsKeyId = args[2]; + final String branchKeyDdbTableName = args[3]; + PutItemQueryItemWithBeaconStyles(ddbTableName, branchKeyId, branchKeyWrappingKmsKeyId, branchKeyDdbTableName); + } +} diff --git a/Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/searchableencryption/TestBeaconStylesSearchableEncryptionExample.java b/Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/searchableencryption/TestBeaconStylesSearchableEncryptionExample.java new file mode 100644 index 000000000..d09e1ddef --- /dev/null +++ b/Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/searchableencryption/TestBeaconStylesSearchableEncryptionExample.java @@ -0,0 +1,27 @@ +package software.amazon.cryptography.examples.searchableencryption; + +import org.testng.annotations.Test; +import software.amazon.cryptography.examples.CreateKeyStoreKeyExample; + +public class TestBeaconStylesSearchableEncryptionExample { + + @Test + public void TestCompoundItemEncryptDecrypt() throws InterruptedException { + // Create new branch key for test + String keyId = CreateKeyStoreKeyExample.KeyStoreCreateKey( + SearchableEncryptionTestUtils.TEST_BRANCH_KEYSTORE_DDB_TABLE_NAME, + SearchableEncryptionTestUtils.TEST_LOGICAL_KEYSTORE_NAME, + SearchableEncryptionTestUtils.TEST_BRANCH_KEY_WRAPPING_KMS_KEY_ARN); + + // Key creation is eventually consistent, so wait 5 seconds to decrease the likelihood + // our test fails due to eventual consistency issues. + Thread.sleep(5000); + + BeaconStylesSearchableEncryptionExample.PutItemQueryItemWithBeaconStyles( + SearchableEncryptionTestUtils.UNIT_INSPECTION_TEST_DDB_TABLE_NAME, + keyId, + SearchableEncryptionTestUtils.TEST_BRANCH_KEY_WRAPPING_KMS_KEY_ARN, + SearchableEncryptionTestUtils.TEST_BRANCH_KEYSTORE_DDB_TABLE_NAME); + } + +} diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 506b6848d..1bf899e93 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -1215,7 +1215,9 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { keySource := source, standardBeacons := standardBeacons, compoundBeacons := OptSeq(compoundBeacons), - virtualFields := OptSeq(virtualFields) + virtualFields := OptSeq(virtualFields), + encryptedParts := None, + signedParts := None ) ); } diff --git a/specification/searchable-encryption/beacons.md b/specification/searchable-encryption/beacons.md index 99da07025..bbae8e0b1 100644 --- a/specification/searchable-encryption/beacons.md +++ b/specification/searchable-encryption/beacons.md @@ -395,11 +395,15 @@ On initialization of a constructor part, the caller MUST provide: This name MUST match the name of one of the [encrypted](#encrypted-part-initialization) or [signed](#signed-part-initialization) parts. +These parts may come from these locally defined parts lists, or from the +[Global Parts List](search-config.md#global-parts-list), in any combination. + ### Default Construction * If no constructors are configured, a default constructor MUST be generated. * This default constructor MUST be all of the signed parts, followed by all the encrypted parts, all parts being required. +* Initialization MUST fail if no constructors are configured, and no local parts are configured. ### Part diff --git a/specification/searchable-encryption/search-config.md b/specification/searchable-encryption/search-config.md index ee44fa1c1..996f97de2 100644 --- a/specification/searchable-encryption/search-config.md +++ b/specification/searchable-encryption/search-config.md @@ -51,6 +51,8 @@ On initialization of the Beacon Version, the caller MAY provide: - A list of [compound beacons](beacons.md#compound-beacon-initialization) - A list of [virtual fields](virtual.md#virtual-field-initialization) + - A list of [signed parts](beacons.md#signed-part-initialization) + - A list of [encrypted parts](beacons.md#encrypted-part-initialization) Initialization MUST fail if the [version number](#version number) is not `1`. @@ -110,6 +112,16 @@ Initialization MUST fail if the [terminal location](virtual.md#terminal-location reference by a [signed part](beacons.md#signed-part) is `encrypted`, or is not `signed`. +#### Global Parts List + +The [signed parts](beacons.md#signed-part-initialization) and +[encrypted parts](beacons.md#encrypted-part-initialization) together are known as the +Global Parts List. +Parts specified in a [compound beacon's](beacons.md#compound-beacon-initialization) constructor, +may come from any combination of their local definitions or the Global Parts List. + + + ### Version Number A version number MUST be `1`.