chore: include bad item keys in query errors

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

@@ -9,6 +9,8 @@ module DdbMiddlewareConfig {
   import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes
   import DDBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes
   import SearchableEncryptionInfo
+  import DDB = ComAmazonawsDynamodbTypes
+  import HexStrings
 
   datatype TableConfig = TableConfig(
     physicalTableName: ComAmazonawsDynamodbTypes.TableName,
@@ -86,6 +88,35 @@ module DdbMiddlewareConfig {
     tableEncryptionConfigs: map<string, ValidTableConfig>
   )
 
+  function method AttrToString(attr : DDB.AttributeValue) : string
+  {
+    if attr.S? then
+      attr.S
+    else if attr.N? then
+      attr.N
+    else if attr.B? then
+      HexStrings.ToHexString(attr.B)
+    else
+      "unexpected key type"
+  }
+
+  // return human readable string containing primary keys
+  function method KeyString(config : ValidTableConfig, item : DDB.AttributeMap) : string
+  {
+    var partition :=
+      if config.partitionKeyName in item then
+        config.partitionKeyName + " = " + AttrToString(item[config.partitionKeyName])
+      else
+        "";
+    var sort :=
+      if config.sortKeyName.Some? && config.sortKeyName.value in item then
+        "\n" + config.sortKeyName.value + " = " + AttrToString(item[config.sortKeyName.value])
+      else
+        "";
+
+    partition + sort
+  }
+
   function method MapError<T>(r : Result<T, EncTypes.Error>) : Result<T, Error> {
     r.MapFailure(e => AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(e))
   }

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy

@@ -81,16 +81,29 @@ module QueryTransform {
     if keyId.KeyId? {
       keyIdUtf8 :- UTF8.Encode(keyId.value).MapFailure(e => E(e));
     }
-    ghost var originalHistory := tableConfig.itemEncryptor.History.DecryptItem;
-    ghost var historySize := |originalHistory|;
+
+    var decryptErrors : seq<Error> := [];
+    var lastRealError := -1;
+
     for x := 0 to |encryptedItems|
+      invariant lastRealError == -1 || lastRealError < |decryptErrors|
     {
       //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query
       //# Each of these entries on the original response MUST be replaced
       //# with the resulting decrypted [DynamoDB Item](./decrypt-item.md#dynamodb-item-1).
       var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]);
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
-      var decrypted :- MapError(decryptRes);
+      if decryptRes.Failure? {
+        var error := AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(decryptRes.error);
+        var context := E(KeyString(tableConfig, encryptedItems[x]));
+        if lastRealError == -1 || error != decryptErrors[lastRealError] {
+          lastRealError := |decryptErrors|;
+          decryptErrors := decryptErrors + [error];
+        }
+        decryptErrors := decryptErrors + [context];
+        continue;
+      }
+      var decrypted := decryptRes.value;
 
       // If the decrypted result was plaintext, i.e. has no parsedHeader
       // then this is expected IFF the table config allows plaintext read
@@ -111,7 +124,9 @@ module QueryTransform {
         decryptedItems := decryptedItems + [decrypted.plaintextItem];
       }
     }
-
+    if |decryptErrors| != 0 {
+      return Failure(CollectionOfErrors(decryptErrors, message := "Error(s) found decrypting Query results."));
+    }
     //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-query
     //# The resulting decrypted response MUST be [filtered](ddb-support.md#queryoutputforbeacons) from the result.
     var decryptedOutput := input.sdkOutput.(Items := Some(decryptedItems));

DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy

@@ -79,7 +79,11 @@ module ScanTransform {
     if keyId.KeyId? {
       keyIdUtf8 :- UTF8.Encode(keyId.value).MapFailure(e => E(e));
     }
+    var decryptErrors : seq<Error> := [];
+    var lastRealError := -1;
+
     for x := 0 to |encryptedItems|
+      invariant lastRealError == -1 || lastRealError < |decryptErrors|
     {
       //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan
       //# Each of these entries on the original response MUST be replaced
@@ -88,7 +92,17 @@ module ScanTransform {
 
       var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]);
       var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput);
-      var decrypted :- MapError(decryptRes);
+      if decryptRes.Failure? {
+        var error := AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(decryptRes.error);
+        var context := E(KeyString(tableConfig, encryptedItems[x]));
+        if lastRealError == -1 || error != decryptErrors[lastRealError] {
+          lastRealError := |decryptErrors|;
+          decryptErrors := decryptErrors + [error];
+        }
+        decryptErrors := decryptErrors + [context];
+        continue;
+      }
+      var decrypted := decryptRes.value;
 
       // If the decrypted result was plaintext, i.e. has no parsedHeader
       // then this is expected IFF the table config allows plaintext read
@@ -109,6 +123,9 @@ module ScanTransform {
         decryptedItems := decryptedItems + [decrypted.plaintextItem];
       }
     }
+    if |decryptErrors| != 0 {
+      return Failure(CollectionOfErrors(decryptErrors, message := "Error(s) found decrypting Scan results."));
+    }
 
     //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-scan
     //# The resulting decrypted response MUST be [filtered](ddb-support.md#scanoutputforbeacons) from the result.