From 237e4b95686a85a4f70bc820aebca4c1ef009f17 Mon Sep 17 00:00:00 2001 From: Ritvik Kapila Date: Mon, 16 Dec 2024 10:55:44 -0800 Subject: [PATCH] fix(shared-cache): block shared cache for beacons --- .../dafny/DynamoDbEncryption/src/ConfigToInfo.dfy | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy index 09f9393e2..7e30bd5e2 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy @@ -119,6 +119,12 @@ module SearchConfigToInfo { && config.multi.keyFieldName in outer.attributeActionsOnEncrypt && outer.attributeActionsOnEncrypt[config.multi.keyFieldName] == SE.ENCRYPT_AND_SIGN ==> output.Failure? + ensures + && config.multi? + && config.multi.cache.Some? + && config.multi.cache.value.Shared? + ==> output.Failure? + { var mplR := MaterialProviders.MaterialProviders(); var mpl :- mplR.MapFailure(e => AwsCryptographyMaterialProviders(e)); @@ -139,7 +145,7 @@ module SearchConfigToInfo { var cache; if cacheType.Shared? { - cache := cacheType.Shared; + return Failure(E("Scan Beacons and Searchable Encryption do NOT support Shared caches.")); } 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)