From ac87a66479200716ab4270ce704606989893b70f Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 19 Jun 2025 14:55:47 -0400 Subject: [PATCH 01/10] chore(dafny): Add bucket beacon support --- ...yptographyDbEncryptionSdkDynamoDbTypes.dfy | 9 +++- .../Model/DynamoDbEncryption.smithy | 5 +++ ...DbEncryptionSdkDynamoDbTransformsTypes.dfy | 2 +- ...ncryptionSdkDynamoDbItemEncryptorTypes.dfy | 2 +- ...EncryptionSdkStructuredEncryptionTypes.dfy | 2 +- .../to_dafny.go | 13 +++++- .../to_native.go | 12 +++++ .../types.go | 7 +++ .../to_dafny.go | 13 +++++- .../to_native.go | 12 +++++ .../types.go | 7 +++ .../dbencryptionsdk/dynamodb/ToDafny.java | 11 ++++- .../dbencryptionsdk/dynamodb/ToNative.java | 5 +++ .../dynamodb/model/BeaconVersion.java | 44 +++++++++++++++++++ .../DynamoDbEncryption/BeaconVersion.cs | 18 ++++++++ .../TypeConversion.cs | 22 +++++++++- 16 files changed, 172 insertions(+), 12 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index 2712ba605..476c7706d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald import AwsCryptographyKeyStoreTypes import AwsCryptographyPrimitivesTypes import ComAmazonawsDynamodbTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types @@ -46,12 +46,17 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald nameonly compoundBeacons: Option := Option.None , nameonly virtualFields: Option := Option.None , nameonly encryptedParts: Option := Option.None , - nameonly signedParts: Option := Option.None + nameonly signedParts: Option := Option.None , + nameonly numberOfBuckets: Option := Option.None ) type BeaconVersionList = x: seq | IsValid_BeaconVersionList(x) witness * predicate method IsValid_BeaconVersionList(x: seq) { ( 1 <= |x| <= 1 ) } + type BucketCount = x: int32 | IsValid_BucketCount(x) witness * + predicate method IsValid_BucketCount(x: int32) { + ( 1 <= x ) + } type Char = x: string | IsValid_Char(x) witness * predicate method IsValid_Char(x: string) { ( 1 <= |x| <= 1 ) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy index 87716dcc5..f4a14bda8 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy @@ -286,6 +286,9 @@ integer BeaconBitLength @range(min: 1) integer VersionNumber +@range(min: 1) +integer BucketCount + @length(min: 1, max: 1) string Char @@ -796,6 +799,8 @@ structure BeaconVersion { encryptedParts : EncryptedPartsList, @javadoc("The list of Signed Parts that may be included in any compound beacon.") signedParts : SignedPartsList, + @javadoc("The number of separate buckets across which beacons should be divided.") + numberOfBuckets : BucketCount } //= specification/searchable-encryption/search-config.md#initialization diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy index de056cf74..9e2f86575 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy @@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import AwsCryptographyMaterialProvidersTypes import ComAmazonawsDynamodbTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy index 2a2c00d7f..e712158c7 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy @@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry import AwsCryptographyMaterialProvidersTypes import AwsCryptographyPrimitivesTypes import ComAmazonawsDynamodbTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy index 7c14e9f87..0ad88e609 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy @@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti import opened UTF8 import AwsCryptographyMaterialProvidersTypes import AwsCryptographyPrimitivesTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go index 015d4054d..d4bf22a22 100644 --- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go +++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go @@ -432,7 +432,7 @@ func VirtualField_ToDafny(nativeInput awscryptographydbencryptionsdkdynamodbsmit func BeaconVersion_ToDafny(nativeInput awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.BeaconVersion) AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { return func() AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { - return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(nativeInput.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(nativeInput.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(nativeInput.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(nativeInput.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(nativeInput.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(nativeInput.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(nativeInput.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(nativeInput.SignedParts)) + return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(nativeInput.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(nativeInput.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(nativeInput.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(nativeInput.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(nativeInput.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(nativeInput.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(nativeInput.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(nativeInput.SignedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_ToDafny(nativeInput.NumberOfBuckets)) }() } @@ -1506,6 +1506,15 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny }() } +func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_ToDafny(input *int32) Wrappers.Option { + return func() Wrappers.Option { + if input == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(*input) + }() +} + func Aws_cryptography_dbEncryptionSdk_dynamoDb_LegacyOverride_policy_ToDafny(input awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy) AwsCryptographyDbEncryptionSdkDynamoDbTypes.LegacyPolicy { return func() AwsCryptographyDbEncryptionSdkDynamoDbTypes.LegacyPolicy { @@ -1621,7 +1630,7 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_SearchConfig_versions_ToDafny(inp func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersionList_member_ToDafny(input awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.BeaconVersion) AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { return func() AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { - return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(input.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(input.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(input.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(input.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(input.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(input.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(input.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(input.SignedParts)) + return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(input.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(input.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(input.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(input.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(input.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(input.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(input.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(input.SignedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_ToDafny(input.NumberOfBuckets)) }() } diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go index b0db0fe5e..e15100c95 100644 --- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go +++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go @@ -408,6 +408,7 @@ func BeaconVersion_FromDafny(input interface{}) awscryptographydbencryptionsdkdy VirtualFields: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_virtualFields().UnwrapOr(nil)), EncryptedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_encryptedParts().UnwrapOr(nil)), SignedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_signedParts().UnwrapOr(nil)), + NumberOfBuckets: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_numberOfBuckets().UnwrapOr(nil)), } } @@ -1367,6 +1368,16 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_FromDaf } return fieldValue } +func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_FromDafny(input interface{}) *int32 { + return func() *int32 { + var b int32 + if input == nil { + return nil + } + b = input.(int32) + return &b + }() +} func Aws_cryptography_dbEncryptionSdk_dynamoDb_LegacyOverride_policy_FromDafny(input interface{}) awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy { return func() awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy { var u awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy @@ -1468,6 +1479,7 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersionList_member_FromDafn VirtualFields: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_virtualFields().UnwrapOr(nil)), EncryptedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_encryptedParts().UnwrapOr(nil)), SignedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_signedParts().UnwrapOr(nil)), + NumberOfBuckets: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_numberOfBuckets().UnwrapOr(nil)), } } func Aws_cryptography_dbEncryptionSdk_dynamoDb_SearchConfig_writeVersion_FromDafny(input interface{}) int32 { diff --git a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go index f85e3375a..ffcb8efac 100644 --- a/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go +++ b/DynamoDbEncryption/runtimes/go/ImplementationFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go @@ -783,6 +783,8 @@ type BeaconVersion struct { EncryptedParts []EncryptedPart + NumberOfBuckets *int32 + SignedParts []SignedPart VirtualFields []VirtualField @@ -819,6 +821,11 @@ func (input BeaconVersion) Validate() error { if input.Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_Validate() != nil { return input.Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_Validate() } + if input.NumberOfBuckets != nil { + if *input.NumberOfBuckets < 1 { + return fmt.Errorf("BucketCount has a minimum of 1 but has the value of %d.", *input.NumberOfBuckets) + } + } if len(input.SignedParts) < 1 { return fmt.Errorf("SignedPartsList has a minimum length of 1 but has the length of %d.", len(input.SignedParts)) } diff --git a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go index 015d4054d..d4bf22a22 100644 --- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go +++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_dafny.go @@ -432,7 +432,7 @@ func VirtualField_ToDafny(nativeInput awscryptographydbencryptionsdkdynamodbsmit func BeaconVersion_ToDafny(nativeInput awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.BeaconVersion) AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { return func() AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { - return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(nativeInput.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(nativeInput.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(nativeInput.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(nativeInput.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(nativeInput.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(nativeInput.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(nativeInput.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(nativeInput.SignedParts)) + return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(nativeInput.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(nativeInput.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(nativeInput.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(nativeInput.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(nativeInput.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(nativeInput.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(nativeInput.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(nativeInput.SignedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_ToDafny(nativeInput.NumberOfBuckets)) }() } @@ -1506,6 +1506,15 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny }() } +func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_ToDafny(input *int32) Wrappers.Option { + return func() Wrappers.Option { + if input == nil { + return Wrappers.Companion_Option_.Create_None_() + } + return Wrappers.Companion_Option_.Create_Some_(*input) + }() +} + func Aws_cryptography_dbEncryptionSdk_dynamoDb_LegacyOverride_policy_ToDafny(input awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy) AwsCryptographyDbEncryptionSdkDynamoDbTypes.LegacyPolicy { return func() AwsCryptographyDbEncryptionSdkDynamoDbTypes.LegacyPolicy { @@ -1621,7 +1630,7 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_SearchConfig_versions_ToDafny(inp func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersionList_member_ToDafny(input awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.BeaconVersion) AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { return func() AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion { - return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(input.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(input.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(input.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(input.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(input.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(input.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(input.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(input.SignedParts)) + return AwsCryptographyDbEncryptionSdkDynamoDbTypes.Companion_BeaconVersion_.Create_BeaconVersion_(Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_version_ToDafny(input.Version), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keyStore_ToDafny(input.KeyStore), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_keySource_ToDafny(input.KeySource), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_standardBeacons_ToDafny(input.StandardBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_compoundBeacons_ToDafny(input.CompoundBeacons), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_ToDafny(input.VirtualFields), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_ToDafny(input.EncryptedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_ToDafny(input.SignedParts), Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_ToDafny(input.NumberOfBuckets)) }() } diff --git a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go index b0db0fe5e..e15100c95 100644 --- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go +++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygenerated/to_native.go @@ -408,6 +408,7 @@ func BeaconVersion_FromDafny(input interface{}) awscryptographydbencryptionsdkdy VirtualFields: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_virtualFields().UnwrapOr(nil)), EncryptedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_encryptedParts().UnwrapOr(nil)), SignedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_signedParts().UnwrapOr(nil)), + NumberOfBuckets: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_numberOfBuckets().UnwrapOr(nil)), } } @@ -1367,6 +1368,16 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_FromDaf } return fieldValue } +func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_FromDafny(input interface{}) *int32 { + return func() *int32 { + var b int32 + if input == nil { + return nil + } + b = input.(int32) + return &b + }() +} func Aws_cryptography_dbEncryptionSdk_dynamoDb_LegacyOverride_policy_FromDafny(input interface{}) awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy { return func() awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy { var u awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes.LegacyPolicy @@ -1468,6 +1479,7 @@ func Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersionList_member_FromDafn VirtualFields: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_virtualFields_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_virtualFields().UnwrapOr(nil)), EncryptedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_encryptedParts().UnwrapOr(nil)), SignedParts: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_signedParts_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_signedParts().UnwrapOr(nil)), + NumberOfBuckets: Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_numberOfBuckets_FromDafny(input.(AwsCryptographyDbEncryptionSdkDynamoDbTypes.BeaconVersion).Dtor_numberOfBuckets().UnwrapOr(nil)), } } func Aws_cryptography_dbEncryptionSdk_dynamoDb_SearchConfig_writeVersion_FromDafny(input interface{}) int32 { diff --git a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go index 42d53d241..927bddfaa 100644 --- a/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go +++ b/DynamoDbEncryption/runtimes/go/TestsFromDafny-go/awscryptographydbencryptionsdkdynamodbsmithygeneratedtypes/types.go @@ -783,6 +783,8 @@ type BeaconVersion struct { EncryptedParts []EncryptedPart + NumberOfBuckets *int32 + SignedParts []SignedPart VirtualFields []VirtualField @@ -819,6 +821,11 @@ func (input BeaconVersion) Validate() error { if input.Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_Validate() != nil { return input.Aws_cryptography_dbEncryptionSdk_dynamoDb_BeaconVersion_encryptedParts_Validate() } + if input.NumberOfBuckets != nil { + if *input.NumberOfBuckets < 1 { + return fmt.Errorf("BucketCount has a minimum of 1 but has the value of %d.", *input.NumberOfBuckets) + } + } if len(input.SignedParts) < 1 { return fmt.Errorf("SignedPartsList has a minimum length of 1 but has the length of %d.", len(input.SignedParts)) } 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 def56ee72..0a96eac82 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 @@ -180,6 +180,14 @@ public static BeaconVersion BeaconVersion( : Option.create_None( DafnySequence._typeDescriptor(SignedPart._typeDescriptor()) ); + Option numberOfBuckets; + numberOfBuckets = + Objects.nonNull(nativeValue.numberOfBuckets()) + ? Option.create_Some( + TypeDescriptor.INT, + (nativeValue.numberOfBuckets()) + ) + : Option.create_None(TypeDescriptor.INT); return new BeaconVersion( version, keyStore, @@ -188,7 +196,8 @@ public static BeaconVersion BeaconVersion( compoundBeacons, virtualFields, encryptedParts, - signedParts + signedParts, + numberOfBuckets ); } 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 c953e7bf9..abacfd21a 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 @@ -202,6 +202,11 @@ public static BeaconVersion BeaconVersion( ToNative.SignedPartsList(dafnyValue.dtor_signedParts().dtor_value()) ); } + if (dafnyValue.dtor_numberOfBuckets().is_Some()) { + nativeBuilder.numberOfBuckets( + (dafnyValue.dtor_numberOfBuckets().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 d3cc346c4..9039165e6 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 @@ -52,6 +52,11 @@ public class BeaconVersion { */ private final List signedParts; + /** + * The number of separate buckets across which beacons should be divided. + */ + private final int numberOfBuckets; + protected BeaconVersion(BuilderImpl builder) { this.version = builder.version(); this.keyStore = builder.keyStore(); @@ -61,6 +66,7 @@ protected BeaconVersion(BuilderImpl builder) { this.virtualFields = builder.virtualFields(); this.encryptedParts = builder.encryptedParts(); this.signedParts = builder.signedParts(); + this.numberOfBuckets = builder.numberOfBuckets(); } /** @@ -119,6 +125,13 @@ public List signedParts() { return this.signedParts; } + /** + * @return The number of separate buckets across which beacons should be divided. + */ + public int numberOfBuckets() { + return this.numberOfBuckets; + } + public Builder toBuilder() { return new BuilderImpl(this); } @@ -208,6 +221,16 @@ public interface Builder { */ List signedParts(); + /** + * @param numberOfBuckets The number of separate buckets across which beacons should be divided. + */ + Builder numberOfBuckets(int numberOfBuckets); + + /** + * @return The number of separate buckets across which beacons should be divided. + */ + int numberOfBuckets(); + BeaconVersion build(); } @@ -231,6 +254,10 @@ static class BuilderImpl implements Builder { protected List signedParts; + protected int numberOfBuckets; + + private boolean _numberOfBucketsSet = false; + protected BuilderImpl() {} protected BuilderImpl(BeaconVersion model) { @@ -243,6 +270,8 @@ protected BuilderImpl(BeaconVersion model) { this.virtualFields = model.virtualFields(); this.encryptedParts = model.encryptedParts(); this.signedParts = model.signedParts(); + this.numberOfBuckets = model.numberOfBuckets(); + this._numberOfBucketsSet = true; } public Builder version(int version) { @@ -318,6 +347,16 @@ public List signedParts() { return this.signedParts; } + public Builder numberOfBuckets(int numberOfBuckets) { + this.numberOfBuckets = numberOfBuckets; + this._numberOfBucketsSet = true; + return this; + } + + public int numberOfBuckets() { + return this.numberOfBuckets; + } + public BeaconVersion build() { if (!this._versionSet) { throw new IllegalArgumentException( @@ -382,6 +421,11 @@ public BeaconVersion build() { "The size of `signedParts` must be greater than or equal to 1" ); } + if (this._numberOfBucketsSet && this.numberOfBuckets() < 1) { + throw new IllegalArgumentException( + "`numberOfBuckets` must be greater than or equal to 1" + ); + } return new BeaconVersion(this); } } diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/BeaconVersion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/BeaconVersion.cs index d278e508a..b39d94f35 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/BeaconVersion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryption/BeaconVersion.cs @@ -15,6 +15,7 @@ public class BeaconVersion private System.Collections.Generic.List _virtualFields; private System.Collections.Generic.List _encryptedParts; private System.Collections.Generic.List _signedParts; + private int? _numberOfBuckets; public int Version { get { return this._version.GetValueOrDefault(); } @@ -87,6 +88,15 @@ public bool IsSetSignedParts() { return this._signedParts != null; } + public int NumberOfBuckets + { + get { return this._numberOfBuckets.GetValueOrDefault(); } + set { this._numberOfBuckets = value; } + } + public bool IsSetNumberOfBuckets() + { + return this._numberOfBuckets.HasValue; + } public void Validate() { if (!IsSetVersion()) throw new System.ArgumentException("Missing value for required property 'Version'"); @@ -125,6 +135,14 @@ public void Validate() String.Format("Member SignedParts of structure BeaconVersion has List type SignedPartsList which has a minimum length of 1 but was given a value with length {0}.", SignedParts.Count)); } } + if (IsSetNumberOfBuckets()) + { + if (NumberOfBuckets < 1) + { + throw new System.ArgumentException( + String.Format("Member NumberOfBuckets of structure BeaconVersion has type BucketCount which has a minimum of 1 but was given the value {0}.", NumberOfBuckets)); + } + } } } } diff --git a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs index da4f63a5b..dff33dc71 100644 --- a/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs +++ b/DynamoDbEncryption/runtimes/net/Generated/DynamoDbEncryptionTransforms/TypeConversion.cs @@ -5277,7 +5277,8 @@ public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconVersion FromDafny_ if (concrete._compoundBeacons.is_Some) converted.CompoundBeacons = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_compoundBeacons(concrete._compoundBeacons); if (concrete._virtualFields.is_Some) converted.VirtualFields = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M13_virtualFields(concrete._virtualFields); if (concrete._encryptedParts.is_Some) converted.EncryptedParts = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M14_encryptedParts(concrete._encryptedParts); - if (concrete._signedParts.is_Some) converted.SignedParts = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M11_signedParts(concrete._signedParts); return converted; + if (concrete._signedParts.is_Some) converted.SignedParts = (System.Collections.Generic.List)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M11_signedParts(concrete._signedParts); + if (concrete._numberOfBuckets.is_Some) converted.NumberOfBuckets = (int)FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_numberOfBuckets(concrete._numberOfBuckets); return converted; } public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._IBeaconVersion ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion(AWS.Cryptography.DbEncryptionSDK.DynamoDb.BeaconVersion value) { @@ -5286,7 +5287,8 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn System.Collections.Generic.List var_virtualFields = value.IsSetVirtualFields() ? value.VirtualFields : (System.Collections.Generic.List)null; System.Collections.Generic.List var_encryptedParts = value.IsSetEncryptedParts() ? value.EncryptedParts : (System.Collections.Generic.List)null; System.Collections.Generic.List var_signedParts = value.IsSetSignedParts() ? value.SignedParts : (System.Collections.Generic.List)null; - return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconVersion(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M7_version(value.Version), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M8_keyStore(value.KeyStore), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M9_keySource(value.KeySource), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_standardBeacons(value.StandardBeacons), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_compoundBeacons(var_compoundBeacons), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M13_virtualFields(var_virtualFields), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M14_encryptedParts(var_encryptedParts), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M11_signedParts(var_signedParts)); + int? var_numberOfBuckets = value.IsSetNumberOfBuckets() ? value.NumberOfBuckets : (int?)null; + return new software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.BeaconVersion(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M7_version(value.Version), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M8_keyStore(value.KeyStore), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M9_keySource(value.KeySource), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_standardBeacons(value.StandardBeacons), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_compoundBeacons(var_compoundBeacons), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M13_virtualFields(var_virtualFields), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M14_encryptedParts(var_encryptedParts), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M11_signedParts(var_signedParts), ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_numberOfBuckets(var_numberOfBuckets)); } public static Amazon.DynamoDBv2.BatchStatementErrorCodeEnum FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S27_BatchStatementErrorCodeEnum(software.amazon.cryptography.services.dynamodb.internaldafny.types._IBatchStatementErrorCodeEnum value) { @@ -5410,6 +5412,14 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn { return value == null ? Wrappers_Compile.Option>.create_None() : Wrappers_Compile.Option>.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_SignedPartsList((System.Collections.Generic.List)value)); } + public static int? FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_numberOfBuckets(Wrappers_Compile._IOption value) + { + return value.is_None ? (int?)null : FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S11_BucketCount(value.Extract()); + } + public static Wrappers_Compile._IOption ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S13_BeaconVersion__M15_numberOfBuckets(int? value) + { + return value == null ? Wrappers_Compile.Option.create_None() : Wrappers_Compile.Option.create_Some(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S11_BucketCount((int)value)); + } public static System.Collections.Generic.Dictionary FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S10_PutRequest__M4_Item(Dafny.IMap, software.amazon.cryptography.services.dynamodb.internaldafny.types._IAttributeValue> value) { return FromDafny_N3_com__N9_amazonaws__N8_dynamodb__S24_PutItemInputAttributeMap(value); @@ -5505,6 +5515,14 @@ public static software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafn { return Dafny.Sequence.FromArray(value.Select(ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_SignedPartsList__M6_member).ToArray()); } + public static int FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S11_BucketCount(int value) + { + return value; + } + public static int ToDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S11_BucketCount(int value) + { + return value; + } public static AWS.Cryptography.DbEncryptionSDK.DynamoDb.SingleKeyStore FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S15_BeaconKeySource__M6_single(software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ISingleKeyStore value) { return FromDafny_N3_aws__N12_cryptography__N15_dbEncryptionSdk__N8_dynamoDb__S14_SingleKeyStore(value); From da790a0d0bdbbaad47fa2db4aa21525ba9d7c8ca Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 19 Jun 2025 15:20:43 -0400 Subject: [PATCH 02/10] m --- .../Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy | 2 +- .../AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy | 2 +- ...AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy | 2 +- .../AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy index 476c7706d..b1b3836a1 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy @@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.internald import AwsCryptographyKeyStoreTypes import AwsCryptographyPrimitivesTypes import ComAmazonawsDynamodbTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy index 9e2f86575..de056cf74 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy @@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes import AwsCryptographyMaterialProvidersTypes import ComAmazonawsDynamodbTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy index e712158c7..2a2c00d7f 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/Model/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.dfy @@ -17,7 +17,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry import AwsCryptographyMaterialProvidersTypes import AwsCryptographyPrimitivesTypes import ComAmazonawsDynamodbTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types diff --git a/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy b/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy index 0ad88e609..7c14e9f87 100644 --- a/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy +++ b/DynamoDbEncryption/dafny/StructuredEncryption/Model/AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.dfy @@ -11,7 +11,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.structuredencrypti import opened UTF8 import AwsCryptographyMaterialProvidersTypes import AwsCryptographyPrimitivesTypes - // Generic helpers for verification of mock/unit tests. + // Generic helpers for verification of mock/unit tests. datatype DafnyCallEvent = DafnyCallEvent(input: I, output: O) // Begin Generated Types From c2746c5080cbc854ba9a9b3a76759b6be3c295c0 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 20 Jun 2025 13:42:37 -0400 Subject: [PATCH 03/10] m --- .../dafny/DynamoDbEncryption/src/Beacon.dfy | 98 ++++---- .../DynamoDbEncryption/src/CompoundBeacon.dfy | 66 +++--- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 5 +- .../DynamoDbEncryption/src/DDBSupport.dfy | 39 ++-- .../DynamoDbEncryption/src/FilterExpr.dfy | 36 +-- .../DynamoDbEncryption/src/SearchInfo.dfy | 69 +++--- .../dafny/DynamoDbEncryption/test/Beacon.dfy | 100 ++++---- .../DynamoDbEncryption/test/DDBSupport.dfy | 10 +- .../DynamoDbEncryption/test/FilterExpr.dfy | 214 +++++++++--------- .../src/AttributeResolver.dfy | 4 +- .../src/BatchWriteItemTransform.dfy | 6 +- .../src/DdbMiddlewareConfig.dfy | 13 ++ .../src/DynamoDbMiddlewareSupport.dfy | 28 +-- .../src/PutItemTransform.dfy | 5 +- .../src/QueryTransform.dfy | 6 +- .../src/ScanTransform.dfy | 6 +- .../src/TransactWriteItemsTransform.dfy | 5 +- 17 files changed, 375 insertions(+), 335 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy index 6d423cc91..31389b2e6 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy @@ -42,7 +42,7 @@ module BaseBeacon { //= specification/searchable-encryption/beacons.md#basichash //= type=implication //# * basicHash MUST take an [hmac key](./search-config.md#hmac-key-generation), a [beacon length](#beacon-length) and a sequence of bytes as input. - function method {:opaque} hash(val : Bytes, key : Bytes, length : BeaconLength) + function method {:opaque} hash(val : Bytes, key : Bytes, length : BeaconLength, bucket : Bytes) : (ret : Result) ensures ret.Success? ==> //= specification/searchable-encryption/beacons.md#basichash @@ -50,8 +50,8 @@ module BaseBeacon { //# * basicHash MUST produce a non-empty string as output. && |ret.value| > 0 - && getHmac(val, key).Success? - && var hash := getHmac(val, key).value; + && getHmac(val+bucket, key).Success? + && var hash := getHmac(val+bucket, key).value; //= specification/searchable-encryption/beacons.md#basichash //= type=implication @@ -64,19 +64,19 @@ module BaseBeacon { && |ret.value| == (((length as uint8) + 3) / 4) as nat { - var hash :- getHmac(val, key); + var hash :- getHmac(val + bucket, key); Success(BytesToHex(hash, length)) } // Get the standard hash for the UTF8 encoded representation of this string. - function method {:opaque} hashStr(val : string, key : Bytes, length : BeaconLength) : (res : Result) + function method {:opaque} hashStr(val : string, key : Bytes, length : BeaconLength, bucket : Bytes) : (res : Result) ensures res.Success? ==> |res.value| > 0 { var str := UTF8.Encode(val); if str.Failure? then Failure(E(str.error)) else - hash(str.value, key, length) + hash(str.value, key, length, bucket) } // calculate the HMAC for some bytes @@ -142,16 +142,16 @@ module BaseBeacon { asSet : bool, share : Option ) { - function method {:opaque} hash(val : Bytes, key : Bytes) + function method {:opaque} hash(val : Bytes, key : Bytes, bucket : Bytes) : (ret : Result) ensures ret.Success? ==> && |ret.value| > 0 - && base.hash(val, key, length).Success? - && ret.value == base.hash(val, key, length).value + && base.hash(val, key, length, bucket).Success? + && ret.value == base.hash(val, key, length, bucket).value && |ret.value| == (((length as uint8) + 3) / 4) as nat { - base.hash(val, key, length) + base.hash(val, key, length, bucket) } // return the name of the hmac key to use @@ -170,7 +170,7 @@ module BaseBeacon { //= type=implication //# * string hash MUST take a string and some [key materials](./search-config.md#get-beacon-key-materials) //# as input, and produce a string as output. - function method {:opaque} hashStr(val : string, keys : HmacKeyMap) : (res : Result) + function method {:opaque} hashStr(val : string, keys : HmacKeyMap, bucket : Bytes) : (res : Result) ensures res.Success? ==> |res.value| > 0 //= specification/searchable-encryption/beacons.md#string-hash @@ -182,18 +182,18 @@ module BaseBeacon { && keyName() in keys && UTF8.Encode(val).Success? && var str := UTF8.Encode(val).value; - && hash(str, keys[keyName()]).Success? - && res.value == hash(str, keys[keyName()]).value + && hash(str, keys[keyName()], bucket).Success? + && res.value == hash(str, keys[keyName()], bucket).value { :- Need(keyName() in keys, E("Internal Error, no key for " + keyName())); var str := UTF8.Encode(val); if str.Failure? then Failure(E(str.error)) else - hash(str.value, keys[keyName()]) + hash(str.value, keys[keyName()], bucket) } - function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes) : (ret : Result) + function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes, bucket : Bytes) : (ret : Result) ensures ret.Success? ==> ret.value.SS? ensures !value.SS? && !value.NS? && !value.BS? ==> ret.Failure? ensures ret.Success? ==> HasNoDuplicates(ret.value.SS) @@ -201,9 +201,9 @@ module BaseBeacon { reveal HasNoDuplicates(); assert HasNoDuplicates([]); var beaconSeq :- match value { - case SS(n) => BeaconizeStringSet(n, key) - case NS(n) => BeaconizeNumberSet(n, key) - case BS(n) => BeaconizeBinarySet(n, key) + case SS(n) => BeaconizeStringSet(n, key, bucket) + case NS(n) => BeaconizeNumberSet(n, key, bucket) + case BS(n) => BeaconizeBinarySet(n, key, bucket) case _ => Failure(E("Beacon " + base.name + " has style AsSet, but attribute has type " + AttrTypeToStr(value) + ".")) }; Success(DDB.AttributeValue.SS(beaconSeq)) @@ -212,22 +212,22 @@ module BaseBeacon { //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon //= type=implication //# * This operation MUST take an [hmac key](./search-config.md#hmac-key-generation), a record as input, and produce an optional [AttributeValue](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_AttributeValue.html). - function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result, Error>) + function method {:opaque} getHash(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes, bucket : Bytes) : (ret : Result, Error>) //= specification/searchable-encryption/beacons.md#value-for-a-standard-beacon //= type=implication //# * If this beacon is marked AsSet then this operation MUST return the //# [set value](#value-for-a-set-standard-beacon), //# otherwise it MUST return the [non-set value](#value-for-a-non-set-standard-beacon) - ensures asSet ==> ret == getHashSet(item, key) - ensures !asSet ==> ret == getHashNonSet(item, vf, key) + ensures asSet ==> ret == getHashSet(item, key, bucket) + ensures !asSet ==> ret == getHashNonSet(item, vf, key, bucket) { if asSet then - getHashSet(item, key) + getHashSet(item, key, bucket) else - getHashNonSet(item, vf, key) + getHashNonSet(item, vf, key, bucket) } - function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes) : (ret : Result, Error>) + function method {:opaque} getHashSet(item : DDB.AttributeMap, key : Bytes, bucket : Bytes) : (ret : Result, Error>) requires asSet ensures ret.Success? ==> //= specification/searchable-encryption/beacons.md#value-for-a-set-standard-beacon @@ -254,10 +254,10 @@ module BaseBeacon { //= 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); + var setValue :- ValueToSet(value.value, key, bucket); Success(Some(setValue)) } - function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes) : (ret : Result, Error>) + function method {:opaque} getHashNonSet(item : DDB.AttributeMap, vf : VirtualFieldMap, key : Bytes, bucket : Bytes) : (ret : Result, Error>) requires !asSet ensures ret.Success? ==> //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon @@ -276,17 +276,17 @@ module BaseBeacon { //= type=implication //# * This operation MUST convert the attribute value of the associated field to //# a sequence of bytes, as per [attribute serialization](../dynamodb-encryption-client/ddb-attribute-serialization.md). - && (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key).value)) + && (bytes.Some? ==> ret.value.Some? && hash(bytes.value, key, bucket).Success? && ret.value.value == DDB.AttributeValue.S(hash(bytes.value, key, bucket).value)) //= specification/searchable-encryption/beacons.md#value-for-a-non-set-standard-beacon //= type=implication //# * This operation MUST return the [basicHash](#basichash) of the resulting bytes and the configured [beacon length](#beacon-length). - && (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length).Success? && ret.value.value == DDB.AttributeValue.S(base.hash(bytes.value, key, length).value)) + && (bytes.Some? ==> ret.value.Some? && base.hash(bytes.value, key, length, bucket).Success? && ret.value.value == DDB.AttributeValue.S(base.hash(bytes.value, key, length, bucket).value)) { var bytes :- VirtToBytes(loc, item, vf); if bytes.None? then Success(None) else - var res :- hash(bytes.value, key); + var res :- hash(bytes.value, key, bucket); Success(Some(DDB.AttributeValue.S(res))) } @@ -303,7 +303,7 @@ module BaseBeacon { [loc[0].key] } - function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, converted : seq := []) + function method {:tailrecursion} BeaconizeStringSet(value : DDB.StringSetAttributeValue, key : Bytes, bucket : Bytes, converted : seq := []) : (ret : Result, Error>) requires HasNoDuplicates(converted) ensures ret.Success? ==> HasNoDuplicates(ret.value) @@ -312,15 +312,15 @@ module BaseBeacon { Success(converted) else var bytes :- DynamoToStruct.TopLevelAttributeToBytes(DDB.AttributeValue.S(value[0])).MapFailure(e => E(e)); - var h :- hash(bytes, key); + var h :- hash(bytes, key, bucket); if h in converted then - BeaconizeStringSet(value[1..], key, converted) + BeaconizeStringSet(value[1..], key, bucket, converted) else reveal HasNoDuplicates(); - BeaconizeStringSet(value[1..], key, converted + [h]) + BeaconizeStringSet(value[1..], key, bucket, converted + [h]) } - function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, converted : seq := []) + function method {:tailrecursion} BeaconizeNumberSet(value : DDB.NumberSetAttributeValue, key : Bytes, bucket : Bytes, converted : seq := []) : (ret : Result, Error>) requires HasNoDuplicates(converted) ensures ret.Success? ==> HasNoDuplicates(ret.value) @@ -329,15 +329,15 @@ module BaseBeacon { Success(converted) else var bytes :- DynamoToStruct.TopLevelAttributeToBytes(DDB.AttributeValue.N(value[0])).MapFailure(e => E(e)); - var h :- hash(bytes, key); + var h :- hash(bytes, key, bucket); if h in converted then - BeaconizeNumberSet(value[1..], key, converted) + BeaconizeNumberSet(value[1..], key, bucket, converted) else reveal HasNoDuplicates(); - BeaconizeNumberSet(value[1..], key, converted + [h]) + BeaconizeNumberSet(value[1..], key, bucket, converted + [h]) } - function method {:tailrecursion} BeaconizeBinarySet(value : DDB.BinarySetAttributeValue, key : Bytes, converted : seq := []) + function method {:tailrecursion} BeaconizeBinarySet(value : DDB.BinarySetAttributeValue, key : Bytes, bucket : Bytes, converted : seq := []) : (ret : Result, Error>) requires HasNoDuplicates(converted) ensures ret.Success? ==> HasNoDuplicates(ret.value) @@ -346,32 +346,32 @@ module BaseBeacon { Success(converted) else var bytes :- DynamoToStruct.TopLevelAttributeToBytes(DDB.AttributeValue.B(value[0])).MapFailure(e => E(e)); - var h :- hash(bytes, key); + var h :- hash(bytes, key, bucket); if h in converted then - BeaconizeBinarySet(value[1..], key, converted) + BeaconizeBinarySet(value[1..], key, bucket, converted) else reveal HasNoDuplicates(); - BeaconizeBinarySet(value[1..], key, converted + [h]) + BeaconizeBinarySet(value[1..], key, bucket, converted + [h]) } - function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes, forContains : bool) + function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes, forContains : bool, bucket : Bytes) : (ret : Result) { // in query, allow beaconization of terminals if asSet && !value.S? && !value.N? && !value.B? then - ValueToSet(value, key) + ValueToSet(value, key, bucket) else if forContains && (value.SS? || value.NS? || value.BS?) then - ValueToSet(value, key) + ValueToSet(value, key, bucket) else var bytes :- DynamoToStruct.TopLevelAttributeToBytes(value).MapFailure(e => E(e)); - var h :- hash(bytes, key); + var h :- hash(bytes, key, bucket); Success(DDB.AttributeValue.S(h)) } //= specification/searchable-encryption/beacons.md#getpart-for-a-standard-beacon //= type=implication //# * getPart MUST take an [hmac key](./search-config.md#hmac-key-generation), a sequence of bytes as input, and produce a string. - function method {:opaque} getPart(val : Bytes, key : Bytes) + function method {:opaque} getPart(val : Bytes, key : Bytes, bucket : Bytes) : (ret : Result) requires 0 < |val| @@ -382,10 +382,10 @@ module BaseBeacon { //= specification/searchable-encryption/beacons.md#getpart-for-a-standard-beacon //= type=implication //# * getPart MUST return the [basicHash](#basichash) of the input and the configured [beacon length](#beacon-length). - && base.hash(val, key, length).Success? - && ret.value == base.hash(val, key, length).value + && base.hash(val, key, length, bucket).Success? + && ret.value == base.hash(val, key, length, bucket).value { - base.hash(val, key, length) + base.hash(val, key, length, bucket) } predicate ValidState() {true} } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy index bb1dd0883..a41d6fef5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/CompoundBeacon.dfy @@ -294,11 +294,11 @@ module CompoundBeacon { } // calculate value for a single piece of a compound beacon query string - function method FindAndCalcPart(value : string, keys : MaybeKeyMap) : Result + function method FindAndCalcPart(value : string, keys : MaybeKeyMap, bucket : Bytes) : Result requires !keys.DontUseKeys? { var part :- partFromPrefix(parts, value); - PartValueCalc(value[|part.prefix|..], keys, part) + PartValueCalc(value[|part.prefix|..], keys, part, bucket) } // predicate : is the value simply the prefix, with no value @@ -309,7 +309,7 @@ module CompoundBeacon { } // for the given attribute value, return the beacon value - function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool) : Result + function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool, bucket : Bytes) : Result requires !keys.DontUseKeys? { if !value.S? then @@ -318,7 +318,7 @@ module CompoundBeacon { var parts := Split(value.S, split); var partsUsed :- Sequence.MapWithResult(s => getPartFromPrefix(s), parts); var _ :- ValidatePartOrder(partsUsed, value.S); - var beaconParts :- Sequence.MapWithResult(s => FindAndCalcPart(s, keys), parts); + var beaconParts :- Sequence.MapWithResult(s => FindAndCalcPart(s, keys, bucket), parts); var lastIsPrefix :- justPrefix(Seq.Last(parts)); if !forEquality && lastIsPrefix then var result := Join(beaconParts[..|parts|-1] + [Seq.Last(parts)], [split]); @@ -334,6 +334,7 @@ module CompoundBeacon { item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap, + bucket : Bytes, acc : string := "") : (ret : Result, Error>) ensures ret.Success? && ret.value.Some? ==> |ret.value.value| > 0 @@ -356,15 +357,15 @@ module CompoundBeacon { if keys.DontUseKeys? then Success(part.prefix + strValue.value) else - PartValueCalc(strValue.value, keys, part); + PartValueCalc(strValue.value, keys, part, bucket); if |acc| == 0 then - TryConstructor(consFields[1..], item, vf, keys, val) + TryConstructor(consFields[1..], item, vf, keys, bucket, val) else - TryConstructor(consFields[1..], item, vf, keys, acc + [split] + val) + TryConstructor(consFields[1..], item, vf, keys, bucket, acc + [split] + val) else if consFields[0].required then Success(None) else - TryConstructor(consFields[1..], item, vf, keys, acc) + TryConstructor(consFields[1..], item, vf, keys, bucket, acc) } // attempt each constructor in turn, until one succeeds @@ -372,7 +373,8 @@ module CompoundBeacon { construct : seq, item : DDB.AttributeMap, vf : VirtualFieldMap, - keys : MaybeKeyMap + keys : MaybeKeyMap, + bucket : Bytes ) : (ret : Result, Error>) ensures ret.Success? && ret.value.Some? ==> |ret.value.value| > 0 @@ -382,17 +384,17 @@ module CompoundBeacon { //# * If no constructor succeeds, this operation MUST return no value. Success(None) else - var x :- TryConstructor(construct[0].parts, item, vf, keys); + var x :- TryConstructor(construct[0].parts, item, vf, keys, bucket); if x.Some? then Success(x) else - TryConstructors(construct[1..], item, vf, keys) + TryConstructors(construct[1..], item, vf, keys, bucket) } //= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon //= type=implication //# * This operation MUST take a record as input, and produce an optional string. - function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) : (res : Result, Error>) + function method {:opaque} hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap, bucket : Bytes) : (res : Result, Error>) ensures res.Success? && res.value.Some? ==> //= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon //= type=implication @@ -401,17 +403,17 @@ module CompoundBeacon { //= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon //= type=implication //# * This operation MUST iterate through all constructors, in order, using the first that succeeds. - && TryConstructors(construct, item, vf, keys).Success? + && TryConstructors(construct, item, vf, keys, bucket).Success? { - TryConstructors(construct, item, vf, keys) + TryConstructors(construct, item, vf, keys, bucket) } // return the unhashed beacon value, necessary for final client-side filtering - function method {:opaque} getNaked(item : DDB.AttributeMap, vf : VirtualFieldMap) : (res : Result, Error>) + function method {:opaque} getNaked(item : DDB.AttributeMap, vf : VirtualFieldMap, bucket : Bytes) : (res : Result, Error>) ensures res.Success? && res.value.Some? ==> && |res.value.value| > 0 { - TryConstructors(construct, item, vf, DontUseKeys) + TryConstructors(construct, item, vf, DontUseKeys, bucket) } function method {:opaque} findPart(val : string) @@ -442,7 +444,7 @@ module CompoundBeacon { //= specification/searchable-encryption/beacons.md#getpart-for-a-compound-beacon //= type=implication //# * getPart MUST take a string as input and produce a string. - function method {:opaque} getPart(val : string, keys : HmacKeyMap) + function method {:opaque} getPart(val : string, keys : HmacKeyMap, bucket : Bytes) : (ret : Result) //= specification/searchable-encryption/beacons.md#getpart-for-a-compound-beacon //= type=implication @@ -456,14 +458,14 @@ module CompoundBeacon { //= type=implication //# * The string MUST be split on the `split character` into pieces. && var pieces := Split(val, split); - && calcParts(pieces, keys).Success? - && ret.value == calcParts(pieces, keys).value + && calcParts(pieces, keys, bucket).Success? + && ret.value == calcParts(pieces, keys, bucket).value { var pieces := Split(val, split); - calcParts(pieces, keys) + calcParts(pieces, keys, bucket) } - function method calcPart(piece : string, keys : HmacKeyMap) + function method calcPart(piece : string, keys : HmacKeyMap, bucket : Bytes) : (ret : Result) ensures ret.Success? ==> @@ -475,16 +477,16 @@ module CompoundBeacon { //# * The [Part Value](#part-value-calculation) MUST be calculated for each piece, //# using the prefix and length from the discovered part. && var thePart := findPart(piece).value; - && PartValueCalc(piece, Keys(keys), thePart).Success? - && ret.value == PartValueCalc(piece, Keys(keys), thePart).value + && PartValueCalc(piece, Keys(keys), thePart, bucket).Success? + && ret.value == PartValueCalc(piece, Keys(keys), thePart, bucket).value ensures findPart(piece).Failure? ==> ret.Failure? { var thePart :- findPart(piece); - PartValueCalc(piece, Keys(keys), thePart) + PartValueCalc(piece, Keys(keys), thePart, bucket) } - function method calcParts(pieces : seq, keys : HmacKeyMap, acc : string := []) + function method calcParts(pieces : seq, keys : HmacKeyMap, bucket : Bytes, acc : string := []) : (ret : Result) requires |pieces| > 0 || |acc| > 0 ensures ret.Success? ==> |ret.value| > 0 @@ -494,11 +496,11 @@ module CompoundBeacon { else //= specification/searchable-encryption/beacons.md#getpart-for-a-compound-beacon //# * The value returned MUST be these part values, joined with the `split character`. - var theBeacon :- calcPart(pieces[0], keys); + var theBeacon :- calcPart(pieces[0], keys, bucket); if |acc| == 0 then - calcParts(pieces[1..], keys, theBeacon) + calcParts(pieces[1..], keys, bucket, theBeacon) else - calcParts(pieces[1..], keys, acc + [split] + theBeacon) + calcParts(pieces[1..], keys, bucket, acc + [split] + theBeacon) } // true if neither string is a prefix of the other @@ -568,7 +570,7 @@ module CompoundBeacon { //# Part Value Calculation MUST take some [key materials](./search-config.md#get-beacon-key-materials), //# a string (the value for which the beacon is being calculated) //# and a [Part](#part) as input, and return a string as output. - function method {:opaque} PartValueCalc(data : string, keys : MaybeKeyMap, part : BeaconPart) + function method {:opaque} PartValueCalc(data : string, keys : MaybeKeyMap, part : BeaconPart, bucket : Bytes) : (ret : Result) requires !keys.DontUseKeys? @@ -592,8 +594,8 @@ module CompoundBeacon { ensures part.Encrypted? && ret.Success? ==> && 0 < |ret.value| && keys.Keys? - && part.beacon.hashStr(data, keys.value).Success? - && ret.value == part.prefix + part.beacon.hashStr(data, keys.value).value + && part.beacon.hashStr(data, keys.value, bucket).Success? + && ret.value == part.prefix + part.beacon.hashStr(data, keys.value, bucket).value //= specification/searchable-encryption/beacons.md#value-for-a-compound-beacon //= type=implication //# * This operation MUST fail if any plaintext value used in the construction contains the split character. @@ -603,7 +605,7 @@ module CompoundBeacon { match part { case Encrypted(p, b) => :- Need(keys.Keys?, E("Need KeyId for beacon " + b.base.name + " but no KeyId found in query.")); - var hash :- b.hashStr(data, keys.value); + var hash :- b.hashStr(data, keys.value, bucket); Success(part.prefix + hash) case Signed => Success(part.prefix + data) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 77ed8b645..5b765a38e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -315,12 +315,15 @@ module SearchConfigToInfo { return Failure(E("A beacon key field name of " + name + " was configured, but there's also a virtual field of that name.")); } } + var numBuckets : nat := config.numberOfBuckets.UnwrapOr(1) as nat; + :- Need(0 < numBuckets < INT32_MAX_LIMIT, E("Invalid number of buckets specified")); return I.MakeBeaconVersion( config.version as I.VersionNumber, source, beacons, virtualFields, - outer.attributeActionsOnEncrypt + outer.attributeActionsOnEncrypt, + numBuckets as uint32 ); } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy index c92befb02..bd8b98e4a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy @@ -141,14 +141,14 @@ module DynamoDBSupport { // AddBeacons examines an AttributeMap and modifies it to be appropriate for Searchable Encryption, // returning a replacement AttributeMap. - method GetEncryptedBeacons(search : Option, item : DDB.AttributeMap, keyId : MaybeKeyId) + method GetEncryptedBeacons(search : Option, item : DDB.AttributeMap, keyId : MaybeKeyId, bucket : Bytes) returns (output : Result) modifies if search.Some? then search.value.Modifies() else {} { if search.None? { return Success(map[]); } else { - output := search.value.GenerateEncryptedBeacons(item, keyId); + output := search.value.GenerateEncryptedBeacons(item, keyId, bucket); } } @@ -156,7 +156,7 @@ module DynamoDBSupport { // AddBeacons examines an AttributeMap and modifies it to be appropriate for Searchable Encryption, // returning a replacement AttributeMap. - method AddSignedBeacons(search : Option, item : DDB.AttributeMap) + method AddSignedBeacons(search : Option, item : DDB.AttributeMap, bucket : Bytes) returns (output : Result) modifies if search.Some? then search.value.Modifies() else {} @@ -172,7 +172,7 @@ module DynamoDBSupport { if search.None? { return Success(item); } else { - var newAttrs :- search.value.GenerateSignedBeacons(item); + var newAttrs :- search.value.GenerateSignedBeacons(item, bucket); //= specification/dynamodb-encryption-client/ddb-support.md#addsignedbeacons //# If the attribute NAME already exists, @@ -223,7 +223,7 @@ module DynamoDBSupport { } // Transform a QueryInput object for searchable encryption. - method QueryInputForBeacons(search : Option, actions : AttributeActions, req : DDB.QueryInput) + method QueryInputForBeacons(search : Option, actions : AttributeActions, req : DDB.QueryInput, bucket : Bytes) returns (output : Result) modifies if search.Some? then search.value.Modifies() else {} { @@ -238,7 +238,7 @@ module DynamoDBSupport { } else { var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); - var newContext :- Filter.Beaconize(search.value.curr(), oldContext, keyId); + var newContext :- Filter.Beaconize(search.value.curr(), oldContext, keyId, bucket); return Success(req.( KeyConditionExpression := newContext.keyExpr, FilterExpression := newContext.filterExpr, @@ -249,7 +249,7 @@ module DynamoDBSupport { } // Transform a QueryOutput object for searchable encryption. - method QueryOutputForBeacons(search : Option, req : DDB.QueryInput, resp : DDB.QueryOutput) + method QueryOutputForBeacons(search : Option, req : DDB.QueryInput, resp : DDB.QueryOutput, bucket : Bytes) returns (output : Result) requires resp.Items.Some? ensures output.Success? ==> output.value.Items.Some? @@ -265,7 +265,8 @@ module DynamoDBSupport { req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeNames, - req.ExpressionAttributeValues); + req.ExpressionAttributeValues, + bucket); SequenceIsSafeBecauseItIsInMemory(newItems); :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems); @@ -294,7 +295,7 @@ module DynamoDBSupport { } // Transform a ScanInput object for searchable encryption. - method ScanInputForBeacons(search : Option, actions : AttributeActions, req : DDB.ScanInput) + method ScanInputForBeacons(search : Option, actions : AttributeActions, req : DDB.ScanInput, bucket : Bytes) returns (output : Result) modifies if search.Some? then search.value.Modifies() else {} { @@ -309,7 +310,7 @@ module DynamoDBSupport { } else { var keyId :- Filter.GetBeaconKeyId(search.value.curr(), None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); var context := Filter.ExprContext(None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); - var newContext :- Filter.Beaconize(search.value.curr(), context, keyId); + var newContext :- Filter.Beaconize(search.value.curr(), context, keyId, bucket); return Success(req.( FilterExpression := newContext.filterExpr, ExpressionAttributeNames := newContext.names, @@ -319,7 +320,7 @@ module DynamoDBSupport { } // Transform a ScanOutput object for searchable encryption. - method ScanOutputForBeacons(search : Option, req : DDB.ScanInput, resp : DDB.ScanOutput) + method ScanOutputForBeacons(search : Option, req : DDB.ScanInput, resp : DDB.ScanOutput, bucket : Bytes) returns (ret : Result) requires resp.Items.Some? ensures ret.Success? ==> ret.value.Items.Some? @@ -335,7 +336,8 @@ module DynamoDBSupport { None, req.FilterExpression, req.ExpressionAttributeNames, - req.ExpressionAttributeValues); + req.ExpressionAttributeValues, + bucket); SequenceIsSafeBecauseItIsInMemory(newItems); :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), newItems); @@ -380,6 +382,7 @@ module DynamoDBSupport { fields : seq, bv : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap, + bucket : Bytes, results : map := map[]) : (output : Result, Error>) requires forall x <- fields :: x in bv.beacons @@ -392,20 +395,20 @@ module DynamoDBSupport { else var beacon := bv.beacons[fields[0 as uint32]]; if beacon.Compound? then - var optValue :- beacon.cmp.getNaked(item, bv.virtualFields); + var optValue :- beacon.cmp.getNaked(item, bv.virtualFields, bucket); if optValue.Some? then - GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results[fields[0] := optValue.value]) + GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, bucket, results[fields[0] := optValue.value]) else - GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results) + GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, bucket, results) else - GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, results) + GetCompoundBeaconsLoop(fields[1 as uint32..], bv, item, bucket, results) } - method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap) + method GetCompoundBeacons(beaconVersion : SearchableEncryptionInfo.BeaconVersion, item : DDB.AttributeMap, bucket : Bytes) returns (output : Result, Error>) { var beaconNames := SortedSets.ComputeSetToOrderedSequence2(beaconVersion.beacons.Keys, CharLess); - output := GetCompoundBeaconsLoop(beaconNames, beaconVersion, item); + output := GetCompoundBeaconsLoop(beaconNames, beaconVersion, item, bucket); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index 385935349..d5fa9e1c6 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -539,6 +539,7 @@ module DynamoDBFilterExpr { names : Option, keys : MaybeKeyMap, newValues: DDB.ExpressionAttributeValueMap, + bucket : Bytes, acc : seq := [] ) : Result @@ -557,27 +558,27 @@ module DynamoDBFilterExpr { if OpNeedsBeacon(expr, pos) then var newName := b.beacons[oldName].getBeaconName(); if isIndirectName then - BeaconizeParsedExpr(b, expr, pos+1, oldValues, Some(names.value[expr[pos].s := newName]), keys, newValues, acc + [expr[pos]]) + BeaconizeParsedExpr(b, expr, pos+1, oldValues, Some(names.value[expr[pos].s := newName]), keys, newValues, bucket, acc + [expr[pos]]) else - BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, acc + [Attr(newName, TermLocMap(newName))]) + BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, bucket, acc + [Attr(newName, TermLocMap(newName))]) else - BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, acc + [expr[pos]]) + BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, bucket, acc + [expr[pos]]) else - BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, acc + [expr[pos]]) + BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, bucket, acc + [expr[pos]]) else if expr[pos].Value? then var name := expr[pos].s; :- 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, eb.forContains); + var newValue :- if eb.beacon.None? then Success(oldValue) else eb.beacon.value.GetBeaconValue(oldValue, keys, eb.forEquality, eb.forContains, bucket); //= 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` //# are both beacons, this operation MUST fail. :- Need(name !in newValues || newValues[name] == newValue, E(name + " used in two different contexts, which is not allowed.")); - BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues[name := newValue], acc + [expr[pos]]) + BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues[name := newValue], bucket, acc + [expr[pos]]) else - BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, acc + [expr[pos]]) + BeaconizeParsedExpr(b, expr, pos+1, oldValues, names, keys, newValues, bucket, acc + [expr[pos]]) } // Convert the tokens back into an expression @@ -1517,7 +1518,8 @@ module DynamoDBFilterExpr { parsed : seq, ItemList : DDB.ItemList, names : Option, - values : DDB.ExpressionAttributeValueMap + values : DDB.ExpressionAttributeValueMap, + bucket : Bytes ) returns (output : Result) requires b.ValidState() @@ -1526,7 +1528,7 @@ module DynamoDBFilterExpr { { var acc : DDB.ItemList := []; for i := 0 to |ItemList| { - var newAttrs :- b.GeneratePlainBeacons(ItemList[i]); + var newAttrs :- b.GeneratePlainBeacons(ItemList[i], bucket); var doesMatch :- EvalExpr(parsed, ItemList[i] + newAttrs, names, values); if doesMatch { acc := acc + [ItemList[i]]; @@ -1542,7 +1544,8 @@ module DynamoDBFilterExpr { KeyExpression : Option, FilterExpression : Option, names : Option, - values: Option) + values: Option, + bucket : Bytes) returns (output : Result) requires b.ValidState() ensures b.ValidState() @@ -1554,19 +1557,19 @@ module DynamoDBFilterExpr { var afterKeys; if KeyExpression.Some? { var parsed := ParseExpr(KeyExpression.value); - var expr :- BeaconizeParsedExpr(b, parsed, 0, values.UnwrapOr(map[]), names, DontUseKeys, map[]); + var expr :- BeaconizeParsedExpr(b, parsed, 0, values.UnwrapOr(map[]), names, DontUseKeys, map[], bucket); var expr1 := ConvertToPrefix(expr.expr); var expr2 := ConvertToRpn(expr1); - afterKeys :- FilterItems(b, expr2, ItemList, expr.names, expr.values); + afterKeys :- FilterItems(b, expr2, ItemList, expr.names, expr.values, bucket); } else { afterKeys := ItemList; } if FilterExpression.Some? { var parsed := ParseExpr(FilterExpression.value); - var expr :- BeaconizeParsedExpr(b, parsed, 0, values.UnwrapOr(map[]), names, DontUseKeys, map[]); + var expr :- BeaconizeParsedExpr(b, parsed, 0, values.UnwrapOr(map[]), names, DontUseKeys, map[], bucket); var expr1 := ConvertToPrefix(expr.expr); var expr2 := ConvertToRpn(expr1); - output := FilterItems(b, expr2, afterKeys, expr.names, expr.values); + output := FilterItems(b, expr2, afterKeys, expr.names, expr.values, bucket); } else { return Success(afterKeys); } @@ -1738,6 +1741,7 @@ module DynamoDBFilterExpr { b : SI.BeaconVersion, context : ExprContext, keyId : MaybeKeyId, + bucket : Bytes, naked : bool := false ) returns (output : Result) @@ -1764,14 +1768,14 @@ module DynamoDBFilterExpr { if context.keyExpr.Some? { var parsed := ParseExpr(context.keyExpr.value); - var newContext :- BeaconizeParsedExpr(b, parsed, 0, values, newNames, keys, newValues); + var newContext :- BeaconizeParsedExpr(b, parsed, 0, values, newNames, keys, newValues, bucket); 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, values, newNames, keys, newValues); + var newContext :- BeaconizeParsedExpr(b, parsed, 0, values, newNames, keys, newValues, bucket); newFilterExpr := Some(ParsedExprToString(newContext.expr)); newValues := newContext.values; newNames := newContext.names; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index 348535a56..0ceabe403 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy @@ -518,25 +518,25 @@ module SearchableEncryptionInfo { versions[currWrite].IsVirtualField(field) } - method GeneratePlainBeacons(item : DDB.AttributeMap) returns (output : Result) + method GeneratePlainBeacons(item : DDB.AttributeMap, bucket : Bytes) returns (output : Result) requires ValidState() { - output := versions[currWrite].GeneratePlainBeacons(item); + output := versions[currWrite].GeneratePlainBeacons(item, bucket); } - method GenerateSignedBeacons(item : DDB.AttributeMap) returns (output : Result) + method GenerateSignedBeacons(item : DDB.AttributeMap, bucket : Bytes) returns (output : Result) requires ValidState() ensures ValidState() modifies Modifies() { - output := versions[currWrite].GenerateSignedBeacons(item); + output := versions[currWrite].GenerateSignedBeacons(item, bucket); } - method GenerateEncryptedBeacons(item : DDB.AttributeMap, keyId : MaybeKeyId) returns (output : Result) + method GenerateEncryptedBeacons(item : DDB.AttributeMap, keyId : MaybeKeyId, bucket : Bytes) returns (output : Result) requires ValidState() ensures ValidState() modifies Modifies() { - output := versions[currWrite].GenerateEncryptedBeacons(item, keyId); + output := versions[currWrite].GenerateEncryptedBeacons(item, keyId, bucket); } } @@ -551,7 +551,7 @@ module SearchableEncryptionInfo { else cmp.isEncrypted() } - function method hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) + function method hash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap, bucket : Bytes) : (ret : Result, Error>) requires !keys.DontUseKeys? @@ -564,33 +564,33 @@ module SearchableEncryptionInfo { if Standard? then :- Need(keys.Keys?, E("Need key for beacon " + std.keyName() + " but no keyId found in query.")); if std.keyName() in keys.value then - std.getHash(item, vf, keys.value[std.keyName()]) + std.getHash(item, vf, keys.value[std.keyName()], bucket) else Failure(E("Internal error. Beacon " + std.keyName() + " has no key!")) else - var strHash :- cmp.hash(item, vf, keys); + var strHash :- cmp.hash(item, vf, keys, bucket); if strHash.None? then Success(None) else Success(Some(DDB.AttributeValue.S(strHash.value))) } - function method naked(item : DDB.AttributeMap, vf : VirtualFieldMap) : Result, Error> + function method naked(item : DDB.AttributeMap, vf : VirtualFieldMap, bucket : Bytes) : Result, Error> { if Standard? then std.getNaked(item, vf) else - var str :- cmp.getNaked(item, vf); + var str :- cmp.getNaked(item, vf, bucket); if str.None? then Success(None) else Success(Some(DS(str.value))) } - function method attrHash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap) : Result, Error> + function method attrHash(item : DDB.AttributeMap, vf : VirtualFieldMap, keys : MaybeKeyMap, bucket : Bytes) : Result, Error> { if keys.DontUseKeys? then - naked(item, vf) + naked(item, vf, bucket) else - hash(item, vf, keys) + hash(item, vf, keys, bucket) } function method getName() : string { @@ -614,7 +614,7 @@ module SearchableEncryptionInfo { cmp.GetFields(virtualFields) } - function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool, forContains : bool) + function method GetBeaconValue(value : DDB.AttributeValue, keys : MaybeKeyMap, forEquality : bool, forContains : bool, bucket : Bytes) : Result { if keys.DontUseKeys? then @@ -623,11 +623,11 @@ 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()], forContains) + std.GetBeaconValue(value, keys[std.keyName()], forContains, bucket) else Failure(E("Internal error. Beacon " + std.keyName() + " has no key.")) else - cmp.GetBeaconValue(value, keys, forEquality) + cmp.GetBeaconValue(value, keys, forEquality, bucket) } predicate ValidState() @@ -721,18 +721,20 @@ module SearchableEncryptionInfo { keySource : KeySource, beacons : BeaconMap, virtualFields : VirtualFieldMap, - actions : AttributeActions + actions : AttributeActions, + numBuckets : uint32 ) : (ret : Result) requires version == 1 requires keySource.ValidState() + requires 0 < numBuckets { // We happen to order these values, but this ordering MUST NOT be relied upon. var beaconNames := SortedSets.ComputeSetToOrderedSequence2(beacons.Keys, CharLess); var stdKeys := Seq.Filter((k : string) => k in beacons && beacons[k].Standard?, beaconNames); FilterPreservesHasNoDuplicates((k : string) => k in beacons && beacons[k].Standard?, beaconNames); var encrypted := set k <- actions | actions[k] == SE.ENCRYPT_AND_SIGN :: k; - var bv := BeaconVersion.BeaconVersion(version, keySource, virtualFields, beacons, beaconNames, stdKeys, encrypted); + var bv := BeaconVersion.BeaconVersion(version, keySource, virtualFields, beacons, beaconNames, stdKeys, encrypted, numBuckets); assert bv.ValidState(); Success(bv) } @@ -747,7 +749,8 @@ module SearchableEncryptionInfo { // The ordering of `beaconNames` MUST NOT be relied upon. beaconNames : seq, stdNames : seq, - encryptedFields : set + encryptedFields : set, + numBuckets : uint32 ) { function Modifies() : set @@ -764,6 +767,7 @@ module SearchableEncryptionInfo { && |beaconNames| == |beacons| && (forall k <- stdNames :: k in beacons) && Seq.HasNoDuplicates(stdNames) + && 0 < numBuckets } predicate method IsBeacon(field : string) @@ -800,15 +804,15 @@ module SearchableEncryptionInfo { } // Get all beacons with plaintext values - method GeneratePlainBeacons(item : DDB.AttributeMap) + method GeneratePlainBeacons(item : DDB.AttributeMap, bucket : Bytes) returns (output : Result) requires ValidState() { - output := GenerateBeacons2(beaconNames, item, DontUseKeys, AnyBeacon); + output := GenerateBeacons2(beaconNames, item, DontUseKeys, AnyBeacon, bucket); } // Get all beacons on fields that are signed, but not encrypted - method GenerateSignedBeacons(item : DDB.AttributeMap) + method GenerateSignedBeacons(item : DDB.AttributeMap, bucket : Bytes) returns (output : Result) requires ValidState() ensures ValidState() @@ -827,11 +831,11 @@ module SearchableEncryptionInfo { //= specification/dynamodb-encryption-client/ddb-support.md#addsignedbeacons //# The value of this attribute MUST be a string, //# and must have the value defined in [beacons](../searchable-encryption/beacons.md#beacon-value). - output := GenerateBeacons2(beaconNames, item, DontUseKeys, SignedBeacon); + output := GenerateBeacons2(beaconNames, item, DontUseKeys, SignedBeacon, bucket); } // Get all beacons on encrypted fields - method GenerateEncryptedBeacons(item : DDB.AttributeMap, keyId : MaybeKeyId) + method GenerateEncryptedBeacons(item : DDB.AttributeMap, keyId : MaybeKeyId, bucket : Bytes) returns (output : Result) requires ValidState() ensures ValidState() @@ -865,13 +869,13 @@ module SearchableEncryptionInfo { //# The result of GetEncryptedBeacons MUST NOT contain any keys //# in the [Encrypt Item Output](./encrypt-item.md#output) AttributeMap. - output := GenerateBeacons2(beaconNames, item, hmacKeys, EncryptedBeacon); + output := GenerateBeacons2(beaconNames, item, hmacKeys, EncryptedBeacon, bucket); } - function method GenerateBeacon(name : string, item : DDB.AttributeMap, keys : MaybeKeyMap) : Result, Error> + function method GenerateBeacon(name : string, item : DDB.AttributeMap, keys : MaybeKeyMap, bucket : Bytes) : Result, Error> requires name in beacons { - beacons[name].attrHash(item, virtualFields, keys) + beacons[name].attrHash(item, virtualFields, keys, bucket) } function method GenerateBeacons2( @@ -879,6 +883,7 @@ module SearchableEncryptionInfo { item : DDB.AttributeMap, keys : MaybeKeyMap, bType : BeaconType, + bucket : Bytes, acc : DDB.AttributeMap := map[] ) : Result @@ -889,13 +894,13 @@ module SearchableEncryptionInfo { //= specification/searchable-encryption/beacons.md#partonly-initialization //# The Standard Beacon MUST NOT be stored in the item for a PartOnly beacon. else if IsBeaconOfType(beacons[names[0]], bType) && !IsPartOnly(beacons[names[0]]) then - var value :- GenerateBeacon(names[0], item, keys); + var value :- GenerateBeacon(names[0], item, keys, bucket); if value.Some? then - GenerateBeacons2(names[1..], item, keys, bType, acc[beacons[names[0]].getBeaconName() := value.value]) + GenerateBeacons2(names[1..], item, keys, bType, bucket, acc[beacons[names[0]].getBeaconName() := value.value]) else - GenerateBeacons2(names[1..], item, keys, bType, acc) + GenerateBeacons2(names[1..], item, keys, bType, bucket, acc) else - GenerateBeacons2(names[1..], item, keys, bType, acc) + GenerateBeacons2(names[1..], item, keys, bType, bucket, acc) } } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index e0579c635..fc43414f1 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -30,11 +30,11 @@ module TestBaseBeacon { var b := StandardBeacon(bb, 8, TermLocMap("foo"), false, false, None); var bytes :- expect bb.getHmac([1,2,3], key := [1,2]); expect bytes == [0x27, 0x93, 0x93, 0x8b, 0x26, 0xe9, 0x52, 0x7e]; - var str :- expect b.hash([1,2,3], key := [1,2]); + var str :- expect b.hash([1,2,3], key := [1,2], bucket := []); expect str == "7e"; bytes :- expect bb.getHmac([], key := [1,2]); expect bytes[7] == 0x80; - str :- expect b.hash([], key := [1,2]); + str :- expect b.hash([], key := [1,2], bucket := []); expect str == "80"; bytes :- expect bb.getHmac(x123, key := [1,2]); expect bytes[7] == 0x61; @@ -65,9 +65,9 @@ module TestBaseBeacon { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); var badItem := SimpleItem["Name" := DDB.AttributeValue.S("A.B")]; - var badAttrs := bv.GenerateEncryptedBeacons(badItem, DontUseKeyId); + var badAttrs := bv.GenerateEncryptedBeacons(badItem, DontUseKeyId, []); expect badAttrs.Failure?; expect_equal(badAttrs.error, E("Part Name for beacon Mixed has value 'A.B' which contains the split character .'.")); } @@ -98,14 +98,14 @@ module TestBaseBeacon { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); assert "std2" in SimpleItem; assert SimpleItem["std2"] == Std2String; assert Std2String == DDB.AttributeValue.N("1.23"); expect "aws_dbe_b_std2" in goodAttrs; expect goodAttrs["aws_dbe_b_std2"] == DDB.AttributeValue.S(std2_beacon); var newItem := SimpleItem["std2" := DDB.AttributeValue.N("000001.23000000")]; - var newAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var newAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect "aws_dbe_b_std2" in newAttrs; expect goodAttrs["aws_dbe_b_std2"] == newAttrs["aws_dbe_b_std2"]; } @@ -132,18 +132,18 @@ module TestBaseBeacon { var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionId)); var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); - var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect badAttrs.Failure?; // This is expected to pass because we pass a valid KeyStore var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := Some(partitionId)); var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); // This is expected to pass now because the cache already has cached material for this Branch Key ID. // This is a hack to test that the correct material is cached. - var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); } method {:test} TestSharedCacheBeaconsSingleKeyStoreWithDifferentPartitionId() @@ -168,7 +168,7 @@ module TestBaseBeacon { var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionIdBadVersion)); var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); - var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect badAttrs.Failure?; // This is expected to pass because we pass a valid KeyStore @@ -176,10 +176,10 @@ module TestBaseBeacon { var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := Some(partitionIdGoodVersion)); var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); // This is still expected to fail because the partitionId for the cached material is different. - var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect badAttrsNowCached.Failure?; } @@ -204,18 +204,18 @@ module TestBaseBeacon { var badVersion := GetLotsaBeaconsSingleWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := None); var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); - var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect badAttrs.Failure?; // This is expected to pass because we pass a valid KeyStore var version := GetLotsaBeaconsSingleWithSharedCache(cache := sharedCache, partitionId := None); var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); // This is still expected to fail because the partitionId for the cached material is different. // If the user does NOT specify the partitionId, it is set to a random UUID - var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect badAttrsNowCached.Failure?; } @@ -237,22 +237,22 @@ module TestBaseBeacon { // } assume{:axiom} false; - // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist + // // This call is expected to fail because we are providing a Bad KeyStore which does NOT exist var badVersion := GetLotsaBeaconsMultiWithSharedCacheWithBadKeyStore(cache := sharedCache, partitionId := Some(partitionId)); var badSrc :- expect C.MakeKeySource(FullTableConfig, badVersion.keyStore, badVersion.keySource, primitives); var badBv :- expect C.ConvertVersionWithSource(FullTableConfig, badVersion, badSrc); - var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); expect badAttrs.Failure?; // This is expected to pass because we pass a valid KeyStore var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := Some(partitionId)); var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); // This is expected to pass now because the cache already has cached material for this Branch Key ID. // This is a hack to test that the correct material is cached. - var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var badAttrsNowCached :- expect badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); } @@ -281,7 +281,7 @@ module TestBaseBeacon { // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable. // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy, // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource. - var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); expect badAttrs.Failure?; // This is expected to pass because we pass a valid KeyStore @@ -289,10 +289,10 @@ module TestBaseBeacon { var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := Some(partitionIdGoodVersion)); var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); // This is still expected to fail because the partitionId for the cached material is different. - var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); expect badAttrsNowCached.Failure?; } @@ -320,18 +320,18 @@ module TestBaseBeacon { // This KeyId is a valid branch_key_id present in the KeyStoreDdbTable. // Providing a valid branch_key_id is important in this method because unlike other tests in Beacon.dfy, // this is used in a test which actually fetches data from DynamoDb without using a Literal KeySource. - var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var badAttrs := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); expect badAttrs.Failure?; // This is expected to pass because we pass a valid KeyStore var version := GetLotsaBeaconsMultiWithSharedCache(cache := sharedCache, partitionId := None); var src :- expect C.MakeKeySource(FullTableConfig, version.keyStore, version.keySource, primitives); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var goodAttrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); // This is still expected to fail because the partitionId for the cached material is different. // If the user does NOT specify the partitionId, it is set to a random UUID - var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73")); + var badAttrsNowCached := badBv.GenerateEncryptedBeacons(SimpleItem, KeyId("040a32a8-3737-4f16-a3ba-bd4449556d73"), []); expect badAttrsNowCached.Failure?; } @@ -340,9 +340,9 @@ module TestBaseBeacon { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var attrs :- expect bv.GenerateSignedBeacons(SimpleItem); + var attrs :- expect bv.GenerateSignedBeacons(SimpleItem, []); expect attrs == map["JustSigned" := DDB.AttributeValue.S("Y_1984.M_May")]; - attrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + attrs :- expect bv.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect attrs == map[ "aws_dbe_b_Mixed" := DDB.AttributeValue.S("N_" + Name_beacon + ".Y_1984"), "aws_dbe_b_Name" := DDB.AttributeValue.S(Name_beacon), @@ -402,30 +402,30 @@ module TestBaseBeacon { var beaconVersion :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.Y_1984")])); - var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName")])); - newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984")])); - newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo")])); - newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar")])); - newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("T_foo.M_bar")])); - newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("N_MyName.N_MyName")])); - var badContext := Beaconize(beaconVersion, context, DontUseKeyId); + var badContext := Beaconize(beaconVersion, context, DontUseKeyId, []); expect badContext.Failure?; expect badContext.error == E("Compound Beacon value 'N_MyName.N_MyName' cannot be constructed from any available constructor for Mixed value parsed as N_N_ available constructors are N_Y_, T_[M_]."); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("Y_1984.N_MyName")])); - badContext := Beaconize(beaconVersion, context, DontUseKeyId); + badContext := Beaconize(beaconVersion, context, DontUseKeyId, []); expect badContext.Failure?; expect badContext.error == E("Compound Beacon value 'Y_1984.N_MyName' cannot be constructed from any available constructor for Mixed value parsed as Y_N_ available constructors are N_Y_, T_[M_]."); context := context.(values := Some(map[":mixed" := DDB.AttributeValue.S("M_bar.T_foo")])); - badContext := Beaconize(beaconVersion, context, DontUseKeyId); + badContext := Beaconize(beaconVersion, context, DontUseKeyId, []); expect badContext.Failure?; expect badContext.error == E("Compound Beacon value 'M_bar.T_foo' cannot be constructed from any available constructor for Mixed value parsed as M_T_ available constructors are N_Y_, T_[M_]."); } @@ -455,7 +455,7 @@ module TestBaseBeacon { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var beaconVersion :- expect C.ConvertVersionWithSource(FullTableConfig, version, src); - var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); expect newContext.values == Some(map[ ":Mixed" := DDB.AttributeValue.S("N_" + Name_beacon + ".Y_1984"), ":Name" := DDB.AttributeValue.S(Name_beacon), @@ -651,13 +651,13 @@ module TestBaseBeacon { var src := GetLiteralSource([1,2,3,4,5], newVersion); var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + 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") ]; - var goodQuery := Beaconize(bv, context, DontUseKeyId); + var goodQuery := Beaconize(bv, context, DontUseKeyId, []); expect goodQuery.Success?; @@ -670,7 +670,7 @@ module TestBaseBeacon { compoundBeacons := Some(version.compoundBeacons.value + [compoundPart]) ); bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); - goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId, []); //= specification/searchable-encryption/beacons.md#partonly-initialization //= type=test @@ -683,7 +683,7 @@ module TestBaseBeacon { //= specification/searchable-encryption/beacons.md#partonly-initialization //= type=test //# A query MUST fail if it tries to search on a PartOnly beacon directly. - var badQuery := Beaconize(bv, context, DontUseKeyId); + var badQuery := Beaconize(bv, context, DontUseKeyId, []); expect badQuery.Failure?; expect badQuery.error == E("Field partOnly is encrypted, and has a PartOnly beacon, and so can only be used as part of a compound beacon."); } @@ -706,7 +706,7 @@ module TestBaseBeacon { var src := GetLiteralSource([1,2,3,4,5], newVersion); var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); - var goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + 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") @@ -721,7 +721,7 @@ module TestBaseBeacon { standardBeacons := version.standardBeacons + [partBeacon] ); bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); - goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + goodAttrs :- expect bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId, []); //= specification/searchable-encryption/beacons.md#shared-initialization //= type=test @@ -738,7 +738,7 @@ module TestBaseBeacon { Some(map[":pVal" := DDB.AttributeValue.S("foo"), ":sVal" := DDB.AttributeValue.S("foo")]), None ); - var goodQuery :- expect Beaconize(bv, context, DontUseKeyId); + var goodQuery :- expect Beaconize(bv, context, DontUseKeyId, []); expect goodQuery.values == Some(map[":pVal" := DDB.AttributeValue.S("4379a7"), ":sVal" := DDB.AttributeValue.S("4379a7")]); } @@ -765,7 +765,7 @@ module TestBaseBeacon { var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); // also check matching beacon value in query - var goodQuery :- expect Beaconize(bv, context, DontUseKeyId); + var goodQuery :- expect Beaconize(bv, context, DontUseKeyId, []); expect goodQuery.values == Some(map[":setVal" := DDB.AttributeValue.SS(["43c4d8", "2f3278", "f1972e"])]); context := ExprContext ( @@ -774,7 +774,7 @@ module TestBaseBeacon { Some(map[":setVal" := DDB.AttributeValue.S("abc")]), None ); - goodQuery :- expect Beaconize(bv, context, DontUseKeyId); + goodQuery :- expect Beaconize(bv, context, DontUseKeyId, []); context := ExprContext ( None, @@ -782,7 +782,7 @@ module TestBaseBeacon { Some(map[":setVal" := DDB.AttributeValue.L([])]), None ); - var badQuery := Beaconize(bv, context, DontUseKeyId); + var badQuery := Beaconize(bv, context, DontUseKeyId, []); expect badQuery.Failure?; expect badQuery.error == E("Beacon setAttr has style AsSet, but attribute has type L."); } @@ -809,7 +809,7 @@ module TestBaseBeacon { var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); expect "partOnly" in bv.beacons; expect bv.beacons["partOnly"].Standard?; - var goodAttrs := bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + var goodAttrs := bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId, []); if goodAttrs.Failure? { print "\n", goodAttrs.error, "\n"; } @@ -828,7 +828,7 @@ module TestBaseBeacon { //# * Writing an item MUST fail if the item contains this beacon's attribute, //# and that attribute is not of type Set. var BadItem := MyItem["partOnly" := DDB.AttributeValue.S("abc")]; - var badAttrs := bv.GenerateEncryptedBeacons(BadItem, DontUseKeyId); + var badAttrs := bv.GenerateEncryptedBeacons(BadItem, DontUseKeyId, []); expect badAttrs.Failure?; expect badAttrs.error == E("Beacon partOnly has style AsSet, but attribute has type S."); } @@ -855,7 +855,7 @@ module TestBaseBeacon { var bv :- expect C.ConvertVersionWithSource(newConfig, newVersion, src); expect "partOnly" in bv.beacons; expect bv.beacons["partOnly"].Standard?; - var goodAttrs := bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId); + var goodAttrs := bv.GenerateEncryptedBeacons(MyItem, DontUseKeyId, []); if goodAttrs.Failure? { print "\n", goodAttrs.error, "\n"; } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy index 4cf5118cc..8be8879c3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy @@ -22,7 +22,7 @@ module TestDDBSupport { var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); var search := SI.SearchInfo([bv], 0); - var newItem :- expect AddSignedBeacons(Some(search), SimpleItem); + var newItem :- expect AddSignedBeacons(Some(search), SimpleItem, []); assert IsValid_AttributeName("aws_dbe_v_1"); assert IsValid_AttributeName("JustSigned"); var expectedNew : DDB.AttributeMap := map[ @@ -51,7 +51,7 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("TheKeyField = :value") ); - var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); // Verify Success with branch key id plus beacon expressionAttributeValues := map[ @@ -63,7 +63,7 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("TheKeyField = :value AND std2 = :other") ); - result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); // Verify Failure with beacon but no branch key id queryInput := DDB.QueryInput ( @@ -71,7 +71,7 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("std2 = :other") ); - var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); expect result2 == Failure(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.DynamoDbEncryptionException( message := "Need KeyId because of beacon std2 but no KeyId found in query")); @@ -86,6 +86,6 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("#keyfield = :value AND #beacon = :other") ); - result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); + result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy index 9ad7e9004..3d0a4632c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/FilterExpr.dfy @@ -117,7 +117,7 @@ module TestDynamoDBFilterExpr { var version := GetEmptyBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var beaconVersion :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); expect newContext == context; } @@ -144,7 +144,7 @@ module TestDynamoDBFilterExpr { expect OpNeedsBeacon(parsed, 0); expect beaconVersion.beacons[parsed[0].s].getBeaconName() == "aws_dbe_b_std2"; - var newContext :- expect BeaconizeParsedExpr(beaconVersion, parsed, 0, context.values.value, context.names, DontUseKeys, map[]); + var newContext :- expect BeaconizeParsedExpr(beaconVersion, parsed, 0, context.values.value, context.names, DontUseKeys, map[], []); var exprString := ParsedExprToString(newContext.expr); expect exprString == "aws_dbe_b_std2 = :A AND #Field_4 = :B"; } @@ -172,7 +172,7 @@ module TestDynamoDBFilterExpr { expect OpNeedsBeacon(parsed, 0); expect beaconVersion.beacons[parsed[0].s].getBeaconName() == "aws_dbe_b_std2"; - var newContext := BeaconizeParsedExpr(beaconVersion, parsed, 0, context.values.value, context.names, DontUseKeys, map[]); + var newContext := BeaconizeParsedExpr(beaconVersion, parsed, 0, context.values.value, context.names, DontUseKeys, map[], []); expect newContext.Failure?; expect newContext.error == E("Field std4 is encrypted, and cannot be searched without a beacon."); @@ -199,13 +199,13 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var beaconVersion :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId); + var newContext :- expect Beaconize(beaconVersion, context, DontUseKeyId, []); expect_equal(newContext.filterExpr, Some("aws_dbe_b_std2 = :A AND #Field4 = :B")); var newName := "aws_dbe_b_std4"; expect IsValid_AttributeName(newName); var expectedNames: DDB.ExpressionAttributeNameMap := map["#Field4" := newName]; expect_equal(newContext.names, Some(expectedNames)); - var itemBeacons :- expect beaconVersion.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId); + var itemBeacons :- expect beaconVersion.GenerateEncryptedBeacons(SimpleItem, DontUseKeyId, []); expect "aws_dbe_b_std2" in itemBeacons; expect "aws_dbe_b_std4" in itemBeacons; expect_equal(newContext.values, Some(map[":A" := itemBeacons["aws_dbe_b_std2"], ":B" := itemBeacons["aws_dbe_b_std4"]])); @@ -228,7 +228,7 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var beaconVersion :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newContext := Beaconize(beaconVersion, context, DontUseKeyId); + var newContext := Beaconize(beaconVersion, context, DontUseKeyId, []); expect newContext.Failure?; expect newContext.error == E(":A used in two different contexts, which is not allowed."); @@ -240,7 +240,7 @@ module TestDynamoDBFilterExpr { ]), None ); - newContext := Beaconize(beaconVersion, context, DontUseKeyId); + newContext := Beaconize(beaconVersion, context, DontUseKeyId, []); expect newContext.Failure?; expect newContext.error == E(":A used in two different contexts, which is not allowed."); @@ -252,7 +252,7 @@ module TestDynamoDBFilterExpr { ]), None ); - newContext := Beaconize(beaconVersion, context, DontUseKeyId); + newContext := Beaconize(beaconVersion, context, DontUseKeyId, []); expect newContext.Failure?; expect newContext.error == E(":A used in two different contexts, which is not allowed."); } @@ -277,30 +277,30 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one < two"), None, Some(values)); + var newItems :- expect FilterResults(bv, [item1], None, Some("one < two"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one > two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one > two"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("one <= two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one <= two"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one >= two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one >= two"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("one <> two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one <> two"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one = two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one = two"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("three < two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three < two"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("three > two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three > two"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("three <= two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three <= two"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("three >= two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three >= two"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("three <> two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three <> two"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("three = two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three = two"), None, None, []); expect_equal(newItems, [item1]); } @@ -314,7 +314,7 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems := FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values)); + var newItems := FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("Number needs digits either before or after the decimal point. when parsing 'foo'."); } @@ -329,30 +329,30 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values)); + var newItems :- expect FilterResults(bv, [item1], None, Some("one < :two"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("one > :two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one > :two"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("one <= :two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one <= :two"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one >= :two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one >= :two"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one <> :two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one <> :two"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("one = :two"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one = :two"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some(":two < one"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some(":two < one"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some(":two > one"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some(":two > one"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some(":two <= one"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some(":two <= one"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some(":two >= one"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some(":two >= one"), None, Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some(":two <> one"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some(":two <> one"), None, Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some(":two = one"), None, Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some(":two = one"), None, Some(values), []); expect_equal(newItems, [item1]); } @@ -365,15 +365,15 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one in (two, three)"), None, None); + var newItems :- expect FilterResults(bv, [item1], None, Some("one in (two, three)"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("two in (one, three)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two in (one, three)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("three in (two, one)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three in (two, one)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("three in (one, one, one, one, two, one, one)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three in (one, one, one, one, two, one, one)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("three in (one, one, one, one, one, one, one)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("three in (one, one, one, one, one, one, one)"), None, None, []); expect_equal(newItems, []); } @@ -386,15 +386,15 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one between two and three"), None, None); + var newItems :- expect FilterResults(bv, [item1], None, Some("one between two and three"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("two between one and three"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between one and three"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("two between three and one"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between three and one"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("two between two and three"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between two and three"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("two between one and two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between one and two"), None, None, []); expect_equal(newItems, [item1]); } @@ -407,15 +407,15 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one between two and three"), None, None); + var newItems :- expect FilterResults(bv, [item1], None, Some("one between two and three"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("two between one and three"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between one and three"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("two between three and one"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between three and one"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("two between two and three"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between two and three"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("two between one and two"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("two between one and two"), None, None, []); expect_equal(newItems, [item1]); } method {:test} TestFilterSize() { @@ -433,15 +433,15 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("size(one) = :uno"), None, values); + var newItems :- expect FilterResults(bv, [item1], None, Some("size(one) = :uno"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("size(two) between :uno and :tres"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some("size(two) between :uno and :tres"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("size(three) > :dos"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some("size(three) > :dos"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("size(two) in (:uno, :dos)"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some("size(two) in (:uno, :dos)"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("size(two) in (:uno, :tres)"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some("size(two) in (:uno, :tres)"), None, values, []); expect_equal(newItems, []); } method {:test} TestFilterContains() { @@ -456,13 +456,13 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, two)"), None, None); + var newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, two)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, three)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, three)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, four)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, four)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, five)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("contains(one, five)"), None, None, []); expect_equal(newItems, []); } @@ -478,13 +478,13 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, two)"), None, None); + var newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, two)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, three)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, three)"), None, None, []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, four)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, four)"), None, None, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, five)"), None, None); + newItems :- expect FilterResults(bv, [item1], None, Some("begins_with(one, five)"), None, None, []); expect_equal(newItems, []); } method {:test} TestFilterComplex() { @@ -502,9 +502,9 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one < :four and two < :five"), None, values); + var newItems :- expect FilterResults(bv, [item1], None, Some("one < :four and two < :five"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one < :four or two > :five"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some("one < :four or two > :five"), None, values, []); expect_equal(newItems, [item1]); } @@ -528,17 +528,17 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("one < two"), Some(names), Some(values)); + var newItems :- expect FilterResults(bv, [item1], None, Some("one < two"), Some(names), Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("one > two"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("one > two"), Some(names), Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("#eine < #zwei"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("#eine < #zwei"), Some(names), Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("#eine > #zwei"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("#eine > #zwei"), Some(names), Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [item1], None, Some("#eine < :dos"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("#eine < :dos"), Some(names), Some(values), []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some("#eine > :dos"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [item1], None, Some("#eine > :dos"), Some(names), Some(values), []); expect_equal(newItems, []); } @@ -558,13 +558,13 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.Month < :uno"), Some(names), Some(values)); + var newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.Month < :uno"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.Month > :uno"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.Month > :uno"), Some(names), Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.#zwei < :uno"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.#zwei < :uno"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.#zwei > :uno"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("Date.#zwei > :uno"), Some(names), Some(values), []); expect_equal(newItems, []); } @@ -580,21 +580,21 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_exists(Date)"), Some(names), Some(values)); + var newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_exists(Date)"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_exists(Nope)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_exists(Nope)"), Some(names), Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_not_exists(Date)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_not_exists(Date)"), Some(names), Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_not_exists(Nope)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_not_exists(Nope)"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_type(Date, :m)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_type(Date, :m)"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_type(std2, :s)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("attribute_type(std2, :s)"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("not attribute_exists(Date)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("not attribute_exists(Date)"), Some(names), Some(values), []); expect_equal(newItems, []); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("not attribute_exists(Nope)"), Some(names), Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("not attribute_exists(Nope)"), Some(names), Some(values), []); expect_equal(newItems, [SimpleItem]); } method {:test} TestFilterSizeIn() { @@ -612,13 +612,13 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [item1], None, Some("size(one) in (:uno, :dos, :tres)"), None, values); + var newItems :- expect FilterResults(bv, [item1], None, Some("size(one) in (:uno, :dos, :tres)"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some(":uno in (size(one), :dos, :tres)"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some(":uno in (size(one), :dos, :tres)"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some(":uno in (:dos, :tres, size(one))"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some(":uno in (:dos, :tres, size(one))"), None, values, []); expect_equal(newItems, [item1]); - newItems :- expect FilterResults(bv, [item1], None, Some(":uno in (:dos, :tres)"), None, values); + newItems :- expect FilterResults(bv, [item1], None, Some(":uno in (:dos, :tres)"), None, values, []); expect_equal(newItems, []); } @@ -634,16 +634,16 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems :- expect FilterResults(bv, [SimpleItem], None, Some("std2 = :val2"), None, Some(values)); + var newItems :- expect FilterResults(bv, [SimpleItem], None, Some("std2 = :val2"), None, Some(values), []); expect |newItems| == 1; expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("NameTitle = :val3"), None, Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("NameTitle = :val3"), None, Some(values), []); expect |newItems| == 1; expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("contains(NameTitle, :val4)"), None, Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("contains(NameTitle, :val4)"), None, Some(values), []); expect |newItems| == 1; expect_equal(newItems, [SimpleItem]); - newItems :- expect FilterResults(bv, [SimpleItem], None, Some("NameTitleField = :val5)"), None, Some(values)); + newItems :- expect FilterResults(bv, [SimpleItem], None, Some("NameTitleField = :val5)"), None, Some(values), []); expect |newItems| == 1; expect_equal(newItems, [SimpleItem]); } @@ -658,7 +658,7 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val3 and :val4"), None, Some(values)); + var newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val3 and :val4"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("To use BETWEEN with a compound beacon, the part after any common prefix must be LessThanComparable : BETWEEN T_ATitle AND T_MyTitle"); } @@ -672,21 +672,21 @@ module TestDynamoDBFilterExpr { var version := GetLotsaBeacons(); var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems := FilterResults(bv, [SimpleItem], None, Some("std2 = :val"), None, Some(values)); + var newItems := FilterResults(bv, [SimpleItem], None, Some("std2 = :val"), None, Some(values), []); expect newItems.Success?; - newItems := FilterResults(bv, [SimpleItem], None, Some("std2 <> :val"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("std2 <> :val"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("The operation '<>' cannot be used with a standard beacon."); - newItems := FilterResults(bv, [SimpleItem], None, Some("std2 < :val"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("std2 < :val"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("The operation '<' cannot be used with a standard beacon."); - newItems := FilterResults(bv, [SimpleItem], None, Some("std2 > :val"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("std2 > :val"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("The operation '>' cannot be used with a standard beacon."); - newItems := FilterResults(bv, [SimpleItem], None, Some("std2 <= :val"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("std2 <= :val"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("The operation '<=' cannot be used with a standard beacon."); - newItems := FilterResults(bv, [SimpleItem], None, Some("std2 >= :val"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("std2 >= :val"), None, Some(values), []); expect newItems.Failure?; expect newItems.error == E("The operation '>=' cannot be used with a standard beacon."); } @@ -706,35 +706,35 @@ module TestDynamoDBFilterExpr { var src := GetLiteralSource([1,2,3,4,5], version); var bv :- expect ConvertVersionWithSource(FullTableConfig, version, src); - var newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val1 and :val5"), None, Some(values)); + var newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val1 and :val5"), None, Some(values), []); expect newItems.Success?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val3 and :val6"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val3 and :val6"), None, Some(values), []); if newItems.Failure? { print "\n", newItems, "\n\n"; } expect newItems.Success?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val2 and :val3"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val2 and :val3"), None, Some(values), []); expect newItems.Success?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val1 and :val2"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val1 and :val2"), None, Some(values), []); expect newItems.Failure?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val1 and :val4"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle between :val1 and :val4"), None, Some(values), []); expect newItems.Failure?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle < :val1"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle < :val1"), None, Some(values), []); expect newItems.Success?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle = :val1"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle = :val1"), None, Some(values), []); expect newItems.Success?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle < :val2"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle < :val2"), None, Some(values), []); expect newItems.Failure?; - newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle = :val2"), None, Some(values)); + newItems := FilterResults(bv, [SimpleItem], None, Some("NameTitle = :val2"), None, Some(values), []); expect newItems.Success?; - var newContext :- expect Beaconize(bv, ExprContext(None, Some("NameTitle = :val1"), Some(values), None), DontUseKeyId); + var newContext :- expect Beaconize(bv, ExprContext(None, Some("NameTitle = :val1"), Some(values), None), DontUseKeyId, []); expect newContext.values.Some?; expect ":val1" in newContext.values.value; expect newContext.values.value[":val1"] == DS("N_" + EmptyName_beacon); - newContext :- expect Beaconize(bv, ExprContext(None, Some("NameTitle < :val1"), Some(values), None), DontUseKeyId); + newContext :- expect Beaconize(bv, ExprContext(None, Some("NameTitle < :val1"), Some(values), None), DontUseKeyId, []); expect newContext.values.Some?; expect ":val1" in newContext.values.value; expect newContext.values.value[":val1"] == DS("N_"); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy index 2dbaed02b..08aa5b246 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy @@ -7,6 +7,7 @@ module AttributeResolver { import opened DdbMiddlewareConfig import opened DynamoDbMiddlewareSupport import opened Wrappers + import opened StandardLibrary.UInt import DDB = ComAmazonawsDynamodbTypes import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes @@ -31,8 +32,9 @@ module AttributeResolver { ); } else { var tableConfig := config.tableEncryptionConfigs[input.TableName]; + var bucket := GetRandomBucket(tableConfig); // TODO - should this be input? var vf :- GetVirtualFields(tableConfig.search.value, input.Item, input.Version); - var cb :- GetCompoundBeacons(tableConfig.search.value, input.Item, input.Version); + var cb :- GetCompoundBeacons(tableConfig.search.value, input.Item, input.Version, bucket); return Success( ResolveAttributesOutput( VirtualFields := vf, diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index b0633c59d..b9c0f905a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -7,6 +7,7 @@ module BatchWriteItemTransform { import opened DdbMiddlewareConfig import opened DynamoDbMiddlewareSupport import opened Wrappers + import opened StandardLibrary.UInt import DDB = ComAmazonawsDynamodbTypes import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes @@ -53,12 +54,13 @@ module BatchWriteItemTransform { //# The Item MUST be [writable](ddb-support.md#writable). var _ :- IsWriteable(tableConfig, req.PutRequest.value.Item); - var item :- AddSignedBeacons(tableConfig, req.PutRequest.value.Item); + var bucket := GetRandomBucket(tableConfig); + var item :- AddSignedBeacons(tableConfig, req.PutRequest.value.Item, bucket); var encryptRes := tableConfig.itemEncryptor.EncryptItem(EncTypes.EncryptItemInput(plaintextItem:=item)); var encrypted :- MapError(encryptRes); var keyId :- GetKeyIdFromHeader(tableConfig, encrypted); - var beaconAttrs :- GetEncryptedBeacons(tableConfig, req.PutRequest.value.Item, Util.MaybeFromOptionKeyId(keyId)); + var beaconAttrs :- GetEncryptedBeacons(tableConfig, req.PutRequest.value.Item, Util.MaybeFromOptionKeyId(keyId), bucket); //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-batchwriteitem //# The PutRequest request's `Item` field MUST be replaced diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy index e841deb98..e3a54270c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy @@ -5,6 +5,7 @@ include "../Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy" module DdbMiddlewareConfig { import opened Wrappers import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes + import opened StandardLibrary.UInt import DynamoDbItemEncryptor import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes @@ -29,6 +30,18 @@ module DdbMiddlewareConfig { || config.tableEncryptionConfigs[tableName].plaintextOverride == AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ } + function method GetRandomBucket(config : TableConfig) : seq + { + if config.search.Some? then + var numBuckets : uint32 := config.search.value.versions[0].numBuckets; + if numBuckets <= 1 then + [] + else + [1] // TODO + else + [] + } + predicate ValidTableConfig?(config: TableConfig) { var encryptorConfig := config.itemEncryptor.config; && config.logicalTableName == encryptorConfig.logicalTableName diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy index 4e9e956a8..6631250ba 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy @@ -87,27 +87,27 @@ module DynamoDbMiddlewareSupport { // AddSignedBeacons examines an AttributeMap and modifies it to be appropriate for Searchable Encryption, // returning a replacement AttributeMap. - method AddSignedBeacons(config : ValidTableConfig, item : DDB.AttributeMap) + method AddSignedBeacons(config : ValidTableConfig, item : DDB.AttributeMap, bucket : seq) returns (output : Result) requires AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.ValidInternalConfig?(config.itemEncryptor.config) requires OneSearchValidState(config) ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.AddSignedBeacons(config.search, item); + var ret := BS.AddSignedBeacons(config.search, item, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // GetEncryptedBeacons examines an AttributeMap and modifies it to be appropriate for Searchable Encryption, // returning just the new items. - method GetEncryptedBeacons(config : ValidTableConfig, item : DDB.AttributeMap, keyId : Util.MaybeKeyId) + method GetEncryptedBeacons(config : ValidTableConfig, item : DDB.AttributeMap, keyId : Util.MaybeKeyId, bucket : seq) returns (output : Result) requires AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.ValidInternalConfig?(config.itemEncryptor.config) requires OneSearchValidState(config) ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.GetEncryptedBeacons(config.search, item, keyId); + var ret := BS.GetEncryptedBeacons(config.search, item, keyId, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } @@ -185,18 +185,18 @@ module DynamoDbMiddlewareSupport { } // Transform a QueryInput object for searchable encryption. - method {:opaque} QueryInputForBeacons(config : ValidTableConfig, req : DDB.QueryInput) + method {:opaque} QueryInputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, bucket : seq) returns (output : Result) requires OneSearchValidState(config) ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.QueryInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req); + var ret := BS.QueryInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // Transform a QueryOutput object for searchable encryption. - method QueryOutputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, resp : DDB.QueryOutput) + method QueryOutputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, resp : DDB.QueryOutput, bucket : seq) returns (output : Result) requires resp.Items.Some? ensures output.Success? ==> output.value.Items.Some? @@ -204,23 +204,23 @@ module DynamoDbMiddlewareSupport { ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.QueryOutputForBeacons(config.search, req, resp); + var ret := BS.QueryOutputForBeacons(config.search, req, resp, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // Transform a ScanInput object for searchable encryption. - method ScanInputForBeacons(config : ValidTableConfig, req : DDB.ScanInput) + method ScanInputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, bucket : seq) returns (output : Result) requires OneSearchValidState(config) ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.ScanInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req); + var ret := BS.ScanInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // Transform a ScanOutput object for searchable encryption. - method ScanOutputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, resp : DDB.ScanOutput) + method ScanOutputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, resp : DDB.ScanOutput, bucket : seq) returns (output : Result) requires resp.Items.Some? ensures output.Success? ==> output.value.Items.Some? @@ -228,7 +228,7 @@ module DynamoDbMiddlewareSupport { ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.ScanOutputForBeacons(config.search, req, resp); + var ret := BS.ScanOutputForBeacons(config.search, req, resp, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } @@ -242,13 +242,13 @@ module DynamoDbMiddlewareSupport { return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } - method GetCompoundBeacons(search : SearchableEncryptionInfo.ValidSearchInfo, item : DDB.AttributeMap, version : Option) + method GetCompoundBeacons(search : SearchableEncryptionInfo.ValidSearchInfo, item : DDB.AttributeMap, version : Option, bucket : seq) returns (output : Result, Error>) { if version.Some? && version.value != 1 { return Failure(E("Beacon Version Number must be '1'")); } - var ret := BS.GetCompoundBeacons(search.curr(), item); + var ret := BS.GetCompoundBeacons(search.curr(), item, bucket); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy index dca21dff9..f2dc0c34c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy @@ -58,13 +58,14 @@ module PutItemTransform { input.sdkInput.ConditionExpression, input.sdkInput.ExpressionAttributeNames, input.sdkInput.ExpressionAttributeValues); - var item :- AddSignedBeacons(tableConfig, input.sdkInput.Item); + var bucket := GetRandomBucket(tableConfig); + var item :- AddSignedBeacons(tableConfig, input.sdkInput.Item, bucket); var encryptRes := tableConfig.itemEncryptor.EncryptItem( EncTypes.EncryptItemInput(plaintextItem:=item) ); var encrypted :- MapError(encryptRes); var keyId :- GetKeyIdFromHeader(tableConfig, encrypted); - var beacons :- GetEncryptedBeacons(tableConfig, input.sdkInput.Item, Util.MaybeFromOptionKeyId(keyId)); + var beacons :- GetEncryptedBeacons(tableConfig, input.sdkInput.Item, Util.MaybeFromOptionKeyId(keyId), bucket); return Success(PutItemInputTransformOutput(transformedInput := input.sdkInput.(Item := encrypted.encryptedItem + beacons))); } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index e9d601f94..2041e1466 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -45,7 +45,8 @@ module QueryTransform { :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in Query with Encryption")); var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; - var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput); + var bucket := []; // TODO + var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput, bucket); return Success(QueryInputTransformOutput(transformedInput := finalResult)); } } @@ -105,7 +106,8 @@ module QueryTransform { //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query //# The resulting decrypted response MUST be [filtered](ddb-support.md#queryoutputforbeacons) from the result. var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems)); - var finalResult :- QueryOutputForBeacons(tableConfig, input.originalInput, decryptedOutput); + var bucket := []; // Not used + var finalResult :- QueryOutputForBeacons(tableConfig, input.originalInput, decryptedOutput, bucket); return Success(QueryOutputTransformOutput(transformedOutput := finalResult)); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index e412e5121..6860aa049 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -43,7 +43,8 @@ module ScanTransform { :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption")); var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; - var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput); + var bucket := []; // TODO + var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput, bucket); return Success(ScanInputTransformOutput(transformedInput := finalResult)); } } @@ -103,7 +104,8 @@ module ScanTransform { //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan //# The resulting decrypted response MUST be [filtered](ddb-support.md#scanoutputforbeacons) from the result. var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems)); - var finalResult :- ScanOutputForBeacons(tableConfig, input.originalInput, decryptedOutput); + var bucket := []; // Not used + var finalResult :- ScanOutputForBeacons(tableConfig, input.originalInput, decryptedOutput, bucket); return Success(ScanOutputTransformOutput(transformedOutput := finalResult)); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy index 4e6ce42b4..eed8025b4 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy @@ -89,14 +89,15 @@ module TransactWriteItemsTransform { item.Put.value.ExpressionAttributeNames, item.Put.value.ExpressionAttributeValues); - var beaconItem :- AddSignedBeacons(tableConfig, item.Put.value.Item); + var bucket := GetRandomBucket(tableConfig); + var beaconItem :- AddSignedBeacons(tableConfig, item.Put.value.Item, bucket); var encryptRes := tableConfig.itemEncryptor.EncryptItem( EncTypes.EncryptItemInput(plaintextItem:=beaconItem) ); var encrypted :- MapError(encryptRes); var keyId :- GetKeyIdFromHeader(tableConfig, encrypted); - var beaconAttrs :- GetEncryptedBeacons(tableConfig, item.Put.value.Item, Util.MaybeFromOptionKeyId(keyId)); + var beaconAttrs :- GetEncryptedBeacons(tableConfig, item.Put.value.Item, Util.MaybeFromOptionKeyId(keyId), bucket); //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-transactwriteitems //# - The PutItem request's `Item` field MUST be replaced From 7e1700837f9d84691518bf4a77b3344b250d606a Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 20 Jun 2025 16:05:23 -0400 Subject: [PATCH 04/10] m --- .../src/AttributeResolver.dfy | 2 +- .../src/BatchWriteItemTransform.dfy | 2 +- .../src/DdbMiddlewareConfig.dfy | 30 +++++++++++++------ .../src/PutItemTransform.dfy | 2 +- .../src/ScanTransform.dfy | 2 +- .../src/TransactWriteItemsTransform.dfy | 2 +- 6 files changed, 26 insertions(+), 14 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy index 08aa5b246..0f45faccd 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/AttributeResolver.dfy @@ -32,7 +32,7 @@ module AttributeResolver { ); } else { var tableConfig := config.tableEncryptionConfigs[input.TableName]; - var bucket := GetRandomBucket(tableConfig); // TODO - should this be input? + var bucket :- GetRandomBucket(tableConfig); var vf :- GetVirtualFields(tableConfig.search.value, input.Item, input.Version); var cb :- GetCompoundBeacons(tableConfig.search.value, input.Item, input.Version, bucket); return Success( diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index b9c0f905a..11d279093 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -54,7 +54,7 @@ module BatchWriteItemTransform { //# The Item MUST be [writable](ddb-support.md#writable). var _ :- IsWriteable(tableConfig, req.PutRequest.value.Item); - var bucket := GetRandomBucket(tableConfig); + var bucket :- GetRandomBucket(tableConfig); var item :- AddSignedBeacons(tableConfig, req.PutRequest.value.Item, bucket); var encryptRes := tableConfig.itemEncryptor.EncryptItem(EncTypes.EncryptItemInput(plaintextItem:=item)); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy index e3a54270c..b7196d834 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy @@ -12,6 +12,7 @@ module DdbMiddlewareConfig { import SearchableEncryptionInfo import DDB = ComAmazonawsDynamodbTypes import HexStrings + import Random datatype TableConfig = TableConfig( physicalTableName: ComAmazonawsDynamodbTypes.TableName, @@ -30,16 +31,27 @@ module DdbMiddlewareConfig { || config.tableEncryptionConfigs[tableName].plaintextOverride == AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ } - function method GetRandomBucket(config : TableConfig) : seq + method GetRandomBucket(config : TableConfig) returns (output : Result, Error>) { - if config.search.Some? then - var numBuckets : uint32 := config.search.value.versions[0].numBuckets; - if numBuckets <= 1 then - [] - else - [1] // TODO - else - [] + if config.search.None? { + return Success([]); + } + var numBuckets : uint32 := config.search.value.versions[0].numBuckets; + if numBuckets <= 1 { + return Success([]); + } + if (numBuckets > 255) { + return Failure(E("Number of buckets exceeds 255")); + } + + var randR := Random.GenerateBytes(1); + var rand : seq :- randR.MapFailure(e => E("Failed to get random byte")); + var bucket := rand[0] % (numBuckets as uint8); + if bucket == 0 { + return Success([]); + } else { + return Success([bucket as uint8]); + } } predicate ValidTableConfig?(config: TableConfig) { diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy index f2dc0c34c..3020d8666 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy @@ -58,7 +58,7 @@ module PutItemTransform { input.sdkInput.ConditionExpression, input.sdkInput.ExpressionAttributeNames, input.sdkInput.ExpressionAttributeValues); - var bucket := GetRandomBucket(tableConfig); + var bucket :- GetRandomBucket(tableConfig); var item :- AddSignedBeacons(tableConfig, input.sdkInput.Item, bucket); var encryptRes := tableConfig.itemEncryptor.EncryptItem( EncTypes.EncryptItemInput(plaintextItem:=item) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index 6860aa049..059dc981e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -43,7 +43,7 @@ module ScanTransform { :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption")); var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; - var bucket := []; // TODO + var bucket := []; // TODO var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput, bucket); return Success(ScanInputTransformOutput(transformedInput := finalResult)); } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy index eed8025b4..19655a741 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy @@ -89,7 +89,7 @@ module TransactWriteItemsTransform { item.Put.value.ExpressionAttributeNames, item.Put.value.ExpressionAttributeValues); - var bucket := GetRandomBucket(tableConfig); + var bucket :- GetRandomBucket(tableConfig); var beaconItem :- AddSignedBeacons(tableConfig, item.Put.value.Item, bucket); var encryptRes := tableConfig.itemEncryptor.EncryptItem( From ab174cbba8c2b9f49d5690a4875bf1848f6d162c Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 20 Jun 2025 16:58:32 -0400 Subject: [PATCH 05/10] m --- TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy | 2 +- TestVectors/dafny/DDBEncryption/src/TestVectors.dfy | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy index 7eaf1ebc8..c09f39a7d 100644 --- a/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy +++ b/TestVectors/dafny/DDBEncryption/src/JsonConfig.dfy @@ -571,7 +571,7 @@ module {:options "-functionSyntax:4"} JsonConfig { var src := SI.KeySource(client, store, SI.SingleLoc("foo"), cache, 100 as uint32, partitionIdBytes, logicalKeyStoreNameBytes); - var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[]); + var bv :- expect SI.MakeBeaconVersion(1, src, map[], map[], map[], 1); return Success(bv); } diff --git a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy index 580dbb3ad..373189a89 100644 --- a/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy +++ b/TestVectors/dafny/DDBEncryption/src/TestVectors.dfy @@ -151,7 +151,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors { var query := SimpleQuery(None, None, expr, []); var items1 := FullScan(client, query, Some(map[]), vals); var bv :- expect GetFakeBeaconVersion(); - var items2 :- expect Filter.FilterResults(bv, subRecords, None, expr, None, vals); + var items2 :- expect Filter.FilterResults(bv, subRecords, None, expr, None, vals, []); CompareRecordsDisordered2(items1, items2); } } From 913085989f4b1355a126f63bc3f6f907595f6f53 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Fri, 20 Jun 2025 18:40:27 -0400 Subject: [PATCH 06/10] m --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 5b765a38e..84360e9f8 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -315,8 +315,13 @@ module SearchConfigToInfo { return Failure(E("A beacon key field name of " + name + " was configured, but there's also a virtual field of that name.")); } } - var numBuckets : nat := config.numberOfBuckets.UnwrapOr(1) as nat; - :- Need(0 < numBuckets < INT32_MAX_LIMIT, E("Invalid number of buckets specified")); + + var numBuckets : int := config.numberOfBuckets.UnwrapOr(1) as int; + :- Need(0 <= numBuckets < INT32_MAX_LIMIT, E("Invalid number of buckets specified, " + Base10Int2String(numBuckets) + ", must be 0 < numberOfBuckets <= 255.")); + // Zero is invalid, but in Java we can't distinguish None from Some(0) + if numBuckets == 0 { + numBuckets := 1; + } return I.MakeBeaconVersion( config.version as I.VersionNumber, source, From bd5e532cccd8831f69a6224b0cb16ed86b4d60df Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 23 Jun 2025 10:31:24 -0400 Subject: [PATCH 07/10] m --- .../DynamoDbEncryption/src/DDBSupport.dfy | 70 ++++++++++++++++--- .../DynamoDbEncryption/src/FilterExpr.dfy | 20 +++++- .../DynamoDbEncryption/test/DDBSupport.dfy | 8 +-- .../src/DynamoDbMiddlewareSupport.dfy | 16 ++--- .../src/QueryTransform.dfy | 7 +- .../src/ScanTransform.dfy | 6 +- 6 files changed, 95 insertions(+), 32 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy index bd8b98e4a..83b7b1a9a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy @@ -23,12 +23,14 @@ module DynamoDBSupport { import opened DynamoDbEncryptionUtil import opened DdbVirtualFields import opened SearchableEncryptionInfo + import StandardLibrary.String import UTF8 import SortedSets import Seq import Update = DynamoDbUpdateExpr import Filter = DynamoDBFilterExpr import SET = AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes + import NN = DynamoDbNormalizeNumber // IsWritable examines an AttributeMap and fails if it is unsuitable for writing. // At the moment, this means that no attribute names starts with "aws_dbe_", @@ -222,8 +224,51 @@ module DynamoDBSupport { Success(DoRemoveBeacons(item)) } + // If filter expression is 'bucket=NN ...' return (..., NN) + // else return (None, 0) + function method ExtractBucketNumber(filterExpr : Option) : (Option, uint32) + { + if filterExpr.None? then + (None, 0) + else if "bucket=" < filterExpr.value then + var nFilter := filterExpr.value[7..]; + var nDigits := NN.CountDigits(nFilter); + if nDigits == 0 then + (None, 0) + else + var num := NN.StrToInt(nFilter[..nDigits]); + if num.Failure? then + (None, 0) + else if INT32_MAX_LIMIT < num.value then + (None, 0) + else + (Some(nFilter[nDigits..]), num.value as uint32) + else + (None, 0) + } + + // Extract aws_dbe_bucket = NN from filterExpr and return bucket + function method ExtractBucket(search : SearchableEncryptionInfo.BeaconVersion, filterExpr : Option) + : Result<(Option, seq), Error> + { + if search.numBuckets <= 1 then + Success((filterExpr, [])) + else + var (nFilter, bucket) := ExtractBucketNumber(filterExpr); + if nFilter.Some? then + :- Need(bucket < search.numBuckets, E("Bucket number specified in FilterExpression was " + String.Base10Int2String(bucket as int) + "but it must be less than the number of buckets " + String.Base10Int2String(search.numBuckets as int))); + :- Need(bucket < 256, E("Bucket must be less than 256")); // unreachable + if bucket == 0 then + Success((nFilter, [])) + else + Success((nFilter, [bucket as uint8])) + else + // TODO - if no encrypted beacons then OK + Failure(E("When numberOfBuckets is greater than one, FilterExpression must start with 'aws_dbe_bucket = NN && '")) + } + // Transform a QueryInput object for searchable encryption. - method QueryInputForBeacons(search : Option, actions : AttributeActions, req : DDB.QueryInput, bucket : Bytes) + method QueryInputForBeacons(search : Option, actions : AttributeActions, req : DDB.QueryInput) returns (output : Result) modifies if search.Some? then search.value.Modifies() else {} { @@ -237,7 +282,10 @@ module DynamoDBSupport { return Success(req); } else { var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); - var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); + + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); + var (newFilter, bucket) := foo; + var oldContext := Filter.ExprContext(req.KeyConditionExpression, newFilter, req.ExpressionAttributeValues, req.ExpressionAttributeNames); var newContext :- Filter.Beaconize(search.value.curr(), oldContext, keyId, bucket); return Success(req.( KeyConditionExpression := newContext.keyExpr, @@ -249,7 +297,7 @@ module DynamoDBSupport { } // Transform a QueryOutput object for searchable encryption. - method QueryOutputForBeacons(search : Option, req : DDB.QueryInput, resp : DDB.QueryOutput, bucket : Bytes) + method QueryOutputForBeacons(search : Option, req : DDB.QueryInput, resp : DDB.QueryOutput) returns (output : Result) requires resp.Items.Some? ensures output.Success? ==> output.value.Items.Some? @@ -259,11 +307,13 @@ module DynamoDBSupport { var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), resp.Items.value); return Success(resp.(Items := Some(trimmedItems))); } else { + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); + var (newFilter, bucket) := foo; var newItems :- Filter.FilterResults( search.value.curr(), resp.Items.value, req.KeyConditionExpression, - req.FilterExpression, + newFilter, req.ExpressionAttributeNames, req.ExpressionAttributeValues, bucket); @@ -295,7 +345,7 @@ module DynamoDBSupport { } // Transform a ScanInput object for searchable encryption. - method ScanInputForBeacons(search : Option, actions : AttributeActions, req : DDB.ScanInput, bucket : Bytes) + method ScanInputForBeacons(search : Option, actions : AttributeActions, req : DDB.ScanInput) returns (output : Result) modifies if search.Some? then search.value.Modifies() else {} { @@ -309,7 +359,9 @@ module DynamoDBSupport { return Success(req); } else { var keyId :- Filter.GetBeaconKeyId(search.value.curr(), None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); - var context := Filter.ExprContext(None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); + var (newFilter, bucket) := foo; + var context := Filter.ExprContext(None, newFilter, req.ExpressionAttributeValues, req.ExpressionAttributeNames); var newContext :- Filter.Beaconize(search.value.curr(), context, keyId, bucket); return Success(req.( FilterExpression := newContext.filterExpr, @@ -320,7 +372,7 @@ module DynamoDBSupport { } // Transform a ScanOutput object for searchable encryption. - method ScanOutputForBeacons(search : Option, req : DDB.ScanInput, resp : DDB.ScanOutput, bucket : Bytes) + method ScanOutputForBeacons(search : Option, req : DDB.ScanInput, resp : DDB.ScanOutput) returns (ret : Result) requires resp.Items.Some? ensures ret.Success? ==> ret.value.Items.Some? @@ -330,11 +382,13 @@ module DynamoDBSupport { var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), resp.Items.value); return Success(resp.(Items := Some(trimmedItems))); } else { + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); + var (newFilter, bucket) := foo; var newItems :- Filter.FilterResults( search.value.curr(), resp.Items.value, None, - req.FilterExpression, + newFilter, req.ExpressionAttributeNames, req.ExpressionAttributeValues, bucket); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index d5fa9e1c6..895185be5 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -1794,21 +1794,35 @@ module DynamoDBFilterExpr { } // return an error if any encrypted field exists in the query - method TestParsedExpr( + method UsesEncryptedField( expr : seq, encrypted : set, names : Option ) - returns (output : Outcome) + returns (output : Option) { for i := 0 to |expr| { if expr[i].Attr? { var name := GetAttrName(expr[i], names); if name in encrypted { - return Fail(E("Query is using encrypted field : " + name + ".")); + return Some(name); } } } + return None; + } + + method TestParsedExpr( + expr : seq, + encrypted : set, + names : Option + ) + returns (output : Outcome) + { + var hasEncField := UsesEncryptedField(expr, encrypted, names); + if hasEncField.Some? { + return Fail(E("Query is using encrypted field : " + hasEncField.value + ".")); + } return Pass; } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy index 8be8879c3..33f778f29 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/DDBSupport.dfy @@ -51,7 +51,7 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("TheKeyField = :value") ); - var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); + var result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); // Verify Success with branch key id plus beacon expressionAttributeValues := map[ @@ -63,7 +63,7 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("TheKeyField = :value AND std2 = :other") ); - result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); + result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); // Verify Failure with beacon but no branch key id queryInput := DDB.QueryInput ( @@ -71,7 +71,7 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("std2 = :other") ); - var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); + var result2 := QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); expect result2 == Failure(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.DynamoDbEncryptionException( message := "Need KeyId because of beacon std2 but no KeyId found in query")); @@ -86,6 +86,6 @@ module TestDDBSupport { ExpressionAttributeValues := Some(expressionAttributeValues), KeyConditionExpression := Some("#keyfield = :value AND #beacon = :other") ); - result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput, []); + result :- expect QueryInputForBeacons(Some(search), FullTableConfig.attributeActionsOnEncrypt, queryInput); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy index 6631250ba..470dcd84a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy @@ -185,18 +185,18 @@ module DynamoDbMiddlewareSupport { } // Transform a QueryInput object for searchable encryption. - method {:opaque} QueryInputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, bucket : seq) + method {:opaque} QueryInputForBeacons(config : ValidTableConfig, req : DDB.QueryInput) returns (output : Result) requires OneSearchValidState(config) ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.QueryInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req, bucket); + var ret := BS.QueryInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // Transform a QueryOutput object for searchable encryption. - method QueryOutputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, resp : DDB.QueryOutput, bucket : seq) + method QueryOutputForBeacons(config : ValidTableConfig, req : DDB.QueryInput, resp : DDB.QueryOutput) returns (output : Result) requires resp.Items.Some? ensures output.Success? ==> output.value.Items.Some? @@ -204,23 +204,23 @@ module DynamoDbMiddlewareSupport { ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.QueryOutputForBeacons(config.search, req, resp, bucket); + var ret := BS.QueryOutputForBeacons(config.search, req, resp); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // Transform a ScanInput object for searchable encryption. - method ScanInputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, bucket : seq) + method ScanInputForBeacons(config : ValidTableConfig, req : DDB.ScanInput) returns (output : Result) requires OneSearchValidState(config) ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.ScanInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req, bucket); + var ret := BS.ScanInputForBeacons(config.search, config.itemEncryptor.config.attributeActionsOnEncrypt, req); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } // Transform a ScanOutput object for searchable encryption. - method ScanOutputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, resp : DDB.ScanOutput, bucket : seq) + method ScanOutputForBeacons(config : ValidTableConfig, req : DDB.ScanInput, resp : DDB.ScanOutput) returns (output : Result) requires resp.Items.Some? ensures output.Success? ==> output.value.Items.Some? @@ -228,7 +228,7 @@ module DynamoDbMiddlewareSupport { ensures OneSearchValidState(config) modifies OneSearchModifies(config) { - var ret := BS.ScanOutputForBeacons(config.search, req, resp, bucket); + var ret := BS.ScanOutputForBeacons(config.search, req, resp); return ret.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDb(e)); } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index 2041e1466..e1b0434a6 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -44,9 +44,7 @@ module QueryTransform { :- Need(NoMap(input.sdkInput.QueryFilter), E("Legacy parameter 'QueryFilter' not supported in Query with Encryption")); :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in Query with Encryption")); var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; - - var bucket := []; // TODO - var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput, bucket); + var finalResult :- QueryInputForBeacons(tableConfig, input.sdkInput); return Success(QueryInputTransformOutput(transformedInput := finalResult)); } } @@ -106,8 +104,7 @@ module QueryTransform { //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query //# The resulting decrypted response MUST be [filtered](ddb-support.md#queryoutputforbeacons) from the result. var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems)); - var bucket := []; // Not used - var finalResult :- QueryOutputForBeacons(tableConfig, input.originalInput, decryptedOutput, bucket); + var finalResult :- QueryOutputForBeacons(tableConfig, input.originalInput, decryptedOutput); return Success(QueryOutputTransformOutput(transformedOutput := finalResult)); } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index 059dc981e..e412e5121 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -43,8 +43,7 @@ module ScanTransform { :- Need(input.sdkInput.ConditionalOperator.None?, E("Legacy parameter 'ConditionalOperator' not supported in UpdateItem with Encryption")); var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; - var bucket := []; // TODO - var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput, bucket); + var finalResult :- ScanInputForBeacons(tableConfig, input.sdkInput); return Success(ScanInputTransformOutput(transformedInput := finalResult)); } } @@ -104,8 +103,7 @@ module ScanTransform { //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan //# The resulting decrypted response MUST be [filtered](ddb-support.md#scanoutputforbeacons) from the result. var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems)); - var bucket := []; // Not used - var finalResult :- ScanOutputForBeacons(tableConfig, input.originalInput, decryptedOutput, bucket); + var finalResult :- ScanOutputForBeacons(tableConfig, input.originalInput, decryptedOutput); return Success(ScanOutputTransformOutput(transformedOutput := finalResult)); } } From 4ff8d8cf9170be6f9857bdaafa24241e633caa91 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 23 Jun 2025 12:10:43 -0400 Subject: [PATCH 08/10] m --- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 2 +- .../DynamoDbEncryption/src/DDBSupport.dfy | 110 ++++++++++-------- .../DynamoDbEncryption/src/FilterExpr.dfy | 9 ++ 3 files changed, 72 insertions(+), 49 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 84360e9f8..3fffb81f3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -141,7 +141,7 @@ module SearchConfigToInfo { && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN ==> output.Failure? { - // TODO-FutureCleanUp : https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1510 + // FutureCleanUp : https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1510 // It is not-good that the MPL is initialized here; // The MPL has a config object that could hold customer intent that affects behavior. // Today, it does not. But tomorrow? diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy index 83b7b1a9a..01c04539d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/DDBSupport.dfy @@ -223,48 +223,62 @@ module DynamoDBSupport { { Success(DoRemoveBeacons(item)) } + const BucketName : string := ":aws_dbe_bucket" - // If filter expression is 'bucket=NN ...' return (..., NN) - // else return (None, 0) - function method ExtractBucketNumber(filterExpr : Option) : (Option, uint32) + function method GetNumber(val : DDB.AttributeValue) : Result { - if filterExpr.None? then - (None, 0) - else if "bucket=" < filterExpr.value then - var nFilter := filterExpr.value[7..]; - var nDigits := NN.CountDigits(nFilter); - if nDigits == 0 then - (None, 0) + if val.N? then + var val :- NN.StrToInt(val.N).MapFailure(e => E(e)); + :- Need(0 <= val < INT32_MAX_LIMIT, E("Value of " + BucketName + " out of range.")); + Success(val as uint32) + else + Failure(E("Value of " + BucketName + " is not numeric (i.e. 'N')")) + } + // If names[":aws_dbe_bucket"] holds S(N)' return (Some(names - {":aws_dbe_bucket"}), Some(N)) + // else return (None, None) + function method ExtractBucketNumber(names : Option) : Result<(Option, Option), Error> + { + if names.None? then + Success((None, None)) + else if BucketName in names.value then + var val :- GetNumber(names.value[BucketName]); + if |names.value| == 1 then + Success((None, Some(val))) else - var num := NN.StrToInt(nFilter[..nDigits]); - if num.Failure? then - (None, 0) - else if INT32_MAX_LIMIT < num.value then - (None, 0) - else - (Some(nFilter[nDigits..]), num.value as uint32) + Success((Some(names.value - {BucketName}), Some(val))) else - (None, 0) + Success((None, None)) } // Extract aws_dbe_bucket = NN from filterExpr and return bucket - function method ExtractBucket(search : SearchableEncryptionInfo.BeaconVersion, filterExpr : Option) - : Result<(Option, seq), Error> + method ExtractBucket(search : SearchableEncryptionInfo.BeaconVersion, keyExpr : Option, filterExpr : Option, names : Option, values : Option, actions : AttributeActions) + returns (output : Result<(Option, seq), Error>) { - if search.numBuckets <= 1 then - Success((filterExpr, [])) - else - var (nFilter, bucket) := ExtractBucketNumber(filterExpr); - if nFilter.Some? then - :- Need(bucket < search.numBuckets, E("Bucket number specified in FilterExpression was " + String.Base10Int2String(bucket as int) + "but it must be less than the number of buckets " + String.Base10Int2String(search.numBuckets as int))); - :- Need(bucket < 256, E("Bucket must be less than 256")); // unreachable - if bucket == 0 then - Success((nFilter, [])) - else - Success((nFilter, [bucket as uint8])) - else - // TODO - if no encrypted beacons then OK - Failure(E("When numberOfBuckets is greater than one, FilterExpression must start with 'aws_dbe_bucket = NN && '")) + if search.numBuckets <= 1 { + return Success((values, [])); + } + + var foo :- ExtractBucketNumber(values); + var (nValues, bucket) := foo; + if bucket.Some? { + :- Need(bucket.value < search.numBuckets, E("Bucket number specified in FilterExpression was " + String.Base10Int2String(bucket.value as int) + "but it must be less than the number of buckets " + String.Base10Int2String(search.numBuckets as int))); + :- Need(bucket.value < 256, E("Bucket must be less than 256")); // unreachable + var nbucket := (bucket.value as nat) as uint8; + if nbucket == 0 { + return Success((nValues, [])); + } else { + return Success((nValues, [nbucket])); + } + } + // No bucket specified is OK if no encrypted fields are searched + var encrypted := set k <- actions | actions[k] == SE.ENCRYPT_AND_SIGN :: k; + var filterHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(filterExpr), encrypted, names); + var keyHasEncField := Filter.UsesEncryptedField(Filter.ParseExprOpt(keyExpr), encrypted, names); + if keyHasEncField.Some? || filterHasEncField.Some? { + return Failure(E("When numberOfBuckets is greater than one, FilterExpression must start with 'aws_dbe_bucket = NN && '")); + } else { + return Success((values, [])); + } } // Transform a QueryInput object for searchable encryption. @@ -283,9 +297,9 @@ module DynamoDBSupport { } else { var keyId :- Filter.GetBeaconKeyId(search.value.curr(), req.KeyConditionExpression, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); - var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); - var (newFilter, bucket) := foo; - var oldContext := Filter.ExprContext(req.KeyConditionExpression, newFilter, req.ExpressionAttributeValues, req.ExpressionAttributeNames); + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, req.KeyConditionExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions); + var (newValues, bucket) := foo; + var oldContext := Filter.ExprContext(req.KeyConditionExpression, req.FilterExpression, newValues, req.ExpressionAttributeNames); var newContext :- Filter.Beaconize(search.value.curr(), oldContext, keyId, bucket); return Success(req.( KeyConditionExpression := newContext.keyExpr, @@ -307,15 +321,15 @@ module DynamoDBSupport { var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), resp.Items.value); return Success(resp.(Items := Some(trimmedItems))); } else { - var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); - var (newFilter, bucket) := foo; + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, req.KeyConditionExpression, req.ExpressionAttributeNames, req.ExpressionAttributeValues, map[]); + var (newValues, bucket) := foo; var newItems :- Filter.FilterResults( search.value.curr(), resp.Items.value, req.KeyConditionExpression, - newFilter, + req.FilterExpression, req.ExpressionAttributeNames, - req.ExpressionAttributeValues, + newValues, bucket); SequenceIsSafeBecauseItIsInMemory(newItems); :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); @@ -359,9 +373,9 @@ module DynamoDBSupport { return Success(req); } else { var keyId :- Filter.GetBeaconKeyId(search.value.curr(), None, req.FilterExpression, req.ExpressionAttributeValues, req.ExpressionAttributeNames); - var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); - var (newFilter, bucket) := foo; - var context := Filter.ExprContext(None, newFilter, req.ExpressionAttributeValues, req.ExpressionAttributeNames); + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, None, req.ExpressionAttributeNames, req.ExpressionAttributeValues, actions); + var (newValues, bucket) := foo; + var context := Filter.ExprContext(None, req.FilterExpression, newValues, req.ExpressionAttributeNames); var newContext :- Filter.Beaconize(search.value.curr(), context, keyId, bucket); return Success(req.( FilterExpression := newContext.filterExpr, @@ -382,15 +396,15 @@ module DynamoDBSupport { var trimmedItems := Seq.Map(i => DoRemoveBeacons(i), resp.Items.value); return Success(resp.(Items := Some(trimmedItems))); } else { - var foo :- ExtractBucket(search.value.curr(), req.FilterExpression); - var (newFilter, bucket) := foo; + var foo :- ExtractBucket(search.value.curr(), req.FilterExpression, None, req.ExpressionAttributeNames, req.ExpressionAttributeValues, map[]); + var (newValues, bucket) := foo; var newItems :- Filter.FilterResults( search.value.curr(), resp.Items.value, None, - newFilter, + req.FilterExpression, req.ExpressionAttributeNames, - req.ExpressionAttributeValues, + newValues, bucket); SequenceIsSafeBecauseItIsInMemory(newItems); :- Need(|newItems| as uint64 < INT32_MAX_LIMIT as uint64, DynamoDbEncryptionUtil.E("This is impossible.")); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy index 895185be5..d664a7bf3 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/FilterExpr.dfy @@ -677,6 +677,15 @@ module DynamoDBFilterExpr { if 0 < tup.0 then [tup.1] + ParseExpr(s, Add(pos, tup.0)) else [] } + function method {:tailrecursion} ParseExprOpt(s: Option) : (res: seq) + ensures s.None? || s.value == [] ==> res == [] + { + if s.None? then + [] + else + ParseExpr(s.value) + } + // convert ch to lower case function method ByteLower(ch: uint8): uint8 { From c3ae7ca19cc43e3e7fa3fed26c1133849d5f701b Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 23 Jun 2025 13:04:22 -0400 Subject: [PATCH 09/10] m --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c1806faab..7bede0e44 100644 --- a/Makefile +++ b/Makefile @@ -51,7 +51,7 @@ format_java_misc-check: setup_prettier npx prettier --plugin=prettier-plugin-java . --check setup_prettier: - npm i --no-save prettier@3 prettier-plugin-java@2.5 + npm i --no-save prettier@3.5.3 prettier-plugin-java@2.5 # Generate the top-level project.properties file using smithy-dafny. # This is for the benefit of the nightly Dafny CI, From fc77cebd4f92152a3a925ea12c272f73093662b6 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 1 Jul 2025 15:21:03 -0400 Subject: [PATCH 10/10] m --- .../dafny/DynamoDbEncryption/test/Beacon.dfy | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy index fc43414f1..31bb4b884 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/test/Beacon.dfy @@ -32,6 +32,10 @@ module TestBaseBeacon { expect bytes == [0x27, 0x93, 0x93, 0x8b, 0x26, 0xe9, 0x52, 0x7e]; var str :- expect b.hash([1,2,3], key := [1,2], bucket := []); expect str == "7e"; + str :- expect b.hash([1,2,3], key := [1,2], bucket := [1]); + expect str == "1d"; + str :- expect b.hash([1,2,3], key := [1,2], bucket := [2]); + expect str == "ef"; bytes :- expect bb.getHmac([], key := [1,2]); expect bytes[7] == 0x80; str :- expect b.hash([], key := [1,2], bucket := []); @@ -365,7 +369,7 @@ module TestBaseBeacon { ]; } - method GetBeaconValue(name : string, key : Bytes, value : string, length : BeaconLength) returns (output : string) + method GetBeaconValue(name : string, key : Bytes, value : string, length : BeaconLength, bucket : Bytes := []) returns (output : string) { var info :- expect UTF8.Encode("AWS_DBE_SCAN_BEACON" + name); var client :- expect Primitives.AtomicPrimitives(); @@ -379,6 +383,7 @@ module TestBaseBeacon { )); var data :- expect UTF8.Encode(value); + data := data + bucket; var input := Prim.HMacInput ( digestAlgorithm := Prim.SHA_384, key := key,