chore: do not add beacons when FORCE_PLAINTEXT_WRITE is used. (#1232)

* chore: respect FORCE_PLAINTEXT_WRITE when using multi-tenant 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

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<AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride>) {
+    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(

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<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
+
+  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<AwsCryptographyDbEncryptionSdkDynamoDbTypes.PlaintextOverride>)
+    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);
   }
+
 }