From 8f3139bebb7b37b4c868a120a512f172cb2b0f2e Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Jul 2024 14:16:07 -0400 Subject: [PATCH 1/5] chore: respect FORCE_PLAINTEXT_WRITE when using multitenant and search config --- .../src/BatchWriteItemTransform.dfy | 2 +- .../src/DdbMiddlewareConfig.dfy | 10 +++++++++- .../dafny/DynamoDbEncryptionTransforms/src/Index.dfy | 3 ++- .../src/PutItemTransform.dfy | 4 ++-- .../src/TransactWriteItemsTransform.dfy | 2 +- 5 files changed, 15 insertions(+), 6 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index 2f1690510..482a222c1 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -32,7 +32,7 @@ module BatchWriteItemTransform { //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-batchwriteitem //# If the table name does not refer to an [encrypted-table](#encrypted-table), //# the list of operations MUST be unchanged. - if tableName in config.tableEncryptionConfigs { + if !IsPlainWrite(config, tableName) { var tableConfig := config.tableEncryptionConfigs[tableName]; var encryptedItems : seq := []; for x := 0 to |writeRequests| diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy index f74e9f29b..8f49557fb 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy @@ -16,9 +16,17 @@ module DdbMiddlewareConfig { partitionKeyName: string, sortKeyName: Option, itemEncryptor: DynamoDbItemEncryptor.DynamoDbItemEncryptorClient, - search : Option + search : Option, + plaintextOverride: AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride ) + // return true if records written to the table should NOT be encrypted or otherwise modified + predicate method IsPlainWrite(config : Config, tableName : string) + { + || tableName !in config.tableEncryptionConfigs + || config.tableEncryptionConfigs[tableName].plaintextOverride == AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ + } + predicate ValidTableConfig?(config: TableConfig) { var encryptorConfig := config.itemEncryptor.config; && config.logicalTableName == encryptorConfig.logicalTableName diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy index 44feaad03..bf08e3e59 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy @@ -199,7 +199,8 @@ module partitionKeyName := inputConfig.partitionKeyName, sortKeyName := inputConfig.sortKeyName, itemEncryptor := itemEncryptor, - search := search + search := search, + plaintextOverride := inputConfig.plaintextOverride.UnwrapOr(AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ) ); internalConfigs := internalConfigs[tableName := internalConfig]; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy index 9a1086170..376c92d95 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy @@ -26,7 +26,7 @@ module PutItemTransform { ensures output.Success? && input.sdkInput.TableName !in config.tableEncryptionConfigs ==> output.value.transformedInput == input.sdkInput - ensures output.Success? && input.sdkInput.TableName in config.tableEncryptionConfigs ==> + ensures output.Success? && !IsPlainWrite(config, input.sdkInput.TableName) ==> && var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-putitem //= type=implication @@ -55,7 +55,7 @@ module PutItemTransform { input.sdkInput.ExpressionAttributeValues).Success? { - if input.sdkInput.TableName !in config.tableEncryptionConfigs { + if IsPlainWrite(config, input.sdkInput.TableName) { return Success(PutItemInputTransformOutput(transformedInput := input.sdkInput)); } var tableConfig := config.tableEncryptionConfigs[input.sdkInput.TableName]; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy index fc559c68c..4e6ce42b4 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/TransactWriteItemsTransform.dfy @@ -75,7 +75,7 @@ module TransactWriteItemsTransform { item.Update.value.ExpressionAttributeValues); } - if item.Put.Some? && item.Put.value.TableName in config.tableEncryptionConfigs { + if item.Put.Some? && !IsPlainWrite(config, item.Put.value.TableName) { var tableConfig := config.tableEncryptionConfigs[item.Put.value.TableName]; //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#encrypt-before-transactwriteitems From e5687d0787d55b0d03fd5edcd0e24d13f0560b09 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Jul 2024 15:44:34 -0400 Subject: [PATCH 2/5] test --- .../test/PutItemTransform.dfy | 84 +++++++++++++++++++ .../test/TestFixtures.dfy | 60 ++++++++++++- 2 files changed, 141 insertions(+), 3 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index ebbf62e37..584ab4e9a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -9,6 +9,7 @@ module PutItemTransformTest { import opened TestFixtures import DDB = ComAmazonawsDynamodbTypes import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes + import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes method {:test} TestPutItemInputPassthrough() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); @@ -35,6 +36,89 @@ module PutItemTransformTest { expect_equal("PutItemInput", transformed.value.transformedInput, input); } + // DynamoDB String :: cast string to DDB.AttributeValue.S + function method DS(x : string) : DDB.AttributeValue + { + DDB.AttributeValue.S(x) + } + function method BasicItem() : DDB.AttributeMap + { + map[ + "bar" := DS("baz") + ] + } + method {:test} TestPutItemInputMultiNone() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(None); + var tableName := GetTableName("foo"); + var input := DDB.PutItemInput( + TableName := tableName, + Item := BasicItem() + ); + var transformed := middlewareUnderTest.PutItemInputTransform( + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( + sdkInput := input + ) + ); + expect transformed.Failure?; + expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( + message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); + } + + method {:test} TestPutItemInputMultiForbidForbid() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli( + Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ) + ); + var tableName := GetTableName("foo"); + var input := DDB.PutItemInput( + TableName := tableName, + Item := BasicItem() + ); + var transformed := middlewareUnderTest.PutItemInputTransform( + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( + sdkInput := input + ) + ); + expect transformed.Failure?; + expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( + message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); + } + + method {:test} TestPutItemInputMultiForbidAllow() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli( + Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ) + ); + var tableName := GetTableName("foo"); + var input := DDB.PutItemInput( + TableName := tableName, + Item := BasicItem() + ); + var transformed := middlewareUnderTest.PutItemInputTransform( + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( + sdkInput := input + ) + ); + expect transformed.Failure?; + expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( + message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); + } + + method {:test} TestPutItemInputMultiForceAllow() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli( + Some(PlaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ) + ); + var tableName := GetTableName("foo"); + var input := DDB.PutItemInput( + TableName := tableName, + Item := BasicItem() + ); + var transformed := middlewareUnderTest.PutItemInputTransform( + AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( + sdkInput := input + ) + ); + expect transformed.Success?; + } + method {:test} TestPutItemOutputPassthrough() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); var output := DDB.PutItemOutput( diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index 8ae5ea78a..204a33d93 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -1,6 +1,7 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 include "../src/Index.dfy" +include "../../DynamoDbEncryption/test/BeaconTestFixtures.dfy" module TestFixtures { import opened Wrappers @@ -9,6 +10,7 @@ module TestFixtures { import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import opened AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes + import opened BeaconTestFixtures import DynamoDbEncryptionTransforms import DynamoDbItemEncryptor import AwsCryptographyMaterialProvidersTypes @@ -216,7 +218,7 @@ module TestFixtures { ensures fresh(encryption.Modifies) { var keyring := GetKmsKeyring(); - var encryption2 : IDynamoDbEncryptionTransformsClient :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( + encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( DynamoDbTablesEncryptionConfig( tableEncryptionConfigs := map[ "foo" := DynamoDbTableEncryptionConfig( @@ -241,8 +243,60 @@ module TestFixtures { ] ) ); - assert encryption2 is DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient; - encryption := encryption2 as DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient; assume {:axiom} fresh(encryption.Modifies); } + + // type AttributeActions = map + + function method GetMultiActions() : AttributeActions + { + map[ + "bar" := SE.SIGN_ONLY, + "std2" := SE.ENCRYPT_AND_SIGN, + "std4" := SE.ENCRYPT_AND_SIGN, + "std6" := SE.ENCRYPT_AND_SIGN, + "Name" := SE.ENCRYPT_AND_SIGN, + "Title" := SE.ENCRYPT_AND_SIGN, + "TooBad" := SE.ENCRYPT_AND_SIGN, + "Year" := SE.SIGN_ONLY, + "Date" := SE.SIGN_ONLY, + "TheKeyField" := SE.SIGN_ONLY + ] + } + + method GetDynamoDbEncryptionTransformsMutli(plaintextOverride : Option) + returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient) + ensures encryption.ValidState() + ensures fresh(encryption) + ensures fresh(encryption.Modifies) + { + var keyring := GetKmsKeyring(); + var beacons := GetLotsaBeaconsMulti(); + var search := SearchConfig ( + versions := [beacons], + writeVersion := 1 + ); + encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( + DynamoDbTablesEncryptionConfig( + tableEncryptionConfigs := map[ + "foo" := DynamoDbTableEncryptionConfig( + logicalTableName := "foo", + partitionKeyName := "bar", + sortKeyName := None(), + attributeActionsOnEncrypt := GetMultiActions(), + allowedUnsignedAttributes := Some(["plain"]), + allowedUnsignedAttributePrefix := None(), + algorithmSuiteId := None(), + keyring := Some(keyring), + cmm := None(), + search := Some(search), + legacyOverride := None, + plaintextOverride := plaintextOverride + ) + ] + ) + ); + assume {:axiom} fresh(encryption.Modifies); + } + } From 2d23f1acb672bcb720d33b38594d8bb9442e22ee Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Jul 2024 16:15:13 -0400 Subject: [PATCH 3/5] test --- .../test/PutItemTransform.dfy | 45 +++---------------- 1 file changed, 7 insertions(+), 38 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index 584ab4e9a..3185044e4 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -47,27 +47,9 @@ module PutItemTransformTest { "bar" := DS("baz") ] } - method {:test} TestPutItemInputMultiNone() { - var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(None); - var tableName := GetTableName("foo"); - var input := DDB.PutItemInput( - TableName := tableName, - Item := BasicItem() - ); - var transformed := middlewareUnderTest.PutItemInputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( - sdkInput := input - ) - ); - expect transformed.Failure?; - expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( - message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); - } - method {:test} TestPutItemInputMultiForbidForbid() { - var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli( - Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ) - ); + method {:test} TestPutItemInputMultiFail(plaintextOverride : Option) { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(plaintextOverride); var tableName := GetTableName("foo"); var input := DDB.PutItemInput( TableName := tableName, @@ -81,25 +63,12 @@ module PutItemTransformTest { expect transformed.Failure?; expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); - } - method {:test} TestPutItemInputMultiForbidAllow() { - var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli( - Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ) - ); - var tableName := GetTableName("foo"); - var input := DDB.PutItemInput( - TableName := tableName, - Item := BasicItem() - ); - var transformed := middlewareUnderTest.PutItemInputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( - sdkInput := input - ) - ); - expect transformed.Failure?; - expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( - message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); + } + method {:test} TestPutItemInputMulti() { + TestPutItemInputMultiFail(None); + TestPutItemInputMultiFail(Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ)); + TestPutItemInputMultiFail(Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ)); } method {:test} TestPutItemInputMultiForceAllow() { From 2d9a689ac81c298418a05b63149dab0dac394ce4 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Jul 2024 16:24:33 -0400 Subject: [PATCH 4/5] test --- .../DynamoDbEncryptionTransforms/test/PutItemTransform.dfy | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index 3185044e4..c977d6e1d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -41,6 +41,7 @@ module PutItemTransformTest { { DDB.AttributeValue.S(x) } + function method BasicItem() : DDB.AttributeMap { map[ @@ -48,7 +49,7 @@ module PutItemTransformTest { ] } - method {:test} TestPutItemInputMultiFail(plaintextOverride : Option) { + method TestPutItemInputMultiFail(plaintextOverride : Option) { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(plaintextOverride); var tableName := GetTableName("foo"); var input := DDB.PutItemInput( @@ -63,8 +64,8 @@ module PutItemTransformTest { expect transformed.Failure?; expect transformed.error == AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.DynamoDbEncryptionTransformsException( message := "In multi-tenant mode, keyProviderId must be aws-kms-hierarchy"); - } + method {:test} TestPutItemInputMulti() { TestPutItemInputMultiFail(None); TestPutItemInputMultiFail(Some(PlaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ)); From 200c3d6b2beb7d5521ff6464b76e479883e519c6 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Mon, 29 Jul 2024 17:14:30 -0400 Subject: [PATCH 5/5] m --- .../test/PutItemTransform.dfy | 37 +++---------------- .../test/TestFixtures.dfy | 27 +++----------- 2 files changed, 10 insertions(+), 54 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index c977d6e1d..dd2ddbb07 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -16,15 +16,7 @@ module PutItemTransformTest { var tableName := GetTableName("no_such_table"); var input := DDB.PutItemInput( TableName := tableName, - Item := map[], - Expected := None(), - ReturnValues := None(), - ReturnConsumedCapacity := None(), - ReturnItemCollectionMetrics := None(), - ConditionalOperator := None(), - ConditionExpression := None(), - ExpressionAttributeNames := None(), - ExpressionAttributeValues := None() + Item := map[] ); var transformed := middlewareUnderTest.PutItemInputTransform( AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( @@ -36,25 +28,14 @@ module PutItemTransformTest { expect_equal("PutItemInput", transformed.value.transformedInput, input); } - // DynamoDB String :: cast string to DDB.AttributeValue.S - function method DS(x : string) : DDB.AttributeValue - { - DDB.AttributeValue.S(x) - } - - function method BasicItem() : DDB.AttributeMap - { - map[ - "bar" := DS("baz") - ] - } + const BasicItem : DDB.AttributeMap := map["bar" := DDB.AttributeValue.S("baz")] method TestPutItemInputMultiFail(plaintextOverride : Option) { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransformsMutli(plaintextOverride); var tableName := GetTableName("foo"); var input := DDB.PutItemInput( TableName := tableName, - Item := BasicItem() + Item := BasicItem ); var transformed := middlewareUnderTest.PutItemInputTransform( AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( @@ -79,7 +60,7 @@ module PutItemTransformTest { var tableName := GetTableName("foo"); var input := DDB.PutItemInput( TableName := tableName, - Item := BasicItem() + Item := BasicItem ); var transformed := middlewareUnderTest.PutItemInputTransform( AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemInputTransformInput( @@ -99,15 +80,7 @@ module PutItemTransformTest { var tableName := GetTableName("no_such_table"); var input := DDB.PutItemInput( TableName := tableName, - Item := map[], - Expected := None(), - ReturnValues := None(), - ReturnConsumedCapacity := None(), - ReturnItemCollectionMetrics := None(), - ConditionalOperator := None(), - ConditionExpression := None(), - ExpressionAttributeNames := None(), - ExpressionAttributeValues := None() + Item := map[] ); var transformed := middlewareUnderTest.PutItemOutputTransform( AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.PutItemOutputTransformInput( diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index 204a33d93..235270ff6 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -124,11 +124,7 @@ module TestFixtures { attributeActionsOnEncrypt := config.attributeActionsOnEncrypt, allowedUnsignedAttributes := config.allowedUnsignedAttributes, allowedUnsignedAttributePrefix := config.allowedUnsignedAttributePrefix, - keyring := Some(keyring), - cmm := None(), - algorithmSuiteId := None(), - legacyOverride := None(), - plaintextOverride := None() + keyring := Some(keyring) ); var encryptor2 : IDynamoDbItemEncryptorClient :- expect DynamoDbItemEncryptor.DynamoDbItemEncryptor(encryptorConfig); assert encryptor2 is DynamoDbItemEncryptor.DynamoDbItemEncryptorClient; @@ -186,10 +182,7 @@ module TestFixtures { { var matProv :- expect MaterialProviders.MaterialProviders(MaterialProviders.DefaultMaterialProvidersConfig()); var keyringInput := AwsCryptographyMaterialProvidersTypes.CreateAwsKmsMultiKeyringInput( - generator := Some(PUBLIC_US_WEST_2_KMS_TEST_KEY), - kmsKeyIds := None(), - clientSupplier := None(), - grantTokens := None() + generator := Some(PUBLIC_US_WEST_2_KMS_TEST_KEY) ); keyring :- expect matProv.CreateAwsKmsMultiKeyring(keyringInput); } @@ -234,11 +227,7 @@ module TestFixtures { allowedUnsignedAttributes := Some(["plain"]), allowedUnsignedAttributePrefix := None(), algorithmSuiteId := None(), - keyring := Some(keyring), - cmm := None(), - search := None, - legacyOverride := None, - plaintextOverride := None + keyring := Some(keyring) ) ] ) @@ -248,8 +237,7 @@ module TestFixtures { // type AttributeActions = map - function method GetMultiActions() : AttributeActions - { + const MultiActions : AttributeActions := map[ "bar" := SE.SIGN_ONLY, "std2" := SE.ENCRYPT_AND_SIGN, @@ -262,7 +250,6 @@ module TestFixtures { "Date" := SE.SIGN_ONLY, "TheKeyField" := SE.SIGN_ONLY ] - } method GetDynamoDbEncryptionTransformsMutli(plaintextOverride : Option) returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient) @@ -283,14 +270,10 @@ module TestFixtures { logicalTableName := "foo", partitionKeyName := "bar", sortKeyName := None(), - attributeActionsOnEncrypt := GetMultiActions(), + attributeActionsOnEncrypt := MultiActions, allowedUnsignedAttributes := Some(["plain"]), - allowedUnsignedAttributePrefix := None(), - algorithmSuiteId := None(), keyring := Some(keyring), - cmm := None(), search := Some(search), - legacyOverride := None, plaintextOverride := plaintextOverride ) ]