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 diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy index ebbf62e37..dd2ddbb07 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/PutItemTransform.dfy @@ -9,21 +9,14 @@ module PutItemTransformTest { import opened TestFixtures import DDB = ComAmazonawsDynamodbTypes import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes + import opened AwsCryptographyDbEncryptionSdkDynamoDbTypes method {:test} TestPutItemInputPassthrough() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); 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( @@ -35,6 +28,48 @@ module PutItemTransformTest { expect_equal("PutItemInput", transformed.value.transformedInput, input); } + 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 + ); + 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() { + 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( @@ -45,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 8ae5ea78a..235270ff6 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 @@ -122,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; @@ -184,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); } @@ -216,7 +211,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( @@ -232,17 +227,59 @@ module TestFixtures { allowedUnsignedAttributes := Some(["plain"]), allowedUnsignedAttributePrefix := None(), algorithmSuiteId := None(), + keyring := Some(keyring) + ) + ] + ) + ); + assume {:axiom} fresh(encryption.Modifies); + } + + // type AttributeActions = map + + const MultiActions : 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 := MultiActions, + allowedUnsignedAttributes := Some(["plain"]), keyring := Some(keyring), - cmm := None(), - search := None, - legacyOverride := None, - plaintextOverride := None + search := Some(search), + plaintextOverride := plaintextOverride ) ] ) ); - assert encryption2 is DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient; - encryption := encryption2 as DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient; assume {:axiom} fresh(encryption.Modifies); } + }