Fix: Decrypt attributes returned by all DDB APIs

CHANGELOG.md

@@ -1,5 +1,13 @@
 # Changelog
 
+## 3.1.2 2023-11-13
+
+### Fix
+
+Fixed an issue where, when using the DynamoDbEncryptionInterceptor,
+an encrypted item in the Attributes field of a DeleteItem, PutItem, or UpdateItem
+response was passed through unmodified instead of being decrypted.
+
 ## 3.1.1 2023-11-07
 
 ### Fix

DecryptWithPermute/runtimes/java/build.gradle.kts

@@ -68,7 +68,7 @@ repositories {
 val dynamodb by configurations.creating
 
 dependencies {
-    implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:3.1.1")
+    implementation("software.amazon.cryptography:aws-database-encryption-sdk-dynamodb:3.1.2")
     implementation("org.dafny:DafnyRuntime:4.1.0")
     implementation("software.amazon.smithy.dafny:conversion:0.1")
     implementation("software.amazon.cryptography:aws-cryptographic-material-providers:1.0.0")

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DeleteItemTransform.dfy

@@ -66,8 +66,79 @@ module DeleteItemTransform {
 
   method Output(config: Config, input: DeleteItemOutputTransformInput)
     returns (output: Result<DeleteItemOutputTransformOutput, Error>)
-    ensures output.Success? && output.value.transformedOutput == input.sdkOutput
+
+    //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-deleteitem
+    //= type=implication
+    //# After a [DeleteItem](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_DeleteItem.html)
+    //# call is made to DynamoDB,
+    //# the resulting response MUST be modified before
+    //# being returned to the caller if:
+    //  - there exists an Item Encryptor specified within the
+    //    [DynamoDB Encryption Client Config](#dynamodb-encryption-client-configuration)
+    //    with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
+    //    equal to the `TableName` on the DeleteItem request.
+    //  - the response contains [Attributes](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_DeleteItem.html#DDB-DeleteItem-response-Attributes).
+    //    The response will contain Attributes if the related DeleteItem request's
+    //    [ReturnValues](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_DeleteItem.html#DDB-DeleteItem-request-ReturnValues)
+    //    had a value of `ALL_OLD` and an item was deleted.
+    ensures (
+      && output.Success?
+      && input.originalInput.TableName in config.tableEncryptionConfigs
+      && input.sdkOutput.Attributes.Some?
+    ) ==>
+      && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
+      && var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
+      && var newHistory := tableConfig.itemEncryptor.History.DecryptItem;
+
+      && |newHistory| == |oldHistory|+1
+      && Seq.Last(newHistory).output.Success?
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-deleteitem
+      //= type=implication
+      //# In this case, the [Item Encryptor](./ddb-item-encryptor.md) MUST perform
+      //# [Decrypt Item](./decrypt-item.md) where the input
+      //# [DynamoDB Item](./decrypt-item.md#dynamodb-item)
+      //# is the `Attributes` field in the original response
+      && Seq.Last(newHistory).input.encryptedItem == input.sdkOutput.Attributes.value
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-deleteitem
+      //= type=implication
+      //# Beacons MUST be [removed](ddb-support.md#removebeacons) from the result.
+      && RemoveBeacons(tableConfig, Seq.Last(newHistory).output.value.plaintextItem).Success?
+      && var item := RemoveBeacons(tableConfig, Seq.Last(newHistory).output.value.plaintextItem).value;
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-deleteitem
+      //= type=implication
+      //# The DeleteItem response's `Attributes` field MUST be
+      //# replaced by the encrypted DynamoDb Item outputted above.
+      && output.value.transformedOutput.Attributes.Some?
+      && (item == output.value.transformedOutput.Attributes.value)
+
+    // Passthrough the response if the above specification is not met
+    ensures (
+      && output.Success?
+      && (
+        || input.originalInput.TableName !in config.tableEncryptionConfigs
+        || input.sdkOutput.Attributes.None?
+      )
+    ) ==>
+        output.value.transformedOutput == input.sdkOutput
+
+    requires ValidConfig?(config)
+    ensures ValidConfig?(config)
+    modifies ModifiesConfig(config)
   {
-    return Success(DeleteItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    var tableName := input.originalInput.TableName;
+    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
+      {
+      return Success(DeleteItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    }
+    var tableConfig := config.tableEncryptionConfigs[tableName];
+    var decryptRes := tableConfig.itemEncryptor.DecryptItem(
+      EncTypes.DecryptItemInput(encryptedItem:=input.sdkOutput.Attributes.value)
+    );
+    var decrypted :- MapError(decryptRes);
+    var item :- RemoveBeacons(tableConfig, decrypted.plaintextItem);
+    return Success(DeleteItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Attributes := Some(item))));
   }
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DynamoDbMiddlewareSupport.dfy

@@ -30,6 +30,15 @@ module DynamoDbMiddlewareSupport {
     .MapFailure(e => E(e))
   }
 
+  // IsSigned returned whether this attribute is signed according to this config
+  predicate method {:opaque} IsSigned(
+    config : ValidTableConfig,
+    attr : string
+  )
+  {
+    BS.IsSigned(config.itemEncryptor.config.attributeActionsOnEncrypt, attr)
+  }
+
   // TestConditionExpression fails if a condition expression is not suitable for the
   // given encryption schema.
   // Generally this means no encrypted attribute is referenced.

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/PutItemTransform.dfy

@@ -83,8 +83,79 @@ module PutItemTransform {
 
   method Output(config: Config, input: PutItemOutputTransformInput)
     returns (output: Result<PutItemOutputTransformOutput, Error>)
-    ensures output.Success? && output.value.transformedOutput == input.sdkOutput
+
+    //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-putitem
+    //= type=implication
+    //# After a [PutItem](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_PutItem.html)
+    //# call is made to DynamoDB,
+    //# the resulting response MUST be modified before
+    //# being returned to the caller if:
+    //  - there exists an Item Encryptor specified within the
+    //    [DynamoDB Encryption Client Config](#dynamodb-encryption-client-configuration)
+    //    with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
+    //    equal to the `TableName` on the PutItem request.
+    //  - the response contains [Attributes](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_PutItem.html#DDB-PutItem-response-Attributes).
+    //    The response will contain Attributes if the related PutItem request's
+    //    [ReturnValues](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_PutItem.html#DDB-PutItem-request-ReturnValues)
+    //    had a value of `ALL_OLD` and the PutItem call replaced a pre-existing item.
+    ensures (
+      && output.Success?
+      && input.originalInput.TableName in config.tableEncryptionConfigs
+      && input.sdkOutput.Attributes.Some?
+    ) ==>
+      && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
+      && var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
+      && var newHistory := tableConfig.itemEncryptor.History.DecryptItem;
+
+      && |newHistory| == |oldHistory|+1
+      && Seq.Last(newHistory).output.Success?
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-putitem
+      //= type=implication
+      //# In this case, the [Item Encryptor](./ddb-item-encryptor.md) MUST perform
+      //# [Decrypt Item](./decrypt-item.md) where the input
+      //# [DynamoDB Item](./decrypt-item.md#dynamodb-item)
+      //# is the `Attributes` field in the original response
+      && Seq.Last(newHistory).input.encryptedItem == input.sdkOutput.Attributes.value
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-putitem
+      //= type=implication
+      //# Beacons MUST be [removed](ddb-support.md#removebeacons) from the result.
+      && RemoveBeacons(tableConfig, Seq.Last(newHistory).output.value.plaintextItem).Success?
+      && var item := RemoveBeacons(tableConfig, Seq.Last(newHistory).output.value.plaintextItem).value;
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-putitem
+      //= type=implication
+      //# The PutItem response's `Attributes` field MUST be
+      //# replaced by the encrypted DynamoDb Item outputted above.
+      && output.value.transformedOutput.Attributes.Some?
+      && (item == output.value.transformedOutput.Attributes.value)
+
+    // Passthrough the response if the above specification is not met
+    ensures (
+      && output.Success?
+      && (
+        || input.originalInput.TableName !in config.tableEncryptionConfigs
+        || input.sdkOutput.Attributes.None?
+      )
+    ) ==>
+        output.value.transformedOutput == input.sdkOutput
+
+    requires ValidConfig?(config)
+    ensures ValidConfig?(config)
+    modifies ModifiesConfig(config)
   {
-    return Success(PutItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    var tableName := input.originalInput.TableName;
+    if tableName !in config.tableEncryptionConfigs || input.sdkOutput.Attributes.None?
+      {
+      return Success(PutItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    }
+    var tableConfig := config.tableEncryptionConfigs[tableName];
+    var decryptRes := tableConfig.itemEncryptor.DecryptItem(
+      EncTypes.DecryptItemInput(encryptedItem:=input.sdkOutput.Attributes.value)
+    );
+    var decrypted :- MapError(decryptRes);
+    var item :- RemoveBeacons(tableConfig, decrypted.plaintextItem);
+    return Success(PutItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Attributes := Some(item))));
   }
 }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/UpdateItemTransform.dfy

@@ -65,8 +65,142 @@ module UpdateItemTransform {
 
   method Output(config: Config, input: UpdateItemOutputTransformInput)
     returns (output: Result<UpdateItemOutputTransformOutput, Error>)
-    ensures output.Success? && output.value.transformedOutput == input.sdkOutput
+
+    //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
+    //= type=implication
+    //# After a [UpdateItem](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_UpdateItem.html)
+    //# call is made to DynamoDB,
+    //# the resulting response MUST be modified before
+    //# being returned to the caller if:
+    //  - there exists an Item Encryptor specified within the
+    //    [DynamoDB Encryption Client Config](#dynamodb-encryption-client-configuration)
+    //    with a [DynamoDB Table Name](./ddb-item-encryptor.md#dynamodb-table-name)
+    //    equal to the `TableName` on the UpdateItem request.
+    //  - the response contains [Attributes](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_UpdateItem.html#DDB-UpdateItem-response-Attributes).
+    //  - the original UpdateItem request had a 
+    //    [ReturnValues](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_UpdateItem.html#DDB-UpdateItem-request-ReturnValues)
+    //    with a value of `ALL_OLD` or `ALL_NEW`.
+    ensures (
+      && output.Success?
+      && input.originalInput.TableName in config.tableEncryptionConfigs
+      && input.sdkOutput.Attributes.Some?
+      && input.originalInput.ReturnValues.Some?
+      && (
+        || input.originalInput.ReturnValues.value.ALL_OLD?
+        || input.originalInput.ReturnValues.value.ALL_NEW?
+      )
+    ) ==>
+      && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
+      && var oldHistory := old(tableConfig.itemEncryptor.History.DecryptItem);
+      && var newHistory := tableConfig.itemEncryptor.History.DecryptItem;
+
+      && |newHistory| == |oldHistory|+1
+      && Seq.Last(newHistory).output.Success?
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
+      //= type=implication
+      //# In this case, the [Item Encryptor](./ddb-item-encryptor.md) MUST perform
+      //# [Decrypt Item](./decrypt-item.md) where the input
+      //# [DynamoDB Item](./decrypt-item.md#dynamodb-item)
+      //# is the `Attributes` field in the original response
+      && Seq.Last(newHistory).input.encryptedItem == input.sdkOutput.Attributes.value
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
+      //= type=implication
+      //# Beacons MUST be [removed](ddb-support.md#removebeacons) from the result.
+      && RemoveBeacons(tableConfig, Seq.Last(newHistory).output.value.plaintextItem).Success?
+      && var item := RemoveBeacons(tableConfig, Seq.Last(newHistory).output.value.plaintextItem).value;
+
+      //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
+      //= type=implication
+      //# The UpdateItem response's `Attributes` field MUST be
+      //# replaced by the encrypted DynamoDb Item outputted above.
+      && output.value.transformedOutput.Attributes.Some?
+      && (item == output.value.transformedOutput.Attributes.value)
+
+    //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
+    //= type=implication
+    //# In all other cases, the UpdateItem response MUST NOT be modified.
+    ensures (
+      && output.Success?
+      && (
+        || input.originalInput.TableName !in config.tableEncryptionConfigs
+        || input.sdkOutput.Attributes.None?
+      )
+    ) ==> (
+      && output.value.transformedOutput == input.sdkOutput
+    )
+
+    ensures (
+      && output.Success?
+      && input.originalInput.TableName in config.tableEncryptionConfigs
+      && input.sdkOutput.Attributes.Some?
+      && (input.originalInput.ReturnValues.Some? ==> (
+            || input.originalInput.ReturnValues.value.UPDATED_NEW?
+            || input.originalInput.ReturnValues.value.UPDATED_OLD?
+          )
+        )
+      ) ==> (
+        && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
+        && output.value.transformedOutput == input.sdkOutput
+        && forall k <- input.sdkOutput.Attributes.value.Keys :: !IsSigned(tableConfig, k)
+      )
+
+    //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-updateitem
+    //= type=implication
+    //# Additionally, if a value of `UPDATED_OLD` or `UPDATED_NEW` was used,
+    //# and any Attributes in the response are authenticated
+    //# per the [DynamoDB Encryption Client Config](#dynamodb-encryption-client-configuration),
+    //# an error MUST be raised.
+    ensures (
+      && input.originalInput.TableName in config.tableEncryptionConfigs
+      && var tableConfig := config.tableEncryptionConfigs[input.originalInput.TableName];
+      && input.sdkOutput.Attributes.Some?
+      && (input.originalInput.ReturnValues.Some? ==> (
+            || input.originalInput.ReturnValues.value.UPDATED_NEW?
+            || input.originalInput.ReturnValues.value.UPDATED_OLD?
+          )
+        )
+      && exists k <- input.sdkOutput.Attributes.value.Keys :: IsSigned(tableConfig, k)
+    ) ==>
+      output.Failure?
+
+    requires ValidConfig?(config)
+    ensures ValidConfig?(config)
+    modifies ModifiesConfig(config)
   {
-    return Success(UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    var tableName := input.originalInput.TableName;
+
+    if
+      || tableName !in config.tableEncryptionConfigs
+      || input.sdkOutput.Attributes.None?
+    {
+      return Success(UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    }
+
+    var tableConfig := config.tableEncryptionConfigs[tableName];
+    var attributes := input.sdkOutput.Attributes.value;
+
+    if !(
+      && input.originalInput.ReturnValues.Some?
+      && (
+       || input.originalInput.ReturnValues.value.ALL_NEW?
+       || input.originalInput.ReturnValues.value.ALL_OLD?)
+      )
+    {
+      // This error should not be possible to reach if we assume the DDB API contract is correct.
+      // We include this runtime check for defensive purposes.
+      :- Need(forall k <- attributes.Keys :: !IsSigned(tableConfig, k),
+        E("UpdateItems response contains signed attributes, but does not include the entire item which is required for verification."));
+
+      return Success(UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput));
+    }
+
+    var decryptRes := tableConfig.itemEncryptor.DecryptItem(
+      EncTypes.DecryptItemInput(encryptedItem:=attributes)
+    );
+    var decrypted :- MapError(decryptRes);
+    var item :- RemoveBeacons(tableConfig, decrypted.plaintextItem);
+    return Success(UpdateItemOutputTransformOutput(transformedOutput := input.sdkOutput.(Attributes := Some(item))));
   }
 }

DynamoDbEncryption/runtimes/java/build.gradle.kts

@@ -12,7 +12,7 @@ plugins {
 }
 
 group = "software.amazon.cryptography"
-version = "3.1.1"
+version = "3.1.2"
 description = "Aws Database Encryption Sdk for DynamoDb Java"
 
 java {

DynamoDbEncryption/runtimes/java/src/main/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptor.java

@@ -252,6 +252,17 @@ public SdkResponse modifyResponse(Context.ModifyResponse context, ExecutionAttri
                         .sdkHttpResponse(originalResponse.sdkHttpResponse())
                         .build();
                 break;
+            } case "DeleteItem": {
+                DeleteItemResponse transformedResponse = transformer.DeleteItemOutputTransform(
+                        DeleteItemOutputTransformInput.builder()
+                                .sdkOutput((DeleteItemResponse) originalResponse)
+                                .originalInput((DeleteItemRequest) originalRequest)
+                                .build()).transformedOutput();
+                outgoingResponse = transformedResponse.toBuilder()
+                        .responseMetadata(((DeleteItemResponse) originalResponse).responseMetadata())
+                        .sdkHttpResponse(originalResponse.sdkHttpResponse())
+                        .build();
+                break;
             } case "ExecuteStatement": {
                 ExecuteStatementResponse transformedResponse = transformer.ExecuteStatementOutputTransform(
                         ExecuteStatementOutputTransformInput.builder()

DynamoDbEncryption/runtimes/java/src/main/sdkv1/com/amazonaws/services/dynamodbv2/datamodeling/encryption/DoNotEncrypt.java

@@ -21,6 +21,9 @@
 import java.lang.annotation.Target;
 
 /**
+ * Warning: This annotation only works with the DynamoDBMapper for AWS SDK for Java 1.x.
+ * If you are using the AWS SDK for Java 2.x, use @DynamoDbEncryptionSignOnly instead.
+ *
  * Prevents the associated item (class or attribute) from being encrypted.
  *
  * <p>For guidance on performing a safe data model change procedure, please see <a
@@ -32,4 +35,5 @@
 @DynamoDB
 @Target(value = {ElementType.TYPE, ElementType.METHOD, ElementType.FIELD})
 @Retention(value = RetentionPolicy.RUNTIME)
+@Deprecated
 public @interface DoNotEncrypt {}