chore: respect FORCE_PLAINTEXT_WRITE when using multitenant and search config

Author: ajewellamz

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<DDB.WriteRequest> := [];
         for x := 0 to |writeRequests|

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

@@ -16,9 +16,17 @@ module DdbMiddlewareConfig {
     partitionKeyName: string,
     sortKeyName: Option<string>,
     itemEncryptor: DynamoDbItemEncryptor.DynamoDbItemEncryptorClient,
-    search : Option<SearchableEncryptionInfo.ValidSearchInfo>
+    search : Option<SearchableEncryptionInfo.ValidSearchInfo>,
+    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

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];

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];

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