From ff7b6f00b3c6bede6752958efc1c63d831ec3d0f Mon Sep 17 00:00:00 2001 From: texastony <5892063+texastony@users.noreply.github.com> Date: Mon, 16 Dec 2024 10:49:09 -0800 Subject: [PATCH 1/5] fix(SearchableEncryption): disable shared cached --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 09f9393e2..ab0a2cd58 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -139,7 +139,8 @@ module SearchConfigToInfo { var cache; if cacheType.Shared? { - cache := cacheType.Shared; + return Failure(DynamoDbEncryptionException(message:="Searchable Encryption does not support shared caches")); + // cache := cacheType.Shared; } else { //= specification/searchable-encryption/search-config.md#key-store-cache //# For a Beacon Key Source a [CMC](../../submodules/MaterialProviders/aws-encryption-sdk-specification/framework/cryptographic-materials-cache.md) From bd49ea164375e222a851e5342568c68f419e8ec9 Mon Sep 17 00:00:00 2001 From: texastony <5892063+texastony@users.noreply.github.com> Date: Mon, 16 Dec 2024 11:28:20 -0800 Subject: [PATCH 2/5] test(SearchableEncryption): test disable shared cache via formal verificaiton --- .../DynamoDbEncryption/src/ConfigToInfo.dfy | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index ab0a2cd58..5d56271ee 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -119,7 +119,21 @@ module SearchConfigToInfo { && config.multi.keyFieldName in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN ==> output.Failure? + // Not in Spec, but for now, SE does not support the Shared Cache Type + ensures + && config.multi? + && config.multi.cache.Some? + && config.multi.cache.value.Shared? + && output.Failure? + // If the failure was NOT caused by booting up the MPL + && !output.error.AwsCryptographyMaterialProviders? + ==> + && output.error.DynamoDbEncryptionException? + && output.error.message == "Searchable Encryption does not support the Shared Cache type at this time." { + // TODO-FutureCleanUp : It is not-good that the MPL is initialized here; + // The MPL has a config object that could hold customer intent that affects behavior. + // Today, it does not. But tomorrow? var mplR := MaterialProviders.MaterialProviders(); var mpl :- mplR.MapFailure(e => AwsCryptographyMaterialProviders(e)); @@ -139,7 +153,7 @@ module SearchConfigToInfo { var cache; if cacheType.Shared? { - return Failure(DynamoDbEncryptionException(message:="Searchable Encryption does not support shared caches")); + return Failure(DynamoDbEncryptionException(message:="Searchable Encryption does not support the Shared Cache type at this time.")); // cache := cacheType.Shared; } else { //= specification/searchable-encryption/search-config.md#key-store-cache From 65c5aaf04970ba2813da4be71102ffaad5bc097a Mon Sep 17 00:00:00 2001 From: Tony Knapp <5892063+texastony@users.noreply.github.com> Date: Mon, 16 Dec 2024 12:16:16 -0800 Subject: [PATCH 3/5] refactor(SE): make TODO good --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 5d56271ee..2478e89e2 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -131,7 +131,8 @@ module SearchConfigToInfo { && output.error.DynamoDbEncryptionException? && output.error.message == "Searchable Encryption does not support the Shared Cache type at this time." { - // TODO-FutureCleanUp : It is not-good that the MPL is initialized here; + // TODO-FutureCleanUp : https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1510 + // It is not-good that the MPL is initialized here; // The MPL has a config object that could hold customer intent that affects behavior. // Today, it does not. But tomorrow? var mplR := MaterialProviders.MaterialProviders(); From 1e56fa0911c9f18a35daaba823148b70188be66f Mon Sep 17 00:00:00 2001 From: Tony Knapp <5892063+texastony@users.noreply.github.com> Date: Mon, 16 Dec 2024 12:22:02 -0800 Subject: [PATCH 4/5] Update DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy Co-authored-by: Ritvik Kapila <61410899+RitvikKapila@users.noreply.github.com> --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 2478e89e2..a0dd33611 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -120,16 +120,17 @@ module SearchConfigToInfo { && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN ==> output.Failure? // Not in Spec, but for now, SE does not support the Shared Cache Type - ensures + ensures && config.multi? && config.multi.cache.Some? && config.multi.cache.value.Shared? - && output.Failure? - // If the failure was NOT caused by booting up the MPL - && !output.error.AwsCryptographyMaterialProviders? - ==> - && output.error.DynamoDbEncryptionException? - && output.error.message == "Searchable Encryption does not support the Shared Cache type at this time." + ==> + && output.Failure? + // If the failure was NOT caused by booting up the MPL + && !output.error.AwsCryptographyMaterialProviders? + ==> + && output.error.DynamoDbEncryptionException? + && output.error.message == "Searchable Encryption does not support the Shared Cache type at this time." { // TODO-FutureCleanUp : https://github.com/aws/aws-database-encryption-sdk-dynamodb/issues/1510 // It is not-good that the MPL is initialized here; From 54ecddac4f59e077bdb6a22b6f643f367c4f03af Mon Sep 17 00:00:00 2001 From: texastony <5892063+texastony@users.noreply.github.com> Date: Mon, 16 Dec 2024 12:24:53 -0800 Subject: [PATCH 5/5] chore: format --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index a0dd33611..916005d6e 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -120,13 +120,13 @@ module SearchConfigToInfo { && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN ==> output.Failure? // Not in Spec, but for now, SE does not support the Shared Cache Type - ensures + ensures && config.multi? && config.multi.cache.Some? && config.multi.cache.value.Shared? - ==> + ==> && output.Failure? - // If the failure was NOT caused by booting up the MPL + // If the failure was NOT caused by booting up the MPL && !output.error.AwsCryptographyMaterialProviders? ==> && output.error.DynamoDbEncryptionException?