From d6cd210ad06c560387385e9b112765bc41f5ee07 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 22 Sep 2023 14:44:36 -0400 Subject: [PATCH 01/16] feat: Global Parts List --- ...yptographyDbEncryptionSdkDynamoDbTypes.dfy | 8 +- .../Model/DynamoDbEncryption.smithy | 9 ++- .../dafny/DynamoDbEncryption/test/Beacon.dfy | 4 +- .../test/BeaconTestFixtures.dfy | 8 +- .../dbencryptionsdk/dynamodb/ToDafny.java | 10 ++- .../dbencryptionsdk/dynamodb/ToNative.java | 6 ++ .../dynamodb/model/BeaconVersion.java | 76 +++++++++++++++++++ .../dynamodb/model/CompoundBeacon.java | 8 +- .../dafny/DDBEncryption/src/TestVectors.dfy | 4 +- 9 files changed, 119 insertions(+), 14 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index c3e33b3ae..0f5c2a976 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 encrypted: Option , + nameonly signed: Option ) type BeaconVersionList = x: seq | IsValid_BeaconVersionList(x) witness * predicate method IsValid_BeaconVersionList(x: seq) { @@ -236,7 +238,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" ) type EncryptedPartsList = x: seq | IsValid_EncryptedPartsList(x) witness * predicate method IsValid_EncryptedPartsList(x: seq) { - ( 1 <= |x| ) + ( 0 <= |x| ) } datatype GetBranchKeyIdFromDdbKeyInput = | GetBranchKeyIdFromDdbKeyInput ( nameonly ddbKey: ComAmazonawsDynamodbTypes.Key @@ -341,7 +343,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" ) type SignedPartsList = x: seq | IsValid_SignedPartsList(x) witness * predicate method IsValid_SignedPartsList(x: seq) { - ( 1 <= |x| ) + ( 0 <= |x| ) } datatype SingleKeyStore = | SingleKeyStore ( nameonly keyId: string , diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index 43a48f726..9e094c0ab 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -265,12 +265,12 @@ list CompoundBeaconList { member: CompoundBeacon } -@length(min: 1) +@length(min: 0) list EncryptedPartsList { member: EncryptedPart } -@length(min: 1) +@length(min: 0) list SignedPartsList { member: SignedPart } @@ -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.") + encrypted : EncryptedPartsList, + @javadoc("The list of Signed Parts that may be included in any compound beacon.") + signed : SignedPartsList, } //= specification/searchable-encryption/search-config.md#initialization diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index 4a3745329..fbe472912 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, + encrypted := None, + signed := None ); var src := GetLiteralSource([1,2,3,4,5], version); var res := C.ConvertVersionWithSource(FullTableConfig, version, src); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index d4dbad813..d0f1a25b5 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, + encrypted := None, + signed := 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]), + encrypted := None, + signed := 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..377ab23e8 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> encrypted; + encrypted = (Objects.nonNull(nativeValue.encrypted()) && nativeValue.encrypted().size() > 0) ? + Option.create_Some(ToDafny.EncryptedPartsList(nativeValue.encrypted())) + : Option.create_None(); + Option> signed; + signed = (Objects.nonNull(nativeValue.signed()) && nativeValue.signed().size() > 0) ? + Option.create_Some(ToDafny.SignedPartsList(nativeValue.signed())) + : Option.create_None(); + return new BeaconVersion(version, keyStore, keySource, standardBeacons, compoundBeacons, virtualFields, encrypted, signed); } 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..c2bd1ebdc 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_encrypted().is_Some()) { + nativeBuilder.encrypted(ToNative.EncryptedPartsList(dafnyValue.dtor_encrypted().dtor_value())); + } + if (dafnyValue.dtor_signed().is_Some()) { + nativeBuilder.signed(ToNative.SignedPartsList(dafnyValue.dtor_signed().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..345a0241f 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 encrypted; + + /** + * The list of Signed Parts that may be included in any compound beacon. + */ + private final List signed; + 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.encrypted = builder.encrypted(); + this.signed = builder.signed(); } /** @@ -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 encrypted() { + return this.encrypted; + } + + /** + * @return The list of Signed Parts that may be included in any compound beacon. + */ + public List signed() { + return this.signed; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -161,6 +187,26 @@ public interface Builder { */ List virtualFields(); + /** + * @param encrypted The list of Encrypted Parts that may be included in any compound beacon. + */ + Builder encrypted(List encrypted); + + /** + * @return The list of Encrypted Parts that may be included in any compound beacon. + */ + List encrypted(); + + /** + * @param signed The list of Signed Parts that may be included in any compound beacon. + */ + Builder signed(List signed); + + /** + * @return The list of Signed Parts that may be included in any compound beacon. + */ + List signed(); + BeaconVersion build(); } @@ -179,6 +225,10 @@ static class BuilderImpl implements Builder { protected List virtualFields; + protected List encrypted; + + protected List signed; + protected BuilderImpl() { } @@ -190,6 +240,8 @@ protected BuilderImpl(BeaconVersion model) { this.standardBeacons = model.standardBeacons(); this.compoundBeacons = model.compoundBeacons(); this.virtualFields = model.virtualFields(); + this.encrypted = model.encrypted(); + this.signed = model.signed(); } public Builder version(int version) { @@ -247,6 +299,24 @@ public List virtualFields() { return this.virtualFields; } + public Builder encrypted(List encrypted) { + this.encrypted = encrypted; + return this; + } + + public List encrypted() { + return this.encrypted; + } + + public Builder signed(List signed) { + this.signed = signed; + return this; + } + + public List signed() { + return this.signed; + } + 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.encrypted()) && this.encrypted().size() < 0) { + throw new IllegalArgumentException("The size of `encrypted` must be greater than or equal to 0"); + } + if (Objects.nonNull(this.signed()) && this.signed().size() < 0) { + throw new IllegalArgumentException("The size of `signed` must be greater than or equal to 0"); + } return new BeaconVersion(this); } } diff --git a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java index 92ab41ff1..3ea753dc0 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java @@ -220,11 +220,11 @@ public CompoundBeacon build() { if (Objects.nonNull(this.split()) && this.split().length() > 1) { throw new IllegalArgumentException("The size of `split` must be less than or equal to 1"); } - if (Objects.nonNull(this.encrypted()) && this.encrypted().size() < 1) { - throw new IllegalArgumentException("The size of `encrypted` must be greater than or equal to 1"); + if (Objects.nonNull(this.encrypted()) && this.encrypted().size() < 0) { + throw new IllegalArgumentException("The size of `encrypted` must be greater than or equal to 0"); } - if (Objects.nonNull(this.signed()) && this.signed().size() < 1) { - throw new IllegalArgumentException("The size of `signed` must be greater than or equal to 1"); + if (Objects.nonNull(this.signed()) && this.signed().size() < 0) { + throw new IllegalArgumentException("The size of `signed` must be greater than or equal to 0"); } if (Objects.nonNull(this.constructors()) && this.constructors().size() < 1) { throw new IllegalArgumentException("The size of `constructors` must be greater than or equal to 1"); diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 506b6848d..289f3205d 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), + encrypted := None, + signed := None ) ); } From eecde988d90170f0ac37be7e953b8f9ec62ca176 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 25 Sep 2023 12:57:55 -0400 Subject: [PATCH 02/16] implement --- ...yptographyDbEncryptionSdkDynamoDbTypes.dfy | 4 +- .../Model/DynamoDbEncryption.smithy | 4 +- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 343 +++++++++++++----- .../dafny/DynamoDbEncryption/test/Beacon.dfy | 204 ++++++++--- .../test/BeaconTestFixtures.dfy | 8 +- .../dbencryptionsdk/dynamodb/ToDafny.java | 14 +- .../dbencryptionsdk/dynamodb/ToNative.java | 8 +- .../dynamodb/model/BeaconVersion.java | 60 +-- .../dafny/DDBEncryption/src/TestVectors.dfy | 4 +- 9 files changed, 461 insertions(+), 188 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index 0f5c2a976..e159e475e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -45,8 +45,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" nameonly standardBeacons: StandardBeaconList , nameonly compoundBeacons: Option , nameonly virtualFields: Option , - nameonly encrypted: Option , - nameonly signed: 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 9e094c0ab..9e22dd3c5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -724,9 +724,9 @@ structure BeaconVersion { virtualFields : VirtualFieldList, @javadoc("The list of Encrypted Parts that may be included in any compound beacon.") - encrypted : EncryptedPartsList, + encryptedParts : EncryptedPartsList, @javadoc("The list of Signed Parts that may be included in any compound beacon.") - signed : SignedPartsList, + signedParts : SignedPartsList, } //= specification/searchable-encryption/search-config.md#initialization diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 4e475b014..d04918f1e 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,9 +406,9 @@ 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 @@ -399,7 +416,7 @@ module SearchConfigToInfo { 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(converted[twin].std.length as int) + ".")) else Failure(E("Beacon " + name + " is twinned to " + twin + " but " + twin + " is a compound beacon.")) else @@ -471,7 +488,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 +528,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 +618,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 +650,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,13 +816,120 @@ 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 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 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 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 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( beacon : CompoundBeacon, outer : DynamoDbTableEncryptionConfig, client: Primitives.AtomicPrimitivesClient, virtualFields : V.VirtualFieldMap, - converted : I.BeaconMap + converted : I.BeaconMap, + globalSignedParts : PartSet, + globalEncryptedParts : PartSet ) : (ret : Result) @@ -767,29 +937,38 @@ module SearchConfigToInfo { //= 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); + && ret.value.base.name == beacon.name + && encrypted.Success? + && (|encrypted.value| == 0 ==> ret.value.base.beaconName == beacon.name) + && (|encrypted.value| != 0 ==> ret.value.base.beaconName == BeaconPrefix + beacon.name) { - // 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 +980,7 @@ module SearchConfigToInfo { beaconName := beaconName ), beacon.split[0], - parts, + allParts, numNon, constructors ) @@ -812,7 +991,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 +1022,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 +1052,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 +1082,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/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index fbe472912..0ce1d230f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -44,8 +44,8 @@ module TestBaseBeacon { standardBeacons := [NameB, TitleB, TooBadB], compoundBeacons := Some([BadPrefix]), virtualFields := None, - encrypted := None, - signed := None + encryptedParts := None, + signedParts := None ); var src := GetLiteralSource([1,2,3,4,5], version); var res := C.ConvertVersionWithSource(FullTableConfig, version, src); @@ -264,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])); @@ -377,8 +377,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]); @@ -387,21 +387,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); @@ -410,9 +410,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 @@ -433,7 +433,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]); @@ -442,17 +442,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); @@ -461,9 +461,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 ( @@ -485,13 +485,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]); @@ -527,7 +527,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]); @@ -545,9 +545,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 @@ -573,7 +573,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]); @@ -591,9 +591,123 @@ 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); + } + + + /* + both w/o constructor + just global w/ constructor + + var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); + print "\n", bv.error, "\n"; + + + + */ + + } + diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy index d0f1a25b5..fb9bff6fe 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/BeaconTestFixtures.dfy @@ -154,8 +154,8 @@ module BeaconTestFixtures { standardBeacons := [std2], compoundBeacons := None, virtualFields := None, - encrypted := None, - signed := None + encryptedParts := None, + signedParts := None ); } @@ -172,8 +172,8 @@ module BeaconTestFixtures { standardBeacons := [std2, std4, std6, NameTitleBeacon, NameB, TitleB], compoundBeacons := Some([NameTitle, YearName, Mixed, JustSigned]), virtualFields := Some([NameTitleField]), - encrypted := None, - signed := None + 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 377ab23e8..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,15 +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(); - Option> encrypted; - encrypted = (Objects.nonNull(nativeValue.encrypted()) && nativeValue.encrypted().size() > 0) ? - Option.create_Some(ToDafny.EncryptedPartsList(nativeValue.encrypted())) + Option> encryptedParts; + encryptedParts = (Objects.nonNull(nativeValue.encryptedParts()) && nativeValue.encryptedParts().size() > 0) ? + Option.create_Some(ToDafny.EncryptedPartsList(nativeValue.encryptedParts())) : Option.create_None(); - Option> signed; - signed = (Objects.nonNull(nativeValue.signed()) && nativeValue.signed().size() > 0) ? - Option.create_Some(ToDafny.SignedPartsList(nativeValue.signed())) + 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, encrypted, signed); + 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 c2bd1ebdc..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,11 +127,11 @@ public static BeaconVersion BeaconVersion( if (dafnyValue.dtor_virtualFields().is_Some()) { nativeBuilder.virtualFields(ToNative.VirtualFieldList(dafnyValue.dtor_virtualFields().dtor_value())); } - if (dafnyValue.dtor_encrypted().is_Some()) { - nativeBuilder.encrypted(ToNative.EncryptedPartsList(dafnyValue.dtor_encrypted().dtor_value())); + if (dafnyValue.dtor_encryptedParts().is_Some()) { + nativeBuilder.encryptedParts(ToNative.EncryptedPartsList(dafnyValue.dtor_encryptedParts().dtor_value())); } - if (dafnyValue.dtor_signed().is_Some()) { - nativeBuilder.signed(ToNative.SignedPartsList(dafnyValue.dtor_signed().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 345a0241f..21135f766 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 @@ -44,12 +44,12 @@ public class BeaconVersion { /** * The list of Encrypted Parts that may be included in any compound beacon. */ - private final List encrypted; + private final List encryptedParts; /** * The list of Signed Parts that may be included in any compound beacon. */ - private final List signed; + private final List signedParts; protected BeaconVersion(BuilderImpl builder) { this.version = builder.version(); @@ -58,8 +58,8 @@ protected BeaconVersion(BuilderImpl builder) { this.standardBeacons = builder.standardBeacons(); this.compoundBeacons = builder.compoundBeacons(); this.virtualFields = builder.virtualFields(); - this.encrypted = builder.encrypted(); - this.signed = builder.signed(); + this.encryptedParts = builder.encryptedParts(); + this.signedParts = builder.signedParts(); } /** @@ -107,15 +107,15 @@ public List virtualFields() { /** * @return The list of Encrypted Parts that may be included in any compound beacon. */ - public List encrypted() { - return this.encrypted; + public List encryptedParts() { + return this.encryptedParts; } /** * @return The list of Signed Parts that may be included in any compound beacon. */ - public List signed() { - return this.signed; + public List signedParts() { + return this.signedParts; } public Builder toBuilder() { @@ -188,24 +188,24 @@ public interface Builder { List virtualFields(); /** - * @param encrypted The list of Encrypted Parts that may be included in any compound beacon. + * @param encryptedParts The list of Encrypted Parts that may be included in any compound beacon. */ - Builder encrypted(List encrypted); + Builder encryptedParts(List encryptedParts); /** * @return The list of Encrypted Parts that may be included in any compound beacon. */ - List encrypted(); + List encryptedParts(); /** - * @param signed The list of Signed Parts that may be included in any compound beacon. + * @param signedParts The list of Signed Parts that may be included in any compound beacon. */ - Builder signed(List signed); + Builder signedParts(List signedParts); /** * @return The list of Signed Parts that may be included in any compound beacon. */ - List signed(); + List signedParts(); BeaconVersion build(); } @@ -225,9 +225,9 @@ static class BuilderImpl implements Builder { protected List virtualFields; - protected List encrypted; + protected List encryptedParts; - protected List signed; + protected List signedParts; protected BuilderImpl() { } @@ -240,8 +240,8 @@ protected BuilderImpl(BeaconVersion model) { this.standardBeacons = model.standardBeacons(); this.compoundBeacons = model.compoundBeacons(); this.virtualFields = model.virtualFields(); - this.encrypted = model.encrypted(); - this.signed = model.signed(); + this.encryptedParts = model.encryptedParts(); + this.signedParts = model.signedParts(); } public Builder version(int version) { @@ -299,22 +299,22 @@ public List virtualFields() { return this.virtualFields; } - public Builder encrypted(List encrypted) { - this.encrypted = encrypted; + public Builder encryptedParts(List encryptedParts) { + this.encryptedParts = encryptedParts; return this; } - public List encrypted() { - return this.encrypted; + public List encryptedParts() { + return this.encryptedParts; } - public Builder signed(List signed) { - this.signed = signed; + public Builder signedParts(List signedParts) { + this.signedParts = signedParts; return this; } - public List signed() { - return this.signed; + public List signedParts() { + return this.signedParts; } public BeaconVersion build() { @@ -342,11 +342,11 @@ 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.encrypted()) && this.encrypted().size() < 0) { - throw new IllegalArgumentException("The size of `encrypted` must be greater than or equal to 0"); + if (Objects.nonNull(this.encryptedParts()) && this.encryptedParts().size() < 0) { + throw new IllegalArgumentException("The size of `encryptedParts` must be greater than or equal to 0"); } - if (Objects.nonNull(this.signed()) && this.signed().size() < 0) { - throw new IllegalArgumentException("The size of `signed` must be greater than or equal to 0"); + if (Objects.nonNull(this.signedParts()) && this.signedParts().size() < 0) { + throw new IllegalArgumentException("The size of `signedParts` must be greater than or equal to 0"); } return new BeaconVersion(this); } diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 289f3205d..1bf899e93 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -1216,8 +1216,8 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { standardBeacons := standardBeacons, compoundBeacons := OptSeq(compoundBeacons), virtualFields := OptSeq(virtualFields), - encrypted := None, - signed := None + encryptedParts := None, + signedParts := None ) ); } From 63e69d3353b7f0b1c326b4e717ed8fd29103ac64 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 25 Sep 2023 13:49:03 -0400 Subject: [PATCH 03/16] faster proofs --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index d04918f1e..1f8721224 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -844,7 +844,7 @@ module SearchConfigToInfo { GetGlobalParts(cons[1..], globalParts, signed, newParts) } - function method GetAllEncryptedParts( + function method {:opaque} GetAllEncryptedParts( parts : seq, cons : seq, globalEncryptedParts : PartSet, @@ -881,7 +881,7 @@ module SearchConfigToInfo { FindGlobalPart(globalParts[1..], cons, signed) } - function method GetAllSignedParts( + function method {:opaque} GetAllSignedParts( parts : seq, cons : seq, globalSignedParts : PartSet, @@ -897,7 +897,7 @@ module SearchConfigToInfo { Success(both.parts) } - function method CheckSignedParts(parts : seq, globals : PartSet, name : string) : Result + function method {:opaque} {:tailrecursion} CheckSignedParts(parts : seq, globals : PartSet, name : string) : Result { if |parts| == 0 then Success(true) @@ -909,7 +909,7 @@ module SearchConfigToInfo { CheckSignedParts(parts[1..], globals, name) } - function method CheckEncryptedParts(parts : seq, globals : PartSet, name : string) : Result + function method {:opaque} {:tailrecursion} CheckEncryptedParts(parts : seq, globals : PartSet, name : string) : Result { if |parts| == 0 then Success(true) @@ -922,7 +922,7 @@ module SearchConfigToInfo { } // Construct a CompoundBeacon from its configuration - function method CreateCompoundBeacon( + function method {:opaque} CreateCompoundBeacon( beacon : CompoundBeacon, outer : DynamoDbTableEncryptionConfig, client: Primitives.AtomicPrimitivesClient, @@ -933,6 +933,9 @@ module SearchConfigToInfo { ) : (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`. @@ -940,8 +943,8 @@ module SearchConfigToInfo { && 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); - && ret.value.base.name == beacon.name && 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) { From b8aa6ad5712ae3e7642ca5dc0690916462013aba Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 25 Sep 2023 14:04:44 -0400 Subject: [PATCH 04/16] m --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 1f8721224..745f91c5f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -931,7 +931,7 @@ module SearchConfigToInfo { 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? From 9cb46b976d9c4f4daf3ed634bc5d47bc7f1b3e00 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 25 Sep 2023 16:19:10 -0400 Subject: [PATCH 05/16] spec --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 8 ++++++++ .../dafny/DynamoDbEncryption/test/Beacon.dfy | 15 --------------- specification/searchable-encryption/beacons.md | 4 ++++ .../searchable-encryption/search-config.md | 12 ++++++++++++ 4 files changed, 24 insertions(+), 15 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 745f91c5f..7c1f6f587 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -947,6 +947,14 @@ module SearchConfigToInfo { && 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?) { var signedParts := if beacon.signed.Some? then beacon.signed.value else []; var encryptedParts := if beacon.encrypted.Some? then beacon.encrypted.value else []; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index 0ce1d230f..6fcdf5063 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -695,19 +695,4 @@ module TestBaseBeacon { var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); } - - - /* - both w/o constructor - just global w/ constructor - - var newConfig := FullTableConfig.(attributeActionsOnEncrypt := FullTableConfig.attributeActionsOnEncrypt["twinBeacon" := SE.ENCRYPT_AND_SIGN]); - print "\n", bv.error, "\n"; - - - - */ - - } - 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`. From 9698c730a59ef7216efb48ee6629e827cf7a15b0 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 26 Sep 2023 15:49:08 -0400 Subject: [PATCH 06/16] add example --- ...yptographyDbEncryptionSdkDynamoDbTypes.dfy | 4 +- .../Model/DynamoDbEncryption.smithy | 4 +- .../dafny/DynamoDbEncryption/src/Beacon.dfy | 25 +- .../DynamoDbEncryption/src/FilterExpr.dfy | 36 +- .../DynamoDbEncryption/src/SearchInfo.dfy | 4 +- .../dafny/DynamoDbEncryption/test/Beacon.dfy | 12 +- .../dynamodb/model/BeaconVersion.java | 8 +- .../dynamodb/model/CompoundBeacon.java | 8 +- ...aconStylesSearchableEncryptionExample.java | 329 ++++++++++++++++++ ...aconStylesSearchableEncryptionExample.java | 27 ++ 10 files changed, 418 insertions(+), 39 deletions(-) create mode 100644 Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java create mode 100644 Examples/runtimes/java/DynamoDbEncryption/src/test/java/software/amazon/cryptography/examples/searchableencryption/TestBeaconStylesSearchableEncryptionExample.java diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index e159e475e..6b5dd95af 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -238,7 +238,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" ) type EncryptedPartsList = x: seq | IsValid_EncryptedPartsList(x) witness * predicate method IsValid_EncryptedPartsList(x: seq) { - ( 0 <= |x| ) + ( 1 <= |x| ) } datatype GetBranchKeyIdFromDdbKeyInput = | GetBranchKeyIdFromDdbKeyInput ( nameonly ddbKey: ComAmazonawsDynamodbTypes.Key @@ -343,7 +343,7 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy" ) type SignedPartsList = x: seq | IsValid_SignedPartsList(x) witness * predicate method IsValid_SignedPartsList(x: seq) { - ( 0 <= |x| ) + ( 1 <= |x| ) } datatype SingleKeyStore = | SingleKeyStore ( nameonly keyId: string , diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index 9e22dd3c5..562bf0a2b 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -265,12 +265,12 @@ list CompoundBeaconList { member: CompoundBeacon } -@length(min: 0) +@length(min: 1) list EncryptedPartsList { member: EncryptedPart } -@length(min: 0) +@length(min: 1) list SignedPartsList { member: SignedPart } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy index 5613bfd90..9a79f8026 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/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 6fcdf5063..b948fcd10 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -508,9 +508,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() @@ -696,3 +704,5 @@ module TestBaseBeacon { var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); } } + +// FIXME -- no twin of a twin \ No newline at end of file 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 21135f766..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 @@ -342,11 +342,11 @@ 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() < 0) { - throw new IllegalArgumentException("The size of `encryptedParts` must be greater than or equal to 0"); + 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() < 0) { - throw new IllegalArgumentException("The size of `signedParts` must be greater than or equal to 0"); + 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/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java index 3ea753dc0..92ab41ff1 100644 --- a/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java +++ b/DynamoDbEncryption/runtimes/java/src/main/smithy-generated/software/amazon/cryptography/dbencryptionsdk/dynamodb/model/CompoundBeacon.java @@ -220,11 +220,11 @@ public CompoundBeacon build() { if (Objects.nonNull(this.split()) && this.split().length() > 1) { throw new IllegalArgumentException("The size of `split` must be less than or equal to 1"); } - if (Objects.nonNull(this.encrypted()) && this.encrypted().size() < 0) { - throw new IllegalArgumentException("The size of `encrypted` must be greater than or equal to 0"); + if (Objects.nonNull(this.encrypted()) && this.encrypted().size() < 1) { + throw new IllegalArgumentException("The size of `encrypted` must be greater than or equal to 1"); } - if (Objects.nonNull(this.signed()) && this.signed().size() < 0) { - throw new IllegalArgumentException("The size of `signed` must be greater than or equal to 0"); + if (Objects.nonNull(this.signed()) && this.signed().size() < 1) { + throw new IllegalArgumentException("The size of `signed` must be greater than or equal to 1"); } if (Objects.nonNull(this.constructors()) && this.constructors().size() < 1) { throw new IllegalArgumentException("The size of `constructors` must be greater than or equal to 1"); 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..c186e00f8 --- /dev/null +++ b/Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java @@ -0,0 +1,329 @@ +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 + 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 + // Wwe 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); + + // 3. 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(); + + // 4. 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() + ); + + // 5. 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); + + // 6. 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 + + // 7. 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); + + // 8. Create config + final DynamoDbTablesEncryptionConfig encryptionConfig = + DynamoDbTablesEncryptionConfig.builder() + .tableEncryptionConfigs(tableConfigs) + .build(); + + // 9. 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()); + + // 10. 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()); + + // 11. Create the DynamoDb Encryption Interceptor + DynamoDbEncryptionInterceptor encryptionInterceptor = DynamoDbEncryptionInterceptor.builder() + .config(encryptionConfig) + .build(); + + // 12. 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(); + + // 13. 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(); + + + // 14. 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); + + // 15. 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); + + // 16. 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); + } + +} From 21c1706c9761bfdfd8981dcc1b7cb1d34e228091 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 27 Sep 2023 09:57:44 -0400 Subject: [PATCH 07/16] more tests --- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 33 +++++++++------- .../dafny/DynamoDbEncryption/test/Beacon.dfy | 39 ++++++++++++++++++- 2 files changed, 57 insertions(+), 15 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 7c1f6f587..3222e20ff 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -411,12 +411,19 @@ module SearchConfigToInfo { && 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 @@ -541,10 +548,10 @@ module SearchConfigToInfo { Failure(E("Duplicate prefix " + part.getPrefix() + " in " + name + ".")) else Success(PartSet( - parts := parts + [part], - names := names + {part.getName()}, - prefixes := prefixes + {part.getPrefix()} - )) + parts := parts + [part], + names := names + {part.getName()}, + prefixes := prefixes + {part.getPrefix()} + )) } function method GetSetAsString(strings : set) : string @@ -553,7 +560,7 @@ module SearchConfigToInfo { var names := SortedSets.ComputeSetToOrderedSequence2(strings, CharLess); Join(names, ", ") } - + function method combine(other : PartSet, name : string, otherName : string) : Result { if |names * other.names| != 0 then @@ -564,10 +571,10 @@ module SearchConfigToInfo { 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 - )) + parts := parts + other.parts, + names := names + other.names, + prefixes := prefixes + other.prefixes + )) } } @@ -1005,7 +1012,7 @@ module SearchConfigToInfo { converted : I.BeaconMap, globalSignedParts : PartSet, globalEncryptedParts : PartSet - ) + ) returns (output : Result) modifies client.Modifies requires client.ValidState() diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index b948fcd10..dbaff8cf5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -320,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(); @@ -704,5 +741,3 @@ module TestBaseBeacon { var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); } } - -// FIXME -- no twin of a twin \ No newline at end of file From c3e844aae69bbbd5d5d11fb49b7f7e66370167c3 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:29:55 -0400 Subject: [PATCH 08/16] Update Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java Co-authored-by: Lucas McDonald --- .../BeaconStylesSearchableEncryptionExample.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 index c186e00f8..db1d96172 100644 --- 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 @@ -253,12 +253,12 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .expressionAttributeValues(expressionAttributeValues) .build(); - ScanResponse scanResponse = ddb.scan(scanRequest); - // Validate query was returned successfully - assert 200 == scanResponse.sdkHttpResponse().statusCode(); + 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; + // Validate only 1 item was returned: item1 + assert scanResponse.items().size() == 1; assert scanResponse.items().get(0).equals(item1); // 15. Test the second type of Set operation : From 9a0f196d12be616709ac5d4e69a0daa2d056eeba Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:30:10 -0400 Subject: [PATCH 09/16] Update Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java Co-authored-by: Lucas McDonald --- .../BeaconStylesSearchableEncryptionExample.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 index db1d96172..14554d407 100644 --- 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 @@ -268,12 +268,12 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .filterExpression("contains(basket, fruit)") .build(); - scanResponse = ddb.scan(scanRequest); - // Validate query was returned successfully - assert 200 == scanResponse.sdkHttpResponse().statusCode(); + 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; + // Validate only 1 item was returned: item1 + assert scanResponse.items().size() == 1; assert scanResponse.items().get(0).equals(item1); // 16. Test the third type of Set operation : From 5a5f369f95ed49419a9509069468118cdc13ad81 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:30:18 -0400 Subject: [PATCH 10/16] Update Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java Co-authored-by: Lucas McDonald --- .../BeaconStylesSearchableEncryptionExample.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 index 14554d407..da05fc688 100644 --- 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 @@ -308,10 +308,10 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String scanResponse = ddb.scan(scanRequest); // Validate query was returned successfully - assert 200 == scanResponse.sdkHttpResponse().statusCode(); + assert 200 == scanResponse.sdkHttpResponse().statusCode(); - // Validate only 1 item was returned: item2 - assert scanResponse.items().size() == 1; + // Validate only 1 item was returned: item2 + assert scanResponse.items().size() == 1; assert scanResponse.items().get(0).equals(item2); } From 851622b8bfd4e9d8dfeb166110f9c219886a2939 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:30:26 -0400 Subject: [PATCH 11/16] Update Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java Co-authored-by: Lucas McDonald --- .../BeaconStylesSearchableEncryptionExample.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 index da05fc688..bda6eafbc 100644 --- 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 @@ -101,7 +101,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String standardBeaconList.add(basketBeacon); // The dessert beacon allows searching on the encrypted dessert attribute - // Wwe need to be able to compare the dessert attribute to the fruit 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") From 67c1e1dab63419939568d0f2006145888ce592db Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:30:43 -0400 Subject: [PATCH 12/16] Update Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java Co-authored-by: Lucas McDonald --- .../BeaconStylesSearchableEncryptionExample.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 index bda6eafbc..478ecc194 100644 --- 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 @@ -85,8 +85,8 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String 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 + // 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() From a52dd63efa192d8b771407dff8f8723454b617cc Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:31:36 -0400 Subject: [PATCH 13/16] Update Examples/runtimes/java/DynamoDbEncryption/src/main/java/software/amazon/cryptography/examples/searchableencryption/BeaconStylesSearchableEncryptionExample.java Co-authored-by: Lucas McDonald --- .../BeaconStylesSearchableEncryptionExample.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 index 478ecc194..e51440669 100644 --- 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 @@ -293,10 +293,10 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String scanResponse = ddb.scan(scanRequest); // Validate query was returned successfully - assert 200 == scanResponse.sdkHttpResponse().statusCode(); + assert 200 == scanResponse.sdkHttpResponse().statusCode(); - // Validate only 1 item was returned: item2 - assert scanResponse.items().size() == 1; + // 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 From 523f154318258f5f89d38cb5caaadc848d7b0c9d Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 27 Sep 2023 13:38:10 -0400 Subject: [PATCH 14/16] improve example comments --- ...aconStylesSearchableEncryptionExample.java | 31 ++++++++++--------- 1 file changed, 17 insertions(+), 14 deletions(-) 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 index e51440669..58a138d84 100644 --- 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 @@ -78,6 +78,9 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String 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) @@ -114,7 +117,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .build(); standardBeaconList.add(dessertBeacon); - // 3. Configure the Keystore + // 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() @@ -126,7 +129,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .build()) .build(); - // 4. Create BeaconVersion. + // 3. Create BeaconVersion. // This is similar to the Basic example List beaconVersions = new ArrayList<>(); beaconVersions.add( @@ -143,7 +146,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .build() ); - // 5. Create a Hierarchical Keyring + // 4. Create a Hierarchical Keyring // This is the same configuration as in the Basic example. final MaterialProviders matProv = MaterialProviders.builder() .MaterialProvidersConfig(MaterialProvidersConfig.builder().build()) @@ -155,7 +158,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .build(); final IKeyring kmsKeyring = matProv.CreateAwsKmsHierarchicalKeyring(keyringInput); - // 6. Configure which attributes are encrypted and/or signed when writing new items. + // 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 @@ -163,7 +166,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String attributeActionsOnEncrypt.put("fruit", CryptoAction.ENCRYPT_AND_SIGN); // Beaconized attributes must be encrypted attributeActionsOnEncrypt.put("basket", CryptoAction.ENCRYPT_AND_SIGN); // Beaconized attributes must be encrypted - // 7. Create the DynamoDb Encryption configuration for the table we will be writing to. + // 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() @@ -179,13 +182,13 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .build(); tableConfigs.put(ddbTableName, config); - // 8. Create config + // 7. Create config final DynamoDbTablesEncryptionConfig encryptionConfig = DynamoDbTablesEncryptionConfig.builder() .tableEncryptionConfigs(tableConfigs) .build(); - // 9. Create item one, specifically with "dessert != fruit", and "fruit in basket". + // 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()); @@ -197,7 +200,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String basket.add("pear"); item1.put("basket", AttributeValue.builder().ss(basket).build()); - // 10. Create item two, specifically with "dessert == fruit", and "fruit not in basket". + // 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()); @@ -209,12 +212,12 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String basket.add("blackberry"); item2.put("basket", AttributeValue.builder().ss(basket).build()); - // 11. Create the DynamoDb Encryption Interceptor + // 10. Create the DynamoDb Encryption Interceptor DynamoDbEncryptionInterceptor encryptionInterceptor = DynamoDbEncryptionInterceptor.builder() .config(encryptionConfig) .build(); - // 12. Create a new AWS SDK DynamoDb client using the DynamoDb Encryption Interceptor above + // 11. Create a new AWS SDK DynamoDb client using the DynamoDb Encryption Interceptor above final DynamoDbClient ddb = DynamoDbClient.builder() .overrideConfiguration( ClientOverrideConfiguration.builder() @@ -222,7 +225,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String .build()) .build(); - // 13. Add the two items + // 12. Add the two items PutItemRequest putRequest = PutItemRequest.builder() .tableName(ddbTableName) .item(item1) @@ -242,7 +245,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String assert 200 == putResponse.sdkHttpResponse().statusCode(); - // 14. Test the first type of Set operation : + // 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()); @@ -261,7 +264,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String assert scanResponse.items().size() == 1; assert scanResponse.items().get(0).equals(item1); - // 15. Test the second type of Set operation : + // 14. Test the second type of Set operation : // Select records where the basket attribute holds the fruit attribute scanRequest = ScanRequest.builder() .tableName(ddbTableName) @@ -276,7 +279,7 @@ public static void PutItemQueryItemWithBeaconStyles(String ddbTableName, String assert scanResponse.items().size() == 1; assert scanResponse.items().get(0).equals(item1); - // 16. Test the third type of Set operation : + // 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"); From 374dda698a2adc44766c798929f7f6457ad7ed65 Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:48:03 -0400 Subject: [PATCH 15/16] Update DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy Co-authored-by: seebees --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy index 9a79f8026..44cd0f975 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy @@ -245,7 +245,7 @@ module BaseBeacon { //# * 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? + && (value.Some? && !(value.value.SS? || value.value.NS? || value.value.BS?) ==> ret.Failure?) { var value := TermLoc.TermToAttr(loc, item, None); if value.None? then From 67a3715444edd2889201cf77b7ca12d0e9ff2b1d Mon Sep 17 00:00:00 2001 From: Andrew Jewell <107044381+ajewellamz@users.noreply.github.com> Date: Wed, 27 Sep 2023 13:50:57 -0400 Subject: [PATCH 16/16] Update DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy Co-authored-by: seebees --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 1 + 1 file changed, 1 insertion(+) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 3222e20ff..35d1a324c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -963,6 +963,7 @@ module SearchConfigToInfo { && 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 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 [];