From 4446d78bceb8e854a7e32fa65569739e42e7d107 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 11 Feb 2025 11:45:02 -0500 Subject: [PATCH 1/3] fix: return plaintext items in UnprocessedItems in BatchWriteIttem --- .../src/BatchWriteItemTransform.dfy | 80 ++++++++++++++++++- 1 file changed, 78 insertions(+), 2 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index 1a4fd48ef..268ccca15 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -13,6 +13,7 @@ module BatchWriteItemTransform { import Seq import SortedSets import Util = DynamoDbEncryptionUtil + import Types = AwsCryptographyDbEncryptionSdkDynamoDbTypes method {:vcs_split_on_every_assert} Input(config: Config, input: BatchWriteItemInputTransformInput) returns (output: Result) @@ -80,11 +81,86 @@ module BatchWriteItemTransform { return Success(BatchWriteItemInputTransformOutput(transformedInput := input.sdkInput.(RequestItems := result))); } + method GetOrigItem( + tableConfig : ValidTableConfig, + srcRequests : DDB.WriteRequests, + itemReq : DDB.WriteRequest + ) returns (ret : Result) + requires itemReq.PutRequest.Some? + ensures ret.Success? ==> ret.value.PutRequest.Some? + { + var partKey := tableConfig.partitionKeyName; + var sortKey := tableConfig.sortKeyName; + var item := itemReq.PutRequest.value.Item; + :- Need(partKey in item, E("Required partition key not in unprocessed item")); + :- Need(sortKey.None? || sortKey.value in item, E("Required sort key not in unprocessed item")); + for i := 0 to |srcRequests| { + if srcRequests[i].PutRequest.Some? { + var req := srcRequests[i].PutRequest.value.Item; + if partKey in req && req[partKey] == item[partKey] { + if sortKey.None? || (sortKey.value in req && req[sortKey.value] == item[sortKey.value]) { + return Success(srcRequests[i]); + } + } + } + } + return Failure(E("Item in UnprocessedItems not found in original request.")); + } + method Output(config: Config, input: BatchWriteItemOutputTransformInput) returns (output: Result) - ensures output.Success? && output.value.transformedOutput == input.sdkOutput { - return Success(BatchWriteItemOutputTransformOutput(transformedOutput := input.sdkOutput)); + if input.sdkOutput.UnprocessedItems.None? { + return Success(BatchWriteItemOutputTransformOutput(transformedOutput := input.sdkOutput)); + } + + var srcItems := input.originalInput.RequestItems; + var unprocessed := input.sdkOutput.UnprocessedItems.value; + var tableNames := unprocessed.Keys; + var result : map := map[]; + var tableNamesSeq := SortedSets.ComputeSetToSequence(tableNames); + ghost var tableNamesSet' := tableNames; + var i := 0; + while i < |tableNamesSeq| + invariant Seq.HasNoDuplicates(tableNamesSeq) + invariant forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' + invariant |tableNamesSet'| == |tableNamesSeq| - i + invariant tableNamesSet' <= unprocessed.Keys + { + var tableName := tableNamesSeq[i]; + + var writeRequests : DDB.WriteRequests := unprocessed[tableName]; + if !IsPlainWrite(config, tableName) { + if tableName !in srcItems { + return Failure(E(tableName + " in UnprocessedItems for BatchWriteItem response, but not in original request.")); + } + var srcRequests := srcItems[tableName]; + var tableConfig := config.tableEncryptionConfigs[tableName]; + var origItems : seq := []; + for x := 0 to |writeRequests| + invariant |origItems| == x + { + var req : DDB.WriteRequest := writeRequests[x]; + if req.PutRequest.None? { + // We only transform PutRequests, so no PutRequest ==> no change + origItems := origItems + [req]; + } else { + var orig_item :- GetOrigItem(tableConfig, srcRequests, req); + origItems := origItems + [orig_item]; + } + } + writeRequests := origItems; + } + tableNamesSet' := tableNamesSet' - {tableName}; + i := i + 1; + assert forall j | i <= j < |tableNamesSeq| :: tableNamesSeq[j] in tableNamesSet' by { + reveal Seq.HasNoDuplicates(); + } + result := result[tableName := writeRequests]; + } + :- Need(|result| == |unprocessed|, E("Internal Error")); // Dafny gets too confused + var new_output := input.sdkOutput.(UnprocessedItems := Some(result)); + return Success(BatchWriteItemOutputTransformOutput(transformedOutput := new_output)); } } From 4bb289a9800145d12d40ad3b616de076fcd8be86 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 11 Feb 2025 11:49:22 -0500 Subject: [PATCH 2/3] m --- .../src/BatchWriteItemTransform.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index 268ccca15..9702ef17e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -85,7 +85,7 @@ module BatchWriteItemTransform { tableConfig : ValidTableConfig, srcRequests : DDB.WriteRequests, itemReq : DDB.WriteRequest - ) returns (ret : Result) + ) returns (ret : Result) requires itemReq.PutRequest.Some? ensures ret.Success? ==> ret.value.PutRequest.Some? { From 07946e72406327e79a4959a88e2206e1f3f9b72c Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Tue, 11 Feb 2025 16:56:12 -0500 Subject: [PATCH 3/3] m --- .../src/BatchWriteItemTransform.dfy | 11 + .../test/BatchWriteItemTransform.dfy | 206 +++++++++++++++++- .../test/TestFixtures.dfy | 57 ++--- .../ddb-sdk-integration.md | 7 + 4 files changed, 253 insertions(+), 28 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy index 9702ef17e..b0633c59d 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/BatchWriteItemTransform.dfy @@ -81,6 +81,8 @@ module BatchWriteItemTransform { return Success(BatchWriteItemInputTransformOutput(transformedInput := input.sdkInput.(RequestItems := result))); } + // Given the encrypted item, find the original plaintext item, based on the never encrypted PK and SK. + // We don't have to worry about duplicates, because DynamoDB will report an error if there are duplicates method GetOrigItem( tableConfig : ValidTableConfig, srcRequests : DDB.WriteRequests, @@ -109,11 +111,20 @@ module BatchWriteItemTransform { method Output(config: Config, input: BatchWriteItemOutputTransformInput) returns (output: Result) + + //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-batchwriteitem + //= type=implication + //# If there are no UnprocessedItems, then the BatchWriteItemOutput MUST be returned unchanged. + ensures input.sdkOutput.UnprocessedItems.None? ==> + && output.Success? + && output.value.transformedOutput == input.sdkOutput { if input.sdkOutput.UnprocessedItems.None? { return Success(BatchWriteItemOutputTransformOutput(transformedOutput := input.sdkOutput)); } + //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-batchwriteitem + //# Each item in UnprocessedItems MUST be replaced by its original plaintext value. var srcItems := input.originalInput.RequestItems; var unprocessed := input.sdkOutput.UnprocessedItems.value; var tableNames := unprocessed.Keys; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/BatchWriteItemTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/BatchWriteItemTransform.dfy index cc707d789..b2fdd090c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/BatchWriteItemTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/BatchWriteItemTransform.dfy @@ -8,7 +8,7 @@ module BatchWriteItemTransformTest { import opened DynamoDbEncryptionTransforms import opened TestFixtures import DDB = ComAmazonawsDynamodbTypes - import AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes + import TTypes = AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes method {:test} TestBatchWriteItemInputTransform() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); @@ -25,7 +25,7 @@ module BatchWriteItemTransformTest { ReturnItemCollectionMetrics := None ); var transformed := middlewareUnderTest.BatchWriteItemInputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.BatchWriteItemInputTransformInput( + TTypes.BatchWriteItemInputTransformInput( sdkInput := input ) ); @@ -34,6 +34,35 @@ module BatchWriteItemTransformTest { expect_equal("BatchWriteItemInput", transformed.value.transformedInput, input); } + + const Item1 : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar1"), + "sign" := DDB.AttributeValue.S("sign1"), + "encrypt" := DDB.AttributeValue.S("encrypt1"), + "plain" := DDB.AttributeValue.S("plain1") + ] + + const Item2 : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar2"), + "sign" := DDB.AttributeValue.S("sign2"), + "encrypt" := DDB.AttributeValue.S("encrypt2"), + "plain" := DDB.AttributeValue.S("plain2") + ] + + const Item3 : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar3"), + "sign" := DDB.AttributeValue.S("sign3"), + "encrypt" := DDB.AttributeValue.S("encrypt3"), + "plain" := DDB.AttributeValue.S("plain3") + ] + + const Item4 : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar4"), + "sign" := DDB.AttributeValue.S("sign4"), + "encrypt" := DDB.AttributeValue.S("encrypt4"), + "plain" := DDB.AttributeValue.S("plain4") + ] + method {:test} TestBatchWriteItemOutputTransform() { var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); var output := DDB.BatchWriteItemOutput( @@ -55,7 +84,7 @@ module BatchWriteItemTransformTest { ReturnItemCollectionMetrics := None ); var transformed := middlewareUnderTest.BatchWriteItemOutputTransform( - AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.BatchWriteItemOutputTransformInput( + TTypes.BatchWriteItemOutputTransformInput( sdkOutput := output, originalInput := input ) @@ -65,4 +94,175 @@ module BatchWriteItemTransformTest { expect_equal("BatchWriteItemOutput", transformed.value.transformedOutput, output); } + function method MakePut(item : DDB.AttributeMap) : DDB.WriteRequest + { + DDB.WriteRequest ( DeleteRequest := None, PutRequest := Some(DDB.PutRequest(Item := item))) + } + + //= specification/dynamodb-encryption-client/ddb-sdk-integration.md#decrypt-after-batchwriteitem + //= type=test + //# Each item in UnprocessedItems MUST be replaced by its original plaintext value. + method {:test} TestBatchWriteItemOutputTransformUnprocessed() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); + var tableName := GetTableName("foo"); + + var theRequests := GetBatchWriteItemRequestMap(map[tableName := [MakePut(Item1), MakePut(Item2), MakePut(Item3), MakePut(Item4)]]); + + var input := DDB.BatchWriteItemInput( + RequestItems := theRequests + ); + var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform( + TTypes.BatchWriteItemInputTransformInput( + sdkInput := input + ) + ); + + var unProcessed : DDB.BatchWriteItemRequestMap := transInput.transformedInput.RequestItems; + expect unProcessed != input.RequestItems; + var output := DDB.BatchWriteItemOutput( + UnprocessedItems := Some(unProcessed) + ); + + var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform( + TTypes.BatchWriteItemOutputTransformInput( + sdkOutput := output, + originalInput := input + ) + ); + + expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(theRequests)); + } + + method {:test} TestBatchWriteItemOutputTransformUnprocessed2() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); + var tableName1 := GetTableName("foo"); + var tableName2 := GetTableName("baz"); + + var theRequests := GetBatchWriteItemRequestMap(map[tableName1 := [MakePut(Item1), MakePut(Item2)], tableName2 := [MakePut(Item3), MakePut(Item4)]]); + + var input := DDB.BatchWriteItemInput( + RequestItems := theRequests + ); + var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform( + TTypes.BatchWriteItemInputTransformInput( + sdkInput := input + ) + ); + + var unProcessed : DDB.BatchWriteItemRequestMap := transInput.transformedInput.RequestItems; + expect unProcessed != input.RequestItems; + var output := DDB.BatchWriteItemOutput( + UnprocessedItems := Some(unProcessed) + ); + + var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform( + TTypes.BatchWriteItemOutputTransformInput( + sdkOutput := output, + originalInput := input + ) + ); + + expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(theRequests)); + } + + method {:test} {:vcs_split_on_every_assert} TestBatchWriteItemOutputTransformUnprocessed3() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms(); + var tableName1 := GetTableName("foo"); + var tableName2 := GetTableName("baz"); + + var theRequests := GetBatchWriteItemRequestMap(map[tableName1 := [MakePut(Item1), MakePut(Item2)], tableName2 := [MakePut(Item3), MakePut(Item4)]]); + + var input := DDB.BatchWriteItemInput( + RequestItems := theRequests + ); + var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform( + TTypes.BatchWriteItemInputTransformInput( + sdkInput := input + ) + ); + + expect tableName1 in transInput.transformedInput.RequestItems; + expect tableName2 in transInput.transformedInput.RequestItems; + + var list := map[ + tableName1 := transInput.transformedInput.RequestItems[tableName1][0..1], + tableName2 := transInput.transformedInput.RequestItems[tableName2][0..1] + ]; + expect DDB.IsValid_BatchWriteItemRequestMap(list); + var unProcessed : DDB.BatchWriteItemRequestMap := list; + + var orig_list := map [ + tableName1 := [MakePut(Item1)], + tableName2 := [MakePut(Item3)] + ]; + expect DDB.IsValid_BatchWriteItemRequestMap(orig_list); + var originalUnProcessed : DDB.BatchWriteItemRequestMap := orig_list; + + expect unProcessed != input.RequestItems; + var output := DDB.BatchWriteItemOutput( + UnprocessedItems := Some(unProcessed) + ); + + var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform( + TTypes.BatchWriteItemOutputTransformInput( + sdkOutput := output, + originalInput := input + ) + ); + + expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(originalUnProcessed)); + } + + const Item1a : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar1"), + "sign" := DDB.AttributeValue.S("sign2"), + "encrypt" := DDB.AttributeValue.S("encrypt2"), + "plain" := DDB.AttributeValue.S("plain2") + ] + + const Item1b : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar1"), + "sign" := DDB.AttributeValue.S("sign3"), + "encrypt" := DDB.AttributeValue.S("encrypt3"), + "plain" := DDB.AttributeValue.S("plain3") + ] + + const Item1c : DDB.AttributeMap := map[ + "bar" := DDB.AttributeValue.S("bar1"), + "sign" := DDB.AttributeValue.S("sign4"), + "encrypt" := DDB.AttributeValue.S("encrypt4"), + "plain" := DDB.AttributeValue.S("plain4") + ] + + method {:test} TestBatchWriteItemOutputTransformUnprocessed4() { + var middlewareUnderTest := TestFixtures.GetDynamoDbEncryptionTransforms2(); + var tableName1 := GetTableName("foo"); + var tableName2 := GetTableName("baz"); + + var theRequests := GetBatchWriteItemRequestMap(map[tableName1 := [MakePut(Item1), MakePut(Item1a)], tableName2 := [MakePut(Item1b), MakePut(Item1c)]]); + + var input := DDB.BatchWriteItemInput( + RequestItems := theRequests + ); + var transInput :- expect middlewareUnderTest.BatchWriteItemInputTransform( + TTypes.BatchWriteItemInputTransformInput( + sdkInput := input + ) + ); + + var unProcessed : DDB.BatchWriteItemRequestMap := transInput.transformedInput.RequestItems; + expect unProcessed != input.RequestItems; + var output := DDB.BatchWriteItemOutput( + UnprocessedItems := Some(unProcessed) + ); + + var transOutput :- expect middlewareUnderTest.BatchWriteItemOutputTransform( + TTypes.BatchWriteItemOutputTransformInput( + sdkOutput := output, + originalInput := input + ) + ); + + expect_equal("BatchWriteOutput", transOutput.transformedOutput.UnprocessedItems, Some(theRequests)); + } } diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index f287a4c47..0ae49457a 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -19,6 +19,7 @@ module TestFixtures { import DDB = ComAmazonawsDynamodbTypes method GetTableName(s : string) returns (output : DDB.TableName) + ensures DDB.IsValid_TableArn(output) { expect DDB.IsValid_TableName(s); return s; @@ -237,31 +238,37 @@ module TestFixtures { assume {:axiom} fresh(encryption.Modifies); } - // method GetDynamoDbEncryptionTransforms2(actions : AttributeActions, sortKey : Option) - // returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient) - // ensures encryption.ValidState() - // ensures fresh(encryption) - // ensures fresh(encryption.Modifies) - // { - // var keyring := GetKmsKeyring(); - // encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( - // DynamoDbTablesEncryptionConfig( - // tableEncryptionConfigs := map[ - // "foo" := DynamoDbTableEncryptionConfig( - // logicalTableName := "foo", - // partitionKeyName := "bar", - // sortKeyName := sortKey, - // attributeActionsOnEncrypt := actions, - // allowedUnsignedAttributes := Some(["plain"]), - // allowedUnsignedAttributePrefix := None(), - // algorithmSuiteId := None(), - // keyring := Some(keyring) - // ) - // ] - // ) - // ); - // assume {:axiom} fresh(encryption.Modifies); - // } + method GetDynamoDbEncryptionTransforms2() + returns (encryption: DynamoDbEncryptionTransforms.DynamoDbEncryptionTransformsClient) + ensures encryption.ValidState() + ensures fresh(encryption) + ensures fresh(encryption.Modifies) + { + expect DDB.IsValid_TableName("foo"); + var keyring := GetKmsKeyring(); + encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( + DynamoDbTablesEncryptionConfig( + tableEncryptionConfigs := map[ + "foo" := DynamoDbTableEncryptionConfig( + logicalTableName := "foo", + partitionKeyName := "bar", + sortKeyName := Some("sign"), + attributeActionsOnEncrypt := map[ + "bar" := CSE.SIGN_ONLY, + "sign" := CSE.SIGN_ONLY, + "encrypt" := CSE.ENCRYPT_AND_SIGN, + "plain" := CSE.DO_NOTHING + ], + allowedUnsignedAttributes := Some(["plain"]), + allowedUnsignedAttributePrefix := None(), + algorithmSuiteId := None(), + keyring := Some(keyring) + ) + ] + ) + ); + assume {:axiom} fresh(encryption.Modifies); + } // type AttributeActions = map diff --git a/specification/dynamodb-encryption-client/ddb-sdk-integration.md b/specification/dynamodb-encryption-client/ddb-sdk-integration.md index b109dcc7a..d8737b2e6 100644 --- a/specification/dynamodb-encryption-client/ddb-sdk-integration.md +++ b/specification/dynamodb-encryption-client/ddb-sdk-integration.md @@ -125,6 +125,7 @@ MUST have the following modified behavior: - [Encrypt before PutItem](#encrypt-before-putitem) - [Encrypt before BatchWriteItem](#encrypt-before-batchwriteitem) - [Encrypt before TransactWriteItems](#encrypt-before-transactwriteitems) +- [Decrypt after BatchWriteItem](#encrypt-before-batchwriteitem) - [Decrypt after GetItem](#decrypt-after-getitem) - [Decrypt after PutItem](#decrypt-after-putitem) - [Decrypt after UpdateItem](#decrypt-after-updateitem) @@ -319,6 +320,12 @@ If there is a `Put` that refers to a `TableName` that refers to an [encrypted-ta the result [Encrypted DynamoDB Item](./encrypt-item.md#encrypted-dynamodb-item) calculated above. +### Decrypt after BatchWriteItem + +If there are no UnprocessedItems, then the BatchWriteItemOutput MUST be returned unchanged. + +Each item in UnprocessedItems MUST be replaced by its original plaintext value. + ### Decrypt after GetItem After a [GetItem](https://docs.aws.amazon.com/amazondynamodb/latest/APIReference/API_GetItem.html)