From dd6c776078fc0c8a7357268ad9ca0aa8b6c8fcca Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 22 Aug 2024 13:12:11 -0400 Subject: [PATCH] fix: revert change in error type --- .../src/QueryTransform.dfy | 23 +-- .../src/ScanTransform.dfy | 19 +- .../test/QueryTransform.dfy | 171 ++---------------- 3 files changed, 23 insertions(+), 190 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index 974117876..6eefe7fa2 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -81,29 +81,16 @@ module QueryTransform { if keyId.KeyId? { keyIdUtf8 :- UTF8.Encode(keyId.value).MapFailure(e => E(e)); } - - var decryptErrors : seq := []; - var lastRealError := -1; - + ghost var originalHistory := tableConfig.itemEncryptor.History.DecryptItem; + ghost var historySize := |originalHistory|; 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); - 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; + var decrypted :- MapError(decryptRes); // If the decrypted result was plaintext, i.e. has no parsedHeader // then this is expected IFF the table config allows plaintext read @@ -124,9 +111,7 @@ 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)); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index 8e24394ce..034cd7943 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -79,11 +79,7 @@ module ScanTransform { if keyId.KeyId? { keyIdUtf8 :- UTF8.Encode(keyId.value).MapFailure(e => E(e)); } - var decryptErrors : seq := []; - 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 @@ -92,17 +88,7 @@ module ScanTransform { var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]); var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); - 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; + var decrypted :- MapError(decryptRes); // If the decrypted result was plaintext, i.e. has no parsedHeader // then this is expected IFF the table config allows plaintext read @@ -123,9 +109,6 @@ 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. diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy index 382e6e0fc..c524bd5b9 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/QueryTransform.dfy @@ -8,10 +8,7 @@ module QueryTransformTest { import opened DynamoDbEncryptionTransforms import opened TestFixtures import DDB = ComAmazonawsDynamodbTypes - import DBT = AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes - import DBE = AwsCryptographyDbEncryptionSdkDynamoDbTypes - import Types = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes - import AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes + import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes method {:test} TestQueryInputPassthrough() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); @@ -56,7 +53,23 @@ module QueryTransformTest { ); var tableName := GetTableName("no_such_table"); var input := DDB.QueryInput( - TableName := tableName + TableName := tableName, + IndexName := None(), + Select := None(), + AttributesToGet := None(), + Limit := None(), + ConsistentRead := None(), + KeyConditions := None(), + QueryFilter := None(), + ConditionalOperator := None(), + ScanIndexForward := None(), + ExclusiveStartKey := None(), + ReturnConsumedCapacity := None(), + ProjectionExpression := None(), + FilterExpression := None(), + KeyConditionExpression := None(), + ExpressionAttributeNames := None(), + ExpressionAttributeValues := None() ); var transformed := middlewareUnderTest.QueryOutputTransform( AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput( @@ -68,152 +81,4 @@ module QueryTransformTest { expect_ok("QueryOutput", transformed); expect_equal("QueryOutput", transformed.value.transformedOutput, output); } - - function method DDBS(x : string) : DDB.AttributeValue { - DDB.AttributeValue.S(x) - } - - const Actions1 : DBE.AttributeActions := map[ - GetAttrName("bar") := CSE.SIGN_ONLY, - GetAttrName("sortKey") := CSE.SIGN_ONLY, - GetAttrName("encrypt1") := CSE.ENCRYPT_AND_SIGN, - GetAttrName("encrypt2") := CSE.ENCRYPT_AND_SIGN, - GetAttrName("sign1") := CSE.SIGN_ONLY, - GetAttrName("sign2") := CSE.SIGN_ONLY - ] - - method {:test} TestDecryptErrorWithSortKey() { - var config := TestFixtures.GetEncryptorConfigFromActions(Actions1, Some("sortKey")); - var encryptor := TestFixtures.GetDynamoDbItemEncryptorFrom(config); - - var inputItem : map := map[ - "bar" := DDB.AttributeValue.N("00001234"), - "sortKey" := DDB.AttributeValue.B([1,2,3,4]), - "encrypt1" := DDBS("some text"), - "encrypt2" := DDBS("more text"), - "sign1" := DDBS("stuff"), - "sign2" := DDB.AttributeValue.BOOL(false) - ]; - - var encryptRes :- expect encryptor.EncryptItem( - Types.EncryptItemInput( - plaintextItem:=inputItem - ) - ); - var item1 := encryptRes.encryptedItem; - expect "encrypt1" in item1; - expect item1["encrypt1"] != DDBS("some text"); - - inputItem := map[ - "bar" := DDB.AttributeValue.N("567"), - "sortKey" := DDB.AttributeValue.B([5,6,7]), - "encrypt1" := DDBS("some text"), - "encrypt2" := DDBS("more text"), - "sign1" := DDBS("stuff"), - "sign2" := DDB.AttributeValue.BOOL(false) - ]; - encryptRes :- expect encryptor.EncryptItem( - Types.EncryptItemInput( - plaintextItem:=inputItem - ) - ); - var item2 := encryptRes.encryptedItem; - expect "encrypt1" in item2; - expect item2["encrypt1"] != DDBS("some text"); - - inputItem := map[ - "bar" := DDB.AttributeValue.N("890"), - "sortKey" := DDB.AttributeValue.B([3,1,4]), - "encrypt1" := DDBS("some text"), - "encrypt2" := DDBS("more text"), - "sign1" := DDBS("stuff"), - "sign2" := DDB.AttributeValue.BOOL(false) - ]; - encryptRes :- expect encryptor.EncryptItem( - Types.EncryptItemInput( - plaintextItem:=inputItem - ) - ); - var item3 := encryptRes.encryptedItem; - expect "encrypt1" in item3; - expect item3["encrypt1"] != DDBS("some text"); - - var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms2(Actions1, Some("sortKey")); - var tableName := GetTableName("foo"); - var input := DDB.QueryInput( - TableName := tableName - ); - - var transformed := middlewareUnderTest.QueryOutputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput( - sdkOutput := DDB.QueryOutput(Items := Some([item1, item2, item3])), - originalInput := input - ) - ); - - TestFixtures.expect_ok("QueryOutput", transformed); - expect transformed.value.transformedOutput.Items.Some?; - var itemList := transformed.value.transformedOutput.Items.value; - expect |itemList| == 3; - expect "encrypt1" in itemList[0]; - expect itemList[0]["encrypt1"] == DDBS("some text"); - - -/// now do some damage - item1 := item1["encrypt1" := item2["encrypt1"]]; - transformed := middlewareUnderTest.QueryOutputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput( - sdkOutput := DDB.QueryOutput(Items := Some([item1, item2, item3])), - originalInput := input - ) - ); - expect transformed.Failure?; - print "\n", transformed.error, "\n"; - expect transformed.error == - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors( - [ - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "Signature of record does not match the signature computed when the record was encrypted.")))), - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234; sortKey = 01020304") - ], - message := "Error(s) found decrypting Query results." - ); - -/// do more damage - item3 := item3["encrypt1" := item2["encrypt1"]]; - transformed := middlewareUnderTest.QueryOutputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.QueryOutputTransformInput( - sdkOutput := DDB.QueryOutput(Items := Some([item1, item2, item3])), - originalInput := input - ) - ); - expect transformed.Failure?; - print "\n", transformed.error, "\n"; - expect transformed.error == - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors( - [ - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "Signature of record does not match the signature computed when the record was encrypted.")))), - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234; sortKey = 01020304"), - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 890; sortKey = 030104") - ], - message := "Error(s) found decrypting Query results." - ); - - var transformed_scan := middlewareUnderTest.ScanOutputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.ScanOutputTransformInput( - sdkOutput := DDB.ScanOutput(Items := Some([item1, item2, item3])), - originalInput := DDB.ScanInput(TableName := tableName) - ) - ); - expect transformed_scan.Failure?; - print "\n", transformed_scan.error, "\n"; - expect transformed_scan.error == - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.CollectionOfErrors( - [ - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptor(AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes.Error.AwsCryptographyDbEncryptionSdkDynamoDb(AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error.AwsCryptographyDbEncryptionSdkStructuredEncryption(AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.Error.StructuredEncryptionException(message := "Signature of record does not match the signature computed when the record was encrypted.")))), - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 1234; sortKey = 01020304"), - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.Error.DynamoDbEncryptionTransformsException(message := "bar = 890; sortKey = 030104") - ], - message := "Error(s) found decrypting Scan results." - ); - } }