From a5a4aca02032a50fa9d15248183c317fea411d0a Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 31 Jul 2024 08:50:05 -0400 Subject: [PATCH 1/3] fix: allow multi-tenant queries with allow_plaintext --- .../DynamoDbEncryptionTransforms/src/QueryTransform.dfy | 6 +++--- .../DynamoDbEncryptionTransforms/src/ScanTransform.dfy | 5 +++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index 1b9fab3fd..9f29a4b89 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -90,10 +90,10 @@ module QueryTransform { //# 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 keyId.KeyId? { - :- Need(decrypted.parsedHeader.Some?, E("Decrypted query result has no parsed header.")); + + // No parsed header is ok, because it means ALLOW_PLAINTEXT_READ and a plain text item + if keyId.KeyId? && decrypted.parsedHeader.Some? { :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Query result has more than one Encrypted Data Key")); if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 { decryptedItems := decryptedItems + [decrypted.plaintextItem]; diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index 58fa69227..c00244d42 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -88,9 +88,10 @@ module ScanTransform { var decryptInput := EncTypes.DecryptItemInput(encryptedItem := encryptedItems[x]); var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); - var decrypted :- MapError(decryptRes); - if keyId.KeyId? { + + // No parsed header is ok, because it means ALLOW_PLAINTEXT_READ and a plain text item + if keyId.KeyId? && decrypted.parsedHeader.Some? { :- Need(decrypted.parsedHeader.Some?, E("Decrypted scan result has no parsed header.")); :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key")); if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 { From 46b0aaf6c578409f3ea5b7467286696499f5c66b Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Wed, 31 Jul 2024 14:07:30 -0400 Subject: [PATCH 2/3] m --- .../src/QueryTransform.dfy | 14 ++++++++++++-- .../src/ScanTransform.dfy | 14 ++++++++++++-- 2 files changed, 24 insertions(+), 4 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index 9f29a4b89..955a1d27c 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -10,7 +10,7 @@ module QueryTransform { import DDB = ComAmazonawsDynamodbTypes import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes - import Seq + import EncOps = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations method Input(config: Config, input: QueryInputTransformInput) returns (output: Result) @@ -92,7 +92,17 @@ module QueryTransform { var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); var decrypted :- MapError(decryptRes); - // No parsed header is ok, because it means ALLOW_PLAINTEXT_READ and a plain text item + if decrypted.parsedHeader.None? { + :- Need( + && EncOps.IsPlaintextItem(encryptedItems[x]) + && ( + || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? + || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? + ), + E("Unexpected lack of parsed header.") + ); + } + if keyId.KeyId? && decrypted.parsedHeader.Some? { :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Query result has more than one Encrypted Data Key")); if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 { diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index c00244d42..49b554766 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -10,7 +10,7 @@ module ScanTransform { import DDB = ComAmazonawsDynamodbTypes import opened AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes import EncTypes = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorTypes - import Seq + import EncOps = AwsCryptographyDbEncryptionSdkDynamoDbItemEncryptorOperations method Input(config: Config, input: ScanInputTransformInput) returns (output: Result) @@ -90,7 +90,17 @@ module ScanTransform { var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); var decrypted :- MapError(decryptRes); - // No parsed header is ok, because it means ALLOW_PLAINTEXT_READ and a plain text item + if decrypted.parsedHeader.None? { + :- Need( + && EncOps.IsPlaintextItem(encryptedItems[x]) + && ( + || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? + || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? + ), + E("Unexpected lack of parsed header.") + ); + } + if keyId.KeyId? && decrypted.parsedHeader.Some? { :- Need(decrypted.parsedHeader.Some?, E("Decrypted scan result has no parsed header.")); :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key")); From 99f9561503c219749326a06174fecf8f72a5e094 Mon Sep 17 00:00:00 2001 From: seebees Date: Wed, 31 Jul 2024 11:22:45 -0700 Subject: [PATCH 3/3] what about this? --- .../src/QueryTransform.dfy | 11 +++++------ .../src/ScanTransform.dfy | 12 +++++------- 2 files changed, 10 insertions(+), 13 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index 955a1d27c..6eefe7fa2 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -92,16 +92,15 @@ module QueryTransform { var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); var decrypted :- MapError(decryptRes); - if decrypted.parsedHeader.None? { - :- Need( + // If the decrypted result was plaintext, i.e. has no parsedHeader + // then this is expected IFF the table config allows plaintext read + assert decrypted.parsedHeader.None? ==> && EncOps.IsPlaintextItem(encryptedItems[x]) + && !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ? && ( || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? - ), - E("Unexpected lack of parsed header.") - ); - } + ); if keyId.KeyId? && decrypted.parsedHeader.Some? { :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Query result has more than one Encrypted Data Key")); diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy index 49b554766..034cd7943 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -90,19 +90,17 @@ module ScanTransform { var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); var decrypted :- MapError(decryptRes); - if decrypted.parsedHeader.None? { - :- Need( + // If the decrypted result was plaintext, i.e. has no parsedHeader + // then this is expected IFF the table config allows plaintext read + assert decrypted.parsedHeader.None? ==> && EncOps.IsPlaintextItem(encryptedItems[x]) + && !tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_FORBID_PLAINTEXT_READ? && ( || tableConfig.plaintextOverride.FORBID_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? || tableConfig.plaintextOverride.FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ? - ), - E("Unexpected lack of parsed header.") - ); - } + ); if keyId.KeyId? && decrypted.parsedHeader.Some? { - :- Need(decrypted.parsedHeader.Some?, E("Decrypted scan result has no parsed header.")); :- Need(|decrypted.parsedHeader.value.encryptedDataKeys| == 1, E("Scan result has more than one Encrypted Data Key")); if decrypted.parsedHeader.value.encryptedDataKeys[0].keyProviderInfo == keyIdUtf8 { decryptedItems := decryptedItems + [decrypted.plaintextItem];