From 8adb90a7927d6cd4ac69a4ba69fb950e1ff910c2 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Thu, 22 Aug 2024 10:16:35 -0700 Subject: [PATCH 1/6] chore: Test with MPL main head --- submodules/MaterialProviders | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/submodules/MaterialProviders b/submodules/MaterialProviders index cdd4885cb..d51d6482e 160000 --- a/submodules/MaterialProviders +++ b/submodules/MaterialProviders @@ -1 +1 @@ -Subproject commit cdd4885cb22957b04167b11d8b40edbdf4301d8d +Subproject commit d51d6482e3d8ca668111a4695d1adc0c67c3f0a3 From c54ed4c225e25727daf50cb371919c1b10313e64 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 22 Aug 2024 17:29:48 -0400 Subject: [PATCH 2/6] remove unnecessary asserts --- .../src/QueryTransform.dfy | 10 ---------- .../DynamoDbEncryptionTransforms/src/ScanTransform.dfy | 10 ---------- 2 files changed, 20 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy index 6eefe7fa2..e9d601f94 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/QueryTransform.dfy @@ -92,16 +92,6 @@ module QueryTransform { var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); 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 - 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? - ); - 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 034cd7943..e412e5121 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/ScanTransform.dfy @@ -90,16 +90,6 @@ module ScanTransform { var decryptRes := tableConfig.itemEncryptor.DecryptItem(decryptInput); 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 - 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? - ); - if keyId.KeyId? && decrypted.parsedHeader.Some? { :- 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 18cd605369f1967a3116a93a7665e0ade5df29f6 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 22 Aug 2024 18:27:43 -0400 Subject: [PATCH 3/6] m --- .../dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy | 1 + 1 file changed, 1 insertion(+) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index 2667e361c..eebc07f85 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -243,6 +243,7 @@ module TestFixtures { ensures fresh(encryption) ensures fresh(encryption.Modifies) { + expect sortKey.None? || IsValid_KeySchemaAttributeName(sortKey.value); var keyring := GetKmsKeyring(); encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( DynamoDbTablesEncryptionConfig( From b3552931b5152213efdfabd5ba3f97048939cc74 Mon Sep 17 00:00:00 2001 From: Andy Jewell Date: Thu, 22 Aug 2024 18:30:37 -0400 Subject: [PATCH 4/6] m --- .../dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy index eebc07f85..bb6633666 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/test/TestFixtures.dfy @@ -243,7 +243,7 @@ module TestFixtures { ensures fresh(encryption) ensures fresh(encryption.Modifies) { - expect sortKey.None? || IsValid_KeySchemaAttributeName(sortKey.value); + expect sortKey.None? || DDB.IsValid_KeySchemaAttributeName(sortKey.value); var keyring := GetKmsKeyring(); encryption :- expect DynamoDbEncryptionTransforms.DynamoDbEncryptionTransforms( DynamoDbTablesEncryptionConfig( From ab07c137dfc591366b791c3e3b3b9fd91006e5c1 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 23 Aug 2024 11:07:23 -0700 Subject: [PATCH 5/6] merge --- project.properties | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/project.properties b/project.properties index a20b1ec57..1d808a93c 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,5 @@ -projectJavaVersion=3.6.2 -mplDependencyJavaVersion=1.5.1 +projectJavaVersion=3.6.2-SNAPSHOT +mplDependencyJavaVersion=1.5.1-SNAPSHOT dafnyVersion=4.2.0 dafnyVerifyVersion=4.7.0 dafnyRuntimeJavaVersion=4.2.0 From 79aea91fd02b0a02c03925fde992d3dbf2911855 Mon Sep 17 00:00:00 2001 From: Lucas McDonald Date: Fri, 23 Aug 2024 12:24:46 -0700 Subject: [PATCH 6/6] Update project.properties --- project.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/project.properties b/project.properties index 1d808a93c..1a4050afc 100644 --- a/project.properties +++ b/project.properties @@ -1,5 +1,5 @@ projectJavaVersion=3.6.2-SNAPSHOT -mplDependencyJavaVersion=1.5.1-SNAPSHOT +mplDependencyJavaVersion=1.5.1 dafnyVersion=4.2.0 dafnyVerifyVersion=4.7.0 dafnyRuntimeJavaVersion=4.2.0