diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy index fc0991825..7d56fd9cd 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations.dfy @@ -227,7 +227,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs //# If this item does not have a sort key attribute, //# the DynamoDB Item Context MUST NOT contain the key `aws-crypto-sort-name`. ensures ret.Success? && config.sortKeyName.None? ==> - SORT_NAME !in ret.value + SORT_NAME !in ret.value { UTF8.EncodeAsciiUnique(); :- Need(config.partitionKeyName in item, DDBError("Partition key " + config.partitionKeyName + " not found in Item to be encrypted or decrypted")); @@ -514,15 +514,47 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs { // We can formally verify these properties, but it is too resource intensive :- Need(forall k <- schema.content.SchemaMap :: InSignatureScope(config, k), - DynamoDbItemEncryptorException( message := "Recieved unexpected Crypto Schema: mismatch with signature scope")); + DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: mismatch with signature scope")); :- Need(forall k <- schema.content.SchemaMap :: ComAmazonawsDynamodbTypes.IsValid_AttributeName(k), - DynamoDbItemEncryptorException( message := "Recieved unexpected Crypto Schema: Invalid attribute names")); + DynamoDbItemEncryptorException( message := "Received unexpected Crypto Schema: Invalid attribute names")); Success(map k <- schema.content.SchemaMap :: k := schema.content.SchemaMap[k].content.Action) } predicate EncryptItemEnsuresPublicly(input: EncryptItemInput, output: Result) {true} + function method GetItemNames(item : ComAmazonawsDynamodbTypes.AttributeMap) : string + { + var keys := SortedSets.ComputeSetToOrderedSequence2(item.Keys, CharLess); + if |keys| == 0 then + "item is empty" + else + Join(keys, " ") + } + + function method KeyMissingMsg( + config: InternalConfig, + item : ComAmazonawsDynamodbTypes.AttributeMap, + tag : string) + : string + { + "On " + tag + " : " + + + (if config.partitionKeyName !in item then + "Partition key '" + config.partitionKeyName + "' does not exist in item. " + else + "") + + + + (if config.sortKeyName.Some? && config.sortKeyName.value !in item then + "Sort key '" + config.sortKeyName.value + "' does not exist in item. " + else + "") + + + "Item contains these attributes : " + + GetItemNames(item) + "." + } + // public Encrypt method method {:vcs_split_on_every_assert} EncryptItem(config: InternalConfig, input: EncryptItemInput) returns (output: Result) @@ -621,7 +653,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs :- Need( && config.partitionKeyName in input.plaintextItem && (config.sortKeyName.None? || config.sortKeyName.value in input.plaintextItem) - , DynamoDbItemEncryptorException( message := "Configuration mismatch partition or sort key does not exist in item.")); + , E(KeyMissingMsg(config, input.plaintextItem, "Encrypt"))); if |input.plaintextItem| > MAX_ATTRIBUTE_COUNT { var actCount := String.Base10Int2String(|input.plaintextItem|); @@ -839,7 +871,7 @@ module AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations refines Abs :- Need( && config.partitionKeyName in input.encryptedItem && (config.sortKeyName.None? || config.sortKeyName.value in input.encryptedItem) - , DynamoDbItemEncryptorException( message := "Configuration mismatch partition or sort key does not exist in item.")); + , DynamoDbItemEncryptorException( message := KeyMissingMsg(config, input.encryptedItem, "Decrypt"))); //= specification/dynamodb-encryption-client/decrypt-item.md#behavior //# If a [Legacy Policy](./ddb-table-encryption-config.md#legacy-policy) of diff --git a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy index 61765c732..351517712 100644 --- a/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbItemEncryptor/test/DynamoDBItemEncryptorTest.dfy @@ -39,15 +39,15 @@ module DynamoDbItemEncryptorTest { ); expect encryptRes.Failure?; expect encryptRes.error == Types.AwsCryptographyDbEncryptionSdkDynamoDb( - DDBE.DynamoDbEncryptionException(message := "No Crypto Action configured for attribute unknown")); + DDBE.DynamoDbEncryptionException(message := "No Crypto Action configured for attribute unknown")); } method {:test} TestMissingSortKey() { var config := TestFixtures.GetEncryptorConfig(); var inputItem := map["bar" := DDBS("key"), "encrypt" := DDBS("foo"), "sign" := DDBS("bar"), "nothing" := DDBS("baz")]; var config2 := config.( - sortKeyName := Some("sort"), - attributeActionsOnEncrypt := config.attributeActionsOnEncrypt["sort" := CSE.SIGN_ONLY] + sortKeyName := Some("sort"), + attributeActionsOnEncrypt := config.attributeActionsOnEncrypt["sort" := CSE.SIGN_ONLY] ); var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config2); var encryptRes := encryptor.EncryptItem( @@ -56,7 +56,9 @@ module DynamoDbItemEncryptorTest { ) ); expect encryptRes.Failure?; - expect encryptRes.error == Types.DynamoDbItemEncryptorException(message := "Configuration mismatch partition or sort key does not exist in item."); + expect encryptRes.error == Types.DynamoDbItemEncryptorException( + message := "On Encrypt : Sort key 'sort' does not exist in item. Item contains these attributes : bar encrypt nothing sign." + ); } method {:test} TestRoundTrip() { @@ -148,7 +150,7 @@ module DynamoDbItemEncryptorTest { expect |parsedHeader.value.encryptedDataKeys| == 1; } - method {:test} TestTooManyAttributes() { + method {:test} TestTooManyAttributes() { var inputItem : DDB.AttributeMap := map["bar" := DDBS("key")]; var actions : DDBE.AttributeActions := map["bar" := CSE.SIGN_ONLY]; for i := 0 to MAX_ATTRIBUTE_COUNT { diff --git a/DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptorTest.java b/DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptorTest.java index ea180431b..5f64241e5 100644 --- a/DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptorTest.java +++ b/DynamoDbEncryption/runtimes/java/src/test/java/software/amazon/cryptography/dbencryptionsdk/dynamodb/DynamoDbEncryptionInterceptorTest.java @@ -506,7 +506,7 @@ public void TestPutWithInvalidCryptoAction() { @Test( expectedExceptions = DynamoDbItemEncryptorException.class, - expectedExceptionsMessageRegExp = "Configuration mismatch partition or sort key does not exist in item." + expectedExceptionsMessageRegExp = "On Encrypt : Partition key 'partition_key' does not exist in item. Item contains these attributes : attr1 attr2 sort_key." ) public void TestPutMissingPartition() { Map item = createTestItem("foo", "10", "bar", "awol"); @@ -530,7 +530,7 @@ public void TestPutMissingPartition() { @Test( expectedExceptions = DynamoDbItemEncryptorException.class, - expectedExceptionsMessageRegExp = "Configuration mismatch partition or sort key does not exist in item." + expectedExceptionsMessageRegExp = "On Encrypt : Sort key 'sort_key' does not exist in item. Item contains these attributes : attr1 attr2 partition_key." ) public void TestPutMissingSort() { Map item = createTestItem("foo", "10", "bar", "awol");